From 03d38eb3190eb5e51fb18847fe0792013285bde5 Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Tue, 8 Apr 2014 15:06:40 +1000 Subject: Reorganising source code --- Compare.hs | 43 ---- Concat.hs | 16 -- Delete.hs | 20 -- GeneratorTest.hs | 10 - Library/Command.hs | 203 ------------------- Library/Cost.hs | 29 --- Library/Generator.hs | 82 -------- Library/GraphPart.hs | 161 --------------- Library/Object.hs | 128 ------------ Library/Parse.hs | 75 ------- Library/ProofGraph.hs | 159 --------------- Library/Semantic.hs | 360 --------------------------------- Library/Stack.hs | 50 ----- Library/Term.hs | 193 ------------------ Library/TermNet.hs | 214 -------------------- Library/Theorem.hs | 19 -- Library/TypeVar.hs | 99 --------- Library/Usage.hs | 80 -------- Library/WriteProof.hs | 211 ------------------- Library/alternate_multi_command.hs | 315 ----------------------------- ListThm.hs | 43 ---- MeaningSubst.hs | 166 --------------- ProofGraphMain.hs | 11 - README | 51 ----- SemanticMain.hs | 12 -- Syntactic.hs | 51 ----- TermNetTest.hs | 26 --- Test.hs | 140 ------------- Test/DataTypes.hs | 68 ------- WriteProofMain.hs | 15 -- makefile | 31 ++- readme.txt | 51 +++++ src/Compare.hs | 43 ++++ src/Concat.hs | 16 ++ src/Delete.hs | 20 ++ src/GeneratorTest.hs | 10 + src/Library/Command.hs | 203 +++++++++++++++++++ src/Library/Cost.hs | 29 +++ src/Library/Generator.hs | 82 ++++++++ src/Library/GraphPart.hs | 161 +++++++++++++++ src/Library/Object.hs | 128 ++++++++++++ src/Library/Parse.hs | 75 +++++++ src/Library/ProofGraph.hs | 159 +++++++++++++++ src/Library/Semantic.hs | 360 +++++++++++++++++++++++++++++++++ src/Library/Stack.hs | 50 +++++ src/Library/Term.hs | 193 ++++++++++++++++++ src/Library/TermNet.hs | 214 ++++++++++++++++++++ src/Library/Theorem.hs | 19 ++ src/Library/TypeVar.hs | 99 +++++++++ src/Library/Usage.hs | 80 ++++++++ src/Library/WriteProof.hs | 211 +++++++++++++++++++ src/Library/alternate_multi_command.hs | 315 +++++++++++++++++++++++++++++ src/ListThm.hs | 43 ++++ src/MeaningSubst.hs | 166 +++++++++++++++ src/ProofGraphMain.hs | 11 + src/SemanticMain.hs | 12 ++ src/Syntactic.hs | 51 +++++ src/TermNetTest.hs | 26 +++ src/Test.hs | 140 +++++++++++++ src/Test/DataTypes.hs | 68 +++++++ src/WriteProofMain.hs | 15 ++ 61 files changed, 3071 insertions(+), 3060 deletions(-) delete mode 100644 Compare.hs delete mode 100644 Concat.hs delete mode 100644 Delete.hs delete mode 100644 GeneratorTest.hs delete mode 100644 Library/Command.hs delete mode 100644 Library/Cost.hs delete mode 100644 Library/Generator.hs delete mode 100644 Library/GraphPart.hs delete mode 100644 Library/Object.hs delete mode 100644 Library/Parse.hs delete mode 100644 Library/ProofGraph.hs delete mode 100644 Library/Semantic.hs delete mode 100644 Library/Stack.hs delete mode 100644 Library/Term.hs delete mode 100644 Library/TermNet.hs delete mode 100644 Library/Theorem.hs delete mode 100644 Library/TypeVar.hs delete mode 100644 Library/Usage.hs delete mode 100644 Library/WriteProof.hs delete mode 100644 Library/alternate_multi_command.hs delete mode 100644 ListThm.hs delete mode 100644 MeaningSubst.hs delete mode 100644 ProofGraphMain.hs delete mode 100644 README delete mode 100644 SemanticMain.hs delete mode 100644 Syntactic.hs delete mode 100644 TermNetTest.hs delete mode 100644 Test.hs delete mode 100644 Test/DataTypes.hs delete mode 100644 WriteProofMain.hs create mode 100644 readme.txt create mode 100644 src/Compare.hs create mode 100644 src/Concat.hs create mode 100644 src/Delete.hs create mode 100644 src/GeneratorTest.hs create mode 100644 src/Library/Command.hs create mode 100644 src/Library/Cost.hs create mode 100644 src/Library/Generator.hs create mode 100644 src/Library/GraphPart.hs create mode 100644 src/Library/Object.hs create mode 100644 src/Library/Parse.hs create mode 100644 src/Library/ProofGraph.hs create mode 100644 src/Library/Semantic.hs create mode 100644 src/Library/Stack.hs create mode 100644 src/Library/Term.hs create mode 100644 src/Library/TermNet.hs create mode 100644 src/Library/Theorem.hs create mode 100644 src/Library/TypeVar.hs create mode 100644 src/Library/Usage.hs create mode 100644 src/Library/WriteProof.hs create mode 100644 src/Library/alternate_multi_command.hs create mode 100644 src/ListThm.hs create mode 100644 src/MeaningSubst.hs create mode 100644 src/ProofGraphMain.hs create mode 100644 src/SemanticMain.hs create mode 100644 src/Syntactic.hs create mode 100644 src/TermNetTest.hs create mode 100644 src/Test.hs create mode 100644 src/Test/DataTypes.hs create mode 100644 src/WriteProofMain.hs diff --git a/Compare.hs b/Compare.hs deleted file mode 100644 index b60250f..0000000 --- a/Compare.hs +++ /dev/null @@ -1,43 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse -import Library.Semantic -import qualified Library.Stack as Stack -import qualified Data.Map as Map -import qualified Data.Set as Set -import Data.Maybe - - -main = do - args <- getArgs - listA <- getLines (args!!0) - listB <- getLines (args!!1) - - let result = do resultA <- eval (map stripReturn listA) - resultB <- eval (map stripReturn listB) - let (sA,dA,aA,tA) = resultA - (sB,dB,aB,tB) = resultB - - sA_diff = Stack.diff sA sB - sB_diff = Stack.diff sB sA - - dA_diff = dA Map.\\ dB - dB_diff = dB Map.\\ dA - - aA_diff = aA Set.\\ aB - aB_diff = aB Set.\\ aA - - tA_diff = tA Set.\\ tB - tB_diff = tB Set.\\ tA - return (Just (sA_diff,dA_diff,aA_diff,tA_diff), - Just (sB_diff,dB_diff,aB_diff,tB_diff)) - - output = if (isNothing result) - then "Error in article files\n" - else let (diff_A, diff_B) = fromJust result - in if (diff_A == diff_B) - then "Articles identical\n" - else (args!!0) ++ " has:\n" ++ (fromJust . machineToString $ diff_A) ++ "\n" ++ - (args!!1) ++ " has:\n" ++ (fromJust . machineToString $ diff_B) ++ "\n" - - printf output diff --git a/Concat.hs b/Concat.hs deleted file mode 100644 index 18d0f5d..0000000 --- a/Concat.hs +++ /dev/null @@ -1,16 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse -import Library.ProofGraph -import Library.WriteProof - - - -main = do - args <- getArgs - x <- getLines $ args!!0 - y <- getLines $ args!!1 - let list = x ++ y - graph = doGraphGen (map (stripReturn) list) - trace = doWriteProof graph - output trace diff --git a/Delete.hs b/Delete.hs deleted file mode 100644 index 3b9a1c7..0000000 --- a/Delete.hs +++ /dev/null @@ -1,20 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse -import Library.ProofGraph -import Library.WriteProof - -import qualified Data.Graph.Inductive.Graph as Graph - - - -main = do - args <- getArgs - list <- getLines (head args) - let graph = doGraphGen (map (stripReturn) list) - initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) - thmList = (map (\(_,y) -> y)) . - (filter (\(x,y) -> (show x) `notElem` (tail args))) . - (zip [1..]) $ initList - trace = writeAll graph thmList - output trace diff --git a/GeneratorTest.hs b/GeneratorTest.hs deleted file mode 100644 index 419e904..0000000 --- a/GeneratorTest.hs +++ /dev/null @@ -1,10 +0,0 @@ -import Library.Parse -import Library.Generator -import Library.Term -import Library.TypeVar - - -main = do - let s = substitutionGen ([],[]) - let t = substitutionGen ( [(Name [] "tyvar", AType [] (TypeOp (Name [] "atype")))], [] ) - output t diff --git a/Library/Command.hs b/Library/Command.hs deleted file mode 100644 index 47f0537..0000000 --- a/Library/Command.hs +++ /dev/null @@ -1,203 +0,0 @@ -module Library.Command ( - name, - number, - absTerm, - absThm, - appTerm, - appThm, - assume, - axiom, - betaConv, - constant, - constTerm, - deductAntisym, - defineConst, - defineTypeOp, - eqMp, - opType, - refl, - subst, - thm, - typeOp, - var, - varTerm, - varType - ) where - --- deliberately not included: --- cons, nil, def, ref, remove, pop - --- all functions here deal exclusively with arguments --- and results from/to the stack - -import Control.Monad -import Data.List -import Data.Maybe -import qualified Data.Set as Set -import qualified Data.Map as Map -import Library.TypeVar -import Library.Term -import Library.Theorem -import Library.Object -import Library.Parse - - -name :: String -> Maybe Name -name str = - do guard (isName str) - let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str - return (Name (init wordlist) (last wordlist)) - - -number :: String -> Maybe Number -number num = - do guard (isNumber num) - return (read num) - - -absTerm :: Term -> Var -> Term -absTerm term var = - TAbs (TVar var) term - - -absThm :: Theorem -> Var -> Maybe Theorem -absThm thm var = - do guard (not (Set.member (TVar var) (thmHyp thm))) - return (Theorem (thmHyp thm) (mkEquals (TAbs (TVar var) (getlhs . thmCon $ thm)) - (TAbs (TVar var) (getrhs . thmCon $ thm)))) - - -appTerm :: Term -> Term -> Term -appTerm term1 term2 = - TApp term2 term1 - - -appThm :: Theorem -> Theorem -> Theorem -appThm thm1 thm2 = - Theorem (Set.union (thmHyp thm1) (thmHyp thm2)) - (mkEquals (TApp (getlhs . thmCon $ thm2) (getlhs . thmCon $ thm1)) - (TApp (getrhs . thmCon $ thm2) (getrhs . thmCon $ thm1))) - - -assume :: Term -> Maybe Theorem -assume term = - do guard (typeOf term == typeBool) - return (Theorem (Set.singleton term) term) - - -axiom :: Term -> [Term] -> Maybe Theorem -axiom term termlist = - do guard (all ((== typeBool) . typeOf) termlist) - return (Theorem (Set.fromList termlist) term) - - -betaConv :: Term -> Theorem -betaConv term = - Theorem (Set.empty) - (mkEquals term - (substitute ([], [(tVar . tAbsVar . tAppLeft $ term, tAppRight $ term)]) - (tAbsTerm . tAppLeft $ term))) - - -constant :: Name -> Const -constant name = - Const name - - -constTerm :: Type -> Const -> Term -constTerm ty c = - TConst c ty - - -deductAntisym :: Theorem -> Theorem -> Theorem -deductAntisym x y = - Theorem (Set.union (Set.delete (thmCon $ x) (thmHyp $ y)) - (Set.delete (thmCon $ y) (thmHyp $ x))) - (mkEquals (thmCon $ y) (thmCon $ x)) - - -defineConst :: Term -> Name -> Maybe (Theorem, Const) -defineConst term name = - do guard ((freeVars term == Set.empty) && (typeVarsInTerm term == typeVarsInType (typeOf term))) - let constant = Const name - constTerm = TConst constant (typeOf term) - theorem = Theorem Set.empty (mkEquals constTerm term) - return (theorem, constant) - - -defineTypeOp :: Theorem -> [Name] -> Name -> Name -> Name -> Maybe (Theorem, Theorem, Const, Const, TypeOp) -defineTypeOp thm namelist r a n = - do guard ((typeVarsInTerm . tAppLeft . thmCon $ thm) == (Set.fromList . map (TypeVar) $ namelist) && - (length namelist) == (length . nub $ namelist)) - let rep = Const r - abst = Const a - op = TypeOp n - rtype = typeOf . tAppRight . thmCon $ thm - atype = AType (map (TypeVar) namelist) op - 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 $ thm) r') - (mkEquals (TApp repTerm (TApp absTerm r')) r')) - athm = Theorem Set.empty - (mkEquals (TApp absTerm (TApp repTerm a')) a') - return (rthm, athm, rep, abst, op) - - -eqMp :: Theorem -> Theorem -> Maybe Theorem -eqMp thm1 thm2 = - do guard (thmCon thm1 == (getlhs . thmCon $ thm2)) - return (Theorem (Set.union (thmHyp thm1) (thmHyp thm2)) - (getrhs . thmCon $ thm2)) - - -opType :: [Type] -> TypeOp -> Type -opType typelist tyOp = - AType typelist tyOp - - -refl :: Term -> Theorem -refl term = - Theorem Set.empty (mkEquals term term) - - -subst :: Theorem -> [Object] -> Maybe Theorem -subst thm list = - do s <- makeSubst list - return (Theorem (Set.map (substitute s) (thmHyp thm)) - (substitute s (thmCon thm))) - - -thm :: Term -> [Term] -> Theorem -> Maybe Theorem -thm term termlist oldthm = - do guard ((term == thmCon oldthm) && (Set.fromList termlist == thmHyp oldthm)) - return (Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ oldthm) termlist)) - (alphaConvert (thmCon oldthm) term)) - - -typeOp :: Name -> TypeOp -typeOp name = - TypeOp name - - -var :: Type -> Name -> Maybe Var -var ty name = - do guard ((nameSpace name) == []) - return (Var name ty) - - -varTerm :: Var -> Term -varTerm var = - TVar var - - -varType :: Name -> Maybe Type -varType name = - do guard ((nameSpace name) == []) - return (TypeVar name) - - diff --git a/Library/Cost.hs b/Library/Cost.hs deleted file mode 100644 index 86cabdc..0000000 --- a/Library/Cost.hs +++ /dev/null @@ -1,29 +0,0 @@ -module Library.Cost( - cost, - nodeCost, - listCost - ) where - - - -import Data.Maybe -import Data.Graph.Inductive.Graph( Node ) -import qualified Data.Graph.Inductive.Graph as Graph -import Library.ProofGraph - - - -cost :: String -> Int -cost x = 1 - - -nodeCost :: PGraph -> Node -> Int -nodeCost graph node = - let label = fromJust (Graph.lab graph node) - nextCostLayer = map (nodeCost graph) (Graph.suc graph node) - in (cost label) + (sum nextCostLayer) - - -listCost :: [String] -> Int -listCost = sum . (map cost) - diff --git a/Library/Generator.hs b/Library/Generator.hs deleted file mode 100644 index ef9dfe2..0000000 --- a/Library/Generator.hs +++ /dev/null @@ -1,82 +0,0 @@ -module Library.Generator ( - listGen, - substitutionGen, - termGen, - varGen, - typeGen, - typeOpGen, - constGen, - nameGen - ) where - - -import Data.List -import Library.Term -import Library.TypeVar - - - -listGen :: (a -> [String]) -> [a] -> [String] -listGen f list = - concat (map f list) ++ ["nil"] ++ replicate (length list) "cons" - - - -substitutionGen :: Substitution -> [String] -substitutionGen sub = - let varTermList = listGen varTermPair (snd sub) - nameTypeList = listGen nameTypePair (fst sub) - in nameTypeList ++ varTermList ++ ["nil", "cons", "cons"] - - - -varTermPair :: (Var, Term) -> [String] -varTermPair (var, term) = - (varGen var) ++ (termGen term) ++ ["nil", "cons", "cons"] - - - -nameTypePair :: (Name, Type) -> [String] -nameTypePair (name, ty) = - (nameGen name) ++ (typeGen ty) ++ ["nil", "cons", "cons"] - - - -termGen :: Term -> [String] -termGen (TVar v) = (varGen v) ++ ["varTerm"] -termGen (TConst c ty) = (constGen c) ++ (typeGen ty) ++ ["constTerm"] -termGen (TApp h x) = (termGen h) ++ (termGen x) ++ ["appTerm"] -termGen (TAbs x t) = (termGen x) ++ (termGen t) ++ ["absTerm"] - - - -varGen :: Var -> [String] -varGen var = - (nameGen . varName $ var) ++ (typeGen . varTy $ var) ++ ["var"] - - - -typeGen :: Type -> [String] -typeGen (TypeVar v) = (nameGen v) ++ ["varType"] -typeGen (AType ty op) = - let list = listGen typeGen ty - in (typeOpGen op) ++ list ++ ["opType"] - - - -typeOpGen :: TypeOp -> [String] -typeOpGen op = - (nameGen . tyOp $ op) ++ ["typeOp"] - - - -constGen :: Const -> [String] -constGen c = - (nameGen . constName $ c) ++ ["const"] - - - -nameGen :: Name -> [String] -nameGen name = - ["\"" ++ intercalate "." (nameSpace name ++ [nameId name]) ++ "\""] - diff --git a/Library/GraphPart.hs b/Library/GraphPart.hs deleted file mode 100644 index 02a95c0..0000000 --- a/Library/GraphPart.hs +++ /dev/null @@ -1,161 +0,0 @@ -module Library.GraphPart ( - GraphPart, - - graphPart, - makeGraphPart, - - nodes, - edges, - inputNode, - outputNode, - inputLab, - outputLab, - - graphAdd, - graphAddList, - graphDel, - size, - addedSize, - overlap, - join - ) where - - - -import Data.Maybe -import Data.List -import Data.Map( Map ) -import qualified Data.Map as Map -import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) -import qualified Data.Graph.Inductive.Graph as Graph -import Data.Graph.Inductive.Tree -import Library.ProofGraph - - -data GraphPart = GraphPart { getGraph :: Gr String (Int,Int) - , getInput :: Maybe (Node,Int) - , getOutput :: Maybe (Node,Int) } - - -graphPart :: [LNode String] -> [LEdge (Int,Int)] -> Maybe (Node,Int) -> Maybe (Node,Int) -> GraphPart -graphPart nodes edges = - let graph = checkDupe (Graph.mkGraph nodes edges) - in GraphPart graph - - -makeGraphPart :: PGraph -> Maybe (Node,Int) -> Maybe (Node,Int) -> GraphPart -makeGraphPart = GraphPart - - -nodes :: GraphPart -> [LNode String] -nodes = Graph.labNodes . getGraph - - -edges :: GraphPart -> [LEdge (Int,Int)] -edges = Graph.labEdges . getGraph - - -inputNode :: GraphPart -> Maybe Node -inputNode gpart = do - input <- getInput gpart - return (fst input) - - -outputNode :: GraphPart -> Maybe Node -outputNode gpart = do - output <- getOutput gpart - return (fst output) - - -inputLab :: GraphPart -> Maybe Int -inputLab gpart = do - input <- getInput gpart - return (snd input) - - -outputLab :: GraphPart -> Maybe Int -outputLab gpart = do - output <- getOutput gpart - return (snd output) - - - -graphAddImp :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph -graphAddImp gpart i o graph = - let (resolved, dict) = resolveNodeClash graph (getGraph gpart) - base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) $ graph - - inputAdded = if (isNothing i || isNothing (getInput gpart)) - then base - else Graph.insEdge (fromJust (Map.lookup (fst . fromJust . getInput $ gpart) dict), - fst . fromJust $ i, - (snd . fromJust . getInput $ gpart, snd . fromJust $ i)) base - - outputAdded = if (o == [] || isNothing (getOutput gpart)) - then inputAdded - else let outEdge = map (\(x,y) -> (x, fromJust (Map.lookup (fst . fromJust . getOutput $ gpart) dict), - (y, snd . fromJust . getOutput $ gpart))) o - in Graph.insEdges outEdge inputAdded - - graph' = outputAdded - in graph' - - - -graphAdd :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph -graphAdd gpart i o graph = - let graph' = graphAddImp gpart i o graph - in checkDupe graph' - - - -graphAddList :: [(GraphPart, Maybe (Node,Int), [(Node,Int)])] -> PGraph -> PGraph -graphAddList partList graph = - let graph' = foldl' (\g (x,y,z) -> graphAddImp x y z g) graph partList - in checkDupe graph' - - - -graphDel :: GraphPart -> PGraph -> PGraph -graphDel gpart graph = - let n = map fst . nodes $ gpart - e = map (\(a,b,_) -> (a,b)) . edges $ gpart - in (Graph.delNodes n) . (Graph.delEdges e) $ graph - - - -size :: GraphPart -> Int -size = Graph.noNodes . getGraph - - - -addedSize :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> Int -addedSize gpart i o graph = - let oldSize = Graph.noNodes graph - newSize = Graph.noNodes (graphAdd gpart i o graph) - in newSize - oldSize - - - -overlap :: GraphPart -> GraphPart -> Int -overlap one two = - let added = Graph.noNodes (graphAdd one Nothing [] (getGraph two)) - total = Graph.noNodes (getGraph one) + Graph.noNodes (getGraph two) - in total - added - - - -join :: GraphPart -> GraphPart -> GraphPart -join one two | (isJust (getOutput one) && isJust (getInput two)) = - let (resolved, dict) = resolveNodeClash (getGraph one) (getGraph two) - base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) . getGraph $ one - - from = (\(x,y) -> (fromJust (Map.lookup x dict), y)) . fromJust . getInput $ two - to = fromJust . getOutput $ one - ioEdge = (fst from, fst to, (snd from, snd to)) - - newOutput = (\(x,y) -> (fromJust (Map.lookup x dict), y)) . fromJust . getOutput $ two - - in makeGraphPart (checkDupe (Graph.insEdge ioEdge base)) (getInput one) (Just newOutput) - - diff --git a/Library/Object.hs b/Library/Object.hs deleted file mode 100644 index dd65ded..0000000 --- a/Library/Object.hs +++ /dev/null @@ -1,128 +0,0 @@ -module Library.Object ( - Object(..), - objNum, - objName, - objList, - objTyOp, - objType, - objConst, - objVar, - objTerm, - objThm, - - List, - - makeSubst - ) where - - - -import Data.Maybe -import Data.List -import Library.TypeVar -import Library.Term -import Library.Theorem - - - -data Object = ObjNum Number - | ObjName Name - | ObjList List - | ObjTyOp TypeOp - | ObjType Type - | ObjConst Const - | ObjVar Var - | ObjTerm Term - | ObjThm Theorem deriving (Eq, Ord) - -type List = [Object] - - - -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 - - - -makeSubst :: [Object] -> Maybe Substitution -makeSubst l = - let list = (map (mapMaybe objList)) . (mapMaybe objList) $ l - f g h x = (g . head $ x, h . last $ x) - check = f (map (f objName objType)) (map (f objVar objTerm)) list - g = all (\x -> (isJust . fst $ x) && (isJust . snd $ x)) - h x = (fromJust . fst $ x, fromJust . snd $ x) - in if ((g . fst $ check) && (g . snd $ check)) - then Just (map h (fst check), map h (snd check)) - else Nothing - - -objNum :: Object -> Maybe Number -objNum obj = - case (obj) of - (ObjNum n) -> Just n - (_) -> Nothing - - -objName :: Object -> Maybe Name -objName obj = - case (obj) of - (ObjName n) -> Just n - (_) -> Nothing - - -objList :: Object -> Maybe List -objList obj = - case (obj) of - (ObjList l) -> Just l - (_) -> Nothing - - -objTyOp :: Object -> Maybe TypeOp -objTyOp obj = - case (obj) of - (ObjTyOp tyop) -> Just tyop - (_) -> Nothing - - -objType :: Object -> Maybe Type -objType obj = - case (obj) of - (ObjType ty) -> Just ty - (_) -> Nothing - - -objConst :: Object -> Maybe Const -objConst obj = - case (obj) of - (ObjConst c) -> Just c - (_) -> Nothing - - -objVar :: Object -> Maybe Var -objVar obj = - case (obj) of - (ObjVar var) -> Just var - (_) -> Nothing - - -objTerm :: Object -> Maybe Term -objTerm obj = - case (obj) of - (ObjTerm term) -> Just term - (_) -> Nothing - - -objThm :: Object -> Maybe Theorem -objThm obj = - case (obj) of - (ObjThm thm) -> Just thm - (_) -> Nothing - diff --git a/Library/Parse.hs b/Library/Parse.hs deleted file mode 100644 index 7494822..0000000 --- a/Library/Parse.hs +++ /dev/null @@ -1,75 +0,0 @@ -module Library.Parse ( - getLines, - stripReturn, - removeEscChars, - removeQuotes, - separateBy, - isComment, - isNumber, - isName, - output, - fst3, - snd3, - thd3 - ) where - -import Control.Monad( liftM ) -import qualified Data.Char as Char - - -getLines :: FilePath -> IO [String] -getLines = liftM lines . readFile - - -stripReturn :: String -> String -stripReturn s = if (last s == '\r') then init s else s - - -removeEscChars :: String -> String -removeEscChars [] = [] -removeEscChars (x:[]) = [x] -removeEscChars x = if (head x == '\\') - then (x!!1) : (removeEscChars . (drop 2) $ x) - else (head x) : (removeEscChars . tail $ x) - - -removeQuotes :: String -> String -removeQuotes = init . tail - - -separateBy :: Char -> String -> [String] -separateBy char list = - let f x = if (x == char) then ' ' else x - in words . (map f) $ list - - -isComment :: String -> Bool -isComment = (==) '#' . head - - -isNumber :: String -> Bool -isNumber ('0':[]) = True -isNumber ('-':ns) - | (ns /= [] && head ns /= '0') = isNumber ns -isNumber n = all (Char.isNumber) n - - -isName :: String -> Bool -isName s = all ((==) '"') [head s, last s] - - -output :: [String] -> IO () -output [] = return () -output list = do - putStrLn (head list) - output (tail list) - - -fst3 :: (a,b,c) -> a -fst3 (a,_,_) = a - -snd3 :: (a,b,c) -> b -snd3 (_,b,_) = b - -thd3 :: (a,b,c) -> c -thd3 (_,_,c) = c diff --git a/Library/ProofGraph.hs b/Library/ProofGraph.hs deleted file mode 100644 index 0e7e80a..0000000 --- a/Library/ProofGraph.hs +++ /dev/null @@ -1,159 +0,0 @@ -module Library.ProofGraph ( - PGraph, - doGraphGen, - - checkDupe, - nodeEquals, - resolveNodeClash, - - argMap - ) where - - - -import Data.Maybe -import Data.List -import Data.Set( Set ) -import qualified Data.Set as Set -import Data.Map( Map, (!) ) -import qualified Data.Map as Map - -import Data.Graph.Inductive.Graph( Node, LNode, LEdge, (&) ) -import qualified Data.Graph.Inductive.Graph as Graph -import Data.Graph.Inductive.Tree - -import Library.Stack( Stack, at, (<:>) ) -import qualified Library.Stack as Stack -import Library.Parse( isNumber, isName ) - - - -type PGraph = Gr String (Int,Int) -type PStack = Stack (Int, LNode String) -type PMap = Map Int (Int, LNode String) - - -data CommandIO = IO { args :: Int - , results :: Int } - - -argMap :: String -> CommandIO -argMap "absTerm" = IO 2 1 -argMap "absThm" = IO 2 1 -argMap "appTerm" = IO 2 1 -argMap "appThm" = IO 2 1 -argMap "assume" = IO 1 1 -argMap "axiom" = IO 2 1 -argMap "betaConv" = IO 1 1 -argMap "cons" = IO 2 1 -argMap "const" = IO 1 1 -argMap "constTerm" = IO 2 1 -argMap "deductAntisym" = IO 2 1 -argMap "defineConst" = IO 2 2 -argMap "defineTypeOp" = IO 5 5 -argMap "eqMp" = IO 2 1 -argMap "nil" = IO 0 1 -argMap "opType" = IO 2 1 -argMap "refl" = IO 1 1 -argMap "subst" = IO 2 1 -argMap "thm" = IO 3 0 -argMap "typeOp" = IO 1 1 -argMap "var" = IO 2 1 -argMap "varTerm" = IO 1 1 -argMap "varType" = IO 1 1 -argMap x | (isName x) = IO 0 1 - - - -process :: String -> CommandIO -> PGraph -> PStack -> (PGraph, PStack) -process str io graph stack = - let argList = map (\x -> fromJust (stack `at` x)) [0..((args io) - 1)] - nextNum = head (Graph.newNodes 1 graph) - node = (nextNum, str) - edgeList = map (\x -> (nextNum, (fst . snd . snd $ x), (fst x, fst . snd $ x))) (zip [1..(args io)] argList) - graph' = (Graph.insEdges edgeList) . (Graph.insNode node) $ graph - nodeList = map (\x -> (x, node)) [1..(results io)] - stack' = foldr (<:>) (Stack.pop (args io) stack) nodeList - in (graph', stack') - - - -parse :: (PGraph,PStack,PMap) -> String -> (PGraph,PStack,PMap) -parse gs@(graph,stack,dictionary) str = - case str of - "def" -> let num = fst . fromJust $ stack `at` 0 - node = fromJust $ stack `at` 1 - dictionary' = Map.insert num node dictionary - stack' = Stack.pop 1 stack - in (graph, stack', dictionary') - - "ref" -> let num = fst . fromJust $ stack `at` 0 - node = fromJust (Map.lookup num dictionary) - stack' = node <:> (Stack.pop 1 stack) - in (graph, stack', dictionary) - - "remove" -> let num = fst . fromJust $ stack `at` 0 - node = fromJust (Map.lookup num dictionary) - stack' = node <:> (Stack.pop 1 stack) - dictionary' = Map.delete num dictionary - in (graph, stack', dictionary') - - "pop" -> (graph, (Stack.pop 1 stack), dictionary) - - '#':rest -> gs - - n | (isNumber n) -> let node = (read n, (0,"")) - stack' = node <:> stack - in (graph, stack', dictionary) - - x -> let (graph', stack') = process x (argMap x) graph stack - in (graph', stack', dictionary) - - - -checkDupe :: PGraph -> PGraph -checkDupe graph = - let f g n = let list = filter (\x -> (x /= n) && (nodeEquals g n x)) (Graph.nodes g) - in if (list == []) then g else merge g n (head list) - - merge g n r = - let edgesFixed = map (\(a,b,c) -> (a,r,c)) (Graph.inn g n) - in (Graph.insEdges edgesFixed) . (Graph.delNode n) $ g - - in foldl' f graph (Graph.nodes graph) - - - -nodeEquals :: Gr String (Int,Int) -> Node -> Node -> Bool -nodeEquals graph one two = - let edgesOne = sortBy sortFunc (Graph.out graph one) - edgesTwo = sortBy sortFunc (Graph.out graph two) - sortFunc = (\(_,_,x) (_,_,y) -> compare x y) - paired = zip (map (\(_,x,_) -> x) edgesOne) (map (\(_,x,_) -> x) edgesTwo) - - in (Graph.gelem one graph) && - (Graph.gelem two graph) && - (Graph.lab graph one == Graph.lab graph two) && - (length edgesOne == length edgesTwo) && - (all (\x -> nodeEquals graph (fst x) (snd x)) paired) - - - -resolveNodeClash :: Gr String (Int,Int) -> Gr String (Int,Int) -> (Gr String (Int,Int), Map Int Int) -resolveNodeClash ref graph = - let dict = Map.fromList (zip (Graph.nodes graph) (Graph.newNodes (Graph.noNodes graph) ref)) - nodeList = map (\(x,y) -> (fromJust (Map.lookup x dict), y)) (Graph.labNodes graph) - edgeList = map (\(x,y,z) -> (fromJust (Map.lookup x dict), - fromJust (Map.lookup y dict), z)) (Graph.labEdges graph) - in (Graph.mkGraph nodeList edgeList, dict) - - - -doGraphGen :: [String] -> PGraph -doGraphGen list = - let graph = Graph.empty - stack = Stack.empty - dictionary = Map.empty - result = foldl' parse (graph,stack,dictionary) list - in case result of (g,s,d) -> checkDupe g - 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" - diff --git a/Library/Stack.hs b/Library/Stack.hs deleted file mode 100644 index 99cd8e1..0000000 --- a/Library/Stack.hs +++ /dev/null @@ -1,50 +0,0 @@ -module Library.Stack ( - Stack, - empty, - at, - pop, - (<:>), - size, - diff - ) where - - -import Data.List - - -data Stack a = Stack [a] deriving (Eq) - - -instance Show a => Show (Stack a) where - show (Stack x) = "Stack:\n" ++ intercalate "\n" (map (show) x) ++ "\n\n" - - -infixr 9 <:> - - -empty :: Stack a -empty = Stack [] - - -at :: Stack a -> Int -> Maybe a -at (Stack list) index = - if (index < length list && index >= 0) - then Just (list!!index) - else Nothing - - -pop :: Int -> Stack a -> Stack a -pop n (Stack list) = Stack (drop n list) - - -(<:>) :: a -> Stack a -> Stack a -x <:> (Stack list) = Stack (x : list) - - -size :: Stack a -> Int -size (Stack list) = length list - - -diff :: (Eq a) => Stack a -> Stack a -> Stack a -diff (Stack one) (Stack two) = Stack (one \\ two) - diff --git a/Library/Term.hs b/Library/Term.hs deleted file mode 100644 index be9e53b..0000000 --- a/Library/Term.hs +++ /dev/null @@ -1,193 +0,0 @@ -module Library.Term ( - Term(..), - Substitution, - - alphaEquiv, - alphaConvert, - alphaConvertList, - substitute, - boundVars, - freeVars, - rename, - typeOf, - typeVarsInTerm, - mkEquals, - isEq, - getlhs, - getrhs - ) where - - - -import Data.List -import Data.Maybe -import qualified Data.Set as Set -import qualified Data.Map as Map -import Library.TypeVar - - - -data Term = TVar { tVar :: Var } - | TConst { tConst :: Const - , tConstType :: Type } - | TApp { tAppLeft :: Term - , tAppRight :: Term } - | TAbs { tAbsVar :: Term - , tAbsTerm :: Term } deriving (Ord) - -type Substitution = ( [(Name,Type)], [(Var,Term)] ) - - -instance Show Term where - show (TVar v) = (show v) - show (TConst a _) = (show a) - show (TApp (TApp eq lhs) rhs) - | isEq eq = "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")" - show (TApp a b) = "(" ++ (show a) ++ " " ++ (show b) ++ ")" - show (TAbs a b) = "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")" - - -instance Eq Term where - a == b = a `alphaEquiv` b - - - -alphaEquiv :: Term -> Term -> Bool -alphaEquiv a b = - let equiv term1 term2 varmap1 varmap2 depth = - case (term1,term2) of - (TConst a1 b1, TConst a2 b2) -> - a1 == a2 && b1 == b2 - - (TApp a1 b1, TApp a2 b2) -> - equiv a1 a2 varmap1 varmap2 depth && - equiv b1 b2 varmap1 varmap2 depth - - (TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) -> - equiv b1 b2 newmap1 newmap2 (depth+1) - where newmap1 = Map.insert (Var name1 type1) depth varmap1 - newmap2 = Map.insert (Var name2 type2) depth varmap2 - - (TVar (Var name1 type1), TVar (Var name2 type2)) -> - type1 == type2 && ((name1 == name2 && Map.notMember (Var name1 type1) varmap1 && Map.notMember (Var name2 type2) varmap2) || - Map.lookup (Var name1 type1) varmap1 == Map.lookup (Var name2 type2) varmap2) - - (_,_) -> False - - in equiv a b Map.empty Map.empty 0 - - -alphaConvert :: Term -> Term -> Term -alphaConvert (TConst _ _) (TConst a ty) = TConst a ty -alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2) -alphaConvert (TVar _) (TVar v) = TVar v -alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute ([],[(tVar v1,v2)]) (TAbs v1 (alphaConvert a b)) - - -alphaConvertList :: [Term] -> [Term] -> [Term] -alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b) - - -substitute :: Substitution -> Term -> Term -substitute (t,v) term = - let typesub x y = - case y of - (TConst a ty) -> TConst a (typeVarSub x ty) - (TApp a b) -> TApp (typesub x a) (typesub x b) - (TAbs (TVar (Var n ty)) a) -> TAbs (TVar (Var n (typeVarSub x ty))) (typesub x a) - (TVar (Var n ty)) -> TVar (Var n (typeVarSub x ty)) - - varsub x y = - case y of - (TConst a ty) -> TConst a ty - (TApp a b) -> TApp (varsub x a) (varsub x b) - (TVar v) -> if (Map.member v x) - then fromJust (Map.lookup v x) - else TVar v - (TAbs v a) -> let safe = rename (TAbs v a) (Set.union (Map.keysSet x) (Set.unions . (map freeVars) . (Map.elems) $ x)) - in case safe of - (TAbs m n) -> TAbs m (varsub x n) - - tymap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty t - vmap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty v - - in (varsub vmap) . (typesub tymap) $ term - - -boundVars :: Term -> Set.Set Var -boundVars (TConst a b) = Set.empty -boundVars (TApp a b) = Set.union (boundVars a) (boundVars b) -boundVars (TVar a) = Set.empty -boundVars (TAbs a b) = Set.insert (tVar a) (boundVars b) - - -freeVars :: Term -> Set.Set Var -freeVars (TConst a b) = Set.empty -freeVars (TApp a b) = Set.union (freeVars a) (freeVars b) -freeVars (TVar a) = Set.singleton a -freeVars (TAbs a b) = Set.delete (tVar a) (freeVars b) - - -rename :: Term -> Set.Set Var -> Term -rename (TAbs (TVar v) t) vars = - let doRename x y z = - case x of - (TAbs (TVar a) b) -> - if (a == y) - then TAbs (TVar z) (doRename b y z) - else TAbs (TVar a) (doRename b y z) - (TConst a b) -> TConst a b - (TApp a b) -> TApp (doRename a y z) (doRename b y z) - (TVar a) -> - if (a == y) - then TVar z - else TVar a - - findSafe x y = - if (Set.member x y) - then case x of - (Var a b) -> - case a of - (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y - else x - - in if (Set.member v vars) - then doRename (TAbs (TVar v) t) v (findSafe v vars) - else TAbs (TVar v) t - - -typeOf :: Term -> Type -typeOf (TConst _ ty) = ty -typeOf (TVar v) = varTy v -typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t) -typeOf (TApp f _) = - -- type of f is of the form [[a,b], "->"] - last . aType . typeOf $ f - - -typeVarsInTerm :: Term -> Set.Set Type -typeVarsInTerm (TConst _ ty) = typeVarsInType ty -typeVarsInTerm (TVar v) = typeVarsInType . varTy $ v -typeVarsInTerm (TAbs v t) = Set.union (typeVarsInType . varTy . tVar $ v) (typeVarsInTerm t) -typeVarsInTerm (TApp f x) = Set.union (typeVarsInTerm f) (typeVarsInTerm x) - - -mkEquals :: Term -> Term -> Term -mkEquals lhs rhs = - let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs)) - in TApp (TApp eqConst lhs) rhs - - -getlhs :: Term -> Term -getlhs (TApp (TApp eq lhs) _) - | (isEq eq) = lhs - - -getrhs :: Term -> Term -getrhs (TApp (TApp eq _) rhs) - | (isEq eq) = rhs - - -isEq :: Term -> Bool -isEq (TConst (Const (Name [] "=")) _) = True -isEq _ = False diff --git a/Library/TermNet.hs b/Library/TermNet.hs deleted file mode 100644 index 16b5446..0000000 --- a/Library/TermNet.hs +++ /dev/null @@ -1,214 +0,0 @@ -module Library.TermNet( - TermNet, - - empty, - getLeafList, - getBranchList, - - genThm, - termToTermString, - thmToTermString, - - addThm, - addThmFromNode, - matchThm - ) where - - - -import Data.Maybe -import Data.List -import qualified Data.Set as Set -import Data.Graph.Inductive.Graph( Node ) -import qualified Data.Graph.Inductive.Graph as Graph -import Library.ProofGraph -import Library.WriteProof -import Library.Object -import Library.Theorem -import Library.Term -import Library.Parse -import Library.Semantic -import Library.Stack( Stack, at, (<:>) ) -import qualified Library.Stack as Stack - - - -data TermNet = Leaf [(Theorem, Node)] | Branch [(String, TermNet)] - deriving (Eq, Show) - - - -empty :: TermNet -empty = Branch [] - - - -isLeaf :: TermNet -> Bool -isLeaf (Leaf _) = True -isLeaf _ = False - - - -isBranch :: TermNet -> Bool -isBranch (Branch _) = True -isBranch _ = False - - - -getLeafList :: TermNet -> Maybe [(Theorem, Node)] -getLeafList net = - case net of - Leaf list -> Just list - Branch list -> Nothing - - - -getBranchList :: TermNet -> Maybe [(String, TermNet)] -getBranchList net = - case net of - Leaf list -> Nothing - Branch list -> Just list - - - -genThm :: PGraph -> Node -> Theorem -genThm graph node = - let gen g n num = - let edge = filter (\x -> (fst . thd3 $ x) == num) (Graph.out g n) - node = (snd3 . head $ edge) - listing = write g node - in fromJust (((\(a,_,_,_) -> a) . fromJust $ (eval listing)) `at` 0) - - hypList = map (fromJust . objTerm) (fromJust . objList $ (gen graph node 2)) - con = fromJust . objTerm $ (gen graph node 1) - - in Theorem (Set.fromList hypList) con - - - -termToTermString :: Term -> [String] -termToTermString term = - case term of - (TConst _ _) -> - ["const"] - - (TApp func arg) -> - ["app"] ++ (termToTermString func) ++ (termToTermString arg) - - (TAbs var body) -> - ["abs", "var"] ++ (termToTermString body) - - (TVar var) -> - ["var"] - - - -thmToTermString :: Theorem -> [String] -thmToTermString theorem = - let hypList = Set.toList (thmHyp theorem) - f soFar hyp = soFar ++ ["hyp"] ++ (termToTermString hyp) - in (foldl' f [] hypList) ++ ["con"] ++ (termToTermString . thmCon $ theorem) - - - -addThm :: TermNet -> Theorem -> Node -> TermNet -addThm net theorem node = - addThmImp net (theorem,node) (thmToTermString theorem) - - - -addThmFromNode :: TermNet -> PGraph -> Node -> TermNet -addThmFromNode net graph node = - let theorem = genThm graph node - in addThmImp net (theorem,node) (thmToTermString theorem) - - - -addThmImp :: TermNet -> (Theorem,Node) -> [String] -> TermNet -addThmImp (Branch branchList) item (x:[]) = - let (sameKey, rest) = partition (\(y,z) -> y == x && isLeaf z) branchList - in if (sameKey == []) - then let leaf' = Leaf [item] - in Branch ((x,leaf'):rest) - else let leaf = snd . head $ sameKey - leafList = fromJust . getLeafList $ leaf - in if (item `elem` leafList) - then Branch branchList - else let leaf' = Leaf (item:leafList) - in Branch ((x,leaf'):rest) - -addThmImp (Branch branchList) item (x:xs) = - let (sameKey, rest) = partition (\(y,z) -> y == x) branchList - in if (sameKey == []) - then let net' = addThmImp empty item xs - in Branch ((x,net'):rest) - else let nextStepDown = snd . head $ sameKey - net' = addThmImp nextStepDown item xs - in Branch ((x,net'):rest) - - - -matchThm :: TermNet -> Theorem -> [(Theorem,Node)] -matchThm net theorem = - let hyp = Set.toList (thmHyp theorem) - con = thmCon theorem - (curPrefix, curTerm) = if (hyp == []) - then ("con", con) - else ("hyp", head hyp) - - r = do a <- matchImp curPrefix net - let b = matchTermImp curTerm a - (branches, leaves) = partition (\x -> isBranch x) b - - c <- if (hyp == []) - then getLeafList (foldl' unify (Leaf []) leaves) - else let theorem' = Theorem (Set.fromList (tail hyp)) con - in return (matchThm (foldl' unify empty branches) theorem') - return c - - in if (isNothing r) then [] else fromJust r - - - -matchImp :: String -> TermNet -> Maybe TermNet -matchImp key net = - do list <- getBranchList net - let result = filter (\(x,y) -> x == key) list - r <- if (result == []) then Nothing else Just (snd . head $ result) - return r - - - -matchTermImp :: Term -> TermNet -> [TermNet] -matchTermImp term net = - let list = getBranchList net - var = matchImp "var" net - result = - case term of - (TConst c ty) -> - do a <- matchImp "const" net - return [a] - - (TApp f x) -> - do a <- matchImp "app" net - let b = matchTermImp f a - return (concat (map (matchTermImp x) b)) - - (TAbs v x) -> - do a <- matchImp "abs" net - b <- matchImp "var" a - return (matchTermImp x b) - - (TVar v) -> Nothing --don't need to do anything because variables are already taken care of - - var' = if (isNothing var) then [] else [fromJust var] - result' = if (isNothing result) then [] else fromJust result - - in var' ++ result' - - - -unify :: TermNet -> TermNet -> TermNet -unify (Branch a) (Branch b) = Branch (a ++ b) -unify (Leaf a) (Leaf b) = Leaf (a ++ b) - diff --git a/Library/Theorem.hs b/Library/Theorem.hs deleted file mode 100644 index fc66cc2..0000000 --- a/Library/Theorem.hs +++ /dev/null @@ -1,19 +0,0 @@ -module Library.Theorem ( - Theorem(..), - ) where - - - -import qualified Data.Set as Set -import Library.TypeVar -import Library.Term - - - -data Theorem = Theorem { thmHyp :: Set.Set Term - , thmCon :: Term } deriving (Eq, Ord) - - - -instance Show Theorem where - show a = (show . Set.toList . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a) diff --git a/Library/TypeVar.hs b/Library/TypeVar.hs deleted file mode 100644 index d2915e6..0000000 --- a/Library/TypeVar.hs +++ /dev/null @@ -1,99 +0,0 @@ -module Library.TypeVar ( - Number, - - Name(..), - - TypeOp(..), - - Type(..), - - Const(..), - - Var(..), - - mkEqualsType, - typeFunc, - typeBool, - typeVarsInType, - isTypeVar, - typeVarSub - ) where - - - -import Data.List -import Data.Maybe -import qualified Data.Set as Set -import Data.Map( Map, (!) ) -import qualified Data.Map as Map - - - -type Number = Int - -data Name = Name { nameSpace :: [String] - , nameId :: String } deriving (Eq, Ord) - -data TypeOp = TypeOp { tyOp :: Name } deriving (Eq, Ord) - -data Type = TypeVar { typeVar :: Name } - | AType { aType :: [Type] - , aTypeOp :: TypeOp } deriving (Eq, Ord) - -data Const = Const { constName :: Name } deriving (Eq, Ord) - -data Var = Var { varName :: Name - , varTy :: Type } deriving (Eq, Ord) - - - -instance Show Name where - show a = intercalate "." (nameSpace a ++ [nameId a]) - -instance Show TypeOp where - show a = "typeOp " ++ (show $ tyOp a) - -instance Show Type where - show (TypeVar tyVar) = "V " ++ (show tyVar) - show (AType [] (TypeOp (Name [] "bool"))) = "bool" - show (AType [d,r] (TypeOp (Name [] "->"))) = "(" ++ show d ++ " -> " ++ show r ++ ")" - show (AType list typeOp) = "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list) - -instance Show Const where - show (Const a) = show a - -instance Show Var where - show (Var a _) = show a - - - -mkEqualsType :: Type -> Type -mkEqualsType ty = typeFunc ty (typeFunc ty typeBool) - - -typeFunc :: Type -> Type -> Type -typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->")) - - -typeBool :: Type -typeBool = AType [] (TypeOp (Name [] "bool")) - - -typeVarsInType :: Type -> Set.Set Type -typeVarsInType (TypeVar t) = Set.singleton (TypeVar t) -typeVarsInType (AType list _) = Set.unions . (map typeVarsInType) $ list - - -isTypeVar :: Type -> Bool -isTypeVar (TypeVar _) = True -isTypeVar _ = False - - -typeVarSub :: Map Name Type -> Type -> Type -typeVarSub m (TypeVar a) = - if (Map.member a m) - then fromJust (Map.lookup a m) - else TypeVar a -typeVarSub m (AType list op) = - AType (map (typeVarSub m) list) op - diff --git a/Library/Usage.hs b/Library/Usage.hs deleted file mode 100644 index a307274..0000000 --- a/Library/Usage.hs +++ /dev/null @@ -1,80 +0,0 @@ -module Library.Usage( - UsageMap, - usageMap, - useSort, - nodeOutput, - getArg - ) where - - - -import Data.Map( Map ) -import qualified Data.Map as Map -import Data.Set( Set ) -import qualified Data.Set as Set -import Data.List -import Data.Maybe -import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) -import qualified Data.Graph.Inductive.Graph as Graph -import Library.Parse -import Library.ProofGraph - - - -type UsageMap = Map Node (Map (LEdge (Int,Int)) (Int,[Int])) - - --- Takes a graph, a starting list of nodes, a set of nodes of interest, and --- follows the starting nodes up the graph to find which edges the starting nodes --- will encounter the nodes of interest through. -usageMap :: PGraph -> [Node] -> Set Node -> UsageMap -usageMap graph order interest = - let unionFunc a b = Map.unionWith min a b - - addFunc index prev umap edge = - let node = snd3 edge - curIn = Graph.outdeg graph (fst3 edge) - prev' = (curIn - (fst . thd3 $ edge)):prev - toAdd = Map.singleton node (Map.singleton edge (index,prev')) - in if (Set.member node interest) - then Map.unionWith unionFunc toAdd umap - else umap - - f umap (index,node,prev) = - let edgeList = Graph.out graph node - sucMapList = map (f Map.empty) (map (\x -> (index, snd3 x, (length edgeList - (fst . thd3 $ x)):prev)) edgeList) - umap' = foldl' (addFunc index prev) umap edgeList - in Map.unionsWith unionFunc (umap':sucMapList) - - in foldl' f Map.empty (zip3 [1..] order (repeat [])) - - - -useSort :: (LEdge a, (Int,[Int])) -> (LEdge a, (Int,[Int])) -> Ordering -useSort (_,(w,x)) (_,(y,z)) = - let check = compare w y - in if (check == EQ) - then compare (reverse x) (reverse z) - else check - - - -nodeOutput :: PGraph -> Node -> Int -nodeOutput graph node = - let label = fromJust (Graph.lab graph node) - in case label of - "thm" -> 0 - "pop" -> 0 - "defineConst" -> 2 - "defineTypeOp" -> 5 - x -> 1 - - - -getArg :: PGraph -> Node -> Int -> Maybe Node -getArg graph node arg = - let edge = filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node) - in if (edge == []) - then Nothing - else Just (snd3 . head $ edge) - diff --git a/Library/WriteProof.hs b/Library/WriteProof.hs deleted file mode 100644 index 2c15b74..0000000 --- a/Library/WriteProof.hs +++ /dev/null @@ -1,211 +0,0 @@ -module Library.WriteProof ( - write, - writeAll, - doWriteProof, - singleCommands, - next, - genPart, - writeGraph - ) where - - - -import Data.Maybe -import Data.Graph.Inductive.Graph( LNode, LEdge, Node, Edge, (&) ) -import qualified Data.Graph.Inductive.Graph as Graph -import Data.Graph.Inductive.Tree -import Data.Map( Map, (!) ) -import qualified Data.Map as Map -import Data.Set( Set ) -import qualified Data.Set as Set -import Data.List -import Library.Stack( Stack, at, (<:>) ) -import qualified Library.Stack as Stack -import Library.Parse( isNumber, fst3, snd3, thd3 ) -import Library.Cost -import Library.ProofGraph -import Library.GraphPart -import Library.Usage - - - -orderNodes :: PGraph -> [Node] -> [Node] -orderNodes graph nodeList = nodeList ---placeholder - - - --- buggy -multiCommandsSimple :: PGraph -> UsageMap -> [Node] -> PGraph -multiCommandsSimple graph usemap nodeList = - let multiNodes = filter (\x -> nodeOutput graph x > 1 && x `notElem` nodeList) (Graph.nodes graph) - umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap - - f = (\gr node edgemap -> - let out = nodeOutput gr node - index = next out gr - - edgeList = Map.toList edgemap - edgeToNode = (\x -> (fst3 x, fst . thd3 $ x)) - - sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edgeList - grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted - - defEdge = fst (minimumBy useSort edgeList) - removeEdges = map (fst . (maximumBy useSort)) grouped - refEdges = map (filter (\x -> x /= defEdge && x `notElem` removeEdges) . (map fst)) grouped - - usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeEdges)) [1..out] - - defGen = (\num -> - if (num > out) - then let reqEdges = filter (\x -> (snd . thd3 . fst $ x) == (snd . thd3 $ defEdge) && fst x /= defEdge) edgeList - refArg = (snd . thd3 $ defEdge) - 1 - in if (reqEdges == []) - then [index!!refArg, "ref"] --remove - else [index!!refArg, "ref"] - else if (num == (snd . thd3 $ defEdge) && num == out) - then if (filter (\x -> x /= defEdge && (snd . thd3 $ x) == num) (map fst edgeList) == []) - then [] - else [index!!(num-1), "def"] - else if (num `elem` usedArgs) - then [index!!(num-1), "def", "pop"] ++ defGen (num+1) - else ["pop"] ++ defGen (num+1)) - - defPart = (genPart (defGen 1) True, Just (node,1), [edgeToNode defEdge]) - - removeList = filter (\(x,y) -> y /= defEdge) (zip usedArgs removeEdges) - removeParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, [edgeToNode y])) removeList - - refList = filter (\(x,y) -> y /= []) (zip usedArgs refEdges) - refParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, map edgeToNode y)) refList - - partList = defPart:(removeParts ++ refParts) - edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList - partsAdded = graphAddList partList edgesRemoved - in partsAdded) - - in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes - - - -singleCommands :: PGraph -> UsageMap -> [Node] -> PGraph -singleCommands graph usemap nodeList = - let singleNodes = filter (\x -> nodeOutput graph x == 1 && Graph.indeg graph x > 1) (Graph.nodes graph) - umap = Map.filterWithKey (\n _ -> n `elem` singleNodes) usemap - - s = (\gr node edgemap -> - let index = head (next 1 gr) - edgeList = Map.toList edgemap - - defEdge = fst (minimumBy useSort edgeList) - removeEdge = fst (maximumBy useSort edgeList) - refEdgeList = filter (\x -> x /= defEdge && x /= removeEdge) (map fst edgeList) - - defPart = genPart [index, "def"] True - refPart = genPart [index, "ref"] False - removePart = genPart [index, "ref"] False - - defNode = (fst3 defEdge, fst . thd3 $ defEdge) - removeNode = (fst3 removeEdge, fst . thd3 $ removeEdge) - refNodeList = map (\x -> (fst3 x, fst . thd3 $ x)) refEdgeList - - partList = [(defPart, Just (node, 1), [defNode]), (removePart, Nothing, [removeNode])] - partList' = if (refNodeList == []) then partList else (refPart, Nothing, refNodeList):partList - - edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList - partsAdded = graphAddList partList' edgesRemoved - in partsAdded) - - f = (\gr node edgemap -> - let reuse = Graph.indeg graph node - costToStore = (nodeCost graph node) + (listCost ["def","0"]) + (reuse - 1) * (listCost ["ref","0"]) - costToIgnore = reuse * (nodeCost graph node) - in if (costToStore >= costToIgnore) - then gr - else s gr node edgemap) - - in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph singleNodes - - - -genPart :: [String] -> Bool -> GraphPart -genPart labels hasInput = - let nodeList = zip [1..] labels - edgeFunc = (\edges nodes -> - if (nodes == [] || (tail nodes) == []) - then edges - else let newEdge = (fst (nodes!!1), fst (nodes!!0), (1,1)) - in edgeFunc (newEdge:edges) (tail nodes)) - edgeList = edgeFunc [] nodeList - input = if (hasInput) then Just (1,1) else Nothing - output = Just (length labels, 1) - in graphPart nodeList edgeList input output - - - -next :: Int -> PGraph -> [String] -next num graph = - let nodeList = filter (isNumber . snd) (Graph.labNodes graph) - numList = nub . (map (read . snd)) $ nodeList - f x y = if (x `elem` y) then f (x + 1) y else x - g x y = if (x == 0) then y else g (x - 1) (f 0 (y ++ numList) : y) - in map show (g num []) - - - -removeUnused :: PGraph -> [Node] -> PGraph -removeUnused graph nodeList = - let unused = filter (\x -> Graph.indeg graph x == 0 && x `notElem` nodeList) (Graph.nodes graph) - in if (unused == []) - then graph - else removeUnused (Graph.delNodes unused graph) nodeList - - - -resolve :: PGraph -> [Node] -> PGraph -resolve graph nodeList = - let liveGraph = removeUnused graph nodeList - umap = usageMap graph nodeList (Set.fromList (Graph.nodes liveGraph)) - singlesDone = singleCommands liveGraph umap nodeList - multisDone = multiCommandsSimple singlesDone umap nodeList - in multisDone - - - -writeGraph :: PGraph -> Node -> [String] -writeGraph graph node = - let label = fromJust (Graph.lab graph node) - argList = [1 .. (Graph.outdeg graph node)] - f s a = let arg = getArg graph node a - in if (isNothing arg) - then s - else (writeGraph graph (fromJust arg)) ++ s - in foldl' f [label] argList - - - -write :: PGraph -> Node -> [String] -write graph node = - writeGraph (resolve graph [node]) node - - - -writeAll :: PGraph -> [Node] -> [String] -writeAll graph nodeList = - let ordered = orderNodes graph nodeList - resolved = resolve graph ordered - f g n = if (n == []) - then [] - else (writeGraph g (head n)) ++ (f g (tail n)) - in f resolved ordered - - --- metric relates to minimum amount of work done not-on-top of the stack - - -doWriteProof :: PGraph -> [String] -doWriteProof graph = - let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) - in writeAll graph initList - diff --git a/Library/alternate_multi_command.hs b/Library/alternate_multi_command.hs deleted file mode 100644 index da49a7d..0000000 --- a/Library/alternate_multi_command.hs +++ /dev/null @@ -1,315 +0,0 @@ -multiCommands :: PGraph -> UsageMap -> [Node] -> PGraph -multiCommands graph usemap nodeList = - let multiNodes = filter (\x -> nodeOutput graph x > 1) (Graph.nodes graph) - umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap - - before = (\gr node edgemap arg indexList -> - let edges = filter (\x -> snd . thd3 . fst $ x < arg) edgemap - - -- sorts and groups by which output of the command each edge is using - sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges - grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted - - -- makes a list of pairs of (maximum, restOfList) - maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped - - refNodeEdges = map (fst . snd) maxSplit - removeNodeEdges = concat (map (fst . fst) maxSplit) - - usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeNodeEdges)) [1..(arg-1)] - - -- creates a graphpart to define and pop all the initial outputs to get to the used one in the middle - defGen = (\num -> - if (num == arg) - then [] - else if (index!!num `elem` usedArgs) - then [index!!num, "def", "pop"] ++ defGen (num+1) - else ["pop"] ++ defGen (num+1)) - defPart = genPart (defGen 0) True - - -- creates graphparts for removing all the items stored in the dictionary, including node attachments - removeList = zip usedArgs removeNodeEdges - removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList - - -- creates graphparts to reference all the items stored in the dictionary, including node attachments - refList = zip usedArgs refNodeEdges - refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList - - in (defPart, refPart ++ removePart)) - - - after = (\gr node edgemap arg indexList -> - let -- obtain edges after the cutoff argument - edges = filter (\x -> snd . thd3 . fst $ x > arg) edgemap - - -- sort and group by which output of the command each edge is using - sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges - grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted - - mins = map (minimumBy useSort) grouped - initEdge = minimumBy useSort (Map.toList edgemap) - - usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) mins)) [(arg+1)..(nodeOutput gr node)] - edgeToNode = (\x -> (fst3 x, fst . thd3 $ x)) - - -- finds the argument where you have to pop everything and store it all in the dictionary before - -- proceeding - findAttach = (\x y -> - if (x == []) - then nodeOutput gr node - else let allZero = all (=0) (snd . snd . head $ x) - headIsMin = (head x) == (minimumBy useSort x) - headThmLowestStrict = let testList = map (fst . snd) x - in all (> head testList) (tail testList) - nextUsedArg = snd . thd3 . fst . head . tail $ x - in if (allZero && headIsMin && headThmLowestStrict) - then findAttach (tail x) nextUsedArg - else y) - - argToAttach = findAttach initEdge:mins arg - - process = (\attach curArg modp ordp -> - case (compare arg argToAttach) of - LT -> - EQ -> - GT ->) - - (modParts, ordinaryParts) = process argToAttach arg [] [] - - -- calculate the def/pop/ref defPart - afterPartInit = - afterPart = - if (argToAttach == arg) - then - else - - -- calculate def nodes/parts for outputs before the argToAttach - defs = - makeDefList = - defPart = map (\(x,y) -> (genPart [index!!(x-1), "def"] False, Nothing, [edgeToNode y])) makeDefList - - -- calculate ref and remove nodes/parts - maxes = map (maximumBy useSort) grouped - refs = map (filter (\x -> x `notElem` maxes && x `notElem` defs)) grouped - - removeList = zip usedArgs maxes - removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList - - -- creates graphparts to reference all the items stored in the dictionary, including node attachments - refList = zip usedArgs refs - refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList - - in (modParts, ordinaryParts)) - - addPreserveNodeParts = (\partList graph -> - ) - - f = (\gr node edgemap -> - let edgeList = Map.toList edgemap - - out = nodeOutput gr node - index = next (out + 1) gr - - initEdge = fst (minimumBy useSort edgeList) - initArg = snd . thd3 $ initEdge - (defBefore, beforeParts) = before gr node edgemap initArg (take (initArg-1) index) - (defAfter, afterParts) = after gr node edgemap initArg (drop initArg index) - edgesToRemove = filter (\x -> x /= initEdge) (map fst edgeList) - - gr' = addPreserveNodeParts defAfter gr - - edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) gr' edgesToRemove - partsAdded = graphAddList partList edgesRemoved - in partsAdded) - - in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes - - - - - - - - - - - - - -multiCommands :: PGraph -> PGraph -> UsageMap -> [Node] -> PGraph -multiCommands graph orig usemap nodeList = - let process = (\gr stack dict workmap edge -> - let node = snd3 edge - label = fromJust (Graph.lab gr node) - in if (label == "def" || label == "ref" || label == "remove" || isNumber label) - then dictProcess gr stack dict workmap edge - else regProcess gr stack dict workmap edge - - - dictProcess = (\gr stack dict workmap edge -> - let node = snd3 edge - label = fromJust (Graph.lab gr node) - index = fromJust (Graph.lab gr (head (Graph.suc gr node))) - - in if (label == "def") - then let dict' = Map.insert index (head stack) dict - in (gr, stack, dict', workmap) - - else if (label == "ref") - then let stack' = (fromJust (Map.lookup index dict)):stack - in (gr, stack', dict, workmap) - - else if (label == "remove") - then let stack' = (fromJust (Map.lookup index dict)):stack - dict' = Map.delete index dict - in (gr, stack', dict', workmap) - else -- isNumber label - (gr, stack, dict, workmap) - - - regProcess = (\gr stack dict workmap edge -> - let node = snd3 edge - label = fromJust (Graph.lab gr node) - - io = argMap label - sortedIns = sortBy (\x y -> compare (fst . thd3 $ x) (fst . thd3 $ y)) (Graph.out orig node) - expectedInput = map (\(a,b,(c,d)) -> (b,d)) sortedIns - - consume = (\(g,s,d,w) inList -> - if (inList == []) - then if (nodeOutput == 1) - then (g, (node,1):s, d, w) - else initial (g,s,d,w) - else let i = head inList - in if (head s == i) - then consume (g, tail s, d, w) (tail inList) - else store (g, s, d, w) inList) - - initial = (\(g,s,d,w) inList -> - let edgemap = Map.toList (fromJust (Map.lookup node usemap)) - sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ b)) edgemap - grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted - minimals = map (minimumBy useSort) grouped - usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) minimals)) [1..nodeOutput] - atArg = snd . thd3 $ edge - atArgReuse = length (filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap) - fromStart = fst . snd $ (head (filter (\x -> ((snd . thd3 . fst $ x) == atArg)) minimals)) - edgesToRemove = filter (\x -> (snd . thd3 $ x) < upTo) (map fst edgemap) - - upTo = let shortList = filter (\x -> (snd . thd3 . fst $ x) > atArg && (fst . snd $ x) > fromStart) minimals - in if (shortList == []) - then nodeOutput + 1 - else let shortNum = snd . thd3 . fst . head $ shortList - calc = (\num -> - if (filter (\x -> (snd . thd3 . fst $ x) == num - 1) edgemap == []) - then calc (num - 1) - else num) - in calc shortNum - index = next upTo g - - defPartGen = (\num -> - if (num == upTo) - then if (atArg + 1 < upTo) - then if (atArgReuse > 1) - then [index!!atArg, "ref"] - else [index!!atArg, "remove"] - else [] - else if (num `elem` usedArgs) - then if (num + 1 == atArg &&) - else if (num == atArg) - then if (atArgReuse <= 1 && atArg + 1 == upTo) - then defPartGen (num+1) - else if (atArg + 1 < upTo) - then [index!!num, "def", "pop"] ++ (defPartGen (num+1)) - else [index!!num, "def"] ++ (defPartGen (num+1)) - else [index!!num, "def", "pop"] ++ (defPartGen (num+1)) - else ["pop"] ++ (defPartGen (num+1))) - defPart = genPart (defPartGen 1) True - - maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped - refNodeEdges = map (fst . snd) maxSplit - removeNodeEdges = concat (map (fst . fst) maxSplit) - - removeList = zip usedArgs removeNodeEdges - removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList - - refList = zip usedArgs refNodeEdges - refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refPart - - workingEdge = - let atArgEdges = filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap - initEdge = fst . head $ (filter (\x -> (snd . thd3 $ x) == atArg && - (x `notElem` (delete (minimumBy useSort atArgEdges) - atArgEdges))) (Graph.inn g' node)) - calc = (\e -> - if (fst3 e == fst3 edge) - then e - else calc (head (Graph.inn g' (fst3 e)))) - in calc initEdge - w' = Map.insert node workingEdge - - storedArgs = if (atArgReuse > 1 || atArg + 1 < upTo) - then filter (< upTo) usedArgs - else delete atArg (filter (< upTo) usedArgs) - dictAddList = map (\x -> (index!!(x-1), (node,x))) storedArgs - d' = foldl' (\x (y,z) -> Map.insert y z x) d dictAddList - - stackArgs = atArg:(filter (>= upTo) usedArgs) - stackAddList = map (\x -> (node,x)) stackArgs - s' = stackArgs ++ s - - edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) g edgesToRemove - g' = graphAddList (defPart:(refPart ++ removePart)) edgesRemoved - - in (g', s', d', w')) - - - store = (\(g,s,d,w) inList -> - let s' = tail s - (node, arg) = head s -- the thing on the stack that shouldnt be there - workEdge = Map.lookup node w - (reqNode, reqArg) = head inList -- what we want on the stack instead - - index = head (next 1 g) - edgemap = Map.toList (Map.lookup node usemap) -- map of the edges leading into the node - edgesOfArg = filter (\(x,y) -> (snd . thd3 $ x) == arg) edgemap -- edges using the arg we want to get rid of - - removeEdge = maximumBy useSort edgesOfArg - refEdgeList = delete removeEdge edgesOfArg - - defPart = genPart [index, "def"] True - refPart = genPart [index, "ref"] False - removePart = genPart [index, "remove" False - popPart = genPart ["pop"] True - - in consume (g', s', d', w') inList - - in consume (gr,stack,dict,workmap) expectedInput) - - - h = (\gr st di ma edge -> - let node = snd3 edge - (gr',st',di',ma') = f gr st di ma node - in process gr' st' di' ma' edge) - - f = (\gr st di ma no -> - let args = reverse [1..(nodeOutput gr no)] - func = (\(g,s,d,m) a -> - let edge = filter (\x -> fst . thd3 $ x == a) (Graph.out g no) - in if (edge == []) - then (g,s,d,m) - else h gr st di ma (head edge) - in foldl' func (gr,st,di,ma) args - - stack = [] - dictionary = Map.empty - workmap = Map.empty - - (graph',stack',dictionary',workmap') = - foldl' (\(g,s,d,m) n -> f g s d m n) (graph, stack, dictionary, workmap) nodeList - - in graph' - - - - \ No newline at end of file diff --git a/ListThm.hs b/ListThm.hs deleted file mode 100644 index 540486d..0000000 --- a/ListThm.hs +++ /dev/null @@ -1,43 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse -import Library.ProofGraph -import Library.WriteProof -import Library.Semantic -import Library.Stack - -import Data.Maybe -import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) -import qualified Data.Graph.Inductive.Graph as Graph - - - -fst4 :: (a,b,c,d) -> a -fst4 (a,_,_,_) = a - - - -toThms :: PGraph -> [Node] -> [String] -toThms graph nodeList = - let hyp = (\g n -> let edge = filter (\x -> (fst . thd3 $ x) == 2) (Graph.out g n) - node = snd3 . head $ edge - in write g node) - - con = (\g n -> let edge = filter (\x -> (fst . thd3 $ x) == 1) (Graph.out g n) - node = snd3 . head $ edge - in write g node) - - f = (\x -> (show . fst $ x) ++ ". " ++ (show . fromJust $ ((fst4 . fromJust $ (eval (hyp graph (snd x)))) `at` 0)) ++ - " |- " ++ (show . fromJust $ ((fst4 . fromJust $ (eval (con graph (snd x)))) `at` 0))) - - in map f (zip [1..] nodeList) - - - -main = do - args <- getArgs - list <- getLines (head args) - let graph = doGraphGen (map (stripReturn) list) - initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) - theorems = toThms graph initList - output theorems diff --git a/MeaningSubst.hs b/MeaningSubst.hs deleted file mode 100644 index a0821b5..0000000 --- a/MeaningSubst.hs +++ /dev/null @@ -1,166 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse -import Library.ProofGraph -import Library.GraphPart -import Library.Theorem -import Library.Term -import Library.TypeVar -import Library.Generator -import Library.TermNet( TermNet ) -import qualified Library.TermNet as TermNet -import Data.Graph.Inductive.Graph( Node, LNode ) -import qualified Data.Graph.Inductive.Graph as Graph -import Data.Map( Map ) -import qualified Data.Map as Map -import qualified Data.Set as Set -import Data.List -import Data.Maybe - - - -data Step = Step { from :: Node - , to :: Node - , sub :: Substitution } - - - -alreadyMatchedElem :: (Ord a, Eq b) => a -> b -> Map a b -> Bool -alreadyMatchedElem x y xymap = - Map.member x xymap && Map.lookup x xymap /= Just y - - - -createSubst :: Theorem -> Theorem -> Maybe Substitution -createSubst one two = - let f = (\x y tymap varmap -> - case (x,y) of - (TVar (Var n ty), term) -> - if (alreadyMatchedElem (Var n ty) term varmap) - then Nothing - else let varmap' = if (Map.lookup (Var n ty) varmap == Nothing) - then Map.insert (Var n ty) term varmap - else varmap - in Just (tymap, varmap') - - (TConst a1 ty1, TConst a2 ty2) -> - if (alreadyMatchedElem (typeVar ty1) ty2 tymap || a1 /= a2 || (ty1 /= ty2 && not (isTypeVar ty1))) - then Nothing - else let tymap' = if (ty1 /= ty2) - then Map.insert (typeVar ty1) ty2 tymap - else tymap - in Just (tymap', varmap) - - (TApp a1 b1, TApp a2 b2) -> - do (tymap', varmap') <- f a1 a2 tymap varmap - f b1 b2 tymap' varmap' - - (TAbs a1 b1, TAbs a2 b2) -> - do (tymap', varmap') <- f a1 a2 tymap varmap - f b1 b2 tymap' varmap' - - (other, combination) -> Nothing) - - g = (\x y tymap varmap -> - let (hyp1,hyp2) = (Set.toList . thmHyp $ x, Set.toList . thmHyp $ y) - in if (hyp1 == [] && hyp2 == []) - then f (thmCon x) (thmCon y) tymap varmap - else do (tymap', varmap') <- f (head hyp1) (head hyp2) tymap varmap - g (Theorem (Set.fromList . tail $ hyp1) (thmCon x)) - (Theorem (Set.fromList . tail $ hyp2) (thmCon y)) - tymap' varmap') - - maps = g one two Map.empty Map.empty - - in if ((Set.size . thmHyp $ one) /= (Set.size . thmHyp $ two) || isNothing maps) - then Nothing - else do (t,v) <- maps - return (Map.toList t, Map.toList v) - - - -checkNode :: PGraph -> TermNet -> Node -> (TermNet, Maybe (GraphPart, GraphPart), Maybe (Node,Node)) -checkNode graph termnet node = - let theorem = TermNet.genThm graph node - possibles = TermNet.matchThm termnet theorem - - canBeSubbed = (\inn out -> - if (inn == []) - then out - else let sub = createSubst theorem (fst . head $ inn) - out' = if (isNothing sub) - then out - else (Step node (snd . head $ inn) (fromJust sub)) : out - in canBeSubbed (tail inn) out') - - maxPositiveBenefit = (\list -> - let sortVal = (\x -> let added = fst . snd $ x - removed = snd . snd $ x - inn = from . fst $ x - out = to . fst $ x - outNodes = map (\(x,(y,z)) -> (x,y)) (Graph.lpre graph out) - in (size removed) - (addedSize added (Just (inn,1)) outNodes graph) - (overlap added removed)) - sorted = sortBy (\x y -> compare (sortVal x) (sortVal y)) list - check = head sorted - in if (sortVal check > 0) then (Just (snd check), Just (from . fst $ check, to . fst $ check)) else (Nothing, Nothing)) - - (step, between) = maxPositiveBenefit . (map (\x -> (x, stepGen graph x))) $ (canBeSubbed possibles []) - termnet' = TermNet.addThm termnet theorem node - - in (termnet', step, between) - - - -stepGen :: PGraph -> Step -> (GraphPart, GraphPart) -stepGen graph step = - let unusedNodes = findUnused graph (Graph.suc graph (to step)) - unusedLabNodes = filter (\(x,y) -> x `elem` unusedNodes) (Graph.labNodes graph) - unused = graphPart unusedLabNodes [] Nothing Nothing - - base = doGraphGen (substitutionGen . sub $ step) - num = head (Graph.newNodes 1 base) - node = (num, "subst") - cons = head (filter (\x -> Graph.indeg base x == 0) (Graph.nodes base)) - edge = (num, cons, (2,1)) - - substGraph = (Graph.insEdge edge) . (Graph.insNode node) $ base - subst = makeGraphPart substGraph (Just (num,1)) (Just (num,1)) - - in (subst, unused) - - - -findUnused :: PGraph -> [Node] -> [Node] -findUnused graph nodeList = - let nextLayer = concat . (map (Graph.suc graph)) $ nodeList - unused = filter (\x -> all (\y -> y `elem` nodeList) (Graph.pre graph x)) nextLayer - in nodeList ++ (findUnused graph unused) - - - -doMeaningSubst :: PGraph -> PGraph -doMeaningSubst graph = - let f = (\g termnet nodeList -> - if (nodeList == []) - then g - else let working = head nodeList - (termnet', step, between) = checkNode g termnet working - (g', nodeList') = if (isNothing step || isNothing between) - then (g, nodeList) - else let (subst, unused) = fromJust step - (from, to) = fromJust between - toNodes = map (\(x,(y,z)) -> (x,y)) (Graph.lpre g to) - in ((graphAdd subst (Just (from, 1)) toNodes) . (graphDel unused) $ g, - nodeList \\ (map (\(x,y) -> x) (nodes unused))) - in f g' termnet' nodeList') - - in f graph TermNet.empty (Graph.nodes graph) - - - -main = do - args <- getArgs - list <- getLines (head args) - let graph = doGraphGen (map stripReturn list) - result = doMeaningSubst graph - printf $ (show result) ++ "\n" diff --git a/ProofGraphMain.hs b/ProofGraphMain.hs deleted file mode 100644 index 292cf01..0000000 --- a/ProofGraphMain.hs +++ /dev/null @@ -1,11 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse -import Library.ProofGraph - - -main = do - args <- getArgs - list <- getLines (head args) - let result = doGraphGen (map (stripReturn) list) - printf $ (show result) ++ "\n" diff --git a/README b/README deleted file mode 100644 index 9a55603..0000000 --- a/README +++ /dev/null @@ -1,51 +0,0 @@ - - -Semantic - -Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done. - - - - -Syntactic - -Checks a proof trace for syntax errors. - - - - -ProofGraph - -Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace. - - - - -WriteProof > - -Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace. - - - - -Delete [, , ] > - -Removes all theorems of specified numbers from a proof trace. Best used in conjunction with ListThm, so you can -actually know what theorems are what. Generates a simplified proof trace as output. - - - - -Concat > - -Joins two proof traces together, converts it to a DAG and back again, then outputs the result. - - - - -ListThm - -Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you -are deleting. - - diff --git a/SemanticMain.hs b/SemanticMain.hs deleted file mode 100644 index c07fc8c..0000000 --- a/SemanticMain.hs +++ /dev/null @@ -1,12 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse -import Library.Semantic - - - -main = do - args <- getArgs - list <- getLines (head args) - let result = doSemanticCheck (map (stripReturn) list) - printf result diff --git a/Syntactic.hs b/Syntactic.hs deleted file mode 100644 index 870cc35..0000000 --- a/Syntactic.hs +++ /dev/null @@ -1,51 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse - - - -scan :: String -> String -scan s = if (s == "absTerm" || - s == "absThm" || - s == "appTerm" || - s == "appThm" || - s == "assume" || - s == "axiom" || - s == "betaConv" || - s == "cons" || - s == "const" || - s == "constTerm" || - s == "deductAntisym" || - s == "def" || - s == "defineConst" || - s == "defineTypeOp" || - s == "eqMp" || - s == "nil" || - s == "opType" || - s == "pop" || - s == "ref" || - s == "refl" || - s == "remove" || - s == "subst" || - s == "thm" || - s == "typeOp" || - s == "var" || - s == "varTerm" || - s == "varType" || - isComment(s) || - isNumber(s) || - isName(s)) - then s - else error $ "Invalid input " ++ s - - -doScan :: [String] -> [String] -doScan = map (scan . stripReturn) - - -main = do - args <- getArgs - list <- getLines (head args) - plist <- return $ doScan list - printf $ if (args == plist) then "Scan OK\n" else "Syntax error\n" - diff --git a/TermNetTest.hs b/TermNetTest.hs deleted file mode 100644 index 57eb06f..0000000 --- a/TermNetTest.hs +++ /dev/null @@ -1,26 +0,0 @@ -import Library.Theorem -import Library.Term -import qualified Library.TermNet as Net -import Test.DataTypes -import qualified Data.Set as Set -import Data.List - - - -main = do - let thm1 = Theorem (Set.empty) stdConstTerm - thm2 = Theorem (Set.empty) (stdVarTerm "b") - thm3 = Theorem (Set.empty) (stdVarTerm "c") - thm4 = Theorem (Set.empty) (stdAbsTerm "h") - - net1 = Net.addThm Net.empty thm1 0 - net2 = Net.addThm net1 thm2 1 - net3 = Net.addThm net2 thm3 2 - net4 = Net.addThm net3 thm4 3 - - match = Net.matchThm net4 thm4 - - - putStrLn (show net4) - putStrLn "" - putStrLn (show match) diff --git a/Test.hs b/Test.hs deleted file mode 100644 index 47bba79..0000000 --- a/Test.hs +++ /dev/null @@ -1,140 +0,0 @@ -import Test.HUnit -import Library.Command -import Library.TypeVar -import Library.Term -import Library.Theorem -import Test.DataTypes -import qualified Data.Set as Set - - - -name1 = TestCase (assertEqual "for (name \"abc\")" - (Just (Name [] "abc")) - (name "\"abc\"")) - -name2 = TestCase (assertEqual "for (name \"first.second.third\")" - (Just (Name ["first","second"] "third")) - (name "\"first.second.third\"")) - -name3 = TestCase (assertEqual "for (name \"firs\\t.se\\cond.\\t\\h\\ird\")" - (Just (Name ["first","second"] "third")) - (name "\"firs\\t.se\\cond.\\t\\h\\ird\"")) - -name4 = TestCase (assertEqual "for (name abc)" Nothing (name "abc")) - - - -number1 = TestCase (assertEqual "for (number \"90\")" (Just 90) (number "90")) -number2 = TestCase (assertEqual "for (number \"0\")" (Just 0) (number "0")) -number3 = TestCase (assertEqual "for (number \"-1\")" (Just (-1)) (number "-1")) -number4 = TestCase (assertEqual "for (number \"-0\")" Nothing (number "-0")) -number5 = TestCase (assertEqual "for (number \"1.2\")" Nothing (number "1.2")) - - - -assume1 = TestCase (assertEqual "for (assume (TConst ...)" - (Just (Theorem (Set.singleton (TConst stdConst typeBool)) - (TConst stdConst typeBool))) - (assume (TConst stdConst typeBool))) - -assume2 = TestCase (assertEqual "for (assume (TConst ...) --with wrong type" - Nothing - (assume (TConst stdConst stdTypeVar))) - - - -axiom1 = TestCase (assertEqual "for (axiom (TConst ...) [])" - (Just (Theorem Set.empty (TConst stdConst stdTypeVar))) - (axiom (TConst stdConst stdTypeVar) [])) - -axiom2 = TestCase (assertEqual "for (axiom (TConst ...) [term1, term2] --term1 has wrong type" - Nothing - (axiom (TConst stdConst stdTypeVar) - [(TConst stdConst stdTypeVar),(TConst stdConst typeBool)])) - - - -alphaEquiv1 = TestCase (assertEqual "for ((\\xy -> x) `alphaEquiv` (\\yx -> x))" - False - (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))) - (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "x"))))) - -alphaEquiv2 = TestCase (assertEqual "for ((\\xy -> x) `alphaEquiv` (\\xy -> x))" - True - (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))) - (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))))) - -alphaEquiv3 = TestCase (assertEqual "for ((\\xyx -> x) `alphaEquiv` (\\yxx -> x))" - True - (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "x")))) - (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "x") (stdVarTerm "x")))))) - -alphaEquiv4 = TestCase (assertEqual "for ((\\xyz -> y) `alphaEquiv` (\\zyx -> y))" - True - (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "z") (stdVarTerm "y")))) - (TAbs (stdVarTerm "z") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "y")))))) - -alphaEquiv5 = TestCase (assertEqual "for ((\\x -> x) `alphaEquiv` (\\x -> x)) --x of lhs is different type to x of rhs" - False - (alphaEquiv (TAbs (stdVarTerm "x") (stdVarTerm "x")) - (TAbs (altVarTerm "x") (altVarTerm "x")))) - -alphaEquiv6 = TestCase (assertEqual "for ((TAbs ...) `alphaEquiv` (TConst ...))" - False - (alphaEquiv (TAbs (stdVarTerm "x") (stdVarTerm "x")) - (TConst stdConst typeBool))) - - - -substitute1 = TestCase (assertEqual "for (substitute ([],[(x',a)]) (TVar x'))" - (stdConstTerm) - (substitute ([],[((stdVar "x'"),stdConstTerm)]) (stdVarTerm "x'"))) - -substitute2 = TestCase (assertEqual "for (substitute ([],[(x',a)]) (TVar y'))" - (stdVarTerm "y'") - (substitute ([],[((stdVar "x'"),stdConstTerm)]) (stdVarTerm "y'"))) - -substitute3 = TestCase (assertEqual "for (substitute ([],[(x',a)]) (TApp (TVar x') (TVar x')))" - (TApp stdConstTerm stdConstTerm) - (substitute ([],[((stdVar "x'"),stdConstTerm)]) (TApp (stdVarTerm "x'") (stdVarTerm "x'")))) - -substitute4 = TestCase (assertEqual "for (substitute ([],[(x',a)]) (\\y' -> x'))" - (TAbs (stdVarTerm "y'") stdConstTerm) - (substitute ([],[((stdVar "x'"),stdConstTerm)]) (TAbs (stdVarTerm "y'") (stdVarTerm "x'")))) - -substitute5 = TestCase (assertEqual "for (substitute ([],[(x',y')]) (\\y' -> x'))" - (TAbs (stdVarTerm "y''") (stdVarTerm "y'")) - (substitute ([],[((stdVar "x'"),(stdVarTerm "y'"))]) (TAbs (stdVarTerm "y'") (stdVarTerm "x'")))) - -substitute6 = TestCase (assertEqual "for (substitute ([(tx',ta)],[]) (z' with typevar tx'))" - (TVar (Var (stdName "z'") stdType)) - (substitute ([(stdTypeVarName,stdType)],[]) (stdVarTerm "z'"))) - -substitute7 = TestCase (assertEqual "for (substitute ([(tx',ta)],[(y',b)]) (\\z' -> y')) --z' has type tx'" - (TAbs (TVar (Var (stdName "z'") stdType)) stdConstTerm) - (substitute ([(stdTypeVarName,stdType)],[((altVar "y'"),stdConstTerm)]) (TAbs (stdVarTerm "z'") (altVarTerm "y'")))) - -substitute8 = TestCase (assertEqual "for (substitute ([],[(x',y'),(y',z')]) (x'))" - (stdVarTerm "z'") - (substitute ([],[((stdVar "x'"),(stdVarTerm "y'")), - ((stdVar "y'"),(stdVarTerm "z'"))]) (stdVarTerm "x'"))) - -substitute9 = TestCase (assertEqual "for (substitute ([(tx',ty'),(ty',ta)],[]) (z' with typevar tx'))" - (TVar (Var (stdName "z'") stdType)) - (substitute ([(stdTypeVarName,altTypeVar),(altTypeVarName,stdType)],[]) (TVar (Var (stdName "z'") altTypeVar)))) - - -main = - do putStrLn "Command.name" - runTestTT $ TestList [name1,name2,name3,name4] - putStrLn "Command.number" - runTestTT $ TestList [number1,number2,number3,number4,number5] - putStrLn "Command.assume" - runTestTT $ TestList [assume1,assume2] - putStrLn "Command.axiom" - runTestTT $ TestList [axiom1,axiom2] - putStrLn "Term.alphaEquiv" - runTestTT $ TestList [alphaEquiv1,alphaEquiv2,alphaEquiv3,alphaEquiv4,alphaEquiv5,alphaEquiv6] - putStrLn "Term.substitute" - runTestTT $ TestList [substitute1,substitute2,substitute3,substitute4,substitute5,substitute6,substitute7,substitute8,substitute9] - diff --git a/Test/DataTypes.hs b/Test/DataTypes.hs deleted file mode 100644 index 28db135..0000000 --- a/Test/DataTypes.hs +++ /dev/null @@ -1,68 +0,0 @@ -module Test.DataTypes( - stdName, - stdType, - stdConst, - stdConstTerm, - stdTypeVarName, - altTypeVarName, - stdTypeVar, - altTypeVar, - stdVar, - stdVarTerm, - altVar, - altVarTerm, - stdAbsTerm, - stdAppTerm - ) where - - - -import Library.TypeVar -import Library.Term - - - -stdName :: String -> Name -stdName s = Name [] s - -stdType :: Type -stdType = AType [] (TypeOp (stdName "atype")) - -stdConst :: Const -stdConst = Const (stdName "const") - -stdConstTerm :: Term -stdConstTerm = TConst stdConst stdType - -stdTypeVarName :: Name -stdTypeVarName = stdName "typevar" - -altTypeVarName :: Name -altTypeVarName = stdName "alttypevar" - -stdTypeVar :: Type -stdTypeVar = TypeVar stdTypeVarName - -altTypeVar :: Type -altTypeVar = TypeVar altTypeVarName - -stdVar :: String -> Var -stdVar s = Var (stdName s) stdTypeVar - -stdVarTerm :: String -> Term -stdVarTerm s = TVar (stdVar s) - -altVar :: String -> Var -altVar s = Var (stdName s) altTypeVar - -altVarTerm :: String -> Term -altVarTerm s = TVar (altVar s) - -stdAbsTerm :: String -> Term -stdAbsTerm s = TAbs (stdVarTerm s) stdConstTerm - -stdAppTerm :: String -> Term -stdAppTerm s = TApp (stdAbsTerm s) stdConstTerm - - - diff --git a/WriteProofMain.hs b/WriteProofMain.hs deleted file mode 100644 index 2f8625e..0000000 --- a/WriteProofMain.hs +++ /dev/null @@ -1,15 +0,0 @@ -import System.Environment( getArgs ) -import Text.Printf -import Library.Parse -import Library.ProofGraph -import Library.WriteProof - - - -main = do - args <- getArgs - list <- getLines (head args) - let graph = doGraphGen (map (stripReturn) list) - trace = doWriteProof graph - output trace - diff --git a/makefile b/makefile index d4f971b..836c7b7 100644 --- a/makefile +++ b/makefile @@ -1,5 +1,6 @@ OUTPUTDIR = bin +SOURCEDIR = src @@ -11,32 +12,42 @@ clean: semantic: - ghc --make ./SemanticMain.hs -o ${OUTPUTDIR}/Semantic + cd ${SOURCEDIR}; \ + ghc --make SemanticMain.hs -o ../${OUTPUTDIR}/Semantic syntactic: - ghc --make ./Syntactic.hs -o ${OUTPUTDIR}/Syntactic + cd ${SOURCEDIR}; \ + ghc --make Syntactic.hs -o ../${OUTPUTDIR}/Syntactic proofgraph: - ghc --make ./ProofGraphMain.hs -o ${OUTPUTDIR}/ProofGraph + cd ${SOURCEDIR}; \ + ghc --make ProofGraphMain.hs -o ../${OUTPUTDIR}/ProofGraph writeproof: - ghc --make ./WriteProofMain.hs -o ${OUTPUTDIR}/WriteProof + cd ${SOURCEDIR}; \ + ghc --make WriteProofMain.hs -o ../${OUTPUTDIR}/WriteProof delete: - ghc --make ./Delete.hs -o ${OUTPUTDIR}/Delete + cd ${SOURCEDIR}; \ + ghc --make Delete.hs -o ../${OUTPUTDIR}/Delete concat: - ghc --make ./Concat.hs -o ${OUTPUTDIR}/Concat + cd ${SOURCEDIR}; \ + ghc --make Concat.hs -o ../${OUTPUTDIR}/Concat listthm: - ghc --make ./ListThm.hs -o ${OUTPUTDIR}/ListThm + cd ${SOURCEDIR}; \ + ghc --make ListThm.hs -o ../${OUTPUTDIR}/ListThm meaningsubst: - ghc --make ./MeaningSubst.hs -o ${OUTPUTDIR}/MeaningSubst + cd ${SOURCEDIR}; \ + ghc --make MeaningSubst.hs -o ../${OUTPUTDIR}/MeaningSubst unittest: - ghc --make ./Test.hs -o ${OUTPUTDIR}/UnitTest + cd ${SOURCEDIR}; \ + ghc --make Test.hs -o ../${OUTPUTDIR}/UnitTest compare: - ghc --make ./Compare.hs -o ${OUTPUTDIR}/Compare + cd ${SOURCEDIR}; \ + ghc --make Compare.hs -o ../${OUTPUTDIR}/Compare diff --git a/readme.txt b/readme.txt new file mode 100644 index 0000000..9a55603 --- /dev/null +++ b/readme.txt @@ -0,0 +1,51 @@ + + +Semantic + +Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done. + + + + +Syntactic + +Checks a proof trace for syntax errors. + + + + +ProofGraph + +Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace. + + + + +WriteProof > + +Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace. + + + + +Delete [, , ] > + +Removes all theorems of specified numbers from a proof trace. Best used in conjunction with ListThm, so you can +actually know what theorems are what. Generates a simplified proof trace as output. + + + + +Concat > + +Joins two proof traces together, converts it to a DAG and back again, then outputs the result. + + + + +ListThm + +Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you +are deleting. + + diff --git a/src/Compare.hs b/src/Compare.hs new file mode 100644 index 0000000..b60250f --- /dev/null +++ b/src/Compare.hs @@ -0,0 +1,43 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse +import Library.Semantic +import qualified Library.Stack as Stack +import qualified Data.Map as Map +import qualified Data.Set as Set +import Data.Maybe + + +main = do + args <- getArgs + listA <- getLines (args!!0) + listB <- getLines (args!!1) + + let result = do resultA <- eval (map stripReturn listA) + resultB <- eval (map stripReturn listB) + let (sA,dA,aA,tA) = resultA + (sB,dB,aB,tB) = resultB + + sA_diff = Stack.diff sA sB + sB_diff = Stack.diff sB sA + + dA_diff = dA Map.\\ dB + dB_diff = dB Map.\\ dA + + aA_diff = aA Set.\\ aB + aB_diff = aB Set.\\ aA + + tA_diff = tA Set.\\ tB + tB_diff = tB Set.\\ tA + return (Just (sA_diff,dA_diff,aA_diff,tA_diff), + Just (sB_diff,dB_diff,aB_diff,tB_diff)) + + output = if (isNothing result) + then "Error in article files\n" + else let (diff_A, diff_B) = fromJust result + in if (diff_A == diff_B) + then "Articles identical\n" + else (args!!0) ++ " has:\n" ++ (fromJust . machineToString $ diff_A) ++ "\n" ++ + (args!!1) ++ " has:\n" ++ (fromJust . machineToString $ diff_B) ++ "\n" + + printf output diff --git a/src/Concat.hs b/src/Concat.hs new file mode 100644 index 0000000..18d0f5d --- /dev/null +++ b/src/Concat.hs @@ -0,0 +1,16 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse +import Library.ProofGraph +import Library.WriteProof + + + +main = do + args <- getArgs + x <- getLines $ args!!0 + y <- getLines $ args!!1 + let list = x ++ y + graph = doGraphGen (map (stripReturn) list) + trace = doWriteProof graph + output trace diff --git a/src/Delete.hs b/src/Delete.hs new file mode 100644 index 0000000..3b9a1c7 --- /dev/null +++ b/src/Delete.hs @@ -0,0 +1,20 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse +import Library.ProofGraph +import Library.WriteProof + +import qualified Data.Graph.Inductive.Graph as Graph + + + +main = do + args <- getArgs + list <- getLines (head args) + let graph = doGraphGen (map (stripReturn) list) + initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) + thmList = (map (\(_,y) -> y)) . + (filter (\(x,y) -> (show x) `notElem` (tail args))) . + (zip [1..]) $ initList + trace = writeAll graph thmList + output trace diff --git a/src/GeneratorTest.hs b/src/GeneratorTest.hs new file mode 100644 index 0000000..419e904 --- /dev/null +++ b/src/GeneratorTest.hs @@ -0,0 +1,10 @@ +import Library.Parse +import Library.Generator +import Library.Term +import Library.TypeVar + + +main = do + let s = substitutionGen ([],[]) + let t = substitutionGen ( [(Name [] "tyvar", AType [] (TypeOp (Name [] "atype")))], [] ) + output t diff --git a/src/Library/Command.hs b/src/Library/Command.hs new file mode 100644 index 0000000..47f0537 --- /dev/null +++ b/src/Library/Command.hs @@ -0,0 +1,203 @@ +module Library.Command ( + name, + number, + absTerm, + absThm, + appTerm, + appThm, + assume, + axiom, + betaConv, + constant, + constTerm, + deductAntisym, + defineConst, + defineTypeOp, + eqMp, + opType, + refl, + subst, + thm, + typeOp, + var, + varTerm, + varType + ) where + +-- deliberately not included: +-- cons, nil, def, ref, remove, pop + +-- all functions here deal exclusively with arguments +-- and results from/to the stack + +import Control.Monad +import Data.List +import Data.Maybe +import qualified Data.Set as Set +import qualified Data.Map as Map +import Library.TypeVar +import Library.Term +import Library.Theorem +import Library.Object +import Library.Parse + + +name :: String -> Maybe Name +name str = + do guard (isName str) + let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str + return (Name (init wordlist) (last wordlist)) + + +number :: String -> Maybe Number +number num = + do guard (isNumber num) + return (read num) + + +absTerm :: Term -> Var -> Term +absTerm term var = + TAbs (TVar var) term + + +absThm :: Theorem -> Var -> Maybe Theorem +absThm thm var = + do guard (not (Set.member (TVar var) (thmHyp thm))) + return (Theorem (thmHyp thm) (mkEquals (TAbs (TVar var) (getlhs . thmCon $ thm)) + (TAbs (TVar var) (getrhs . thmCon $ thm)))) + + +appTerm :: Term -> Term -> Term +appTerm term1 term2 = + TApp term2 term1 + + +appThm :: Theorem -> Theorem -> Theorem +appThm thm1 thm2 = + Theorem (Set.union (thmHyp thm1) (thmHyp thm2)) + (mkEquals (TApp (getlhs . thmCon $ thm2) (getlhs . thmCon $ thm1)) + (TApp (getrhs . thmCon $ thm2) (getrhs . thmCon $ thm1))) + + +assume :: Term -> Maybe Theorem +assume term = + do guard (typeOf term == typeBool) + return (Theorem (Set.singleton term) term) + + +axiom :: Term -> [Term] -> Maybe Theorem +axiom term termlist = + do guard (all ((== typeBool) . typeOf) termlist) + return (Theorem (Set.fromList termlist) term) + + +betaConv :: Term -> Theorem +betaConv term = + Theorem (Set.empty) + (mkEquals term + (substitute ([], [(tVar . tAbsVar . tAppLeft $ term, tAppRight $ term)]) + (tAbsTerm . tAppLeft $ term))) + + +constant :: Name -> Const +constant name = + Const name + + +constTerm :: Type -> Const -> Term +constTerm ty c = + TConst c ty + + +deductAntisym :: Theorem -> Theorem -> Theorem +deductAntisym x y = + Theorem (Set.union (Set.delete (thmCon $ x) (thmHyp $ y)) + (Set.delete (thmCon $ y) (thmHyp $ x))) + (mkEquals (thmCon $ y) (thmCon $ x)) + + +defineConst :: Term -> Name -> Maybe (Theorem, Const) +defineConst term name = + do guard ((freeVars term == Set.empty) && (typeVarsInTerm term == typeVarsInType (typeOf term))) + let constant = Const name + constTerm = TConst constant (typeOf term) + theorem = Theorem Set.empty (mkEquals constTerm term) + return (theorem, constant) + + +defineTypeOp :: Theorem -> [Name] -> Name -> Name -> Name -> Maybe (Theorem, Theorem, Const, Const, TypeOp) +defineTypeOp thm namelist r a n = + do guard ((typeVarsInTerm . tAppLeft . thmCon $ thm) == (Set.fromList . map (TypeVar) $ namelist) && + (length namelist) == (length . nub $ namelist)) + let rep = Const r + abst = Const a + op = TypeOp n + rtype = typeOf . tAppRight . thmCon $ thm + atype = AType (map (TypeVar) namelist) op + 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 $ thm) r') + (mkEquals (TApp repTerm (TApp absTerm r')) r')) + athm = Theorem Set.empty + (mkEquals (TApp absTerm (TApp repTerm a')) a') + return (rthm, athm, rep, abst, op) + + +eqMp :: Theorem -> Theorem -> Maybe Theorem +eqMp thm1 thm2 = + do guard (thmCon thm1 == (getlhs . thmCon $ thm2)) + return (Theorem (Set.union (thmHyp thm1) (thmHyp thm2)) + (getrhs . thmCon $ thm2)) + + +opType :: [Type] -> TypeOp -> Type +opType typelist tyOp = + AType typelist tyOp + + +refl :: Term -> Theorem +refl term = + Theorem Set.empty (mkEquals term term) + + +subst :: Theorem -> [Object] -> Maybe Theorem +subst thm list = + do s <- makeSubst list + return (Theorem (Set.map (substitute s) (thmHyp thm)) + (substitute s (thmCon thm))) + + +thm :: Term -> [Term] -> Theorem -> Maybe Theorem +thm term termlist oldthm = + do guard ((term == thmCon oldthm) && (Set.fromList termlist == thmHyp oldthm)) + return (Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ oldthm) termlist)) + (alphaConvert (thmCon oldthm) term)) + + +typeOp :: Name -> TypeOp +typeOp name = + TypeOp name + + +var :: Type -> Name -> Maybe Var +var ty name = + do guard ((nameSpace name) == []) + return (Var name ty) + + +varTerm :: Var -> Term +varTerm var = + TVar var + + +varType :: Name -> Maybe Type +varType name = + do guard ((nameSpace name) == []) + return (TypeVar name) + + diff --git a/src/Library/Cost.hs b/src/Library/Cost.hs new file mode 100644 index 0000000..86cabdc --- /dev/null +++ b/src/Library/Cost.hs @@ -0,0 +1,29 @@ +module Library.Cost( + cost, + nodeCost, + listCost + ) where + + + +import Data.Maybe +import Data.Graph.Inductive.Graph( Node ) +import qualified Data.Graph.Inductive.Graph as Graph +import Library.ProofGraph + + + +cost :: String -> Int +cost x = 1 + + +nodeCost :: PGraph -> Node -> Int +nodeCost graph node = + let label = fromJust (Graph.lab graph node) + nextCostLayer = map (nodeCost graph) (Graph.suc graph node) + in (cost label) + (sum nextCostLayer) + + +listCost :: [String] -> Int +listCost = sum . (map cost) + diff --git a/src/Library/Generator.hs b/src/Library/Generator.hs new file mode 100644 index 0000000..ef9dfe2 --- /dev/null +++ b/src/Library/Generator.hs @@ -0,0 +1,82 @@ +module Library.Generator ( + listGen, + substitutionGen, + termGen, + varGen, + typeGen, + typeOpGen, + constGen, + nameGen + ) where + + +import Data.List +import Library.Term +import Library.TypeVar + + + +listGen :: (a -> [String]) -> [a] -> [String] +listGen f list = + concat (map f list) ++ ["nil"] ++ replicate (length list) "cons" + + + +substitutionGen :: Substitution -> [String] +substitutionGen sub = + let varTermList = listGen varTermPair (snd sub) + nameTypeList = listGen nameTypePair (fst sub) + in nameTypeList ++ varTermList ++ ["nil", "cons", "cons"] + + + +varTermPair :: (Var, Term) -> [String] +varTermPair (var, term) = + (varGen var) ++ (termGen term) ++ ["nil", "cons", "cons"] + + + +nameTypePair :: (Name, Type) -> [String] +nameTypePair (name, ty) = + (nameGen name) ++ (typeGen ty) ++ ["nil", "cons", "cons"] + + + +termGen :: Term -> [String] +termGen (TVar v) = (varGen v) ++ ["varTerm"] +termGen (TConst c ty) = (constGen c) ++ (typeGen ty) ++ ["constTerm"] +termGen (TApp h x) = (termGen h) ++ (termGen x) ++ ["appTerm"] +termGen (TAbs x t) = (termGen x) ++ (termGen t) ++ ["absTerm"] + + + +varGen :: Var -> [String] +varGen var = + (nameGen . varName $ var) ++ (typeGen . varTy $ var) ++ ["var"] + + + +typeGen :: Type -> [String] +typeGen (TypeVar v) = (nameGen v) ++ ["varType"] +typeGen (AType ty op) = + let list = listGen typeGen ty + in (typeOpGen op) ++ list ++ ["opType"] + + + +typeOpGen :: TypeOp -> [String] +typeOpGen op = + (nameGen . tyOp $ op) ++ ["typeOp"] + + + +constGen :: Const -> [String] +constGen c = + (nameGen . constName $ c) ++ ["const"] + + + +nameGen :: Name -> [String] +nameGen name = + ["\"" ++ intercalate "." (nameSpace name ++ [nameId name]) ++ "\""] + diff --git a/src/Library/GraphPart.hs b/src/Library/GraphPart.hs new file mode 100644 index 0000000..02a95c0 --- /dev/null +++ b/src/Library/GraphPart.hs @@ -0,0 +1,161 @@ +module Library.GraphPart ( + GraphPart, + + graphPart, + makeGraphPart, + + nodes, + edges, + inputNode, + outputNode, + inputLab, + outputLab, + + graphAdd, + graphAddList, + graphDel, + size, + addedSize, + overlap, + join + ) where + + + +import Data.Maybe +import Data.List +import Data.Map( Map ) +import qualified Data.Map as Map +import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) +import qualified Data.Graph.Inductive.Graph as Graph +import Data.Graph.Inductive.Tree +import Library.ProofGraph + + +data GraphPart = GraphPart { getGraph :: Gr String (Int,Int) + , getInput :: Maybe (Node,Int) + , getOutput :: Maybe (Node,Int) } + + +graphPart :: [LNode String] -> [LEdge (Int,Int)] -> Maybe (Node,Int) -> Maybe (Node,Int) -> GraphPart +graphPart nodes edges = + let graph = checkDupe (Graph.mkGraph nodes edges) + in GraphPart graph + + +makeGraphPart :: PGraph -> Maybe (Node,Int) -> Maybe (Node,Int) -> GraphPart +makeGraphPart = GraphPart + + +nodes :: GraphPart -> [LNode String] +nodes = Graph.labNodes . getGraph + + +edges :: GraphPart -> [LEdge (Int,Int)] +edges = Graph.labEdges . getGraph + + +inputNode :: GraphPart -> Maybe Node +inputNode gpart = do + input <- getInput gpart + return (fst input) + + +outputNode :: GraphPart -> Maybe Node +outputNode gpart = do + output <- getOutput gpart + return (fst output) + + +inputLab :: GraphPart -> Maybe Int +inputLab gpart = do + input <- getInput gpart + return (snd input) + + +outputLab :: GraphPart -> Maybe Int +outputLab gpart = do + output <- getOutput gpart + return (snd output) + + + +graphAddImp :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph +graphAddImp gpart i o graph = + let (resolved, dict) = resolveNodeClash graph (getGraph gpart) + base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) $ graph + + inputAdded = if (isNothing i || isNothing (getInput gpart)) + then base + else Graph.insEdge (fromJust (Map.lookup (fst . fromJust . getInput $ gpart) dict), + fst . fromJust $ i, + (snd . fromJust . getInput $ gpart, snd . fromJust $ i)) base + + outputAdded = if (o == [] || isNothing (getOutput gpart)) + then inputAdded + else let outEdge = map (\(x,y) -> (x, fromJust (Map.lookup (fst . fromJust . getOutput $ gpart) dict), + (y, snd . fromJust . getOutput $ gpart))) o + in Graph.insEdges outEdge inputAdded + + graph' = outputAdded + in graph' + + + +graphAdd :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph +graphAdd gpart i o graph = + let graph' = graphAddImp gpart i o graph + in checkDupe graph' + + + +graphAddList :: [(GraphPart, Maybe (Node,Int), [(Node,Int)])] -> PGraph -> PGraph +graphAddList partList graph = + let graph' = foldl' (\g (x,y,z) -> graphAddImp x y z g) graph partList + in checkDupe graph' + + + +graphDel :: GraphPart -> PGraph -> PGraph +graphDel gpart graph = + let n = map fst . nodes $ gpart + e = map (\(a,b,_) -> (a,b)) . edges $ gpart + in (Graph.delNodes n) . (Graph.delEdges e) $ graph + + + +size :: GraphPart -> Int +size = Graph.noNodes . getGraph + + + +addedSize :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> Int +addedSize gpart i o graph = + let oldSize = Graph.noNodes graph + newSize = Graph.noNodes (graphAdd gpart i o graph) + in newSize - oldSize + + + +overlap :: GraphPart -> GraphPart -> Int +overlap one two = + let added = Graph.noNodes (graphAdd one Nothing [] (getGraph two)) + total = Graph.noNodes (getGraph one) + Graph.noNodes (getGraph two) + in total - added + + + +join :: GraphPart -> GraphPart -> GraphPart +join one two | (isJust (getOutput one) && isJust (getInput two)) = + let (resolved, dict) = resolveNodeClash (getGraph one) (getGraph two) + base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) . getGraph $ one + + from = (\(x,y) -> (fromJust (Map.lookup x dict), y)) . fromJust . getInput $ two + to = fromJust . getOutput $ one + ioEdge = (fst from, fst to, (snd from, snd to)) + + newOutput = (\(x,y) -> (fromJust (Map.lookup x dict), y)) . fromJust . getOutput $ two + + in makeGraphPart (checkDupe (Graph.insEdge ioEdge base)) (getInput one) (Just newOutput) + + diff --git a/src/Library/Object.hs b/src/Library/Object.hs new file mode 100644 index 0000000..dd65ded --- /dev/null +++ b/src/Library/Object.hs @@ -0,0 +1,128 @@ +module Library.Object ( + Object(..), + objNum, + objName, + objList, + objTyOp, + objType, + objConst, + objVar, + objTerm, + objThm, + + List, + + makeSubst + ) where + + + +import Data.Maybe +import Data.List +import Library.TypeVar +import Library.Term +import Library.Theorem + + + +data Object = ObjNum Number + | ObjName Name + | ObjList List + | ObjTyOp TypeOp + | ObjType Type + | ObjConst Const + | ObjVar Var + | ObjTerm Term + | ObjThm Theorem deriving (Eq, Ord) + +type List = [Object] + + + +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 + + + +makeSubst :: [Object] -> Maybe Substitution +makeSubst l = + let list = (map (mapMaybe objList)) . (mapMaybe objList) $ l + f g h x = (g . head $ x, h . last $ x) + check = f (map (f objName objType)) (map (f objVar objTerm)) list + g = all (\x -> (isJust . fst $ x) && (isJust . snd $ x)) + h x = (fromJust . fst $ x, fromJust . snd $ x) + in if ((g . fst $ check) && (g . snd $ check)) + then Just (map h (fst check), map h (snd check)) + else Nothing + + +objNum :: Object -> Maybe Number +objNum obj = + case (obj) of + (ObjNum n) -> Just n + (_) -> Nothing + + +objName :: Object -> Maybe Name +objName obj = + case (obj) of + (ObjName n) -> Just n + (_) -> Nothing + + +objList :: Object -> Maybe List +objList obj = + case (obj) of + (ObjList l) -> Just l + (_) -> Nothing + + +objTyOp :: Object -> Maybe TypeOp +objTyOp obj = + case (obj) of + (ObjTyOp tyop) -> Just tyop + (_) -> Nothing + + +objType :: Object -> Maybe Type +objType obj = + case (obj) of + (ObjType ty) -> Just ty + (_) -> Nothing + + +objConst :: Object -> Maybe Const +objConst obj = + case (obj) of + (ObjConst c) -> Just c + (_) -> Nothing + + +objVar :: Object -> Maybe Var +objVar obj = + case (obj) of + (ObjVar var) -> Just var + (_) -> Nothing + + +objTerm :: Object -> Maybe Term +objTerm obj = + case (obj) of + (ObjTerm term) -> Just term + (_) -> Nothing + + +objThm :: Object -> Maybe Theorem +objThm obj = + case (obj) of + (ObjThm thm) -> Just thm + (_) -> Nothing + diff --git a/src/Library/Parse.hs b/src/Library/Parse.hs new file mode 100644 index 0000000..7494822 --- /dev/null +++ b/src/Library/Parse.hs @@ -0,0 +1,75 @@ +module Library.Parse ( + getLines, + stripReturn, + removeEscChars, + removeQuotes, + separateBy, + isComment, + isNumber, + isName, + output, + fst3, + snd3, + thd3 + ) where + +import Control.Monad( liftM ) +import qualified Data.Char as Char + + +getLines :: FilePath -> IO [String] +getLines = liftM lines . readFile + + +stripReturn :: String -> String +stripReturn s = if (last s == '\r') then init s else s + + +removeEscChars :: String -> String +removeEscChars [] = [] +removeEscChars (x:[]) = [x] +removeEscChars x = if (head x == '\\') + then (x!!1) : (removeEscChars . (drop 2) $ x) + else (head x) : (removeEscChars . tail $ x) + + +removeQuotes :: String -> String +removeQuotes = init . tail + + +separateBy :: Char -> String -> [String] +separateBy char list = + let f x = if (x == char) then ' ' else x + in words . (map f) $ list + + +isComment :: String -> Bool +isComment = (==) '#' . head + + +isNumber :: String -> Bool +isNumber ('0':[]) = True +isNumber ('-':ns) + | (ns /= [] && head ns /= '0') = isNumber ns +isNumber n = all (Char.isNumber) n + + +isName :: String -> Bool +isName s = all ((==) '"') [head s, last s] + + +output :: [String] -> IO () +output [] = return () +output list = do + putStrLn (head list) + output (tail list) + + +fst3 :: (a,b,c) -> a +fst3 (a,_,_) = a + +snd3 :: (a,b,c) -> b +snd3 (_,b,_) = b + +thd3 :: (a,b,c) -> c +thd3 (_,_,c) = c diff --git a/src/Library/ProofGraph.hs b/src/Library/ProofGraph.hs new file mode 100644 index 0000000..0e7e80a --- /dev/null +++ b/src/Library/ProofGraph.hs @@ -0,0 +1,159 @@ +module Library.ProofGraph ( + PGraph, + doGraphGen, + + checkDupe, + nodeEquals, + resolveNodeClash, + + argMap + ) where + + + +import Data.Maybe +import Data.List +import Data.Set( Set ) +import qualified Data.Set as Set +import Data.Map( Map, (!) ) +import qualified Data.Map as Map + +import Data.Graph.Inductive.Graph( Node, LNode, LEdge, (&) ) +import qualified Data.Graph.Inductive.Graph as Graph +import Data.Graph.Inductive.Tree + +import Library.Stack( Stack, at, (<:>) ) +import qualified Library.Stack as Stack +import Library.Parse( isNumber, isName ) + + + +type PGraph = Gr String (Int,Int) +type PStack = Stack (Int, LNode String) +type PMap = Map Int (Int, LNode String) + + +data CommandIO = IO { args :: Int + , results :: Int } + + +argMap :: String -> CommandIO +argMap "absTerm" = IO 2 1 +argMap "absThm" = IO 2 1 +argMap "appTerm" = IO 2 1 +argMap "appThm" = IO 2 1 +argMap "assume" = IO 1 1 +argMap "axiom" = IO 2 1 +argMap "betaConv" = IO 1 1 +argMap "cons" = IO 2 1 +argMap "const" = IO 1 1 +argMap "constTerm" = IO 2 1 +argMap "deductAntisym" = IO 2 1 +argMap "defineConst" = IO 2 2 +argMap "defineTypeOp" = IO 5 5 +argMap "eqMp" = IO 2 1 +argMap "nil" = IO 0 1 +argMap "opType" = IO 2 1 +argMap "refl" = IO 1 1 +argMap "subst" = IO 2 1 +argMap "thm" = IO 3 0 +argMap "typeOp" = IO 1 1 +argMap "var" = IO 2 1 +argMap "varTerm" = IO 1 1 +argMap "varType" = IO 1 1 +argMap x | (isName x) = IO 0 1 + + + +process :: String -> CommandIO -> PGraph -> PStack -> (PGraph, PStack) +process str io graph stack = + let argList = map (\x -> fromJust (stack `at` x)) [0..((args io) - 1)] + nextNum = head (Graph.newNodes 1 graph) + node = (nextNum, str) + edgeList = map (\x -> (nextNum, (fst . snd . snd $ x), (fst x, fst . snd $ x))) (zip [1..(args io)] argList) + graph' = (Graph.insEdges edgeList) . (Graph.insNode node) $ graph + nodeList = map (\x -> (x, node)) [1..(results io)] + stack' = foldr (<:>) (Stack.pop (args io) stack) nodeList + in (graph', stack') + + + +parse :: (PGraph,PStack,PMap) -> String -> (PGraph,PStack,PMap) +parse gs@(graph,stack,dictionary) str = + case str of + "def" -> let num = fst . fromJust $ stack `at` 0 + node = fromJust $ stack `at` 1 + dictionary' = Map.insert num node dictionary + stack' = Stack.pop 1 stack + in (graph, stack', dictionary') + + "ref" -> let num = fst . fromJust $ stack `at` 0 + node = fromJust (Map.lookup num dictionary) + stack' = node <:> (Stack.pop 1 stack) + in (graph, stack', dictionary) + + "remove" -> let num = fst . fromJust $ stack `at` 0 + node = fromJust (Map.lookup num dictionary) + stack' = node <:> (Stack.pop 1 stack) + dictionary' = Map.delete num dictionary + in (graph, stack', dictionary') + + "pop" -> (graph, (Stack.pop 1 stack), dictionary) + + '#':rest -> gs + + n | (isNumber n) -> let node = (read n, (0,"")) + stack' = node <:> stack + in (graph, stack', dictionary) + + x -> let (graph', stack') = process x (argMap x) graph stack + in (graph', stack', dictionary) + + + +checkDupe :: PGraph -> PGraph +checkDupe graph = + let f g n = let list = filter (\x -> (x /= n) && (nodeEquals g n x)) (Graph.nodes g) + in if (list == []) then g else merge g n (head list) + + merge g n r = + let edgesFixed = map (\(a,b,c) -> (a,r,c)) (Graph.inn g n) + in (Graph.insEdges edgesFixed) . (Graph.delNode n) $ g + + in foldl' f graph (Graph.nodes graph) + + + +nodeEquals :: Gr String (Int,Int) -> Node -> Node -> Bool +nodeEquals graph one two = + let edgesOne = sortBy sortFunc (Graph.out graph one) + edgesTwo = sortBy sortFunc (Graph.out graph two) + sortFunc = (\(_,_,x) (_,_,y) -> compare x y) + paired = zip (map (\(_,x,_) -> x) edgesOne) (map (\(_,x,_) -> x) edgesTwo) + + in (Graph.gelem one graph) && + (Graph.gelem two graph) && + (Graph.lab graph one == Graph.lab graph two) && + (length edgesOne == length edgesTwo) && + (all (\x -> nodeEquals graph (fst x) (snd x)) paired) + + + +resolveNodeClash :: Gr String (Int,Int) -> Gr String (Int,Int) -> (Gr String (Int,Int), Map Int Int) +resolveNodeClash ref graph = + let dict = Map.fromList (zip (Graph.nodes graph) (Graph.newNodes (Graph.noNodes graph) ref)) + nodeList = map (\(x,y) -> (fromJust (Map.lookup x dict), y)) (Graph.labNodes graph) + edgeList = map (\(x,y,z) -> (fromJust (Map.lookup x dict), + fromJust (Map.lookup y dict), z)) (Graph.labEdges graph) + in (Graph.mkGraph nodeList edgeList, dict) + + + +doGraphGen :: [String] -> PGraph +doGraphGen list = + let graph = Graph.empty + stack = Stack.empty + dictionary = Map.empty + result = foldl' parse (graph,stack,dictionary) list + in case result of (g,s,d) -> checkDupe g + 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" + diff --git a/src/Library/Stack.hs b/src/Library/Stack.hs new file mode 100644 index 0000000..99cd8e1 --- /dev/null +++ b/src/Library/Stack.hs @@ -0,0 +1,50 @@ +module Library.Stack ( + Stack, + empty, + at, + pop, + (<:>), + size, + diff + ) where + + +import Data.List + + +data Stack a = Stack [a] deriving (Eq) + + +instance Show a => Show (Stack a) where + show (Stack x) = "Stack:\n" ++ intercalate "\n" (map (show) x) ++ "\n\n" + + +infixr 9 <:> + + +empty :: Stack a +empty = Stack [] + + +at :: Stack a -> Int -> Maybe a +at (Stack list) index = + if (index < length list && index >= 0) + then Just (list!!index) + else Nothing + + +pop :: Int -> Stack a -> Stack a +pop n (Stack list) = Stack (drop n list) + + +(<:>) :: a -> Stack a -> Stack a +x <:> (Stack list) = Stack (x : list) + + +size :: Stack a -> Int +size (Stack list) = length list + + +diff :: (Eq a) => Stack a -> Stack a -> Stack a +diff (Stack one) (Stack two) = Stack (one \\ two) + diff --git a/src/Library/Term.hs b/src/Library/Term.hs new file mode 100644 index 0000000..be9e53b --- /dev/null +++ b/src/Library/Term.hs @@ -0,0 +1,193 @@ +module Library.Term ( + Term(..), + Substitution, + + alphaEquiv, + alphaConvert, + alphaConvertList, + substitute, + boundVars, + freeVars, + rename, + typeOf, + typeVarsInTerm, + mkEquals, + isEq, + getlhs, + getrhs + ) where + + + +import Data.List +import Data.Maybe +import qualified Data.Set as Set +import qualified Data.Map as Map +import Library.TypeVar + + + +data Term = TVar { tVar :: Var } + | TConst { tConst :: Const + , tConstType :: Type } + | TApp { tAppLeft :: Term + , tAppRight :: Term } + | TAbs { tAbsVar :: Term + , tAbsTerm :: Term } deriving (Ord) + +type Substitution = ( [(Name,Type)], [(Var,Term)] ) + + +instance Show Term where + show (TVar v) = (show v) + show (TConst a _) = (show a) + show (TApp (TApp eq lhs) rhs) + | isEq eq = "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")" + show (TApp a b) = "(" ++ (show a) ++ " " ++ (show b) ++ ")" + show (TAbs a b) = "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")" + + +instance Eq Term where + a == b = a `alphaEquiv` b + + + +alphaEquiv :: Term -> Term -> Bool +alphaEquiv a b = + let equiv term1 term2 varmap1 varmap2 depth = + case (term1,term2) of + (TConst a1 b1, TConst a2 b2) -> + a1 == a2 && b1 == b2 + + (TApp a1 b1, TApp a2 b2) -> + equiv a1 a2 varmap1 varmap2 depth && + equiv b1 b2 varmap1 varmap2 depth + + (TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) -> + equiv b1 b2 newmap1 newmap2 (depth+1) + where newmap1 = Map.insert (Var name1 type1) depth varmap1 + newmap2 = Map.insert (Var name2 type2) depth varmap2 + + (TVar (Var name1 type1), TVar (Var name2 type2)) -> + type1 == type2 && ((name1 == name2 && Map.notMember (Var name1 type1) varmap1 && Map.notMember (Var name2 type2) varmap2) || + Map.lookup (Var name1 type1) varmap1 == Map.lookup (Var name2 type2) varmap2) + + (_,_) -> False + + in equiv a b Map.empty Map.empty 0 + + +alphaConvert :: Term -> Term -> Term +alphaConvert (TConst _ _) (TConst a ty) = TConst a ty +alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2) +alphaConvert (TVar _) (TVar v) = TVar v +alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute ([],[(tVar v1,v2)]) (TAbs v1 (alphaConvert a b)) + + +alphaConvertList :: [Term] -> [Term] -> [Term] +alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b) + + +substitute :: Substitution -> Term -> Term +substitute (t,v) term = + let typesub x y = + case y of + (TConst a ty) -> TConst a (typeVarSub x ty) + (TApp a b) -> TApp (typesub x a) (typesub x b) + (TAbs (TVar (Var n ty)) a) -> TAbs (TVar (Var n (typeVarSub x ty))) (typesub x a) + (TVar (Var n ty)) -> TVar (Var n (typeVarSub x ty)) + + varsub x y = + case y of + (TConst a ty) -> TConst a ty + (TApp a b) -> TApp (varsub x a) (varsub x b) + (TVar v) -> if (Map.member v x) + then fromJust (Map.lookup v x) + else TVar v + (TAbs v a) -> let safe = rename (TAbs v a) (Set.union (Map.keysSet x) (Set.unions . (map freeVars) . (Map.elems) $ x)) + in case safe of + (TAbs m n) -> TAbs m (varsub x n) + + tymap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty t + vmap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty v + + in (varsub vmap) . (typesub tymap) $ term + + +boundVars :: Term -> Set.Set Var +boundVars (TConst a b) = Set.empty +boundVars (TApp a b) = Set.union (boundVars a) (boundVars b) +boundVars (TVar a) = Set.empty +boundVars (TAbs a b) = Set.insert (tVar a) (boundVars b) + + +freeVars :: Term -> Set.Set Var +freeVars (TConst a b) = Set.empty +freeVars (TApp a b) = Set.union (freeVars a) (freeVars b) +freeVars (TVar a) = Set.singleton a +freeVars (TAbs a b) = Set.delete (tVar a) (freeVars b) + + +rename :: Term -> Set.Set Var -> Term +rename (TAbs (TVar v) t) vars = + let doRename x y z = + case x of + (TAbs (TVar a) b) -> + if (a == y) + then TAbs (TVar z) (doRename b y z) + else TAbs (TVar a) (doRename b y z) + (TConst a b) -> TConst a b + (TApp a b) -> TApp (doRename a y z) (doRename b y z) + (TVar a) -> + if (a == y) + then TVar z + else TVar a + + findSafe x y = + if (Set.member x y) + then case x of + (Var a b) -> + case a of + (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y + else x + + in if (Set.member v vars) + then doRename (TAbs (TVar v) t) v (findSafe v vars) + else TAbs (TVar v) t + + +typeOf :: Term -> Type +typeOf (TConst _ ty) = ty +typeOf (TVar v) = varTy v +typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t) +typeOf (TApp f _) = + -- type of f is of the form [[a,b], "->"] + last . aType . typeOf $ f + + +typeVarsInTerm :: Term -> Set.Set Type +typeVarsInTerm (TConst _ ty) = typeVarsInType ty +typeVarsInTerm (TVar v) = typeVarsInType . varTy $ v +typeVarsInTerm (TAbs v t) = Set.union (typeVarsInType . varTy . tVar $ v) (typeVarsInTerm t) +typeVarsInTerm (TApp f x) = Set.union (typeVarsInTerm f) (typeVarsInTerm x) + + +mkEquals :: Term -> Term -> Term +mkEquals lhs rhs = + let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs)) + in TApp (TApp eqConst lhs) rhs + + +getlhs :: Term -> Term +getlhs (TApp (TApp eq lhs) _) + | (isEq eq) = lhs + + +getrhs :: Term -> Term +getrhs (TApp (TApp eq _) rhs) + | (isEq eq) = rhs + + +isEq :: Term -> Bool +isEq (TConst (Const (Name [] "=")) _) = True +isEq _ = False diff --git a/src/Library/TermNet.hs b/src/Library/TermNet.hs new file mode 100644 index 0000000..16b5446 --- /dev/null +++ b/src/Library/TermNet.hs @@ -0,0 +1,214 @@ +module Library.TermNet( + TermNet, + + empty, + getLeafList, + getBranchList, + + genThm, + termToTermString, + thmToTermString, + + addThm, + addThmFromNode, + matchThm + ) where + + + +import Data.Maybe +import Data.List +import qualified Data.Set as Set +import Data.Graph.Inductive.Graph( Node ) +import qualified Data.Graph.Inductive.Graph as Graph +import Library.ProofGraph +import Library.WriteProof +import Library.Object +import Library.Theorem +import Library.Term +import Library.Parse +import Library.Semantic +import Library.Stack( Stack, at, (<:>) ) +import qualified Library.Stack as Stack + + + +data TermNet = Leaf [(Theorem, Node)] | Branch [(String, TermNet)] + deriving (Eq, Show) + + + +empty :: TermNet +empty = Branch [] + + + +isLeaf :: TermNet -> Bool +isLeaf (Leaf _) = True +isLeaf _ = False + + + +isBranch :: TermNet -> Bool +isBranch (Branch _) = True +isBranch _ = False + + + +getLeafList :: TermNet -> Maybe [(Theorem, Node)] +getLeafList net = + case net of + Leaf list -> Just list + Branch list -> Nothing + + + +getBranchList :: TermNet -> Maybe [(String, TermNet)] +getBranchList net = + case net of + Leaf list -> Nothing + Branch list -> Just list + + + +genThm :: PGraph -> Node -> Theorem +genThm graph node = + let gen g n num = + let edge = filter (\x -> (fst . thd3 $ x) == num) (Graph.out g n) + node = (snd3 . head $ edge) + listing = write g node + in fromJust (((\(a,_,_,_) -> a) . fromJust $ (eval listing)) `at` 0) + + hypList = map (fromJust . objTerm) (fromJust . objList $ (gen graph node 2)) + con = fromJust . objTerm $ (gen graph node 1) + + in Theorem (Set.fromList hypList) con + + + +termToTermString :: Term -> [String] +termToTermString term = + case term of + (TConst _ _) -> + ["const"] + + (TApp func arg) -> + ["app"] ++ (termToTermString func) ++ (termToTermString arg) + + (TAbs var body) -> + ["abs", "var"] ++ (termToTermString body) + + (TVar var) -> + ["var"] + + + +thmToTermString :: Theorem -> [String] +thmToTermString theorem = + let hypList = Set.toList (thmHyp theorem) + f soFar hyp = soFar ++ ["hyp"] ++ (termToTermString hyp) + in (foldl' f [] hypList) ++ ["con"] ++ (termToTermString . thmCon $ theorem) + + + +addThm :: TermNet -> Theorem -> Node -> TermNet +addThm net theorem node = + addThmImp net (theorem,node) (thmToTermString theorem) + + + +addThmFromNode :: TermNet -> PGraph -> Node -> TermNet +addThmFromNode net graph node = + let theorem = genThm graph node + in addThmImp net (theorem,node) (thmToTermString theorem) + + + +addThmImp :: TermNet -> (Theorem,Node) -> [String] -> TermNet +addThmImp (Branch branchList) item (x:[]) = + let (sameKey, rest) = partition (\(y,z) -> y == x && isLeaf z) branchList + in if (sameKey == []) + then let leaf' = Leaf [item] + in Branch ((x,leaf'):rest) + else let leaf = snd . head $ sameKey + leafList = fromJust . getLeafList $ leaf + in if (item `elem` leafList) + then Branch branchList + else let leaf' = Leaf (item:leafList) + in Branch ((x,leaf'):rest) + +addThmImp (Branch branchList) item (x:xs) = + let (sameKey, rest) = partition (\(y,z) -> y == x) branchList + in if (sameKey == []) + then let net' = addThmImp empty item xs + in Branch ((x,net'):rest) + else let nextStepDown = snd . head $ sameKey + net' = addThmImp nextStepDown item xs + in Branch ((x,net'):rest) + + + +matchThm :: TermNet -> Theorem -> [(Theorem,Node)] +matchThm net theorem = + let hyp = Set.toList (thmHyp theorem) + con = thmCon theorem + (curPrefix, curTerm) = if (hyp == []) + then ("con", con) + else ("hyp", head hyp) + + r = do a <- matchImp curPrefix net + let b = matchTermImp curTerm a + (branches, leaves) = partition (\x -> isBranch x) b + + c <- if (hyp == []) + then getLeafList (foldl' unify (Leaf []) leaves) + else let theorem' = Theorem (Set.fromList (tail hyp)) con + in return (matchThm (foldl' unify empty branches) theorem') + return c + + in if (isNothing r) then [] else fromJust r + + + +matchImp :: String -> TermNet -> Maybe TermNet +matchImp key net = + do list <- getBranchList net + let result = filter (\(x,y) -> x == key) list + r <- if (result == []) then Nothing else Just (snd . head $ result) + return r + + + +matchTermImp :: Term -> TermNet -> [TermNet] +matchTermImp term net = + let list = getBranchList net + var = matchImp "var" net + result = + case term of + (TConst c ty) -> + do a <- matchImp "const" net + return [a] + + (TApp f x) -> + do a <- matchImp "app" net + let b = matchTermImp f a + return (concat (map (matchTermImp x) b)) + + (TAbs v x) -> + do a <- matchImp "abs" net + b <- matchImp "var" a + return (matchTermImp x b) + + (TVar v) -> Nothing --don't need to do anything because variables are already taken care of + + var' = if (isNothing var) then [] else [fromJust var] + result' = if (isNothing result) then [] else fromJust result + + in var' ++ result' + + + +unify :: TermNet -> TermNet -> TermNet +unify (Branch a) (Branch b) = Branch (a ++ b) +unify (Leaf a) (Leaf b) = Leaf (a ++ b) + diff --git a/src/Library/Theorem.hs b/src/Library/Theorem.hs new file mode 100644 index 0000000..fc66cc2 --- /dev/null +++ b/src/Library/Theorem.hs @@ -0,0 +1,19 @@ +module Library.Theorem ( + Theorem(..), + ) where + + + +import qualified Data.Set as Set +import Library.TypeVar +import Library.Term + + + +data Theorem = Theorem { thmHyp :: Set.Set Term + , thmCon :: Term } deriving (Eq, Ord) + + + +instance Show Theorem where + show a = (show . Set.toList . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a) diff --git a/src/Library/TypeVar.hs b/src/Library/TypeVar.hs new file mode 100644 index 0000000..d2915e6 --- /dev/null +++ b/src/Library/TypeVar.hs @@ -0,0 +1,99 @@ +module Library.TypeVar ( + Number, + + Name(..), + + TypeOp(..), + + Type(..), + + Const(..), + + Var(..), + + mkEqualsType, + typeFunc, + typeBool, + typeVarsInType, + isTypeVar, + typeVarSub + ) where + + + +import Data.List +import Data.Maybe +import qualified Data.Set as Set +import Data.Map( Map, (!) ) +import qualified Data.Map as Map + + + +type Number = Int + +data Name = Name { nameSpace :: [String] + , nameId :: String } deriving (Eq, Ord) + +data TypeOp = TypeOp { tyOp :: Name } deriving (Eq, Ord) + +data Type = TypeVar { typeVar :: Name } + | AType { aType :: [Type] + , aTypeOp :: TypeOp } deriving (Eq, Ord) + +data Const = Const { constName :: Name } deriving (Eq, Ord) + +data Var = Var { varName :: Name + , varTy :: Type } deriving (Eq, Ord) + + + +instance Show Name where + show a = intercalate "." (nameSpace a ++ [nameId a]) + +instance Show TypeOp where + show a = "typeOp " ++ (show $ tyOp a) + +instance Show Type where + show (TypeVar tyVar) = "V " ++ (show tyVar) + show (AType [] (TypeOp (Name [] "bool"))) = "bool" + show (AType [d,r] (TypeOp (Name [] "->"))) = "(" ++ show d ++ " -> " ++ show r ++ ")" + show (AType list typeOp) = "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list) + +instance Show Const where + show (Const a) = show a + +instance Show Var where + show (Var a _) = show a + + + +mkEqualsType :: Type -> Type +mkEqualsType ty = typeFunc ty (typeFunc ty typeBool) + + +typeFunc :: Type -> Type -> Type +typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->")) + + +typeBool :: Type +typeBool = AType [] (TypeOp (Name [] "bool")) + + +typeVarsInType :: Type -> Set.Set Type +typeVarsInType (TypeVar t) = Set.singleton (TypeVar t) +typeVarsInType (AType list _) = Set.unions . (map typeVarsInType) $ list + + +isTypeVar :: Type -> Bool +isTypeVar (TypeVar _) = True +isTypeVar _ = False + + +typeVarSub :: Map Name Type -> Type -> Type +typeVarSub m (TypeVar a) = + if (Map.member a m) + then fromJust (Map.lookup a m) + else TypeVar a +typeVarSub m (AType list op) = + AType (map (typeVarSub m) list) op + diff --git a/src/Library/Usage.hs b/src/Library/Usage.hs new file mode 100644 index 0000000..a307274 --- /dev/null +++ b/src/Library/Usage.hs @@ -0,0 +1,80 @@ +module Library.Usage( + UsageMap, + usageMap, + useSort, + nodeOutput, + getArg + ) where + + + +import Data.Map( Map ) +import qualified Data.Map as Map +import Data.Set( Set ) +import qualified Data.Set as Set +import Data.List +import Data.Maybe +import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) +import qualified Data.Graph.Inductive.Graph as Graph +import Library.Parse +import Library.ProofGraph + + + +type UsageMap = Map Node (Map (LEdge (Int,Int)) (Int,[Int])) + + +-- Takes a graph, a starting list of nodes, a set of nodes of interest, and +-- follows the starting nodes up the graph to find which edges the starting nodes +-- will encounter the nodes of interest through. +usageMap :: PGraph -> [Node] -> Set Node -> UsageMap +usageMap graph order interest = + let unionFunc a b = Map.unionWith min a b + + addFunc index prev umap edge = + let node = snd3 edge + curIn = Graph.outdeg graph (fst3 edge) + prev' = (curIn - (fst . thd3 $ edge)):prev + toAdd = Map.singleton node (Map.singleton edge (index,prev')) + in if (Set.member node interest) + then Map.unionWith unionFunc toAdd umap + else umap + + f umap (index,node,prev) = + let edgeList = Graph.out graph node + sucMapList = map (f Map.empty) (map (\x -> (index, snd3 x, (length edgeList - (fst . thd3 $ x)):prev)) edgeList) + umap' = foldl' (addFunc index prev) umap edgeList + in Map.unionsWith unionFunc (umap':sucMapList) + + in foldl' f Map.empty (zip3 [1..] order (repeat [])) + + + +useSort :: (LEdge a, (Int,[Int])) -> (LEdge a, (Int,[Int])) -> Ordering +useSort (_,(w,x)) (_,(y,z)) = + let check = compare w y + in if (check == EQ) + then compare (reverse x) (reverse z) + else check + + + +nodeOutput :: PGraph -> Node -> Int +nodeOutput graph node = + let label = fromJust (Graph.lab graph node) + in case label of + "thm" -> 0 + "pop" -> 0 + "defineConst" -> 2 + "defineTypeOp" -> 5 + x -> 1 + + + +getArg :: PGraph -> Node -> Int -> Maybe Node +getArg graph node arg = + let edge = filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node) + in if (edge == []) + then Nothing + else Just (snd3 . head $ edge) + diff --git a/src/Library/WriteProof.hs b/src/Library/WriteProof.hs new file mode 100644 index 0000000..2c15b74 --- /dev/null +++ b/src/Library/WriteProof.hs @@ -0,0 +1,211 @@ +module Library.WriteProof ( + write, + writeAll, + doWriteProof, + singleCommands, + next, + genPart, + writeGraph + ) where + + + +import Data.Maybe +import Data.Graph.Inductive.Graph( LNode, LEdge, Node, Edge, (&) ) +import qualified Data.Graph.Inductive.Graph as Graph +import Data.Graph.Inductive.Tree +import Data.Map( Map, (!) ) +import qualified Data.Map as Map +import Data.Set( Set ) +import qualified Data.Set as Set +import Data.List +import Library.Stack( Stack, at, (<:>) ) +import qualified Library.Stack as Stack +import Library.Parse( isNumber, fst3, snd3, thd3 ) +import Library.Cost +import Library.ProofGraph +import Library.GraphPart +import Library.Usage + + + +orderNodes :: PGraph -> [Node] -> [Node] +orderNodes graph nodeList = nodeList +--placeholder + + + +-- buggy +multiCommandsSimple :: PGraph -> UsageMap -> [Node] -> PGraph +multiCommandsSimple graph usemap nodeList = + let multiNodes = filter (\x -> nodeOutput graph x > 1 && x `notElem` nodeList) (Graph.nodes graph) + umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap + + f = (\gr node edgemap -> + let out = nodeOutput gr node + index = next out gr + + edgeList = Map.toList edgemap + edgeToNode = (\x -> (fst3 x, fst . thd3 $ x)) + + sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edgeList + grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted + + defEdge = fst (minimumBy useSort edgeList) + removeEdges = map (fst . (maximumBy useSort)) grouped + refEdges = map (filter (\x -> x /= defEdge && x `notElem` removeEdges) . (map fst)) grouped + + usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeEdges)) [1..out] + + defGen = (\num -> + if (num > out) + then let reqEdges = filter (\x -> (snd . thd3 . fst $ x) == (snd . thd3 $ defEdge) && fst x /= defEdge) edgeList + refArg = (snd . thd3 $ defEdge) - 1 + in if (reqEdges == []) + then [index!!refArg, "ref"] --remove + else [index!!refArg, "ref"] + else if (num == (snd . thd3 $ defEdge) && num == out) + then if (filter (\x -> x /= defEdge && (snd . thd3 $ x) == num) (map fst edgeList) == []) + then [] + else [index!!(num-1), "def"] + else if (num `elem` usedArgs) + then [index!!(num-1), "def", "pop"] ++ defGen (num+1) + else ["pop"] ++ defGen (num+1)) + + defPart = (genPart (defGen 1) True, Just (node,1), [edgeToNode defEdge]) + + removeList = filter (\(x,y) -> y /= defEdge) (zip usedArgs removeEdges) + removeParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, [edgeToNode y])) removeList + + refList = filter (\(x,y) -> y /= []) (zip usedArgs refEdges) + refParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, map edgeToNode y)) refList + + partList = defPart:(removeParts ++ refParts) + edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList + partsAdded = graphAddList partList edgesRemoved + in partsAdded) + + in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes + + + +singleCommands :: PGraph -> UsageMap -> [Node] -> PGraph +singleCommands graph usemap nodeList = + let singleNodes = filter (\x -> nodeOutput graph x == 1 && Graph.indeg graph x > 1) (Graph.nodes graph) + umap = Map.filterWithKey (\n _ -> n `elem` singleNodes) usemap + + s = (\gr node edgemap -> + let index = head (next 1 gr) + edgeList = Map.toList edgemap + + defEdge = fst (minimumBy useSort edgeList) + removeEdge = fst (maximumBy useSort edgeList) + refEdgeList = filter (\x -> x /= defEdge && x /= removeEdge) (map fst edgeList) + + defPart = genPart [index, "def"] True + refPart = genPart [index, "ref"] False + removePart = genPart [index, "ref"] False + + defNode = (fst3 defEdge, fst . thd3 $ defEdge) + removeNode = (fst3 removeEdge, fst . thd3 $ removeEdge) + refNodeList = map (\x -> (fst3 x, fst . thd3 $ x)) refEdgeList + + partList = [(defPart, Just (node, 1), [defNode]), (removePart, Nothing, [removeNode])] + partList' = if (refNodeList == []) then partList else (refPart, Nothing, refNodeList):partList + + edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList + partsAdded = graphAddList partList' edgesRemoved + in partsAdded) + + f = (\gr node edgemap -> + let reuse = Graph.indeg graph node + costToStore = (nodeCost graph node) + (listCost ["def","0"]) + (reuse - 1) * (listCost ["ref","0"]) + costToIgnore = reuse * (nodeCost graph node) + in if (costToStore >= costToIgnore) + then gr + else s gr node edgemap) + + in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph singleNodes + + + +genPart :: [String] -> Bool -> GraphPart +genPart labels hasInput = + let nodeList = zip [1..] labels + edgeFunc = (\edges nodes -> + if (nodes == [] || (tail nodes) == []) + then edges + else let newEdge = (fst (nodes!!1), fst (nodes!!0), (1,1)) + in edgeFunc (newEdge:edges) (tail nodes)) + edgeList = edgeFunc [] nodeList + input = if (hasInput) then Just (1,1) else Nothing + output = Just (length labels, 1) + in graphPart nodeList edgeList input output + + + +next :: Int -> PGraph -> [String] +next num graph = + let nodeList = filter (isNumber . snd) (Graph.labNodes graph) + numList = nub . (map (read . snd)) $ nodeList + f x y = if (x `elem` y) then f (x + 1) y else x + g x y = if (x == 0) then y else g (x - 1) (f 0 (y ++ numList) : y) + in map show (g num []) + + + +removeUnused :: PGraph -> [Node] -> PGraph +removeUnused graph nodeList = + let unused = filter (\x -> Graph.indeg graph x == 0 && x `notElem` nodeList) (Graph.nodes graph) + in if (unused == []) + then graph + else removeUnused (Graph.delNodes unused graph) nodeList + + + +resolve :: PGraph -> [Node] -> PGraph +resolve graph nodeList = + let liveGraph = removeUnused graph nodeList + umap = usageMap graph nodeList (Set.fromList (Graph.nodes liveGraph)) + singlesDone = singleCommands liveGraph umap nodeList + multisDone = multiCommandsSimple singlesDone umap nodeList + in multisDone + + + +writeGraph :: PGraph -> Node -> [String] +writeGraph graph node = + let label = fromJust (Graph.lab graph node) + argList = [1 .. (Graph.outdeg graph node)] + f s a = let arg = getArg graph node a + in if (isNothing arg) + then s + else (writeGraph graph (fromJust arg)) ++ s + in foldl' f [label] argList + + + +write :: PGraph -> Node -> [String] +write graph node = + writeGraph (resolve graph [node]) node + + + +writeAll :: PGraph -> [Node] -> [String] +writeAll graph nodeList = + let ordered = orderNodes graph nodeList + resolved = resolve graph ordered + f g n = if (n == []) + then [] + else (writeGraph g (head n)) ++ (f g (tail n)) + in f resolved ordered + + +-- metric relates to minimum amount of work done not-on-top of the stack + + +doWriteProof :: PGraph -> [String] +doWriteProof graph = + let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) + in writeAll graph initList + diff --git a/src/Library/alternate_multi_command.hs b/src/Library/alternate_multi_command.hs new file mode 100644 index 0000000..da49a7d --- /dev/null +++ b/src/Library/alternate_multi_command.hs @@ -0,0 +1,315 @@ +multiCommands :: PGraph -> UsageMap -> [Node] -> PGraph +multiCommands graph usemap nodeList = + let multiNodes = filter (\x -> nodeOutput graph x > 1) (Graph.nodes graph) + umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap + + before = (\gr node edgemap arg indexList -> + let edges = filter (\x -> snd . thd3 . fst $ x < arg) edgemap + + -- sorts and groups by which output of the command each edge is using + sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges + grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted + + -- makes a list of pairs of (maximum, restOfList) + maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped + + refNodeEdges = map (fst . snd) maxSplit + removeNodeEdges = concat (map (fst . fst) maxSplit) + + usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeNodeEdges)) [1..(arg-1)] + + -- creates a graphpart to define and pop all the initial outputs to get to the used one in the middle + defGen = (\num -> + if (num == arg) + then [] + else if (index!!num `elem` usedArgs) + then [index!!num, "def", "pop"] ++ defGen (num+1) + else ["pop"] ++ defGen (num+1)) + defPart = genPart (defGen 0) True + + -- creates graphparts for removing all the items stored in the dictionary, including node attachments + removeList = zip usedArgs removeNodeEdges + removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList + + -- creates graphparts to reference all the items stored in the dictionary, including node attachments + refList = zip usedArgs refNodeEdges + refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList + + in (defPart, refPart ++ removePart)) + + + after = (\gr node edgemap arg indexList -> + let -- obtain edges after the cutoff argument + edges = filter (\x -> snd . thd3 . fst $ x > arg) edgemap + + -- sort and group by which output of the command each edge is using + sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges + grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted + + mins = map (minimumBy useSort) grouped + initEdge = minimumBy useSort (Map.toList edgemap) + + usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) mins)) [(arg+1)..(nodeOutput gr node)] + edgeToNode = (\x -> (fst3 x, fst . thd3 $ x)) + + -- finds the argument where you have to pop everything and store it all in the dictionary before + -- proceeding + findAttach = (\x y -> + if (x == []) + then nodeOutput gr node + else let allZero = all (=0) (snd . snd . head $ x) + headIsMin = (head x) == (minimumBy useSort x) + headThmLowestStrict = let testList = map (fst . snd) x + in all (> head testList) (tail testList) + nextUsedArg = snd . thd3 . fst . head . tail $ x + in if (allZero && headIsMin && headThmLowestStrict) + then findAttach (tail x) nextUsedArg + else y) + + argToAttach = findAttach initEdge:mins arg + + process = (\attach curArg modp ordp -> + case (compare arg argToAttach) of + LT -> + EQ -> + GT ->) + + (modParts, ordinaryParts) = process argToAttach arg [] [] + + -- calculate the def/pop/ref defPart + afterPartInit = + afterPart = + if (argToAttach == arg) + then + else + + -- calculate def nodes/parts for outputs before the argToAttach + defs = + makeDefList = + defPart = map (\(x,y) -> (genPart [index!!(x-1), "def"] False, Nothing, [edgeToNode y])) makeDefList + + -- calculate ref and remove nodes/parts + maxes = map (maximumBy useSort) grouped + refs = map (filter (\x -> x `notElem` maxes && x `notElem` defs)) grouped + + removeList = zip usedArgs maxes + removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList + + -- creates graphparts to reference all the items stored in the dictionary, including node attachments + refList = zip usedArgs refs + refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList + + in (modParts, ordinaryParts)) + + addPreserveNodeParts = (\partList graph -> + ) + + f = (\gr node edgemap -> + let edgeList = Map.toList edgemap + + out = nodeOutput gr node + index = next (out + 1) gr + + initEdge = fst (minimumBy useSort edgeList) + initArg = snd . thd3 $ initEdge + (defBefore, beforeParts) = before gr node edgemap initArg (take (initArg-1) index) + (defAfter, afterParts) = after gr node edgemap initArg (drop initArg index) + edgesToRemove = filter (\x -> x /= initEdge) (map fst edgeList) + + gr' = addPreserveNodeParts defAfter gr + + edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) gr' edgesToRemove + partsAdded = graphAddList partList edgesRemoved + in partsAdded) + + in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes + + + + + + + + + + + + + +multiCommands :: PGraph -> PGraph -> UsageMap -> [Node] -> PGraph +multiCommands graph orig usemap nodeList = + let process = (\gr stack dict workmap edge -> + let node = snd3 edge + label = fromJust (Graph.lab gr node) + in if (label == "def" || label == "ref" || label == "remove" || isNumber label) + then dictProcess gr stack dict workmap edge + else regProcess gr stack dict workmap edge + + + dictProcess = (\gr stack dict workmap edge -> + let node = snd3 edge + label = fromJust (Graph.lab gr node) + index = fromJust (Graph.lab gr (head (Graph.suc gr node))) + + in if (label == "def") + then let dict' = Map.insert index (head stack) dict + in (gr, stack, dict', workmap) + + else if (label == "ref") + then let stack' = (fromJust (Map.lookup index dict)):stack + in (gr, stack', dict, workmap) + + else if (label == "remove") + then let stack' = (fromJust (Map.lookup index dict)):stack + dict' = Map.delete index dict + in (gr, stack', dict', workmap) + else -- isNumber label + (gr, stack, dict, workmap) + + + regProcess = (\gr stack dict workmap edge -> + let node = snd3 edge + label = fromJust (Graph.lab gr node) + + io = argMap label + sortedIns = sortBy (\x y -> compare (fst . thd3 $ x) (fst . thd3 $ y)) (Graph.out orig node) + expectedInput = map (\(a,b,(c,d)) -> (b,d)) sortedIns + + consume = (\(g,s,d,w) inList -> + if (inList == []) + then if (nodeOutput == 1) + then (g, (node,1):s, d, w) + else initial (g,s,d,w) + else let i = head inList + in if (head s == i) + then consume (g, tail s, d, w) (tail inList) + else store (g, s, d, w) inList) + + initial = (\(g,s,d,w) inList -> + let edgemap = Map.toList (fromJust (Map.lookup node usemap)) + sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ b)) edgemap + grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted + minimals = map (minimumBy useSort) grouped + usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) minimals)) [1..nodeOutput] + atArg = snd . thd3 $ edge + atArgReuse = length (filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap) + fromStart = fst . snd $ (head (filter (\x -> ((snd . thd3 . fst $ x) == atArg)) minimals)) + edgesToRemove = filter (\x -> (snd . thd3 $ x) < upTo) (map fst edgemap) + + upTo = let shortList = filter (\x -> (snd . thd3 . fst $ x) > atArg && (fst . snd $ x) > fromStart) minimals + in if (shortList == []) + then nodeOutput + 1 + else let shortNum = snd . thd3 . fst . head $ shortList + calc = (\num -> + if (filter (\x -> (snd . thd3 . fst $ x) == num - 1) edgemap == []) + then calc (num - 1) + else num) + in calc shortNum + index = next upTo g + + defPartGen = (\num -> + if (num == upTo) + then if (atArg + 1 < upTo) + then if (atArgReuse > 1) + then [index!!atArg, "ref"] + else [index!!atArg, "remove"] + else [] + else if (num `elem` usedArgs) + then if (num + 1 == atArg &&) + else if (num == atArg) + then if (atArgReuse <= 1 && atArg + 1 == upTo) + then defPartGen (num+1) + else if (atArg + 1 < upTo) + then [index!!num, "def", "pop"] ++ (defPartGen (num+1)) + else [index!!num, "def"] ++ (defPartGen (num+1)) + else [index!!num, "def", "pop"] ++ (defPartGen (num+1)) + else ["pop"] ++ (defPartGen (num+1))) + defPart = genPart (defPartGen 1) True + + maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped + refNodeEdges = map (fst . snd) maxSplit + removeNodeEdges = concat (map (fst . fst) maxSplit) + + removeList = zip usedArgs removeNodeEdges + removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList + + refList = zip usedArgs refNodeEdges + refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refPart + + workingEdge = + let atArgEdges = filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap + initEdge = fst . head $ (filter (\x -> (snd . thd3 $ x) == atArg && + (x `notElem` (delete (minimumBy useSort atArgEdges) + atArgEdges))) (Graph.inn g' node)) + calc = (\e -> + if (fst3 e == fst3 edge) + then e + else calc (head (Graph.inn g' (fst3 e)))) + in calc initEdge + w' = Map.insert node workingEdge + + storedArgs = if (atArgReuse > 1 || atArg + 1 < upTo) + then filter (< upTo) usedArgs + else delete atArg (filter (< upTo) usedArgs) + dictAddList = map (\x -> (index!!(x-1), (node,x))) storedArgs + d' = foldl' (\x (y,z) -> Map.insert y z x) d dictAddList + + stackArgs = atArg:(filter (>= upTo) usedArgs) + stackAddList = map (\x -> (node,x)) stackArgs + s' = stackArgs ++ s + + edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) g edgesToRemove + g' = graphAddList (defPart:(refPart ++ removePart)) edgesRemoved + + in (g', s', d', w')) + + + store = (\(g,s,d,w) inList -> + let s' = tail s + (node, arg) = head s -- the thing on the stack that shouldnt be there + workEdge = Map.lookup node w + (reqNode, reqArg) = head inList -- what we want on the stack instead + + index = head (next 1 g) + edgemap = Map.toList (Map.lookup node usemap) -- map of the edges leading into the node + edgesOfArg = filter (\(x,y) -> (snd . thd3 $ x) == arg) edgemap -- edges using the arg we want to get rid of + + removeEdge = maximumBy useSort edgesOfArg + refEdgeList = delete removeEdge edgesOfArg + + defPart = genPart [index, "def"] True + refPart = genPart [index, "ref"] False + removePart = genPart [index, "remove" False + popPart = genPart ["pop"] True + + in consume (g', s', d', w') inList + + in consume (gr,stack,dict,workmap) expectedInput) + + + h = (\gr st di ma edge -> + let node = snd3 edge + (gr',st',di',ma') = f gr st di ma node + in process gr' st' di' ma' edge) + + f = (\gr st di ma no -> + let args = reverse [1..(nodeOutput gr no)] + func = (\(g,s,d,m) a -> + let edge = filter (\x -> fst . thd3 $ x == a) (Graph.out g no) + in if (edge == []) + then (g,s,d,m) + else h gr st di ma (head edge) + in foldl' func (gr,st,di,ma) args + + stack = [] + dictionary = Map.empty + workmap = Map.empty + + (graph',stack',dictionary',workmap') = + foldl' (\(g,s,d,m) n -> f g s d m n) (graph, stack, dictionary, workmap) nodeList + + in graph' + + + + \ No newline at end of file diff --git a/src/ListThm.hs b/src/ListThm.hs new file mode 100644 index 0000000..540486d --- /dev/null +++ b/src/ListThm.hs @@ -0,0 +1,43 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse +import Library.ProofGraph +import Library.WriteProof +import Library.Semantic +import Library.Stack + +import Data.Maybe +import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) +import qualified Data.Graph.Inductive.Graph as Graph + + + +fst4 :: (a,b,c,d) -> a +fst4 (a,_,_,_) = a + + + +toThms :: PGraph -> [Node] -> [String] +toThms graph nodeList = + let hyp = (\g n -> let edge = filter (\x -> (fst . thd3 $ x) == 2) (Graph.out g n) + node = snd3 . head $ edge + in write g node) + + con = (\g n -> let edge = filter (\x -> (fst . thd3 $ x) == 1) (Graph.out g n) + node = snd3 . head $ edge + in write g node) + + f = (\x -> (show . fst $ x) ++ ". " ++ (show . fromJust $ ((fst4 . fromJust $ (eval (hyp graph (snd x)))) `at` 0)) ++ + " |- " ++ (show . fromJust $ ((fst4 . fromJust $ (eval (con graph (snd x)))) `at` 0))) + + in map f (zip [1..] nodeList) + + + +main = do + args <- getArgs + list <- getLines (head args) + let graph = doGraphGen (map (stripReturn) list) + initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) + theorems = toThms graph initList + output theorems diff --git a/src/MeaningSubst.hs b/src/MeaningSubst.hs new file mode 100644 index 0000000..a0821b5 --- /dev/null +++ b/src/MeaningSubst.hs @@ -0,0 +1,166 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse +import Library.ProofGraph +import Library.GraphPart +import Library.Theorem +import Library.Term +import Library.TypeVar +import Library.Generator +import Library.TermNet( TermNet ) +import qualified Library.TermNet as TermNet +import Data.Graph.Inductive.Graph( Node, LNode ) +import qualified Data.Graph.Inductive.Graph as Graph +import Data.Map( Map ) +import qualified Data.Map as Map +import qualified Data.Set as Set +import Data.List +import Data.Maybe + + + +data Step = Step { from :: Node + , to :: Node + , sub :: Substitution } + + + +alreadyMatchedElem :: (Ord a, Eq b) => a -> b -> Map a b -> Bool +alreadyMatchedElem x y xymap = + Map.member x xymap && Map.lookup x xymap /= Just y + + + +createSubst :: Theorem -> Theorem -> Maybe Substitution +createSubst one two = + let f = (\x y tymap varmap -> + case (x,y) of + (TVar (Var n ty), term) -> + if (alreadyMatchedElem (Var n ty) term varmap) + then Nothing + else let varmap' = if (Map.lookup (Var n ty) varmap == Nothing) + then Map.insert (Var n ty) term varmap + else varmap + in Just (tymap, varmap') + + (TConst a1 ty1, TConst a2 ty2) -> + if (alreadyMatchedElem (typeVar ty1) ty2 tymap || a1 /= a2 || (ty1 /= ty2 && not (isTypeVar ty1))) + then Nothing + else let tymap' = if (ty1 /= ty2) + then Map.insert (typeVar ty1) ty2 tymap + else tymap + in Just (tymap', varmap) + + (TApp a1 b1, TApp a2 b2) -> + do (tymap', varmap') <- f a1 a2 tymap varmap + f b1 b2 tymap' varmap' + + (TAbs a1 b1, TAbs a2 b2) -> + do (tymap', varmap') <- f a1 a2 tymap varmap + f b1 b2 tymap' varmap' + + (other, combination) -> Nothing) + + g = (\x y tymap varmap -> + let (hyp1,hyp2) = (Set.toList . thmHyp $ x, Set.toList . thmHyp $ y) + in if (hyp1 == [] && hyp2 == []) + then f (thmCon x) (thmCon y) tymap varmap + else do (tymap', varmap') <- f (head hyp1) (head hyp2) tymap varmap + g (Theorem (Set.fromList . tail $ hyp1) (thmCon x)) + (Theorem (Set.fromList . tail $ hyp2) (thmCon y)) + tymap' varmap') + + maps = g one two Map.empty Map.empty + + in if ((Set.size . thmHyp $ one) /= (Set.size . thmHyp $ two) || isNothing maps) + then Nothing + else do (t,v) <- maps + return (Map.toList t, Map.toList v) + + + +checkNode :: PGraph -> TermNet -> Node -> (TermNet, Maybe (GraphPart, GraphPart), Maybe (Node,Node)) +checkNode graph termnet node = + let theorem = TermNet.genThm graph node + possibles = TermNet.matchThm termnet theorem + + canBeSubbed = (\inn out -> + if (inn == []) + then out + else let sub = createSubst theorem (fst . head $ inn) + out' = if (isNothing sub) + then out + else (Step node (snd . head $ inn) (fromJust sub)) : out + in canBeSubbed (tail inn) out') + + maxPositiveBenefit = (\list -> + let sortVal = (\x -> let added = fst . snd $ x + removed = snd . snd $ x + inn = from . fst $ x + out = to . fst $ x + outNodes = map (\(x,(y,z)) -> (x,y)) (Graph.lpre graph out) + in (size removed) - (addedSize added (Just (inn,1)) outNodes graph) - (overlap added removed)) + sorted = sortBy (\x y -> compare (sortVal x) (sortVal y)) list + check = head sorted + in if (sortVal check > 0) then (Just (snd check), Just (from . fst $ check, to . fst $ check)) else (Nothing, Nothing)) + + (step, between) = maxPositiveBenefit . (map (\x -> (x, stepGen graph x))) $ (canBeSubbed possibles []) + termnet' = TermNet.addThm termnet theorem node + + in (termnet', step, between) + + + +stepGen :: PGraph -> Step -> (GraphPart, GraphPart) +stepGen graph step = + let unusedNodes = findUnused graph (Graph.suc graph (to step)) + unusedLabNodes = filter (\(x,y) -> x `elem` unusedNodes) (Graph.labNodes graph) + unused = graphPart unusedLabNodes [] Nothing Nothing + + base = doGraphGen (substitutionGen . sub $ step) + num = head (Graph.newNodes 1 base) + node = (num, "subst") + cons = head (filter (\x -> Graph.indeg base x == 0) (Graph.nodes base)) + edge = (num, cons, (2,1)) + + substGraph = (Graph.insEdge edge) . (Graph.insNode node) $ base + subst = makeGraphPart substGraph (Just (num,1)) (Just (num,1)) + + in (subst, unused) + + + +findUnused :: PGraph -> [Node] -> [Node] +findUnused graph nodeList = + let nextLayer = concat . (map (Graph.suc graph)) $ nodeList + unused = filter (\x -> all (\y -> y `elem` nodeList) (Graph.pre graph x)) nextLayer + in nodeList ++ (findUnused graph unused) + + + +doMeaningSubst :: PGraph -> PGraph +doMeaningSubst graph = + let f = (\g termnet nodeList -> + if (nodeList == []) + then g + else let working = head nodeList + (termnet', step, between) = checkNode g termnet working + (g', nodeList') = if (isNothing step || isNothing between) + then (g, nodeList) + else let (subst, unused) = fromJust step + (from, to) = fromJust between + toNodes = map (\(x,(y,z)) -> (x,y)) (Graph.lpre g to) + in ((graphAdd subst (Just (from, 1)) toNodes) . (graphDel unused) $ g, + nodeList \\ (map (\(x,y) -> x) (nodes unused))) + in f g' termnet' nodeList') + + in f graph TermNet.empty (Graph.nodes graph) + + + +main = do + args <- getArgs + list <- getLines (head args) + let graph = doGraphGen (map stripReturn list) + result = doMeaningSubst graph + printf $ (show result) ++ "\n" diff --git a/src/ProofGraphMain.hs b/src/ProofGraphMain.hs new file mode 100644 index 0000000..292cf01 --- /dev/null +++ b/src/ProofGraphMain.hs @@ -0,0 +1,11 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse +import Library.ProofGraph + + +main = do + args <- getArgs + list <- getLines (head args) + let result = doGraphGen (map (stripReturn) list) + printf $ (show result) ++ "\n" diff --git a/src/SemanticMain.hs b/src/SemanticMain.hs new file mode 100644 index 0000000..c07fc8c --- /dev/null +++ b/src/SemanticMain.hs @@ -0,0 +1,12 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse +import Library.Semantic + + + +main = do + args <- getArgs + list <- getLines (head args) + let result = doSemanticCheck (map (stripReturn) list) + printf result diff --git a/src/Syntactic.hs b/src/Syntactic.hs new file mode 100644 index 0000000..870cc35 --- /dev/null +++ b/src/Syntactic.hs @@ -0,0 +1,51 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse + + + +scan :: String -> String +scan s = if (s == "absTerm" || + s == "absThm" || + s == "appTerm" || + s == "appThm" || + s == "assume" || + s == "axiom" || + s == "betaConv" || + s == "cons" || + s == "const" || + s == "constTerm" || + s == "deductAntisym" || + s == "def" || + s == "defineConst" || + s == "defineTypeOp" || + s == "eqMp" || + s == "nil" || + s == "opType" || + s == "pop" || + s == "ref" || + s == "refl" || + s == "remove" || + s == "subst" || + s == "thm" || + s == "typeOp" || + s == "var" || + s == "varTerm" || + s == "varType" || + isComment(s) || + isNumber(s) || + isName(s)) + then s + else error $ "Invalid input " ++ s + + +doScan :: [String] -> [String] +doScan = map (scan . stripReturn) + + +main = do + args <- getArgs + list <- getLines (head args) + plist <- return $ doScan list + printf $ if (args == plist) then "Scan OK\n" else "Syntax error\n" + diff --git a/src/TermNetTest.hs b/src/TermNetTest.hs new file mode 100644 index 0000000..57eb06f --- /dev/null +++ b/src/TermNetTest.hs @@ -0,0 +1,26 @@ +import Library.Theorem +import Library.Term +import qualified Library.TermNet as Net +import Test.DataTypes +import qualified Data.Set as Set +import Data.List + + + +main = do + let thm1 = Theorem (Set.empty) stdConstTerm + thm2 = Theorem (Set.empty) (stdVarTerm "b") + thm3 = Theorem (Set.empty) (stdVarTerm "c") + thm4 = Theorem (Set.empty) (stdAbsTerm "h") + + net1 = Net.addThm Net.empty thm1 0 + net2 = Net.addThm net1 thm2 1 + net3 = Net.addThm net2 thm3 2 + net4 = Net.addThm net3 thm4 3 + + match = Net.matchThm net4 thm4 + + + putStrLn (show net4) + putStrLn "" + putStrLn (show match) diff --git a/src/Test.hs b/src/Test.hs new file mode 100644 index 0000000..47bba79 --- /dev/null +++ b/src/Test.hs @@ -0,0 +1,140 @@ +import Test.HUnit +import Library.Command +import Library.TypeVar +import Library.Term +import Library.Theorem +import Test.DataTypes +import qualified Data.Set as Set + + + +name1 = TestCase (assertEqual "for (name \"abc\")" + (Just (Name [] "abc")) + (name "\"abc\"")) + +name2 = TestCase (assertEqual "for (name \"first.second.third\")" + (Just (Name ["first","second"] "third")) + (name "\"first.second.third\"")) + +name3 = TestCase (assertEqual "for (name \"firs\\t.se\\cond.\\t\\h\\ird\")" + (Just (Name ["first","second"] "third")) + (name "\"firs\\t.se\\cond.\\t\\h\\ird\"")) + +name4 = TestCase (assertEqual "for (name abc)" Nothing (name "abc")) + + + +number1 = TestCase (assertEqual "for (number \"90\")" (Just 90) (number "90")) +number2 = TestCase (assertEqual "for (number \"0\")" (Just 0) (number "0")) +number3 = TestCase (assertEqual "for (number \"-1\")" (Just (-1)) (number "-1")) +number4 = TestCase (assertEqual "for (number \"-0\")" Nothing (number "-0")) +number5 = TestCase (assertEqual "for (number \"1.2\")" Nothing (number "1.2")) + + + +assume1 = TestCase (assertEqual "for (assume (TConst ...)" + (Just (Theorem (Set.singleton (TConst stdConst typeBool)) + (TConst stdConst typeBool))) + (assume (TConst stdConst typeBool))) + +assume2 = TestCase (assertEqual "for (assume (TConst ...) --with wrong type" + Nothing + (assume (TConst stdConst stdTypeVar))) + + + +axiom1 = TestCase (assertEqual "for (axiom (TConst ...) [])" + (Just (Theorem Set.empty (TConst stdConst stdTypeVar))) + (axiom (TConst stdConst stdTypeVar) [])) + +axiom2 = TestCase (assertEqual "for (axiom (TConst ...) [term1, term2] --term1 has wrong type" + Nothing + (axiom (TConst stdConst stdTypeVar) + [(TConst stdConst stdTypeVar),(TConst stdConst typeBool)])) + + + +alphaEquiv1 = TestCase (assertEqual "for ((\\xy -> x) `alphaEquiv` (\\yx -> x))" + False + (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))) + (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "x"))))) + +alphaEquiv2 = TestCase (assertEqual "for ((\\xy -> x) `alphaEquiv` (\\xy -> x))" + True + (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))) + (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))))) + +alphaEquiv3 = TestCase (assertEqual "for ((\\xyx -> x) `alphaEquiv` (\\yxx -> x))" + True + (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "x")))) + (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "x") (stdVarTerm "x")))))) + +alphaEquiv4 = TestCase (assertEqual "for ((\\xyz -> y) `alphaEquiv` (\\zyx -> y))" + True + (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "z") (stdVarTerm "y")))) + (TAbs (stdVarTerm "z") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "y")))))) + +alphaEquiv5 = TestCase (assertEqual "for ((\\x -> x) `alphaEquiv` (\\x -> x)) --x of lhs is different type to x of rhs" + False + (alphaEquiv (TAbs (stdVarTerm "x") (stdVarTerm "x")) + (TAbs (altVarTerm "x") (altVarTerm "x")))) + +alphaEquiv6 = TestCase (assertEqual "for ((TAbs ...) `alphaEquiv` (TConst ...))" + False + (alphaEquiv (TAbs (stdVarTerm "x") (stdVarTerm "x")) + (TConst stdConst typeBool))) + + + +substitute1 = TestCase (assertEqual "for (substitute ([],[(x',a)]) (TVar x'))" + (stdConstTerm) + (substitute ([],[((stdVar "x'"),stdConstTerm)]) (stdVarTerm "x'"))) + +substitute2 = TestCase (assertEqual "for (substitute ([],[(x',a)]) (TVar y'))" + (stdVarTerm "y'") + (substitute ([],[((stdVar "x'"),stdConstTerm)]) (stdVarTerm "y'"))) + +substitute3 = TestCase (assertEqual "for (substitute ([],[(x',a)]) (TApp (TVar x') (TVar x')))" + (TApp stdConstTerm stdConstTerm) + (substitute ([],[((stdVar "x'"),stdConstTerm)]) (TApp (stdVarTerm "x'") (stdVarTerm "x'")))) + +substitute4 = TestCase (assertEqual "for (substitute ([],[(x',a)]) (\\y' -> x'))" + (TAbs (stdVarTerm "y'") stdConstTerm) + (substitute ([],[((stdVar "x'"),stdConstTerm)]) (TAbs (stdVarTerm "y'") (stdVarTerm "x'")))) + +substitute5 = TestCase (assertEqual "for (substitute ([],[(x',y')]) (\\y' -> x'))" + (TAbs (stdVarTerm "y''") (stdVarTerm "y'")) + (substitute ([],[((stdVar "x'"),(stdVarTerm "y'"))]) (TAbs (stdVarTerm "y'") (stdVarTerm "x'")))) + +substitute6 = TestCase (assertEqual "for (substitute ([(tx',ta)],[]) (z' with typevar tx'))" + (TVar (Var (stdName "z'") stdType)) + (substitute ([(stdTypeVarName,stdType)],[]) (stdVarTerm "z'"))) + +substitute7 = TestCase (assertEqual "for (substitute ([(tx',ta)],[(y',b)]) (\\z' -> y')) --z' has type tx'" + (TAbs (TVar (Var (stdName "z'") stdType)) stdConstTerm) + (substitute ([(stdTypeVarName,stdType)],[((altVar "y'"),stdConstTerm)]) (TAbs (stdVarTerm "z'") (altVarTerm "y'")))) + +substitute8 = TestCase (assertEqual "for (substitute ([],[(x',y'),(y',z')]) (x'))" + (stdVarTerm "z'") + (substitute ([],[((stdVar "x'"),(stdVarTerm "y'")), + ((stdVar "y'"),(stdVarTerm "z'"))]) (stdVarTerm "x'"))) + +substitute9 = TestCase (assertEqual "for (substitute ([(tx',ty'),(ty',ta)],[]) (z' with typevar tx'))" + (TVar (Var (stdName "z'") stdType)) + (substitute ([(stdTypeVarName,altTypeVar),(altTypeVarName,stdType)],[]) (TVar (Var (stdName "z'") altTypeVar)))) + + +main = + do putStrLn "Command.name" + runTestTT $ TestList [name1,name2,name3,name4] + putStrLn "Command.number" + runTestTT $ TestList [number1,number2,number3,number4,number5] + putStrLn "Command.assume" + runTestTT $ TestList [assume1,assume2] + putStrLn "Command.axiom" + runTestTT $ TestList [axiom1,axiom2] + putStrLn "Term.alphaEquiv" + runTestTT $ TestList [alphaEquiv1,alphaEquiv2,alphaEquiv3,alphaEquiv4,alphaEquiv5,alphaEquiv6] + putStrLn "Term.substitute" + runTestTT $ TestList [substitute1,substitute2,substitute3,substitute4,substitute5,substitute6,substitute7,substitute8,substitute9] + diff --git a/src/Test/DataTypes.hs b/src/Test/DataTypes.hs new file mode 100644 index 0000000..28db135 --- /dev/null +++ b/src/Test/DataTypes.hs @@ -0,0 +1,68 @@ +module Test.DataTypes( + stdName, + stdType, + stdConst, + stdConstTerm, + stdTypeVarName, + altTypeVarName, + stdTypeVar, + altTypeVar, + stdVar, + stdVarTerm, + altVar, + altVarTerm, + stdAbsTerm, + stdAppTerm + ) where + + + +import Library.TypeVar +import Library.Term + + + +stdName :: String -> Name +stdName s = Name [] s + +stdType :: Type +stdType = AType [] (TypeOp (stdName "atype")) + +stdConst :: Const +stdConst = Const (stdName "const") + +stdConstTerm :: Term +stdConstTerm = TConst stdConst stdType + +stdTypeVarName :: Name +stdTypeVarName = stdName "typevar" + +altTypeVarName :: Name +altTypeVarName = stdName "alttypevar" + +stdTypeVar :: Type +stdTypeVar = TypeVar stdTypeVarName + +altTypeVar :: Type +altTypeVar = TypeVar altTypeVarName + +stdVar :: String -> Var +stdVar s = Var (stdName s) stdTypeVar + +stdVarTerm :: String -> Term +stdVarTerm s = TVar (stdVar s) + +altVar :: String -> Var +altVar s = Var (stdName s) altTypeVar + +altVarTerm :: String -> Term +altVarTerm s = TVar (altVar s) + +stdAbsTerm :: String -> Term +stdAbsTerm s = TAbs (stdVarTerm s) stdConstTerm + +stdAppTerm :: String -> Term +stdAppTerm s = TApp (stdAbsTerm s) stdConstTerm + + + diff --git a/src/WriteProofMain.hs b/src/WriteProofMain.hs new file mode 100644 index 0000000..2f8625e --- /dev/null +++ b/src/WriteProofMain.hs @@ -0,0 +1,15 @@ +import System.Environment( getArgs ) +import Text.Printf +import Library.Parse +import Library.ProofGraph +import Library.WriteProof + + + +main = do + args <- getArgs + list <- getLines (head args) + let graph = doGraphGen (map (stripReturn) list) + trace = doWriteProof graph + output trace + -- cgit