summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Compare.hs43
-rw-r--r--src/Concat.hs16
-rw-r--r--src/Delete.hs20
-rw-r--r--src/GeneratorTest.hs10
-rw-r--r--src/Library/Command.hs203
-rw-r--r--src/Library/Cost.hs29
-rw-r--r--src/Library/Generator.hs82
-rw-r--r--src/Library/GraphPart.hs161
-rw-r--r--src/Library/Object.hs128
-rw-r--r--src/Library/Parse.hs75
-rw-r--r--src/Library/ProofGraph.hs159
-rw-r--r--src/Library/Semantic.hs360
-rw-r--r--src/Library/Stack.hs50
-rw-r--r--src/Library/Term.hs193
-rw-r--r--src/Library/TermNet.hs214
-rw-r--r--src/Library/Theorem.hs19
-rw-r--r--src/Library/TypeVar.hs99
-rw-r--r--src/Library/Usage.hs80
-rw-r--r--src/Library/WriteProof.hs211
-rw-r--r--src/Library/alternate_multi_command.hs315
-rw-r--r--src/ListThm.hs43
-rw-r--r--src/MeaningSubst.hs166
-rw-r--r--src/ProofGraphMain.hs11
-rw-r--r--src/SemanticMain.hs12
-rw-r--r--src/Syntactic.hs51
-rw-r--r--src/TermNetTest.hs26
-rw-r--r--src/Test.hs140
-rw-r--r--src/Test/DataTypes.hs68
-rw-r--r--src/WriteProofMain.hs15
29 files changed, 2999 insertions, 0 deletions
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
+
generated by cgit (git 2.30.0) at 2024-04-27 19:23:09 +0000