Split the Object wrapping from the actual computation in the article commands

6 files changed, 346 insertions, 145 deletions

diff --git a/Command.hs b/Command.hs
new file mode 100644
index 0000000..6df88f8
--- /dev/null
+++ b/Command.hs
@@ -0,0 +1,214 @@
+module Command (
+	name,
+	number,
+	absTerm,
+	absThm,
+	appTerm,
+	appThm,
+	assume,
+	axiom,
+	betaConv,
+	constant,
+	constTerm,
+	deductAntisym,
+	defineConst,
+	defineTypeOp,
+	eqMp,
+	opType,
+	refl,
+	subst,
+	thm,
+	typeOp,
+	var,
+	varTerm,
+	varType
+    ) where
+
+-- deliberately not included:
+-- cons, nil, def, ref, remove, pop
+
+-- all functions here deal exclusively with arguments
+-- and results from/to the stack
+
+import Data.List
+import Data.Maybe
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+import TypeVar
+import Term
+import Theorem
+import Object
+import Parse
+
+
+name :: String -> Maybe Name
+name str =
+	if (not . isName $ str)
+	then Nothing
+	else let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str
+	         name = Name (init wordlist) (last wordlist)
+	     in Just name
+
+
+number :: String -> Maybe Number
+number num =
+	if (not . isNumber $ num)
+	then Nothing
+	else Just (read num)
+
+
+absTerm :: Term -> Var -> Term
+absTerm term var =
+	TAbs (TVar var) term
+
+
+absThm :: Theorem -> Var -> Maybe Theorem
+absThm thm var =
+	if (Set.member (TVar var) (thmHyp thm))
+	then Nothing
+	else Just (Theorem (thmHyp thm) (mkEquals (TAbs (TVar var) (getlhs . thmCon $ thm))
+		                                      (TAbs (TVar var) (getrhs . thmCon $ thm))))
+
+
+appTerm :: Term -> Term -> Term
+appTerm term1 term2 =
+	TApp term2 term1
+
+
+appThm :: Theorem -> Theorem -> Theorem
+appThm thm1 thm2 =
+	Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
+	        (mkEquals (TApp (getlhs . thmCon $ thm2) (getlhs . thmCon $ thm1))
+                      (TApp (getrhs . thmCon $ thm2) (getrhs . thmCon $ thm1)))
+
+
+assume :: Term -> Maybe Theorem
+assume term =
+	if (typeOf term /= typeBool)
+	then Nothing
+	else Just (Theorem (Set.singleton term) term)
+
+
+axiom :: Term -> [Term] -> Maybe Theorem
+axiom term termlist =
+	if (not (all ((== typeBool) . typeOf) termlist))
+	then Nothing
+	else Just (Theorem (Set.fromList termlist) term)
+
+
+betaConv :: Term -> Theorem
+betaConv term =
+	Theorem (Set.empty)
+            (mkEquals term
+                      (substitute ([], [(tVar . tAbsVar . tAppLeft $ term, tAppRight $ term)])
+                                  (tAbsTerm . tAppLeft $ term)))
+
+
+constant :: Name -> Const
+constant name =
+	Const name
+
+
+constTerm :: Type -> Const -> Term
+constTerm ty c =
+	TConst c ty
+
+
+deductAntisym :: Theorem -> Theorem -> Theorem
+deductAntisym x y =
+	Theorem (Set.union (Set.delete (thmCon $ x) (thmHyp $ y))
+                       (Set.delete (thmCon $ y) (thmHyp $ x)))
+            (mkEquals (thmCon $ y) (thmCon $ x))
+
+
+defineConst :: Term -> Name -> Maybe (Theorem, Const)
+defineConst term name =
+	if (freeVars term /= Set.empty || typeVarsInTerm term /= typeVarsInType (typeOf term))
+	then Nothing
+	else let constant = Const name
+	         constTerm = TConst constant (typeOf term)
+	         theorem = Theorem Set.empty (mkEquals constTerm term)
+	     in Just (theorem, constant)
+
+
+defineTypeOp :: Theorem -> [Name] -> Name -> Name -> Name -> Maybe (Theorem, Theorem, Const, Const, TypeOp)
+defineTypeOp thm namelist r a n =
+	if ((typeVarsInTerm . tAppLeft . thmCon $ thm) /= (Set.fromList . map (TypeVar) $ namelist) ||
+		(length namelist) /= (length . nub $ namelist))
+	then Nothing
+	else let rep = Const r
+	         abst = Const a
+	         op = TypeOp n
+	         rtype = typeOf . tAppRight . thmCon $ thm
+	         atype = AType (map (TypeVar) namelist) op
+	         r' = TVar (Var (Name [] "r'") rtype)
+	         a' = TVar (Var (Name [] "a'") atype)
+	         reptype = typeFunc atype rtype
+	         abstype = typeFunc rtype atype
+	         repTerm = TConst rep reptype
+	         absTerm = TConst abst abstype
+	         rthm = Theorem Set.empty 
+	                        (mkEquals (TApp (tAppLeft . thmCon $ thm) r')
+	         	                      (mkEquals (TApp repTerm (TApp absTerm r')) r'))
+	         athm = Theorem Set.empty
+	                        (mkEquals (TApp absTerm (TApp repTerm a')) a')
+	     in Just (rthm, athm, rep, abst, op)
+
+
+eqMp :: Theorem -> Theorem -> Maybe Theorem
+eqMp thm1 thm2 =
+	if (thmCon thm1 /= (getlhs . thmCon $ thm2))
+	then Nothing
+	else Just (Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
+	                   (getrhs . thmCon $ thm2))
+
+
+opType :: [Type] -> TypeOp -> Type
+opType typelist tyOp =
+	AType typelist tyOp
+
+
+refl :: Term -> Theorem
+refl term =
+	Theorem Set.empty (mkEquals term term)
+
+
+subst :: Theorem -> [Object] -> Theorem
+subst thm list =
+	let s = makeSubst list
+	in Theorem (Set.map (substitute s) (thmHyp thm))
+               (substitute s (thmCon thm))
+
+
+thm :: Term -> [Term] -> Theorem -> Maybe Theorem
+thm term termlist oldthm =
+	if ((term /= thmCon oldthm) || (Set.fromList termlist /= thmHyp oldthm))
+	then Nothing
+	else Just (Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ oldthm) termlist))
+                       (alphaConvert (thmCon oldthm) term))
+
+
+typeOp :: Name -> TypeOp
+typeOp name =
+	TypeOp name
+
+
+var :: Type -> Name -> Maybe Var
+var ty name =
+	if (nameSpace name /= [])
+	then Nothing
+	else Just (Var name ty)
+
+
+varTerm :: Var -> Term
+varTerm var =
+	TVar var
+
+
+varType :: Name -> Maybe Type
+varType name =
+	if (nameSpace name /= [])
+	then Nothing
+	else Just (TypeVar name)
+
+
diff --git a/Object.hs b/Object.hs
index 5b2130c..5d0e71e 100644
--- a/Object.hs
+++ b/Object.hs
@@ -1,7 +1,9 @@
 module Object (
 	Object(..),
 
-	List
+	List,
+
+    makeSubst
 	) where
 
 
@@ -37,3 +39,11 @@ instance Show Object where
     show (ObjVar a)    =   show a
     show (ObjTerm a)   =   show a
     show (ObjThm a)    =   show a
+
+
+
+makeSubst :: [Object] -> Substitution
+makeSubst l =
+    let list = (map (map objList)) . (map objList) $ l
+        f = (\g h x -> (g . head $ x, h . last $ x))
+    in f (map (f objName objType)) (map (f objVar objTerm)) list
diff --git a/Semantic.hs b/Semantic.hs
index 73b489e..6a53d49 100644
--- a/Semantic.hs
+++ b/Semantic.hs
@@ -8,13 +8,13 @@ import Term
 import Theorem
 import Object
 import Parse
-
+import qualified Command as Com
 
 
 data Stack = Stack { stackList :: [Object] }
 data Dictionary = Dictionary { dictionMap :: Map.Map Int Object }
-data Assumptions = Assumptions { assumeSet :: Set.Set Object }
-data Theorems = Theorems { theoremSet :: Set.Set Object }
+data Assumptions = Assumptions { assumeSet :: Set.Set Theorem }
+data Theorems = Theorems { theoremSet :: Set.Set Theorem }
 
 
 instance Show Stack where
@@ -71,108 +71,90 @@ parse n = Command (number n)
 
 name :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems))
 name str = \(s,d,a,t) ->
