diff options
| -rw-r--r-- | Semantic.hs | 313 |
1 files changed, 193 insertions, 120 deletions
diff --git a/Semantic.hs b/Semantic.hs index 79b03d0..130deeb 100644 --- a/Semantic.hs +++ b/Semantic.hs @@ -21,11 +21,11 @@ data Name = Name { nameSpace :: [String] type List = [Object] -data TypeOp = TypeOp { tyOp :: Name } deriving (Eq) +data TypeOp = TypeOp { tyOp :: Name } deriving (Eq, Show) data Type = TypeVar { typeVar :: Name } | AType { aType :: [Type] - , aTypeOp :: TypeOp } deriving (Eq) + , aTypeOp :: TypeOp } deriving (Eq, Show) data Const = Const { constName :: Name } deriving (Eq) @@ -44,14 +44,57 @@ data Theorem = Theorem { thmHyp :: [Term] , thmCon :: Term } deriving (Eq) +instance Show Object where + show (ObjNum a) = show a + show (ObjName a) = show a + show (ObjList a) = show a + show (ObjTyOp a) = show a + show (ObjType a) = show a + show (ObjConst a) = show a + show (ObjVar a) = show a + show (ObjTerm a) = show a + show (ObjThm a) = show a + show (ObjSub a) = show a + +instance Show Const where + show (Const a) = show a + +instance Show Var where + show (Var a _) = show a + +instance Show Term where + show (TVar a) = show a + show (TConst a _) = show a + show (TApp a b) = "(" ++ (show a) ++ " " ++ (show b) ++ ")" + show (TAbs a b) = "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")" + +instance Show Theorem where + show a = (show . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a) + +instance Show Name where + show a = intercalate "." (nameSpace a ++ [nameId a]) + instance Eq Term where a == b = a `alphaEquiv` b -type Stack = [Object] -type Dictionary = [(Int,Object)] -type Assumptions = [Object] -type Theorems = [Object] +data Stack = Stack { stackList :: [Object] } +data Dictionary = Dictionary { dictionMap :: [(Int,Object)] } +data Assumptions = Assumptions { assumeList :: [Object] } +data Theorems = Theorems { theoremList :: [Object] } + + +instance Show Stack where + show a = "Stack:\n" ++ intercalate "\n" (map (show) (stackList a)) ++ "\n\n" + +instance Show Dictionary where + show a = "Dictionary:\n" ++ intercalate "\n" (map (show) (dictionMap a)) ++ "\n\n" + +instance Show Assumptions where + show a = "Assumptions:\n" ++ intercalate "\n" (map (show) (assumeList a)) ++ "\n\n" + +instance Show Theorems where + show a = "Theorems:\n" ++ intercalate "\n" (map (show) (theoremList a)) ++ "\n\n" type Substitution = ([(Type,Type)],[(Var,Term)]) @@ -97,135 +140,151 @@ parse n = Command (number n) name :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)) -name str = \(stack,d,a,t) -> (ObjName (Name [] str) : stack, d, a, t) +name str = \(stack,d,a,t) -> (Stack $ ObjName (Name [] str) : (stackList stack), d, a, t) number :: String -> ((Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems)) -number n = \(stack,d,a,t) -> (ObjNum (read n) : stack, d, a, t) +number n = \(stack,d,a,t) -> (Stack $ ObjNum (read n) : (stackList stack), d, a, t) absTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -absTerm (stack,d,a,t) = - let op = (\x y -> TAbs (TVar y) x) +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) - stack' = newTerm : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ newTerm : (drop 2 stack) + in (s',d,a,t) -- need to add guards to check that the variable is not free in the hypothesis absThm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -absThm (stack,d,a,t) = - let op = (\x y -> Theorem (thmHyp x) +absThm (s,d,a,t) = + let stack = stackList s + op = (\x y -> Theorem (thmHyp x) (mkEquals (TAbs (TVar y) (getlhs . thmCon $ x)) (TAbs (TVar y) (getrhs . thmCon $ x)))) - theorem = ObjThm (op (objThm $ stack!!0) (objVar $ stack!!1)) - stack' = theorem : (drop 2 stack) - in (stack',d,a,t) + theorem = ObjThm $ op (objThm $ stack!!0) (objVar $ stack!!1) + s' = Stack $ theorem : (drop 2 stack) + in (s',d,a,t) appTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -appTerm (stack,d,a,t) = - let op = (\x y -> TApp y x) +appTerm (s,d,a,t) = + let stack = stackList s + op = (\x y -> TApp y x) newTerm = ObjTerm $ op (objTerm $ stack!!0) (objTerm $ stack!!1) - stack' = newTerm : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ newTerm : (drop 2 stack) + in (s',d,a,t) appThm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -appThm (stack,d,a,t) = - let op = (\x y -> Theorem (union (thmHyp x) (thmHyp y)) +appThm (s,d,a,t) = + let stack = stackList s + op = (\x y -> Theorem (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) - stack' = theorem : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ theorem : (drop 2 stack) + in (s',d,a,t) assume :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -assume (stack,d,a,t) = - let op = (\x -> Theorem [x] x) +assume (s,d,a,t) = + let stack = stackList s + op = (\x -> Theorem [x] x) theorem = ObjThm $ op (objTerm $ stack!!0) - stack' = theorem : (tail stack) - in (stack',d,a,t) + s' = Stack $ theorem : (tail stack) + in (s',d,a,t) -- need to add guarding for all terms being of type bool axiom :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -axiom (stack,d,assumptions,t) = - let op = (\x y -> Theorem y x) +axiom (s,d,a,t) = + let stack = stackList s + assumptions = assumeList a + op = (\x y -> Theorem y x) theorem = ObjThm $ op (objTerm $ stack!!0) (map (objTerm) . objList $ stack!!1) - stack' = theorem : (drop 2 stack) - assumptions' = theorem : assumptions - in (stack', d, assumptions', t) + s' = Stack $ theorem : (drop 2 stack) + a' = Assumptions $ theorem : assumptions + in (s',d,a',t) betaConv :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -betaConv (stack,d,a,t) = - let op = (\x -> Theorem [] (mkEquals x +betaConv (s,d,a,t) = + let stack = stackList s + op = (\x -> Theorem [] (mkEquals x (substitute ([], [(tVar . tAbsVar . tAppLeft $ x, tAppRight $ x)]) (tAbsTerm . tAppLeft $ x)))) theorem = ObjThm $ op (objTerm $ stack!!0) - stack' = theorem : (tail stack) - in (stack',d,a,t) + s' = Stack $ theorem : (tail stack) + in (s',d,a,t) cons :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -cons (stack,d,a,t) = - let op = (\x y -> y : x) +cons (s,d,a,t) = + let stack = stackList s + op = (\x y -> y : x) newList = ObjList $ op (objList $ stack!!0) (stack!!1) - stack' = newList : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ newList : (drop 2 stack) + in (s',d,a,t) constant :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -constant (stack,d,a,t) = - let op = (\x -> Const x) +constant (s,d,a,t) = + let stack = stackList s + op = (\x -> Const x) constant = ObjConst $ op (objName $ stack!!0) - stack' = constant : (tail stack) - in (stack',d,a,t) + s' = Stack $ constant : (tail stack) + in (s',d,a,t) constTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -constTerm (stack,d,a,t) = - let op = (\x y -> TConst y x) +constTerm (s,d,a,t) = + let stack = stackList s + op = (\x y -> TConst y x) newType = ObjTerm $ op (objType $ stack!!0) (objConst $ stack!!1) - stack' = newType : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ newType : (drop 2 stack) + in (s',d,a,t) deductAntisym :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -deductAntisym (stack,d,a,t) = - let op = (\x y -> Theorem (union ((thmHyp $ y) \\ [(thmCon $ x)]) +deductAntisym (s,d,a,t) = + let stack = stackList s + op = (\x y -> Theorem (union ((thmHyp $ y) \\ [(thmCon $ x)]) ((thmHyp $ x) \\ [(thmCon $ y)])) (mkEquals (thmCon $ y) (thmCon $ x))) theorem = ObjThm $ op (objThm $ stack!!0) (objThm $ stack!!1) - stack' = theorem : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ theorem : (drop 2 stack) + in (s',d,a,t) def :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -def (stack,dictionary,a,t) = - let newEntry = ((objNum $ stack!!0), (stack!!1)) +def (s,d,a,t) = + let stack = stackList s + dictionary = dictionMap d + newEntry = ((objNum $ stack!!0), (stack!!1)) cleanDict = filter ((/=) (objNum $ stack!!0) . fst) dictionary - dictionary' = newEntry : cleanDict - stack' = tail stack - in (stack',dictionary',a,t) + d' = Dictionary $ newEntry : cleanDict + s' = Stack $ tail stack + in (s',d',a,t) defineConst :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -defineConst (stack,d,a,t) = - let op1 = (\x -> Const x) +defineConst (s,d,a,t) = + let stack = stackList s + op1 = (\x -> Const x) op2 = (\x y -> Theorem [] (mkEquals x y)) constant = ObjConst $ op1 (objName $ stack!!1) constTerm = TConst (objConst $ constant) (typeOf (objTerm $ stack!!0)) theorem = ObjThm $ op2 constTerm (objTerm $ stack!!0) - stack' = theorem : constant : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ theorem : constant : (drop 2 stack) + in (s',d,a,t) defineTypeOp :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -defineTypeOp (stack,d,a,t) = - let oldthm = objThm $ stack!!0 +defineTypeOp (s,d,a,t) = + let stack = stackList s + oldthm = objThm $ stack!!0 namelist = map (objName) . objList $ stack!!1 rep = Const . objName $ stack!!2 abst = Const . objName $ stack!!3 @@ -241,111 +300,125 @@ defineTypeOp (stack,d,a,t) = rthm = Theorem [] (mkEquals (TApp (tAppLeft . thmCon $ oldthm) r') (mkEquals (TApp repTerm (TApp absTerm r')) r')) athm = Theorem [] (mkEquals (TApp absTerm (TApp repTerm a')) a') - stack' = (ObjThm rthm) : (ObjThm athm) : (ObjConst rep) : (ObjConst abst) : (ObjTyOp n) : (drop 5 stack) - in (stack',d,a,t) + s' = Stack $ (ObjThm rthm) : (ObjThm athm) : (ObjConst rep) : (ObjConst abst) : (ObjTyOp n) : (drop 5 stack) + in (s',d,a,t) eqMp :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -eqMp (stack,d,a,t) = - let op = (\x y -> if (thmCon x == (getlhs (thmCon y))) then +eqMp (s,d,a,t) = + let stack = stackList s + op = (\x y -> if (thmCon x == (getlhs (thmCon y))) then Theorem (union (thmHyp x) (thmHyp y)) (getrhs (thmCon y)) else error "Theorem consequents not alpha equivalent in eqMp") theorem = ObjThm $ op (objThm $ stack!!0) (objThm $ stack!!1) - stack' = theorem : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ theorem : (drop 2 stack) + in (s',d,a,t) nil :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -nil (stack,d,a,t) = (ObjList [] : stack, d, a, t) +nil (s,d,a,t) = (Stack $ ObjList [] : (stackList s), d, a, t) opType :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -opType (stack,d,a,t) = - let op = (\x y -> AType x y) +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) - stack' = newType : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ newType : (drop 2 stack) + in (s',d,a,t) pop :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -pop (stack,d,a,t) = (tail stack,d,a,t) +pop (s,d,a,t) = (Stack $ tail (stackList s),d,a,t) ref :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -ref (stack,dictionary,a,t) = - let entry = filter (((==) (objNum $ stack!!0)) . fst) $ dictionary +ref (s,d,a,t) = + let stack = stackList s + dictionary = dictionMap d + entry = filter (((==) (objNum $ stack!!0)) . fst) $ dictionary object = snd . head $ entry - stack' = object : tail stack - in (stack',dictionary,a,t) + s' = Stack $ object : tail stack + in (s',d,a,t) refl :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -refl (stack,d,a,t) = - let op = (\x -> Theorem [] (mkEquals x x)) +refl (s,d,a,t) = + let stack = stackList s + op = (\x -> Theorem [] (mkEquals x x)) theorem = ObjThm $ op (objTerm $ stack!!0) - stack' = theorem : (tail stack) - in (stack',d,a,t) + s' = Stack $ theorem : (tail stack) + in (s',d,a,t) remove :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -remove (stack,dictionary,a,t) = - let entry = filter (((==) (objNum $ stack!!0)) . fst) $ dictionary +remove (s,d,a,t) = + let stack = stackList s + dictionary = dictionMap d + entry = filter (((==) (objNum $ stack!!0)) . fst) $ dictionary object = snd . head $ entry - stack' = object : tail stack - dictionary' = dictionary \\ entry - in (stack',dictionary',a,t) + s' = Stack $ object : tail stack + d' = Dictionary $ dictionary \\ entry + in (s',d',a,t) subst :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -subst (stack,d,a,t) = - let op = (\x y -> Theorem (map (substitute y) (thmHyp x)) +subst (s,d,a,t) = + let stack = stackList s + op = (\x y -> Theorem (map (substitute y) (thmHyp x)) (substitute y (thmCon x))) theorem = ObjThm $ op (objThm $ stack!!0) (objSub $ stack!!1) - stack' = theorem : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ theorem : (drop 2 stack) + in (s',d,a,t) thm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -thm (stack,d,a,theorems) = - let op = (\x y z -> Theorem (alphaConvertList (thmHyp z) y) +thm (s,d,a,t) = + let stack = stackList s + theorems = theoremList t + op = (\x y z -> Theorem (alphaConvertList (thmHyp z) y) (alphaConvert (thmCon z) x)) theorem = ObjThm $ op (objTerm $ stack!!0) (map (objTerm) . objList $ stack!!1) (objThm $ stack!!2) - stack' = drop 3 stack - theorems' = union theorems [theorem] - in (stack', d, a, theorems') + s' = Stack $ drop 3 stack + t' = Theorems $ union theorems [theorem] + in (s',d,a,t') typeOp :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -typeOp (stack,d,a,t) = - let op = (\x -> TypeOp x) +typeOp (s,d,a,t) = + let stack = stackList s + op = (\x -> TypeOp x) typeOp = ObjTyOp $ op (objName $ stack!!0) - stack' = typeOp : (tail stack) - in (stack',d,a,t) + s' = Stack $ typeOp : (tail stack) + in (s',d,a,t) var :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -var (stack,d,a,t) = - let op = (\x y -> Var y x) +var (s,d,a,t) = + let stack = stackList s + op = (\x y -> Var y x) var = ObjVar $ op (objType $ stack!!0) (objName $ stack!!1) - stack' = var : (drop 2 stack) - in (stack',d,a,t) + s' = Stack $ var : (drop 2 stack) + in (s',d,a,t) varTerm :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -varTerm (stack,d,a,t) = - let op = (\x -> TVar x) +varTerm (s,d,a,t) = + let stack = stackList s + op = (\x -> TVar x) term = ObjTerm $ op (objVar $ stack!!0) - stack' = term : (tail stack) - in (stack',d,a,t) + s' = Stack $ term : (tail stack) + in (s',d,a,t) varType :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumptions,Theorems) -varType (stack,d,a,t) = - let op = (\x -> TypeVar x) +varType (s,d,a,t) = + let stack = stackList s + op = (\x -> TypeVar x) newType = ObjType $ op (objName $ stack!!0) - stack' = newType : (tail stack) - in (stack',d,a,t) + s' = Stack $ newType : (tail stack) + in (s',d,a,t) @@ -485,10 +558,10 @@ typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->")) doSemanticCheck :: [String] -> (Stack,Dictionary,Assumptions,Theorems) doSemanticCheck = - let s = [] :: Stack - d = [] :: Dictionary - a = [] :: Assumptions - t = [] :: Theorems + let s = Stack [] + d = Dictionary [] + a = Assumptions [] + t = Theorems [] op = (\x y -> case y of (Comment _) -> x (Command z) -> z x) in (foldl' (op) (s,d,a,t)) . (map (parse)) @@ -507,4 +580,4 @@ main = do args <- getArgs list <- getLines $ head args result <- return $ doSemanticCheck (map (stripReturn) list) - print $ "Result OK" + print $ result |