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