Added guards for command functions

1 files changed, 160 insertions, 126 deletions

diff --git a/Semantic.hs b/Semantic.hs
index e40f4bc..73b489e 100644
--- a/Semantic.hs
+++ b/Semantic.hs
@@ -1,5 +1,6 @@
 import System( getArgs )
 import Data.List
+import Data.Maybe
 import qualified Data.Set as Set
 import qualified Data.Map as Map
 import TypeVar
@@ -30,7 +31,7 @@ instance Show Theorems where
 
 
 data ArticleLine = Comment { commentString :: String }
-                 | Command { commandFunc :: ((Stack,Dictionary,Assumptions,Theorems)->(Stack,Dictionary,Assumptions,Theorems)) }
+                 | Command { commandFunc :: ((Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)) }
 
 
 
@@ -68,49 +69,57 @@ parse n = Command (number n)
 
 
 
-name :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems))
+name :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems))
 name str = \(s,d,a,t) ->
-               let wordList = (separateBy '.') . removeEscChars . removeQuotes $ str
-                   name = Name (init wordList) (last wordList)
-                   s' = Stack $ ObjName name : (stackList s)
-               in (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)
 
 
-number :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems))
-number n = \(s,d,a,t) -> (Stack $ ObjNum (read n) : (stackList 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)
 
 
-absTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
--- need to add guards to check that the variable is not free in the hypothesis
-absThm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+absThm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 absThm (s,d,a,t) =
     let stack = stackList s
-        op = (\x y -> Theorem (thmHyp x)
-                              (mkEquals (TAbs (TVar y) (getlhs . thmCon $ x))
-                                        (TAbs (TVar y) (getrhs . thmCon $ x))))
-        theorem = ObjThm $ op (objThm $ stack!!0) (objVar $ stack!!1)
-        s' = Stack $ theorem : (drop 2 stack)
-    in (s',d,a,t)
-
-
-appTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+        oldthm = objThm $ stack!!0
+        var = objVar $ stack!!1
+    in if (Set.member (TVar var) (thmHyp oldthm))
+       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)
+
+
+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)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-appThm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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))
@@ -118,31 +127,36 @@ appThm (s,d,a,t) =
                                         (TApp (getrhs . thmCon $ y) (getrhs . thmCon $ x))))
         theorem = ObjThm $ op (objThm $ stack!!0) (objThm $ stack!!1)
         s' = Stack $ theorem : (drop 2 stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-assume :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+assume :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 assume (s,d,a,t) =
     let stack = stackList s
-        op = (\x -> Theorem (Set.singleton x) x)
-        theorem = ObjThm $ op (objTerm $ stack!!0)
-        s' = Stack $ theorem : (tail stack)
-    in (s',d,a,t)
+        term = objTerm $ stack!!0
+    in if (typeOf term /= typeBool)
+       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)
 
 
--- need to add guarding for all terms being of type bool
-axiom :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+axiom :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 axiom (s,d,a,t) =
     let stack = stackList s
         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 $ Set.insert theorem assumptions
-    in (s',d,a',t)
+        termList = (map (objTerm) . objList $ stack!!1)
+    in if (filter (\x -> typeOf x /= typeBool) termList /= [])
+       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)
 
 
-betaConv :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+betaConv :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 betaConv (s,d,a,t) =
     let stack = stackList s
         op = (\x -> Theorem (Set.empty)
@@ -151,37 +165,37 @@ betaConv (s,d,a,t) =
                                                   (tAbsTerm . tAppLeft $ x))))
         theorem = ObjThm $ op (objTerm $ stack!!0)
         s' = Stack $ theorem : (tail stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-cons :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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)
         s' = Stack $ newList : (drop 2 stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-constant :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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)
         s' = Stack $ constant : (tail stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-constTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-deductAntisym :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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))
@@ -189,110 +203,118 @@ deductAntisym (s,d,a,t) =
                               (mkEquals (thmCon $ y) (thmCon $ x)))
         theorem = ObjThm $ op (objThm $ stack!!0) (objThm $ stack!!1)
         s' = Stack $ theorem : (drop 2 stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-def :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+def :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 def (s,d,a,t) =
     let stack = stackList s
         d' = Dictionary $ Map.insert (objNum $ stack!!0) (stack!!1) (dictionMap d)
         s' = Stack $ tail stack
-    in (s',d',a,t)
+    in Just (s',d',a,t)
 
 
-defineConst :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+defineConst :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 defineConst (s,d,a,t) =
     let stack = stackList s
