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 --- 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 ++ 29 files changed, 2999 insertions(+) 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 (limited to 'src') 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