summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Object.hs2
-rw-r--r--Semantic.hs76
-rw-r--r--Term.hs2
-rw-r--r--Theorem.hs8
-rw-r--r--TypeVar.hs10
5 files changed, 48 insertions, 50 deletions
diff --git a/Object.hs b/Object.hs
index 640cf08..5b2130c 100644
--- a/Object.hs
+++ b/Object.hs
@@ -21,7 +21,7 @@ data Object = ObjNum { objNum :: Number }
| ObjConst { objConst :: Const }
| ObjVar { objVar :: Var }
| ObjTerm { objTerm :: Term }
- | ObjThm { objThm :: Theorem } deriving (Eq)
+ | ObjThm { objThm :: Theorem } deriving (Eq, Ord)
type List = [Object]
diff --git a/Semantic.hs b/Semantic.hs
index d50905c..2f54c94 100644
--- a/Semantic.hs
+++ b/Semantic.hs
@@ -1,6 +1,8 @@
import Control.Monad( liftM )
import System( getArgs )
import Data.List
+import qualified Data.Set as Set
+import qualified Data.Map as Map
import TypeVar
import Term
import Theorem
@@ -9,22 +11,22 @@ import Object
data Stack = Stack { stackList :: [Object] }
-data Dictionary = Dictionary { dictionMap :: [(Int,Object)] }
-data Assumptions = Assumptions { assumeList :: [Object] }
-data Theorems = Theorems { theoremList :: [Object] }
+data Dictionary = Dictionary { dictionMap :: Map.Map Int Object }
+data Assumptions = Assumptions { assumeSet :: Set.Set Object }
+data Theorems = Theorems { theoremSet :: Set.Set Object }
instance Show Stack where
show a = "Stack:\n" ++ intercalate "\n" (map (show) (stackList a)) ++ "\n\n"
instance Show Dictionary where
- show a = "Dictionary:\n" ++ intercalate "\n" (map (show) (dictionMap a)) ++ "\n\n"
+ show a = "Dictionary:\n" ++ intercalate "\n" (map (show) (Map.toList . dictionMap $ a)) ++ "\n\n"
instance Show Assumptions where
- show a = "Assumptions:\n" ++ intercalate "\n" (map (show) (assumeList a)) ++ "\n\n"
+ show a = "Assumptions:\n" ++ intercalate "\n" (map (show) (Set.toList . assumeSet $ a)) ++ "\n\n"
instance Show Theorems where
- show a = "Theorems:\n" ++ intercalate "\n" (map (show) (theoremList a)) ++ "\n\n"
+ show a = "Theorems:\n" ++ intercalate "\n" (map (show) (Set.toList . theoremSet $ a)) ++ "\n\n"
data ArticleLine = Comment { commentString :: String }
@@ -76,7 +78,7 @@ name str = \(s,d,a,t) ->
number :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems))
-number n = \(stack,d,a,t) -> (Stack $ ObjNum (read n) : (stackList stack), d, a, t)
+number n = \(s,d,a,t) -> (Stack $ ObjNum (read n) : (stackList s), d, a, t)
absTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
@@ -112,7 +114,7 @@ appTerm (s,d,a,t) =
appThm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
appThm (s,d,a,t) =
let stack = stackList s
- op = (\x y -> Theorem (union (thmHyp x) (thmHyp y))
+ op = (\x y -> Theorem (Set.union (thmHyp x) (thmHyp y))
(mkEquals (TApp (getlhs . thmCon $ y) (getlhs . thmCon $ x))
(TApp (getrhs . thmCon $ y) (getrhs . thmCon $ x))))
theorem = ObjThm $ op (objThm $ stack!!0) (objThm $ stack!!1)
@@ -123,7 +125,7 @@ appThm (s,d,a,t) =
assume :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
assume (s,d,a,t) =
let stack = stackList s
- op = (\x -> Theorem [x] x)
+ op = (\x -> Theorem (Set.singleton x) x)
theorem = ObjThm $ op (objTerm $ stack!!0)
s' = Stack $ theorem : (tail stack)
in (s',d,a,t)
@@ -133,20 +135,21 @@ assume (s,d,a,t) =
axiom :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
axiom (s,d,a,t) =
let stack = stackList s
- assumptions = assumeList a
- op = (\x y -> Theorem y x)
+ assumptions = assumeSet a
+ op = (\x y -> Theorem (Set.fromList y) x)
theorem = ObjThm $ op (objTerm $ stack!!0) (map (objTerm) . objList $ stack!!1)
s' = Stack $ theorem : (drop 2 stack)
- a' = Assumptions $ theorem : assumptions
+ a' = Assumptions $ Set.insert theorem assumptions
in (s',d,a',t)
betaConv :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
betaConv (s,d,a,t) =
let stack = stackList s
- op = (\x -> Theorem [] (mkEquals x
- (substitute ([], [(tVar . tAbsVar . tAppLeft $ x, tAppRight $ x)])
- (tAbsTerm . tAppLeft $ x))))
+ op = (\x -> Theorem (Set.empty)
+ (mkEquals x
+ (substitute ([], [(tVar . tAbsVar . tAppLeft $ x, tAppRight $ x)])
+ (tAbsTerm . tAppLeft $ x))))
theorem = ObjThm $ op (objTerm $ stack!!0)
s' = Stack $ theorem : (tail stack)
in (s',d,a,t)
@@ -182,8 +185,8 @@ constTerm (s,d,a,t) =
deductAntisym :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
deductAntisym (s,d,a,t) =
let stack = stackList s
- op = (\x y -> Theorem (union ((thmHyp $ y) \\ [(thmCon $ x)])
- ((thmHyp $ x) \\ [(thmCon $ y)]))
+ op = (\x y -> Theorem (Set.union (Set.delete (thmCon $ x) (thmHyp $ y))
+ (Set.delete (thmCon $ y) (thmHyp $ x)))
(mkEquals (thmCon $ y) (thmCon $ x)))
theorem = ObjThm $ op (objThm $ stack!!0) (objThm $ stack!!1)
s' = Stack $ theorem : (drop 2 stack)
@@ -193,10 +196,7 @@ deductAntisym (s,d,a,t) =
def :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
def (s,d,a,t) =
let stack = stackList s
- dictionary = dictionMap d
- newEntry = ((objNum $ stack!!0), (stack!!1))
- cleanDict = filter ((/=) (objNum $ stack!!0) . fst) dictionary
- d' = Dictionary $ newEntry : cleanDict
+ d' = Dictionary $ Map.insert (objNum $ stack!!0) (stack!!1) (dictionMap d)
s' = Stack $ tail stack
in (s',d',a,t)
@@ -205,7 +205,7 @@ defineConst :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assu
defineConst (s,d,a,t) =
let stack = stackList s
op1 = (\x -> Const x)
- op2 = (\x y -> Theorem [] (mkEquals x y))
+ op2 = (\x y -> Theorem Set.empty (mkEquals x y))
constant = ObjConst $ op1 (objName $ stack!!1)
constTerm = TConst (objConst $ constant) (typeOf (objTerm $ stack!!0))
theorem = ObjThm $ op2 constTerm (objTerm $ stack!!0)
@@ -229,9 +229,9 @@ defineTypeOp (s,d,a,t) =
abstype = typeFunc rtype atype
repTerm = TConst rep reptype
absTerm = TConst abst abstype
- rthm = Theorem [] (mkEquals (TApp (tAppLeft . thmCon $ oldthm) r')
- (mkEquals (TApp repTerm (TApp absTerm r')) r'))
- athm = Theorem [] (mkEquals (TApp absTerm (TApp repTerm a')) a')
+ rthm = Theorem Set.empty (mkEquals (TApp (tAppLeft . thmCon $ oldthm) r')
+ (mkEquals (TApp repTerm (TApp absTerm r')) r'))
+ athm = Theorem Set.empty (mkEquals (TApp absTerm (TApp repTerm a')) a')
s' = Stack $ (ObjThm rthm) : (ObjThm athm) : (ObjConst rep) : (ObjConst abst) : (ObjTyOp n) : (drop 5 stack)
in (s',d,a,t)
@@ -240,7 +240,7 @@ eqMp :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions
eqMp (s,d,a,t) =
let stack = stackList s
op = (\x y -> if (thmCon x == (getlhs (thmCon y))) then
- Theorem (union (thmHyp x) (thmHyp y))
+ Theorem (Set.union (thmHyp x) (thmHyp y))
(getrhs (thmCon y))
else error "Theorem consequents not alpha equivalent in eqMp")
theorem = ObjThm $ op (objThm $ stack!!0) (objThm $ stack!!1)
@@ -269,8 +269,7 @@ ref :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,
ref (s,d,a,t) =
let stack = stackList s
dictionary = dictionMap d
- entry = filter (((==) (objNum $ stack!!0)) . fst) $ dictionary
- object = snd . head $ entry
+ object = dictionary Map.! (objNum $ stack!!0)
s' = Stack $ object : tail stack
in (s',d,a,t)
@@ -278,7 +277,7 @@ ref (s,d,a,t) =
refl :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
refl (s,d,a,t) =
let stack = stackList s
- op = (\x -> Theorem [] (mkEquals x x))
+ op = (\x -> Theorem Set.empty (mkEquals x x))
theorem = ObjThm $ op (objTerm $ stack!!0)
s' = Stack $ theorem : (tail stack)
in (s',d,a,t)
@@ -288,17 +287,16 @@ remove :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptio
remove (s,d,a,t) =
let stack = stackList s
dictionary = dictionMap d
- entry = filter (((==) (objNum $ stack!!0)) . fst) $ dictionary
- object = snd . head $ entry
+ object = dictionary Map.! (objNum $ stack!!0)
s' = Stack $ object : tail stack
- d' = Dictionary $ dictionary \\ entry
+ d' = Dictionary $ Map.delete (objNum $ stack!!0) dictionary
in (s',d',a,t)
subst :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
subst (s,d,a,t) =
let stack = stackList s
- op = (\x y -> Theorem (map (substitute y) (thmHyp x))
+ op = (\x y -> Theorem (Set.map (substitute y) (thmHyp x))
(substitute y (thmCon x)))
substitution =
(\x -> let list = (map (map objList)) . (map objList) . objList $ x
@@ -313,12 +311,12 @@ subst (s,d,a,t) =
thm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
thm (s,d,a,t) =
let stack = stackList s
- theorems = theoremList t
- op = (\x y z -> Theorem (alphaConvertList (thmHyp z) y)
+ theorems = theoremSet t
+ op = (\x y z -> Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ z) y))
(alphaConvert (thmCon z) x))
theorem = ObjThm $ op (objTerm $ stack!!0) (map (objTerm) . objList $ stack!!1) (objThm $ stack!!2)
s' = Stack $ drop 3 stack
- t' = Theorems $ union theorems [theorem]
+ t' = Theorems $ Set.insert theorem theorems
in (s',d,a,t')
@@ -362,9 +360,9 @@ varType (s,d,a,t) =
doSemanticCheck :: [String] -> (Stack,Dictionary,Assumptions,Theorems)
doSemanticCheck =
let s = Stack []
- d = Dictionary []
- a = Assumptions []
- t = Theorems []
+ d = Dictionary Map.empty
+ a = Assumptions Set.empty
+ t = Theorems Set.empty
op = (\x y -> case y of (Comment _) -> x
(Command z) -> z x)
in (foldl' (op) (s,d,a,t)) . (map (parse))
diff --git a/Term.hs b/Term.hs
index 626b91c..f8f1b84 100644
--- a/Term.hs
+++ b/Term.hs
@@ -27,7 +27,7 @@ data Term = TVar { tVar :: Var }
| TApp { tAppLeft :: Term
, tAppRight :: Term }
| TAbs { tAbsVar :: Term
- , tAbsTerm :: Term }
+ , tAbsTerm :: Term } deriving (Ord)
type Substitution = ( [(Name,Type)], [(Var,Term)] )
diff --git a/Theorem.hs b/Theorem.hs
index c4a36c8..c97a399 100644
--- a/Theorem.hs
+++ b/Theorem.hs
@@ -4,16 +4,16 @@ module Theorem (
-import Data.List
+import qualified Data.Set as Set
import TypeVar
import Term
-data Theorem = Theorem { thmHyp :: [Term]
- , thmCon :: Term } deriving (Eq)
+data Theorem = Theorem { thmHyp :: Set.Set Term
+ , thmCon :: Term } deriving (Eq, Ord)
instance Show Theorem where
- show a = (show . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a)
+ show a = (show . Set.toList . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a)
diff --git a/TypeVar.hs b/TypeVar.hs
index 2dae613..049a9e2 100644
--- a/TypeVar.hs
+++ b/TypeVar.hs
@@ -24,18 +24,18 @@ import Data.List
type Number = Int
data Name = Name { nameSpace :: [String]
- , nameId :: String } deriving (Eq)
+ , nameId :: String } deriving (Eq, Ord)
-data TypeOp = TypeOp { tyOp :: Name } deriving (Eq)
+data TypeOp = TypeOp { tyOp :: Name } deriving (Eq, Ord)
data Type = TypeVar { typeVar :: Name }
| AType { aType :: [Type]
- , aTypeOp :: TypeOp } deriving (Eq)
+ , aTypeOp :: TypeOp } deriving (Eq, Ord)
-data Const = Const { constName :: Name } deriving (Eq)
+data Const = Const { constName :: Name } deriving (Eq, Ord)
data Var = Var { varName :: Name
- , varTy :: Type } deriving (Eq)
+ , varTy :: Type } deriving (Eq, Ord)