All potential errors now caught into Nothings

6 files changed, 246 insertions, 234 deletions

diff --git a/Command.hs b/Command.hs
index 6df88f8..e6e0e39 100644
--- a/Command.hs
+++ b/Command.hs
@@ -173,11 +173,11 @@ refl term =
 	Theorem Set.empty (mkEquals term term)
 
 
-subst :: Theorem -> [Object] -> Theorem
+subst :: Theorem -> [Object] -> Maybe Theorem
 subst thm list =
-	let s = makeSubst list
-	in Theorem (Set.map (substitute s) (thmHyp thm))
-               (substitute s (thmCon thm))
+	do s <- makeSubst list
+	   return (Theorem (Set.map (substitute s) (thmHyp thm))
+                       (substitute s (thmCon thm)))
 
 
 thm :: Term -> [Term] -> Theorem -> Maybe Theorem
diff --git a/Object.hs b/Object.hs
index 5d0e71e..0fa1736 100644
--- a/Object.hs
+++ b/Object.hs
@@ -1,5 +1,14 @@
 module Object (
 	Object(..),
+    objNum,
+    objName,
+    objList,
+    objTyOp,
+    objType,
+    objConst,
+    objVar,
+    objTerm,
+    objThm,
 
 	List,
 
@@ -8,6 +17,7 @@ module Object (
 
 
 
+import Data.Maybe
 import Data.List
 import TypeVar
 import Term
@@ -15,15 +25,15 @@ import Theorem
 
 
 
-data Object = ObjNum { objNum :: Number }
-            | ObjName { objName :: Name }
-            | ObjList { objList :: List }
-            | ObjTyOp { objTyOp :: TypeOp }
-            | ObjType { objType :: Type }
-            | ObjConst { objConst :: Const }
-            | ObjVar { objVar :: Var }
-            | ObjTerm { objTerm :: Term }
-            | ObjThm { objThm :: Theorem } deriving (Eq, Ord)
+data Object = ObjNum Number
+            | ObjName Name
+            | ObjList List
+            | ObjTyOp TypeOp
+            | ObjType Type
+            | ObjConst Const
+            | ObjVar Var
+            | ObjTerm Term
+            | ObjThm Theorem deriving (Eq, Ord)
 
 type List = [Object]
 
@@ -42,8 +52,77 @@ instance Show Object where
 
 
 
-makeSubst :: [Object] -> Substitution
+makeSubst :: [Object] -> Maybe Substitution
 makeSubst l =
-    let list = (map (map objList)) . (map objList) $ l
+    let list = (map (mapMaybe objList)) . (mapMaybe objList) $ l
         f = (\g h x -> (g . head $ x, h . last $ x))
-    in f (map (f objName objType)) (map (f objVar objTerm)) list
+        check = f (map (f objName objType)) (map (f objVar objTerm)) list
+        g = all (\x -> (isJust . fst $ x) && (isJust . snd $ x))
+        h = (\x -> (fromJust . fst $ x, fromJust . snd $ x))
+    in if ((g . fst $ check) && (g . snd $ check))
+       then Just (map h (fst check), map h (snd check))
+       else Nothing
+
+
+objNum :: Object -> Maybe Number
+objNum obj =
+    case (obj) of
+        (ObjNum n) -> Just n
+        (_) -> Nothing
+
+
+objName :: Object -> Maybe Name
+objName obj =
+    case (obj) of
+        (ObjName n) -> Just n
+        (_) -> Nothing
+
+
+objList :: Object -> Maybe List
+objList obj =
+    case (obj) of
+        (ObjList l) -> Just l
+        (_) -> Nothing
+
+
+objTyOp :: Object -> Maybe TypeOp
+objTyOp obj =
+    case (obj) of
+        (ObjTyOp tyop) -> Just tyop
+        (_) -> Nothing
+
+
+objType :: Object -> Maybe Type
+objType obj =
+    case (obj) of
+        (ObjType ty) -> Just ty
+        (_) -> Nothing
+
+
+objConst :: Object -> Maybe Const
+objConst obj =
+    case (obj) of
+        (ObjConst c) -> Just c
+        (_) -> Nothing
+
+
+objVar :: Object -> Maybe Var
+objVar obj =
+    case (obj) of
+        (ObjVar var) -> Just var
+        (_) -> Nothing
+
+
+objTerm :: Object -> Maybe Term
+objTerm obj =
+    case (obj) of
+        (ObjTerm term) -> Just term
+        (_) -> Nothing
+
+
+objThm :: Object -> Maybe Theorem
+objThm obj =
+    case (obj) of
+        (ObjThm thm) -> Just thm
+        (_) -> Nothing
+
diff --git a/Semantic.hs b/Semantic.hs
index 6a53d49..afa8f75 100644
--- a/Semantic.hs
+++ b/Semantic.hs
@@ -1,3 +1,6 @@
+module Main (main) where
+
+
 import System( getArgs )
 import Data.List
 import Data.Maybe
@@ -8,18 +11,16 @@ import Term
 import Theorem
 import Object
 import Parse
+import Stack( Stack, at, (<:>) )
+import qualified Stack as Stack
 import qualified Command as Com
 
 
-data Stack = Stack { stackList :: [Object] }
 data Dictionary = Dictionary { dictionMap :: Map.Map Int Object }
 data Assumptions = Assumptions { assumeSet :: Set.Set Theorem }
 data Theorems = Theorems { theoremSet :: Set.Set Theorem }
 
 
-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) (Map.toList . dictionMap $ a)) ++ "\n\n"
 
