diff options
Diffstat (limited to 'Semantic.hs')
-rw-r--r-- | Semantic.hs | 221 |
1 files changed, 78 insertions, 143 deletions
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) |