diff options
Diffstat (limited to 'Library/Semantic.hs')
| -rw-r--r-- | Library/Semantic.hs | 360 |
1 files changed, 0 insertions, 360 deletions
diff --git a/Library/Semantic.hs b/Library/Semantic.hs deleted file mode 100644 index 0f08d52..0000000 --- a/Library/Semantic.hs +++ /dev/null @@ -1,360 +0,0 @@ -module Library.Semantic ( - MachineState, - machineToString, - eval, - doSemanticCheck - ) where - - - -import Data.List -import Data.Maybe -import Data.Set( Set ) -import qualified Data.Set as Set -import Data.Map( Map, (!) ) -import qualified Data.Map as Map -import Library.TypeVar -import Library.Term -import Library.Theorem -import Library.Object -import Library.Parse -import Library.Stack( Stack, at, (<:>) ) -import qualified Library.Stack as Stack -import qualified Library.Command as Com - - - -type MachineState = Maybe (Stack Object, - Map Int Object, --dictionary - Set Theorem, --assumptions - Set Theorem) --theorems - - -machineToString :: MachineState -> Maybe String -machineToString x = - do (s,d,a,t) <- x - let s' = show s - d' = "Dictionary:\n" ++ intercalate "\n" (map (show) (Map.toList d)) ++ "\n\n" - a' = "Assumptions:\n" ++ intercalate "\n" (map (show) (Set.toList a)) ++ "\n\n" - t' = "Theorems:\n" ++ intercalate "\n" (map (show) (Set.toList t)) ++ "\n\n" - return (s' ++ d' ++ a' ++ t') - - -data ArticleLine = Comment { commentString :: String } - | Command { commandFunc :: (MachineState -> MachineState) } - - - -parse :: String -> ArticleLine -parse "absTerm" = Command absTerm -parse "absThm" = Command absThm -parse "appTerm" = Command appTerm -parse "appThm" = Command appThm -parse "assume" = Command assume -parse "axiom" = Command axiom -parse "betaConv" = Command betaConv -parse "cons" = Command cons -parse "const" = Command constant -parse "constTerm" = Command constTerm -parse "deductAntisym" = Command deductAntisym -parse "def" = Command def -parse "defineConst" = Command defineConst -parse "defineTypeOp" = Command defineTypeOp -parse "eqMp" = Command eqMp -parse "nil" = Command nil -parse "opType" = Command opType -parse "pop" = Command pop -parse "ref" = Command ref -parse "refl" = Command refl -parse "remove" = Command remove -parse "subst" = Command subst -parse "thm" = Command thm -parse "typeOp" = Command typeOp -parse "var" = Command var -parse "varTerm" = Command varTerm -parse "varType" = Command varType -parse s@('#':rest) = Comment s -parse s@('"':rest) = Command (name s) -parse n = Command (number n) - - - -name :: String -> (MachineState -> MachineState) -name str x = - do (s,d,a,t) <- x - n <- Com.name str - let s' = (ObjName n) <:> s - return (s',d,a,t) - - -number :: String -> (MachineState -> MachineState) -number n x = - do (s,d,a,t) <- x - num <- Com.number n - let s' = (ObjNum num) <:> s - return (s',d,a,t) - - -absTerm :: MachineState -> MachineState -absTerm x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -absThm x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -appTerm x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -appThm x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -assume x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm - thm <- Com.assume te - let s' = (ObjThm thm) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -axiom :: MachineState -> MachineState -axiom x = - do (s,d,a,t) <- x - 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' = Set.insert thm a - return (s',d,a',t) - - -betaConv :: MachineState -> MachineState -betaConv x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm - let thm = Com.betaConv te - s' = (ObjThm thm) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -cons :: MachineState -> MachineState -cons x = - do (s,d,a,t) <- x - l <- (s `at` 0) >>= objList; h <- (s `at` 1) - let s' = (ObjList $ h : l) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -constant :: MachineState -> MachineState -constant x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objName - let constant = Com.constant n - s' = (ObjConst constant) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -constTerm :: MachineState -> MachineState -constTerm x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -deductAntisym x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -def x = - do (s,d,a,t) <- x - num <- (s `at` 0) >>= objNum; obj <- (s `at` 1) - let d' = Map.insert num obj d - s' = Stack.pop 1 s - return (s',d',a,t) - - -defineConst :: MachineState -> MachineState -defineConst x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -defineTypeOp x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -eqMp x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -nil x = - do (s,d,a,t) <- x - return (ObjList [] <:> s, d, a, t) - - -opType :: MachineState -> MachineState -opType x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -pop x = - do (s,d,a,t) <- x - return ((Stack.pop 1 s),d,a,t) - - -ref :: MachineState -> MachineState -ref x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objNum - let object = d ! n - s' = object <:> (Stack.pop 1 s) - return (s',d,a,t) - - -refl :: MachineState -> MachineState -refl x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm - let thm = Com.refl te - s' = (ObjThm thm) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -remove :: MachineState -> MachineState -remove x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objNum - let object = d ! n - s' = object <:> (Stack.pop 1 s) - d' = Map.delete n d - return (s',d',a,t) - - -subst :: MachineState -> MachineState -subst x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -thm x = - do (s,d,a,t) <- x - 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' = Set.insert thm t - return (s',d,a,t') - - -typeOp :: MachineState -> MachineState -typeOp x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objName - let typeOp = Com.typeOp n - s' = (ObjTyOp typeOp) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -var :: MachineState -> MachineState -var x = - do (s,d,a,t) <- x - 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 :: MachineState -> MachineState -varTerm x = - do (s,d,a,t) <- x - v <- (s `at` 0) >>= objVar - let term = Com.varTerm v - s' = (ObjTerm term) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -varType :: MachineState -> MachineState -varType x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objName - newType <- Com.varType n - let s' = (ObjType newType) <:> (Stack.pop 1 s) - return (s',d,a,t) - - - -eval :: [String] -> MachineState -eval list = - let s = Stack.empty - d = Map.empty - a = Set.empty - t = Set.empty - op = (\x y -> case y of (Comment _) -> x - (Command z) -> z x) - - -- important to use foldl here so commands get applied in the correct order - result = (foldl' (op) (Just (s,d,a,t))) . (map (parse)) $ list - - in result - - - -doSemanticCheck :: [String] -> String -doSemanticCheck list = - case (machineToString (eval list)) of - Just x -> x - Nothing -> "Error\n" - |