@@ -30,8 +31,9 @@ instance Show Theorems where
     show a   =   "Theorems:\n" ++ intercalate "\n" (map (show) (Set.toList . theoremSet $ a)) ++ "\n\n"
 
 
+
 data ArticleLine = Comment { commentString :: String }
-                 | Command { commandFunc :: ((Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)) }
+                 | Command { commandFunc :: ((Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)) }
 
 
 
@@ -69,264 +71,236 @@ parse n = Command (number n)
 
 
 
-name :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems))
+name :: String -> ((Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems))
 name str = \(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)
+               do n <- Com.name str
+                  let s' = (ObjName n) <:> s
+                  return (s',d,a,t)
 
 
-number :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems))
+number :: String -> ((Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems))
 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)
+               do num <- Com.number n
+                  let s' = (ObjNum num) <:> s
+                  return (s',d,a,t)
 
 
-absTerm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+absTerm :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 absTerm (s,d,a,t) =
-    let stack = stackList s
-        term = ObjTerm $ Com.absTerm (objTerm $ stack!!0) (objVar $ stack!!1)
-        s' = Stack $ term : (drop 2 stack)
-    in Just (s',d,a,t)
+    do te <- (s `at` 0) >>= objTerm; v <- (s `at` 1) >>= objVar
+       let term = Com.absTerm te v
+           s' = (ObjTerm term) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-absThm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+absThm :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 absThm (s,d,a,t) =
-    let stack = stackList s
-        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 Just (s',d,a,t)
+    do th <- (s `at` 0) >>= objThm; v <- (s `at` 1) >>= objVar
+       thm <- Com.absThm th v
+       let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-appTerm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+appTerm :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 appTerm (s,d,a,t) =
-    let stack = stackList s
-        term = ObjTerm $ Com.appTerm (objTerm $ stack!!0) (objTerm $ stack!!1)
-        s' = Stack $ term : (drop 2 stack)
-    in Just (s',d,a,t)
+    do f <- (s `at` 0) >>= objTerm; x <- (s `at` 1) >>= objTerm
+       let term = Com.appTerm f x
+           s' = (ObjTerm term) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-appThm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+appThm :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 appThm (s,d,a,t) =
-    let stack = stackList s
-        thm = ObjThm $ Com.appThm (objThm $ stack!!0) (objThm $ stack!!1)
-        s' = Stack $ thm : (drop 2 stack)
-    in Just (s',d,a,t)
+    do t1 <- (s  `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+       let thm = Com.appThm t1 t2
+           s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-assume :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+assume :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 assume (s,d,a,t) =
-    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 Just (s',d,a,t)
+    do te <- (s `at` 0) >>= objTerm
+       thm <- Com.assume te
+       let s' = (ObjThm thm) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
 
 
-axiom :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+axiom :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 axiom (s,d,a,t) =
-    let stack = stackList s
-        assumptions = assumeSet a
-        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 Just (s',d,a',t)
+    do te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList
+       thm <- Com.axiom te (mapMaybe objTerm l)
+       let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+           a' = Assumptions $ Set.insert thm (assumeSet a)
+       return (s',d,a',t)
 
 
-betaConv :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+betaConv :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 betaConv (s,d,a,t) =
-    let stack = stackList s
-        thm = ObjThm $ Com.betaConv (objTerm $ stack!!0)
-        s' = Stack $ thm : (tail stack)
-    in Just (s',d,a,t)
+    do te <- (s `at` 0) >>= objTerm
+       let thm = Com.betaConv te
+           s' = (ObjThm thm) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
 
 
-cons :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+cons :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 cons (s,d,a,t) =
-    let stack = stackList s
-        newList = ObjList $ (stack!!1) : (objList $ stack!!0)
-        s' = Stack $ newList : (drop 2 stack)
-    in Just (s',d,a,t)
+    do l <- (s `at` 0) >>= objList; h <- (s `at` 1)
+       let newList = h : l
+           s' = (ObjList newList) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-constant :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+constant :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 constant (s,d,a,t) =
-    let stack = stackList s
-        constant = ObjConst $ Com.constant (objName $ stack!!0)
-        s' = Stack $ constant : (tail stack)
-    in Just (s',d,a,t)
+    do n <- (s `at` 0) >>= objName
+       let constant = Com.constant n
+           s' = (ObjConst constant) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
 
 
-constTerm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+constTerm :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 constTerm (s,d,a,t) =
-    let stack = stackList s
-        term = ObjTerm $ Com.constTerm (objType $ stack!!0) (objConst $ stack!!1)
-        s' = Stack $ term : (drop 2 stack)
-    in Just (s',d,a,t)
+    do ty <- (s `at` 0) >>= objType; c <- (s `at` 1) >>= objConst
+       let term = Com.constTerm ty c
+           s' = (ObjTerm term) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-deductAntisym :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+deductAntisym :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 deductAntisym (s,d,a,t) =
-    let stack = stackList s
-        thm = ObjThm $ Com.deductAntisym (objThm $ stack!!0) (objThm $ stack!!1)
-        s' = Stack $ thm : (drop 2 stack)
-    in Just (s',d,a,t)
+    do t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+       let thm = Com.deductAntisym t1 t2
+           s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-def :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+def :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,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 Just (s',d',a,t)
+    do n <- (s `at` 0) >>= objNum; h <- (s `at` 1)
+       let d' = Dictionary $ Map.insert n h (dictionMap d)
+           s' = (Stack.pop 1 s)
+       return (s',d',a,t)
 
 
-defineConst :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+defineConst :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 defineConst (s,d,a,t) =
-    let stack = stackList s
-        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 Just (s',d,a,t)
+    do te <- (s `at` 0) >>= objTerm; n <- (s `at` 1) >>= objName
+       (thm, constant) <- Com.defineConst te n
+       let s' = (ObjThm thm) <:> (ObjConst constant) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-defineTypeOp :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+defineTypeOp :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 defineTypeOp (s,d,a,t) =
-    let stack = stackList s
-        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 Just (s',d,a,t)
+    do th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList; r <- (s `at` 2) >>= objName
+       ab <- (s `at` 3) >>= objName; y <- (s `at` 4) >>= objName
+       (rthm, athm, rep, abst, n) <- Com.defineTypeOp th (mapMaybe objName l) r ab y
+       let s' = (ObjThm rthm) <:> (ObjThm athm) <:> (ObjConst rep) <:> (ObjConst abst) <:> (ObjTyOp n) <:> (Stack.pop 5 s)
+       return (s',d,a,t)
 
 
-eqMp :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+eqMp :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 eqMp (s,d,a,t) =
-    let stack = stackList s
-        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 Just (s',d,a,t)
+    do t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+       thm <- Com.eqMp t1 t2
+       let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (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)
+nil :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
+nil (s,d,a,t) = Just (ObjList [] <:> s, d, a, t)
 
 
-opType :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+opType :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 opType (s,d,a,t) =
-    let stack = stackList s
-        newType = ObjType $ Com.opType (map (objType) . objList $ stack!!0) (objTyOp $ stack!!1)
-        s' = Stack $ newType : (drop 2 stack)
-    in Just (s',d,a,t)
+    do l <- (s `at` 0) >>= objList; to <- (s `at` 1) >>= objTyOp
+       let newType = Com.opType (mapMaybe objType l) to
+           s' = (ObjType newType) <:> (Stack.pop 2 s)
+       return (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)
+pop :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
+pop (s,d,a,t) = Just ((Stack.pop 1 s),d,a,t)
 
 
-ref :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+ref :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,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 Just (s',d,a,t)
+    do n <- (s `at` 0) >>= objNum
+       let object = (dictionMap d) Map.! n
+           s' = object <:> (Stack.pop 1 s)
+       return (s',d,a,t)
 
 
-refl :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+refl :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 refl (s,d,a,t) =
-    let stack = stackList s
-        thm = ObjThm $ Com.refl (objTerm $ stack!!0)
-        s' = Stack $ thm : (tail stack)
-    in Just (s',d,a,t)
+    do te <- (s `at` 0) >>= objTerm
+       let thm = Com.refl te
+           s' = (ObjThm thm) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
 
 
-remove :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+remove :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,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 Just (s',d',a,t)
+    do n <- (s `at` 0) >>= objNum
+       let object = (dictionMap d) Map.! n
+           s' = object <:> (Stack.pop 1 s)
+           d' = Dictionary $ Map.delete n (dictionMap d)
+       return (s',d',a,t)
 
 
-subst :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+subst :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 subst (s,d,a,t) =
-    let stack = stackList s
-        thm = ObjThm $ Com.subst (objThm $ stack!!0) (objList $ stack!!1)
-        s' = Stack $ thm : (drop 2 stack)
-    in Just (s',d,a,t)
+    do th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList
+       thm <- Com.subst th l
+       let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-thm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+thm :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 thm (s,d,a,t) =
-    let stack = stackList s
-        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 Just (s',d,a,t')
+    do te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList; th <- (s `at` 2) >>= objThm
+       thm <- Com.thm te (mapMaybe objTerm l) th
+       let s' = Stack.pop 3 s
+           t' = Theorems $ Set.insert thm (theoremSet t)
+       return (s',d,a,t')
 
 
-typeOp :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+typeOp :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 typeOp (s,d,a,t) =
-    let stack = stackList s
-        typeOp = ObjTyOp $ Com.typeOp (objName $ stack!!0)
-        s' = Stack $ typeOp : (tail stack)
-    in Just (s',d,a,t)
+    do n <- (s `at` 0) >>= objName
+       let typeOp = Com.typeOp n
+           s' = (ObjTyOp typeOp) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
 
 
-var :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+var :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 var (s,d,a,t) =
-    let stack = stackList s
-        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 Just (s',d,a,t)
+    do ty <- (s `at` 0) >>= objType; n <- (s `at` 1) >>= objName
+       v <- Com.var ty n
+       let s' = (ObjVar v) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
 
 
-varTerm :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+varTerm :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 varTerm (s,d,a,t) =
-    let stack = stackList s
-        term = ObjTerm $ Com.varTerm (objVar $ stack!!0)
-        s' = Stack $ term : (tail stack)
-    in Just (s',d,a,t)
+    do v <- (s `at` 0) >>= objVar
+       let term = Com.varTerm v
+           s' = (ObjTerm term) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
 
 
-varType :: (Stack,Dictionary,Assumptions,Theorems) -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+varType :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 varType (s,d,a,t) =
-    let stack = stackList s
-        newType = Com.varType (objName $ stack!!0)
-        s' = Stack $ (ObjType $ fromMaybe nullType newType) : (tail stack)
-    in if (isNothing newType)
-       then Nothing
-       else Just (s',d,a,t)
+    do n <- (s `at` 0) >>= objName
+       newType <- Com.varType n
+       let s' = (ObjType newType) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
 
 
 
-doSemanticCheck :: [String] -> Maybe (Stack,Dictionary,Assumptions,Theorems)
+doSemanticCheck :: [String] -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)
 doSemanticCheck =
-    let s = Stack []
+    let s = Stack.empty
         d = Dictionary Map.empty
         a = Assumptions Set.empty
         t = Theorems Set.empty
diff --git a/Term.hs b/Term.hs
index 23fc5c5..dfcf1cf 100644
--- a/Term.hs
+++ b/Term.hs
@@ -2,8 +2,6 @@ module Term (
     Term(..),
     Substitution,
 
-    nullTerm,
-
     alphaEquiv,
     alphaConvert,
     alphaConvertList,
@@ -34,8 +32,7 @@ data Term = TVar { tVar :: Var }
           | TApp { tAppLeft :: Term
                  , tAppRight :: Term }
           | TAbs { tAbsVar :: Term
-                 , tAbsTerm :: Term }
-          | TNull deriving (Ord)
+                 , tAbsTerm :: Term } deriving (Ord)
 
 type Substitution = ( [(Name,Type)], [(Var,Term)] )
 
@@ -54,10 +51,6 @@ 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 699c2e8..c97a399 100644
--- a/Theorem.hs
+++ b/Theorem.hs
@@ -1,7 +1,5 @@
 module Theorem (
 	Theorem(..),
-
-	nullThm
 	) where
 
 
@@ -19,8 +17,3 @@ 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 aea20a5..436cde4 100644
--- a/TypeVar.hs
+++ b/TypeVar.hs
@@ -11,13 +11,6 @@ module TypeVar (
 
 	Var(..),
 
-	nullNumber,
-	nullName,
-	nullTyOp,
-	nullType,
-	nullConst,
-	nullVar,
-
 	mkEqualsType,
 	typeFunc,
 	typeBool,
@@ -67,26 +60,6 @@ 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)