From 09fa09802554e8935e271ab73990032944bb760d Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Mon, 4 Jun 2012 18:03:25 +1000 Subject: Cleaned up how the state of the virtual machine is handled --- Semantic.hs | 285 ++++++++++++++++++++++++++++++++++-------------------------- 1 file changed, 160 insertions(+), 125 deletions(-) diff --git a/Semantic.hs b/Semantic.hs index afa8f75..a177d08 100644 --- a/Semantic.hs +++ b/Semantic.hs @@ -1,10 +1,10 @@ -module Main (main) where - - import System( getArgs ) +import Text.Printf 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 TypeVar import Term @@ -16,24 +16,25 @@ import qualified Stack as Stack import qualified Command as Com -data Dictionary = Dictionary { dictionMap :: Map.Map Int Object } -data Assumptions = Assumptions { assumeSet :: Set.Set Theorem } -data Theorems = Theorems { theoremSet :: Set.Set Theorem } - - -instance Show Dictionary where - show a = "Dictionary:\n" ++ intercalate "\n" (map (show) (Map.toList . dictionMap $ a)) ++ "\n\n" -instance Show Assumptions where - show a = "Assumptions:\n" ++ intercalate "\n" (map (show) (Set.toList . assumeSet $ a)) ++ "\n\n" +type MachineState = Maybe (Stack Object, + Map Int Object, --dictionary + Set Theorem, --assumptions + Set Theorem) --theorems -instance Show Theorems where - show a = "Theorems:\n" ++ intercalate "\n" (map (show) (Set.toList . theoremSet $ a)) ++ "\n\n" +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 :: ((Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)) } + | Command { commandFunc :: (MachineState -> MachineState) } @@ -71,248 +72,282 @@ parse n = Command (number n) -name :: String -> ((Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)) -name str = \(s,d,a,t) -> - do n <- Com.name str - let s' = (ObjName n) <:> s - return (s',d,a,t) +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 -> ((Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems)) -number n = \(s,d,a,t) -> - do num <- Com.number n - let s' = (ObjNum num) <:> 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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -absTerm (s,d,a,t) = - do te <- (s `at` 0) >>= objTerm; v <- (s `at` 1) >>= objVar +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -absThm (s,d,a,t) = - do th <- (s `at` 0) >>= objThm; v <- (s `at` 1) >>= objVar +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -appTerm (s,d,a,t) = - do f <- (s `at` 0) >>= objTerm; x <- (s `at` 1) >>= objTerm +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -appThm (s,d,a,t) = - do t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -assume (s,d,a,t) = - do te <- (s `at` 0) >>= objTerm +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -axiom (s,d,a,t) = - do te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList +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' = Assumptions $ Set.insert thm (assumeSet a) + a' = Set.insert thm a return (s',d,a',t) -betaConv :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -betaConv (s,d,a,t) = - do te <- (s `at` 0) >>= objTerm +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -cons (s,d,a,t) = - do l <- (s `at` 0) >>= objList; h <- (s `at` 1) - let newList = h : l - s' = (ObjList newList) <:> (Stack.pop 2 s) +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -constant (s,d,a,t) = - do n <- (s `at` 0) >>= objName +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -constTerm (s,d,a,t) = - do ty <- (s `at` 0) >>= objType; c <- (s `at` 1) >>= objConst +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -deductAntisym (s,d,a,t) = - do t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -def (s,d,a,t) = - do n <- (s `at` 0) >>= objNum; h <- (s `at` 1) - let d' = Dictionary $ Map.insert n h (dictionMap d) - s' = (Stack.pop 1 s) +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -defineConst (s,d,a,t) = - do te <- (s `at` 0) >>= objTerm; n <- (s `at` 1) >>= objName +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -defineTypeOp (s,d,a,t) = - do th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList; r <- (s `at` 2) >>= objName +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -eqMp (s,d,a,t) = - do t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -nil (s,d,a,t) = Just (ObjList [] <:> s, d, a, t) +nil :: MachineState -> MachineState +nil x = + do (s,d,a,t) <- x + return (ObjList [] <:> s, d, a, t) -opType :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -opType (s,d,a,t) = - do l <- (s `at` 0) >>= objList; to <- (s `at` 1) >>= objTyOp +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -pop (s,d,a,t) = Just ((Stack.pop 1 s),d,a,t) +pop :: MachineState -> MachineState +pop x = + do (s,d,a,t) <- x + return ((Stack.pop 1 s),d,a,t) -ref :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -ref (s,d,a,t) = - do n <- (s `at` 0) >>= objNum - let object = (dictionMap d) Map.! n +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -refl (s,d,a,t) = - do te <- (s `at` 0) >>= objTerm +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -remove (s,d,a,t) = - do n <- (s `at` 0) >>= objNum - let object = (dictionMap d) Map.! n +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' = Dictionary $ Map.delete n (dictionMap d) + d' = Map.delete n d return (s',d',a,t) -subst :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -subst (s,d,a,t) = - do th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -thm (s,d,a,t) = - do te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList; th <- (s `at` 2) >>= objThm +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' = Theorems $ Set.insert thm (theoremSet t) + t' = Set.insert thm t return (s',d,a,t') -typeOp :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -typeOp (s,d,a,t) = - do n <- (s `at` 0) >>= objName +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -var (s,d,a,t) = - do ty <- (s `at` 0) >>= objType; n <- (s `at` 1) >>= objName +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -varTerm (s,d,a,t) = - do v <- (s `at` 0) >>= objVar +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 :: (Stack Object,Dictionary,Assumptions,Theorems) -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -varType (s,d,a,t) = - do n <- (s `at` 0) >>= objName +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) -doSemanticCheck :: [String] -> Maybe (Stack Object,Dictionary,Assumptions,Theorems) -doSemanticCheck = +doSemanticCheck :: [String] -> String +doSemanticCheck list = let s = Stack.empty - d = Dictionary Map.empty - a = Assumptions Set.empty - t = Theorems Set.empty - op = (\x y -> case x of (Nothing) -> Nothing - (Just w) -> case y of (Comment _) -> x - (Command z) -> z w) - in (foldl' (op) (Just (s,d,a,t))) . (map (parse)) - -- important to use foldl here so commands get applied in the correct order + 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 case (machineToString result) of + Just x -> x + Nothing -> "Error\n" + main = do args <- getArgs list <- getLines $ head args - result <- return $ doSemanticCheck (map (stripReturn) list) - print $ result + let result = doSemanticCheck (map (stripReturn) list) + printf result -- cgit