From 5faabaf240316300e48cf37eae0d5e2bfd0ec66c Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Tue, 29 May 2012 07:30:50 +1000 Subject: All potential errors now caught into Nothings --- Command.hs | 8 +- Object.hs | 103 ++++++++++++++++--- Semantic.hs | 326 ++++++++++++++++++++++++++++-------------------------------- Term.hs | 9 +- Theorem.hs | 7 -- TypeVar.hs | 27 ----- 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) -- cgit