-        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 (s',d,a,t)
-
-
-defineTypeOp :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+        term = objTerm $ stack!!0
+    in if (freeVars term /= Set.empty || typeVarsInTerm term /= typeVarsInType (typeOf term))
+       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)
+
+
+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
-        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 (s',d,a,t)
-
-
-eqMp :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+    in if ((typeVarsInTerm . tAppLeft . thmCon $ oldthm) /= (Set.fromList . map (\x -> TypeVar x) $ namelist) ||
+           (length namelist) /= (length . nub $ namelist))
+       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)
+
+
+eqMp :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 eqMp (s,d,a,t) =
     let stack = stackList s
-        op = (\x y -> if (thmCon x == (getlhs (thmCon y))) then
-                      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)
-        s' = Stack $ theorem : (drop 2 stack)
-    in (s',d,a,t)
+        thm1 = objThm $ stack!!0
+        thm2 = objThm $ stack!!1
+    in if ((thmCon thm1) /= (getlhs . thmCon $ thm2))
+       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)
 
 
-nil :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
-nil (s,d,a,t) = (Stack $ ObjList [] : (stackList s), d, a, t)
+nil :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+nil (s,d,a,t) = Just (Stack $ ObjList [] : (stackList s), d, a, t)
 
 
-opType :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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)
         s' = Stack $ newType : (drop 2 stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-pop :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
-pop (s,d,a,t) = (Stack $ tail (stackList s),d,a,t)
+pop :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+pop (s,d,a,t) = Just (Stack $ tail (stackList s),d,a,t)
 
 
-ref :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+ref :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 ref (s,d,a,t) =
     let stack = stackList s
         dictionary = dictionMap d
         object = dictionary Map.! (objNum $ stack!!0)
         s' = Stack $ object : tail stack
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-refl :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-remove :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+remove :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 remove (s,d,a,t) =
     let stack = stackList s
         dictionary = dictionMap d
         object = dictionary Map.! (objNum $ stack!!0)
         s' = Stack $ object : tail stack
         d' = Dictionary $ Map.delete (objNum $ stack!!0) dictionary
-    in (s',d',a,t)
+    in Just (s',d',a,t)
 
 
-subst :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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))
@@ -304,67 +326,79 @@ subst (s,d,a,t) =
 
         theorem = ObjThm $ op (objThm $ stack!!0) (substitution $ stack!!1)
         s' = Stack $ theorem : (drop 2 stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-thm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+thm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 thm (s,d,a,t) =
     let stack = stackList s
         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 $ Set.insert theorem theorems
-    in (s',d,a,t')
-
-
-typeOp :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+        term = objTerm $ stack!!0
+        termlist = map (objTerm) . objList $ stack!!1
+        oldthm = objThm $ stack!!2
+    in if ((term /= (thmCon oldthm)) || (Set.fromList termlist /= thmHyp oldthm))
+       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')
+
+
+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)
         s' = Stack $ typeOp : (tail stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-var :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+var :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 var (s,d,a,t) =
     let stack = stackList s
-        op = (\x y -> Var y x)
-        var = ObjVar $ op (objType $ stack!!0) (objName $ stack!!1)
-        s' = Stack $ var : (drop 2 stack)
-    in (s',d,a,t)
+        n = objName $ stack!!1
+    in if (nameSpace n /= [])
+       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)
 
 
-varTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+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)
         s' = Stack $ term : (tail stack)
-    in (s',d,a,t)
+    in Just (s',d,a,t)
 
 
-varType :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)
+varType :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 varType (s,d,a,t) =
     let stack = stackList s
-        op = (\x -> TypeVar x)
-        newType = ObjType $ op (objName $ stack!!0)
-        s' = Stack $ newType : (tail stack)
-    in (s',d,a,t)
+        n = objName $ stack!!0
+    in if (nameSpace n /= [])
+       then Nothing
+       else let op = (\x -> TypeVar x)
+                newType = ObjType $ op n
+                s' = Stack $ newType : (tail stack)
+            in Just (s',d,a,t)
 
 
 
-doSemanticCheck :: [String] -> (Stack,Dictionary,Assumptions,Theorems)
+doSemanticCheck :: [String] -> Maybe (Stack,Dictionary,Assumptions,Theorems)
 doSemanticCheck =
     let s = Stack []
         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))
+        op = (\x y -> case x of (Nothing) -> Nothing
+                                (Just w) -> case y of (Comment _) -> x
+                                                      (Command z) -> z w)
+    in (foldl' (op) (Just (s,d,a,t))) . (map (parse))
     -- important to use foldl here so commands get applied in the correct order