diff options
| -rw-r--r-- | Command.hs | 214 | ||||
| -rw-r--r-- | Object.hs | 12 | ||||
| -rw-r--r-- | Semantic.hs | 221 | ||||
| -rw-r--r-- | Term.hs | 10 | ||||
| -rw-r--r-- | Theorem.hs | 7 | ||||
| -rw-r--r-- | TypeVar.hs | 27 |
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) + + @@ -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) @@ -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 -> @@ -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 @@ -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) |