summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Command.hs8
-rw-r--r--Object.hs103
-rw-r--r--Semantic.hs326
-rw-r--r--Term.hs9
-rw-r--r--Theorem.hs7
-rw-r--r--TypeVar.hs27
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)
generated by cgit (git 2.30.0) at 2024-12-22 20:42:40 +0000