summaryrefslogtreecommitdiff
path: root/src/Library/Semantic.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Library/Semantic.hs')
-rw-r--r--src/Library/Semantic.hs360
1 files changed, 360 insertions, 0 deletions
diff --git a/src/Library/Semantic.hs b/src/Library/Semantic.hs
new file mode 100644
index 0000000..0f08d52
--- /dev/null
+++ b/src/Library/Semantic.hs
@@ -0,0 +1,360 @@
+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"
+
generated by cgit (git 2.30.0) at 2024-04-26 17:46:08 +0000