-               if (not . isName $ str)
-               then Nothing
-               else let wordList = (separateBy '.') . removeEscChars . removeQuotes $ str
-                        name = Name (init wordList) (last wordList)
-                        s' = Stack $ ObjName name : (stackList s)
-                    in Just (s',d,a,t)
+               let n = Com.name str
+                   s' = Stack $ ObjName (fromMaybe nullName n) : (stackList s)
+               in if (isNothing n)
+                  then Nothing
+                  else Just (s',d,a,t)
 
 
 number :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems))
-number n = \(s,d,a,t) -> 
-               if (not . isNumber $ n)
-               then Nothing
-               else Just (Stack $ ObjNum (read n) : (stackList s), d, a, t)
+number n = \(s,d,a,t) ->
+               let num = Com.number $ n
+                   s' = Stack $ ObjNum (fromMaybe nullNumber num) : (stackList s)
+               in if (isNothing num)
+                  then Nothing
+                  else Just (s',d,a,t)
 
 
 absTerm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 absTerm (s,d,a,t) =
     let stack = stackList s
-        op = (\x y -> TAbs (TVar y) x)
-        newTerm = ObjTerm $ op (objTerm $ stack!!0) (objVar $ stack!!1)
-        s' = Stack $ newTerm : (drop 2 stack)
+        term = ObjTerm $ Com.absTerm (objTerm $ stack!!0) (objVar $ stack!!1)
+        s' = Stack $ term : (drop 2 stack)
     in Just (s',d,a,t)
 
 
 absThm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 absThm (s,d,a,t) =
     let stack = stackList s
-        oldthm = objThm $ stack!!0
-        var = objVar $ stack!!1
-    in if (Set.member (TVar var) (thmHyp oldthm))
+        thm = Com.absThm (objThm $ stack!!0) (objVar $ stack!!1)
+        s' = Stack $ (ObjThm $ fromMaybe nullThm thm) : (drop 2 stack)
+    in if (isNothing thm)
        then Nothing
-       else let op = (\x y -> Theorem (thmHyp x)
-                                      (mkEquals (TAbs (TVar y) (getlhs . thmCon $ x))
-                                                (TAbs (TVar y) (getrhs . thmCon $ x))))
-                theorem = ObjThm $ op oldthm var
-                s' = Stack $ theorem : (drop 2 stack)
-            in Just (s',d,a,t)
+       else Just (s',d,a,t)
 
 
 appTerm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 appTerm (s,d,a,t) =
     let stack = stackList s
-        op = (\x y -> TApp y x)
-        newTerm = ObjTerm $ op (objTerm $ stack!!0) (objTerm $ stack!!1)
-        s' = Stack $ newTerm : (drop 2 stack)
+        term = ObjTerm $ Com.appTerm (objTerm $ stack!!0) (objTerm $ stack!!1)
+        s' = Stack $ term : (drop 2 stack)
     in Just (s',d,a,t)
 
 
 appThm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 appThm (s,d,a,t) =
     let stack = stackList s
-        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)
-        s' = Stack $ theorem : (drop 2 stack)
+        thm = ObjThm $ Com.appThm (objThm $ stack!!0) (objThm $ stack!!1)
+        s' = Stack $ thm : (drop 2 stack)
     in Just (s',d,a,t)
 
 
 assume :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 assume (s,d,a,t) =
-    let stack = stackList s
-        term = objTerm $ stack!!0
-    in if (typeOf term /= typeBool)
+    let stack= stackList s
+        thm = Com.assume (objTerm $ stack!!0)
+        s' = Stack $ (ObjThm $ fromMaybe nullThm thm) : (tail stack)
+    in if (isNothing thm)
        then Nothing
-       else let op = (\x -> Theorem (Set.singleton x) x)
-                theorem = ObjThm $ op term
-                s' = Stack $ theorem : (tail stack)
-            in Just (s',d,a,t)
+       else Just (s',d,a,t)
 
 
 axiom :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 axiom (s,d,a,t) =
     let stack = stackList s
         assumptions = assumeSet a
-        termList = (map (objTerm) . objList $ stack!!1)
-    in if (filter (\x -> typeOf x /= typeBool) termList /= [])
+        thm = Com.axiom (objTerm $ stack!!0) (map (objTerm) . objList $ stack!!1)
+        s' = Stack $ (ObjThm $ fromMaybe nullThm thm) : (drop 2 stack)
+        a' = Assumptions $ Set.insert (fromMaybe nullThm thm) assumptions
+    in if (isNothing thm)
        then Nothing
-       else let op = (\x y -> Theorem (Set.fromList y) x)
-                theorem = ObjThm $ op (objTerm $ stack!!0) termList
-                s' = Stack $ theorem : (drop 2 stack)
-                a' = Assumptions $ Set.insert theorem assumptions
-            in Just (s',d,a',t)
+       else Just (s',d,a',t)
 
 
 betaConv :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 betaConv (s,d,a,t) =
     let stack = stackList s
-        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)
+        thm = ObjThm $ Com.betaConv (objTerm $ stack!!0)
+        s' = Stack $ thm : (tail stack)
     in Just (s',d,a,t)
 
 
 cons :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 cons (s,d,a,t) =
     let stack = stackList s
-        op = (\x y -> y : x)
-        newList = ObjList $ op (objList $ stack!!0) (stack!!1)
+        newList = ObjList $ (stack!!1) : (objList $ stack!!0)
         s' = Stack $ newList : (drop 2 stack)
     in Just (s',d,a,t)
 
@@ -180,8 +162,7 @@ cons (s,d,a,t) =
 constant :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 constant (s,d,a,t) =
     let stack = stackList s
-        op = (\x -> Const x)
-        constant = ObjConst $ op (objName $ stack!!0)
+        constant = ObjConst $ Com.constant (objName $ stack!!0)
         s' = Stack $ constant : (tail stack)
     in Just (s',d,a,t)
 
@@ -189,20 +170,16 @@ constant (s,d,a,t) =
 constTerm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 constTerm (s,d,a,t) =
     let stack = stackList s
-        op = (\x y -> TConst y x)
-        newType = ObjTerm $ op (objType $ stack!!0) (objConst $ stack!!1)
-        s' = Stack $ newType : (drop 2 stack)
+        term = ObjTerm $ Com.constTerm (objType $ stack!!0) (objConst $ stack!!1)
+        s' = Stack $ term : (drop 2 stack)
     in Just (s',d,a,t)
 
 
 deductAntisym :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 deductAntisym (s,d,a,t) =
     let stack = stackList s
-        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)
+        thm = ObjThm $ Com.deductAntisym (objThm $ stack!!0) (objThm $ stack!!1)
+        s' = Stack $ thm : (drop 2 stack)
     in Just (s',d,a,t)
 
 
@@ -217,56 +194,34 @@ def (s,d,a,t) =
 defineConst :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 defineConst (s,d,a,t) =
     let stack = stackList s
-        term = objTerm $ stack!!0
-    in if (freeVars term /= Set.empty || typeVarsInTerm term /= typeVarsInType (typeOf term))
+        result = Com.defineConst (objTerm $ stack!!0) (objName $ stack!!1)
+        (thm, constant) = fromMaybe (nullThm, nullConst) result
+        s' = Stack $ (ObjThm thm) : (ObjConst constant) : (drop 2 stack)
+    in if (isNothing result)
        then Nothing
-       else let op1 = (\x -> Const x)
-                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)
-                s' = Stack $ theorem : constant : (drop 2 stack)
-            in Just (s',d,a,t)
+       else Just (s',d,a,t)
 
 
 defineTypeOp :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 defineTypeOp (s,d,a,t) =
     let stack = stackList s
-        oldthm = objThm $ stack!!0
-        namelist = map (objName) . objList $ stack!!1
-    in if ((typeVarsInTerm . tAppLeft . thmCon $ oldthm) /= (Set.fromList . map (\x -> TypeVar x) $ namelist) ||
-           (length namelist) /= (length . nub $ namelist))
+        result = Com.defineTypeOp (objThm $ stack!!0) (map (objName) . objList $ stack!!1)
+                                  (objName $ stack!!2) (objName $ stack!!3) (objName $ stack!!4)
+        (rthm, athm, rep, abst, n) = fromMaybe (nullThm, nullThm, nullConst, nullConst, nullTyOp) result
+        s' = Stack $ (ObjThm rthm) : (ObjThm athm) : (ObjConst rep) : (ObjConst abst) : (ObjTyOp n) : (drop 5 stack)
+    in if (isNothing result)
        then Nothing
-       else let rep = Const . objName $ stack!!2
-                abst = Const . objName $ stack!!3
-                n = TypeOp . objName $ stack!!4
-                rtype = typeOf . tAppRight . thmCon $ oldthm
-                atype = AType (map (\x -> TypeVar x) namelist) n
-                r' = TVar (Var (Name [] "r'") rtype)
-                a' = TVar (Var (Name [] "a'") atype)
-                reptype = typeFunc atype rtype
-                abstype = typeFunc rtype atype
-                repTerm = TConst rep reptype
-                absTerm = TConst abst abstype
-                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 Just (s',d,a,t)
+       else Just (s',d,a,t)
 
 
 eqMp :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 eqMp (s,d,a,t) =
     let stack = stackList s
-        thm1 = objThm $ stack!!0
-        thm2 = objThm $ stack!!1
-    in if ((thmCon thm1) /= (getlhs . thmCon $ thm2))
+        thm = Com.eqMp (objThm $ stack!!0) (objThm $ stack!!1)
+        s' = Stack $ (ObjThm $ fromMaybe nullThm thm) : (drop 2 stack)
+    in if (isNothing thm)
        then Nothing
-       else let op = (\x y -> Theorem (Set.union (thmHyp x) (thmHyp y))
-                                      (getrhs (thmCon y)))
-                theorem = ObjThm $ op thm1 thm2
-                s' = Stack $ theorem : (drop 2 stack)
-            in Just (s',d,a,t)
+       else Just (s',d,a,t)
 
 
 nil :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
@@ -276,8 +231,7 @@ nil (s,d,a,t) = Just (Stack $ ObjList [] : (stackList s), d, a, t)
 opType :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 opType (s,d,a,t) =
     let stack = stackList s
-        op = (\x y -> AType x y)
-        newType = ObjType $ op (map (objType) . objList $ stack!!0) (objTyOp $ stack!!1)
+        newType = ObjType $ Com.opType (map (objType) . objList $ stack!!0) (objTyOp $ stack!!1)
         s' = Stack $ newType : (drop 2 stack)
     in Just (s',d,a,t)
 
@@ -298,9 +252,8 @@ ref (s,d,a,t) =
 refl :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 refl (s,d,a,t) =
     let stack = stackList s
-        op = (\x -> Theorem Set.empty (mkEquals x x))
-        theorem = ObjThm $ op (objTerm $ stack!!0)
-        s' = Stack $ theorem : (tail stack)
+        thm = ObjThm $ Com.refl (objTerm $ stack!!0)
+        s' = Stack $ thm : (tail stack)
     in Just (s',d,a,t)
 
 
@@ -317,40 +270,27 @@ remove (s,d,a,t) =
 subst :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 subst (s,d,a,t) =
     let stack = stackList s
-        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
-                       f = (\g h x -> (g . head $ x, h . last $ x))
-                   in f (map (f objName objType)) (map (f objVar objTerm)) list)
-
-        theorem = ObjThm $ op (objThm $ stack!!0) (substitution $ stack!!1)
-        s' = Stack $ theorem : (drop 2 stack)
+        thm = ObjThm $ Com.subst (objThm $ stack!!0) (objList $ stack!!1)
+        s' = Stack $ thm : (drop 2 stack)
     in Just (s',d,a,t)
 
 
 thm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 thm (s,d,a,t) =
     let stack = stackList s
-        theorems = theoremSet t
-        term = objTerm $ stack!!0
-        termlist = map (objTerm) . objList $ stack!!1
-        oldthm = objThm $ stack!!2
-    in if ((term /= (thmCon oldthm)) || (Set.fromList termlist /= thmHyp oldthm))
+        thmSet = theoremSet t
+        thm = Com.thm (objTerm $ stack!!0) (map (objTerm) . objList $ stack!!1) (objThm $ stack!!2)
+        s' = Stack $ (drop 3 stack)
+        t' = Theorems $ Set.insert (fromMaybe nullThm thm) thmSet
+    in if (isNothing thm)
        then Nothing
-       else let op = (\x y z -> Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ z) y))
-                                        (alphaConvert (thmCon z) x))
-                theorem = ObjThm $ op term termlist oldthm
-                s' = Stack $ drop 3 stack
-                t' = Theorems $ Set.insert theorem theorems
-            in Just (s',d,a,t')
+       else Just (s',d,a,t')
 
 
 typeOp :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 typeOp (s,d,a,t) =
     let stack = stackList s
-        op = (\x -> TypeOp x)
-        typeOp = ObjTyOp $ op (objName $ stack!!0)
+        typeOp = ObjTyOp $ Com.typeOp (objName $ stack!!0)
         s' = Stack $ typeOp : (tail stack)
     in Just (s',d,a,t)
 
@@ -358,20 +298,17 @@ typeOp (s,d,a,t) =
 var :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 var (s,d,a,t) =
     let stack = stackList s
-        n = objName $ stack!!1
-    in if (nameSpace n /= [])
+        v = Com.var (objType $ stack!!0) (objName $ stack!!1)
+        s' = Stack $ (ObjVar $ fromMaybe nullVar v) : (drop 2 stack)
+    in if (isNothing v)
        then Nothing
-       else let op = (\x y -> Var y x)
-                var = ObjVar $ op (objType $ stack!!0) n
-                s' = Stack $ var : (drop 2 stack)
-            in Just (s',d,a,t)
+       else Just (s',d,a,t)
 
 
 varTerm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 varTerm (s,d,a,t) =
     let stack = stackList s
-        op = (\x -> TVar x)
-        term = ObjTerm $ op (objVar $ stack!!0)
+        term = ObjTerm $ Com.varTerm (objVar $ stack!!0)
         s' = Stack $ term : (tail stack)
     in Just (s',d,a,t)
 
@@ -379,13 +316,11 @@ varTerm (s,d,a,t) =
 varType :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 varType (s,d,a,t) =
     let stack = stackList s
-        n = objName $ stack!!0
-    in if (nameSpace n /= [])
+        newType = Com.varType (objName $ stack!!0)
+        s' = Stack $ (ObjType $ fromMaybe nullType newType) : (tail stack)
+    in if (isNothing newType)
        then Nothing
-       else let op = (\x -> TypeVar x)
-                newType = ObjType $ op n
-                s' = Stack $ newType : (tail stack)
-            in Just (s',d,a,t)
+       else Just (s',d,a,t)
 
 
 
diff --git a/Term.hs b/Term.hs
index 20c70ce..23fc5c5 100644
--- a/Term.hs
+++ b/Term.hs
@@ -1,5 +1,8 @@
 module Term (
     Term(..),
+    Substitution,
+
+    nullTerm,
 
     alphaEquiv,
     alphaConvert,
@@ -31,7 +34,8 @@ data Term = TVar { tVar :: Var }
           | TApp { tAppLeft :: Term
                  , tAppRight :: Term }
           | TAbs { tAbsVar :: Term
-                 , tAbsTerm :: Term } deriving (Ord)
+                 , tAbsTerm :: Term }
+          | TNull deriving (Ord)
 
 type Substitution = ( [(Name,Type)], [(Var,Term)] )
 
@@ -50,6 +54,10 @@ instance Eq Term where
 
 
 
+nullTerm :: Term
+nullTerm = TNull
+
+
 alphaEquiv :: Term -> Term -> Bool
 alphaEquiv a b =
     let equiv = \term1 term2 varmap1 varmap2 depth ->
diff --git a/Theorem.hs b/Theorem.hs
index c97a399..699c2e8 100644
--- a/Theorem.hs
+++ b/Theorem.hs
@@ -1,5 +1,7 @@
 module Theorem (
 	Theorem(..),
+
+	nullThm
 	) where
 
 
@@ -17,3 +19,8 @@ data Theorem = Theorem { thmHyp :: Set.Set Term
 
 instance Show Theorem where
     show a   =   (show . Set.toList . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a)
+
+
+
+nullThm :: Theorem
+nullThm = Theorem Set.empty nullTerm
diff --git a/TypeVar.hs b/TypeVar.hs
index 436cde4..aea20a5 100644
--- a/TypeVar.hs
+++ b/TypeVar.hs
@@ -11,6 +11,13 @@ module TypeVar (
 
 	Var(..),
 
+	nullNumber,
+	nullName,
+	nullTyOp,
+	nullType,
+	nullConst,
+	nullVar,
+
 	mkEqualsType,
 	typeFunc,
 	typeBool,
@@ -60,6 +67,26 @@ instance Show Var where
 
 
 
+nullNumber :: Number
+nullNumber = 0
+
+nullTyOp :: TypeOp
+nullTyOp = TypeOp nullName
+
+nullType :: Type
+nullType = TypeVar nullName
+
+nullName :: Name
+nullName = Name [] ""
+
+nullConst :: Const
+nullConst = Const nullName
+
+nullVar :: Var
+nullVar = Var nullName nullType
+
+
+
 mkEqualsType :: Type -> Type
 mkEqualsType ty = typeFunc ty (typeFunc ty typeBool)