summaryrefslogtreecommitdiff
path: root/Library
diff options
context:
space:
mode:
Diffstat (limited to 'Library')
-rw-r--r--Library/Command.hs203
-rw-r--r--Library/Generator.hs82
-rw-r--r--Library/GraphPart.hs186
-rw-r--r--Library/Object.hs128
-rw-r--r--Library/Parse.hs77
-rw-r--r--Library/ProofGraph.hs116
-rw-r--r--Library/Semantic.hs358
-rw-r--r--Library/Stack.hs39
-rw-r--r--Library/Term.hs193
-rw-r--r--Library/TermNet.hs27
-rw-r--r--Library/Theorem.hs19
-rw-r--r--Library/TypeVar.hs77
-rw-r--r--Library/WriteProof.hs241
13 files changed, 1746 insertions, 0 deletions
diff --git a/Library/Command.hs b/Library/Command.hs
new file mode 100644
index 0000000..47f0537
--- /dev/null
+++ b/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/Library/Generator.hs b/Library/Generator.hs
new file mode 100644
index 0000000..ef9dfe2
--- /dev/null
+++ b/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/Library/GraphPart.hs b/Library/GraphPart.hs
new file mode 100644
index 0000000..c63c2eb
--- /dev/null
+++ b/Library/GraphPart.hs
@@ -0,0 +1,186 @@
+module Library.GraphPart (
+ graphPart,
+ makeGraphPart,
+
+ nodes,
+ edges,
+ inputNode,
+ outputNode,
+ inputLab,
+ outputLab,
+
+ graphAdd,
+ graphDel,
+ size,
+ addedSize,
+ overlap,
+ join,
+
+ checkDupe,
+ nodeEquals,
+ resolveNodeClash
+ ) 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
+
+
+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 :: Gr String (Int,Int) -> 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)
+
+
+
+graphAdd :: GraphPart -> Maybe (Node,Int) -> Maybe (Node,Int) -> Gr String (Int,Int) -> Gr String (Int,Int)
+graphAdd 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 (isNothing o || isNothing (getOutput gpart))
+ then inputAdded
+ else Graph.insEdge (fst . fromJust $ o,
+ fromJust (Map.lookup (fst . fromJust . getOutput $ gpart) dict),
+ (snd . fromJust $ o, snd . fromJust . getOutput $ gpart)) inputAdded
+
+ graph' = outputAdded
+
+ in checkDupe graph'
+
+
+
+graphDel :: GraphPart -> Gr String (Int,Int) -> Gr String (Int,Int)
+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) -> Maybe (Node,Int) -> Gr String (Int,Int) -> 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 addedSize = Graph.noNodes (graphAdd one Nothing Nothing (getGraph two))
+ totalSize = Graph.noNodes (getGraph one) + Graph.noNodes (getGraph two)
+ in totalSize - addedSize
+
+
+
+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)
+
+
+
+checkDupe :: Gr String (Int,Int) -> Gr String (Int,Int)
+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)
+
diff --git a/Library/Object.hs b/Library/Object.hs
new file mode 100644
index 0000000..9fc3b94
--- /dev/null
+++ b/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/Library/Parse.hs b/Library/Parse.hs
new file mode 100644
index 0000000..0e2aa25
--- /dev/null
+++ b/Library/Parse.hs
@@ -0,0 +1,77 @@
+module Library.Parse (
+ getLines,
+ stripReturn,
+ removeEscChars,
+ removeQuotes,
+ separateBy,
+ isComment,
+ isNumber,
+ isName,
+ output,
+ fst3,
+ snd3,
+ thd3
+ ) where
+
+import Control.Monad( liftM )
+import qualified Data.Char as Char
+
+
+getLines :: FilePath -> IO [String]
+getLines = liftM lines . readFile
+
+
+stripReturn :: String -> String
+stripReturn s = if (last s == '\r') then init s else s
+
+
+removeEscChars :: String -> String
+removeEscChars [] = []
+removeEscChars (x:[]) = [x]
+removeEscChars x = if (head x == '\\')
+ then (x!!1) : (removeEscChars . (drop 2) $ x)
+ else (head x) : (removeEscChars . tail $ x)
+
+
+removeQuotes :: String -> String
+removeQuotes = init . tail
+
+
+separateBy :: Char -> String -> [String]
+separateBy char list =
+ let f = (\x -> if (x == char)
+ then ' '
+ else x)
+ in words . (map f) $ list
+
+
+isComment :: String -> Bool
+isComment = (==) '#' . head
+
+
+isNumber :: String -> Bool
+isNumber ('0':[]) = True
+isNumber ('-':ns)
+ | (ns /= [] && head ns /= '0') = isNumber ns
+isNumber n = all (Char.isNumber) n
+
+
+isName :: String -> Bool
+isName s = all ((==) '"') [head s, last s]
+
+
+output :: [String] -> IO ()
+output [] = return ()
+output list = do
+ putStrLn (head list)
+ output (tail list)
+
+
+fst3 :: (a,b,c) -> a
+fst3 (a,_,_) = a
+
+snd3 :: (a,b,c) -> b
+snd3 (_,b,_) = b
+
+thd3 :: (a,b,c) -> c
+thd3 (_,_,c) = c
diff --git a/Library/ProofGraph.hs b/Library/ProofGraph.hs
new file mode 100644
index 0000000..f4d956f
--- /dev/null
+++ b/Library/ProofGraph.hs
@@ -0,0 +1,116 @@
+module Library.ProofGraph (
+ PGraph,
+ doGraphGen
+ ) 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( 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 )
+import Library.GraphPart( checkDupe )
+
+
+
+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)
+
+
+
+doGraphGen :: [String] -> PGraph
+doGraphGen list =
+ let graph = Graph.empty
+ stack = Stack.empty
+ dictionary = Map.empty
+ result = foldl' parse (graph,stack,dictionary) list
+ in case result of (g,s,d) -> checkDupe g
+
diff --git a/Library/Semantic.hs b/Library/Semantic.hs
new file mode 100644
index 0000000..eac00a3
--- /dev/null
+++ b/Library/Semantic.hs
@@ -0,0 +1,358 @@
+module Library.Semantic (
+ eval,
+ doSemanticCheck
+ ) where
+
+
+
+import Data.List
+import Data.Maybe
+import Data.Set( Set )
+import qualified Data.Set as Set
+import Data.Map( Map, (!) )
+import qualified Data.Map as Map
+import Library.TypeVar
+import Library.Term
+import Library.Theorem
+import Library.Object
+import Library.Parse
+import Library.Stack( Stack, at, (<:>) )
+import qualified Library.Stack as Stack
+import qualified Library.Command as Com
+
+
+
+type MachineState = Maybe (Stack Object,
+ Map Int Object, --dictionary
+ Set Theorem, --assumptions
+ Set Theorem) --theorems
+
+
+machineToString :: MachineState -> Maybe String
+machineToString x =
+ do (s,d,a,t) <- x
+ let s' = show s
+ d' = "Dictionary:\n" ++ intercalate "\n" (map (show) (Map.toList d)) ++ "\n\n"
+ a' = "Assumptions:\n" ++ intercalate "\n" (map (show) (Set.toList a)) ++ "\n\n"
+ t' = "Theorems:\n" ++ intercalate "\n" (map (show) (Set.toList t)) ++ "\n\n"
+ return (s' ++ d' ++ a' ++ t')
+
+
+data ArticleLine = Comment { commentString :: String }
+ | Command { commandFunc :: (MachineState -> MachineState) }
+
+
+
+parse :: String -> ArticleLine
+parse "absTerm" = Command absTerm
+parse "absThm" = Command absThm
+parse "appTerm" = Command appTerm
+parse "appThm" = Command appThm
+parse "assume" = Command assume
+parse "axiom" = Command axiom
+parse "betaConv" = Command betaConv
+parse "cons" = Command cons
+parse "const" = Command constant
+parse "constTerm" = Command constTerm
+parse "deductAntisym" = Command deductAntisym
+parse "def" = Command def
+parse "defineConst" = Command defineConst
+parse "defineTypeOp" = Command defineTypeOp
+parse "eqMp" = Command eqMp
+parse "nil" = Command nil
+parse "opType" = Command opType
+parse "pop" = Command pop
+parse "ref" = Command ref
+parse "refl" = Command refl
+parse "remove" = Command remove
+parse "subst" = Command subst
+parse "thm" = Command thm
+parse "typeOp" = Command typeOp
+parse "var" = Command var
+parse "varTerm" = Command varTerm
+parse "varType" = Command varType
+parse s@('#':rest) = Comment s
+parse s@('"':rest) = Command (name s)
+parse n = Command (number n)
+
+
+
+name :: String -> (MachineState -> MachineState)
+name str = \x ->
+ do (s,d,a,t) <- x
+ n <- Com.name str
+ let s' = (ObjName n) <:> s
+ return (s',d,a,t)
+
+
+number :: String -> (MachineState -> MachineState)
+number n = \x ->
+ do (s,d,a,t) <- x
+ num <- Com.number n
+ let s' = (ObjNum num) <:> s
+ return (s',d,a,t)
+
+
+absTerm :: MachineState -> MachineState
+absTerm x =
+ do (s,d,a,t) <- x
+ te <- (s `at` 0) >>= objTerm; v <- (s `at` 1) >>= objVar
+ let term = Com.absTerm te v
+ s' = (ObjTerm term) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+absThm :: MachineState -> MachineState
+absThm x =
+ do (s,d,a,t) <- x
+ th <- (s `at` 0) >>= objThm; v <- (s `at` 1) >>= objVar
+ thm <- Com.absThm th v
+ let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+appTerm :: MachineState -> MachineState
+appTerm x =
+ do (s,d,a,t) <- x
+ f <- (s `at` 0) >>= objTerm; x <- (s `at` 1) >>= objTerm
+ let term = Com.appTerm f x
+ s' = (ObjTerm term) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+appThm :: MachineState -> MachineState
+appThm x =
+ do (s,d,a,t) <- x
+ t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+ let thm = Com.appThm t1 t2
+ s' = (ObjThm thm) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+assume :: MachineState -> MachineState
+assume x =
+ do (s,d,a,t) <- x
+ te <- (s `at` 0) >>= objTerm
+ thm <- Com.assume te
+ let s' = (ObjThm thm) <:> (Stack.pop 1 s)
+ return (s',d,a,t)
+
+
+axiom :: MachineState -> MachineState
+axiom x =
+ do (s,d,a,t) <- x
+ te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList
+ thm <- Com.axiom te (mapMaybe objTerm l)
+ let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+ a' = Set.insert thm a
+ return (s',d,a',t)
+
+
+betaConv :: MachineState -> MachineState
+betaConv x =
+ do (s,d,a,t) <- x
+ te <- (s `at` 0) >>= objTerm
+ let thm = Com.betaConv te
+ s' = (ObjThm thm) <:> (Stack.pop 1 s)
+ return (s',d,a,t)
+
+
+cons :: MachineState -> MachineState
+cons x =
+ do (s,d,a,t) <- x
+ l <- (s `at` 0) >>= objList; h <- (s `at` 1)
+ let s' = (ObjList $ h : l) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+constant :: MachineState -> MachineState
+constant x =
+ do (s,d,a,t) <- x
+ n <- (s `at` 0) >>= objName
+ let constant = Com.constant n
+ s' = (ObjConst constant) <:> (Stack.pop 1 s)
+ return (s',d,a,t)
+
+
+constTerm :: MachineState -> MachineState
+constTerm x =
+ do (s,d,a,t) <- x
+ ty <- (s `at` 0) >>= objType; c <- (s `at` 1) >>= objConst
+ let term = Com.constTerm ty c
+ s' = (ObjTerm term) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+deductAntisym :: MachineState -> MachineState
+deductAntisym x =
+ do (s,d,a,t) <- x
+ t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+ let thm = Com.deductAntisym t1 t2
+ s' = (ObjThm thm) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+def :: MachineState -> MachineState
+def x =
+ do (s,d,a,t) <- x
+ num <- (s `at` 0) >>= objNum; obj <- (s `at` 1)
+ let d' = Map.insert num obj d
+ s' = Stack.pop 1 s
+ return (s',d',a,t)
+
+
+defineConst :: MachineState -> MachineState
+defineConst x =
+ do (s,d,a,t) <- x
+ te <- (s `at` 0) >>= objTerm; n <- (s `at` 1) >>= objName
+ (thm, constant) <- Com.defineConst te n
+ let s' = (ObjThm thm) <:> (ObjConst constant) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+defineTypeOp :: MachineState -> MachineState
+defineTypeOp x =
+ do (s,d,a,t) <- x
+ th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList; r <- (s `at` 2) >>= objName
+ ab <- (s `at` 3) >>= objName; y <- (s `at` 4) >>= objName
+ (rthm, athm, rep, abst, n) <- Com.defineTypeOp th (mapMaybe objName l) r ab y
+ let s' = (ObjThm rthm) <:> (ObjThm athm) <:> (ObjConst rep) <:> (ObjConst abst) <:> (ObjTyOp n) <:> (Stack.pop 5 s)
+ return (s',d,a,t)
+
+
+eqMp :: MachineState -> MachineState
+eqMp x =
+ do (s,d,a,t) <- x
+ t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+ thm <- Com.eqMp t1 t2
+ let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+nil :: MachineState -> MachineState
+nil x =
+ do (s,d,a,t) <- x
+ return (ObjList [] <:> s, d, a, t)
+
+
+opType :: MachineState -> MachineState
+opType x =
+ do (s,d,a,t) <- x
+ l <- (s `at` 0) >>= objList; to <- (s `at` 1) >>= objTyOp
+ let newType = Com.opType (mapMaybe objType l) to
+ s' = (ObjType newType) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+pop :: MachineState -> MachineState
+pop x =
+ do (s,d,a,t) <- x
+ return ((Stack.pop 1 s),d,a,t)
+
+
+ref :: MachineState -> MachineState
+ref x =
+ do (s,d,a,t) <- x
+ n <- (s `at` 0) >>= objNum
+ let object = d ! n
+ s' = object <:> (Stack.pop 1 s)
+ return (s',d,a,t)
+
+
+refl :: MachineState -> MachineState
+refl x =
+ do (s,d,a,t) <- x
+ te <- (s `at` 0) >>= objTerm
+ let thm = Com.refl te
+ s' = (ObjThm thm) <:> (Stack.pop 1 s)
+ return (s',d,a,t)
+
+
+remove :: MachineState -> MachineState
+remove x =
+ do (s,d,a,t) <- x
+ n <- (s `at` 0) >>= objNum
+ let object = d ! n
+ s' = object <:> (Stack.pop 1 s)
+ d' = Map.delete n d
+ return (s',d',a,t)
+
+
+subst :: MachineState -> MachineState
+subst x =
+ do (s,d,a,t) <- x
+ th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList
+ thm <- Com.subst th l
+ let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+thm :: MachineState -> MachineState
+thm x =
+ do (s,d,a,t) <- x
+ te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList; th <- (s `at` 2) >>= objThm
+ thm <- Com.thm te (mapMaybe objTerm l) th
+ let s' = Stack.pop 3 s
+ t' = Set.insert thm t
+ return (s',d,a,t')
+
+
+typeOp :: MachineState -> MachineState
+typeOp x =
+ do (s,d,a,t) <- x
+ n <- (s `at` 0) >>= objName
+ let typeOp = Com.typeOp n
+ s' = (ObjTyOp typeOp) <:> (Stack.pop 1 s)
+ return (s',d,a,t)
+
+
+var :: MachineState -> MachineState
+var x =
+ do (s,d,a,t) <- x
+ ty <- (s `at` 0) >>= objType; n <- (s `at` 1) >>= objName
+ v <- Com.var ty n
+ let s' = (ObjVar v) <:> (Stack.pop 2 s)
+ return (s',d,a,t)
+
+
+varTerm :: MachineState -> MachineState
+varTerm x =
+ do (s,d,a,t) <- x
+ v <- (s `at` 0) >>= objVar
+ let term = Com.varTerm v
+ s' = (ObjTerm term) <:> (Stack.pop 1 s)
+ return (s',d,a,t)
+
+
+varType :: MachineState -> MachineState
+varType x =
+ do (s,d,a,t) <- x
+ n <- (s `at` 0) >>= objName
+ newType <- Com.varType n
+ let s' = (ObjType newType) <:> (Stack.pop 1 s)
+ return (s',d,a,t)
+
+
+
+eval :: [String] -> MachineState
+eval list =
+ let s = Stack.empty
+ d = Map.empty
+ a = Set.empty
+ t = Set.empty
+ op = (\x y -> case y of (Comment _) -> x
+ (Command z) -> z x)
+
+ -- important to use foldl here so commands get applied in the correct order
+ result = (foldl' (op) (Just (s,d,a,t))) . (map (parse)) $ list
+
+ in result
+
+
+
+doSemanticCheck :: [String] -> String
+doSemanticCheck list =
+ case (machineToString (eval list)) of
+ Just x -> x
+ Nothing -> "Error\n"
+
diff --git a/Library/Stack.hs b/Library/Stack.hs
new file mode 100644
index 0000000..7292869
--- /dev/null
+++ b/Library/Stack.hs
@@ -0,0 +1,39 @@
+module Library.Stack (
+ Stack,
+ empty,
+ at,
+ pop,
+ (<:>)
+ ) where
+
+
+import Data.List
+
+
+data Stack a = Stack [a]
+
+
+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)
diff --git a/Library/Term.hs b/Library/Term.hs
new file mode 100644
index 0000000..029af7e
--- /dev/null
+++ b/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 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 a) = show a
+ 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) ->
+ type1 == type2 &&
+ 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 a1, TVar a2) ->
+ a1 == a2 && Map.notMember a1 varmap1 && Map.notMember a2 varmap2 ||
+ Map.lookup a1 varmap1 == Map.lookup a2 varmap2
+
+ (_,_) -> False
+ in equiv a b Map.empty Map.empty 0
+
+
+alphaConvert :: Term -> Term -> Term
+alphaConvert (TConst a ty) (TConst _ _) = TConst a ty
+alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2)
+alphaConvert (TVar v) (TVar _) = 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 (tymap,vmap) term =
+ let typesub =
+ (\x y ->
+ case y of
+ (TConst a ty) -> if (ty == (TypeVar . fst $ x))
+ then TConst a (snd x)
+ else TConst a ty
+ (TApp a b) -> TApp (typesub x a) (typesub x b)
+ (TAbs (TVar (Var n ty)) a) -> if (ty == (TypeVar . fst $ x))
+ then TAbs (TVar (Var n (snd x))) (typesub x a)
+ else TAbs (TVar (Var n ty)) (typesub x a)
+ (TVar (Var n ty)) -> if (ty == (TypeVar . fst $ x))
+ then TVar (Var n (snd x))
+ else TVar (Var n 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 (v == (fst x))
+ then snd x
+ else TVar v
+ (TAbs v a) -> let safe = rename (TAbs v a) (Set.insert (fst x) (freeVars . snd $ x))
+ in case safe of
+ (TAbs m n) -> TAbs m (varsub x n))
+ tydone = foldl' (\x y -> typesub y x) term tymap
+ vdone = foldl' (\x y -> varsub y x) tydone vmap
+ in vdone
+
+
+boundVars :: Term -> Set.Set Var
+boundVars (TConst a b) = Set.empty
+boundVars (TApp a b) = Set.union (boundVars a) (boundVars b)
+boundVars (TVar a) = Set.empty
+boundVars (TAbs a b) = Set.insert (tVar a) (boundVars b)
+
+
+freeVars :: Term -> Set.Set Var
+freeVars (TConst a b) = Set.empty
+freeVars (TApp a b) = Set.union (freeVars a) (freeVars b)
+freeVars (TVar a) = Set.singleton a
+freeVars (TAbs a b) = Set.delete (tVar a) (freeVars b)
+
+
+rename :: Term -> Set.Set Var -> Term
+rename (TAbs (TVar v) t) vars =
+ let doRename =
+ (\x y z -> case x of
+ (TAbs (TVar a) b) -> if (a == y)
+ then TAbs (TVar z) (doRename b y z)
+ else TAbs (TVar a) (doRename b y z)
+ (TConst a b) -> TConst a b
+ (TApp a b) -> TApp (doRename a y z) (doRename b y z)
+ (TVar a) -> if (a == y)
+ then TVar z
+ else TVar a)
+ findSafe =
+ (\x y -> if (Set.member x y)
+ then case x of
+ (Var a b) ->
+ case a of
+ (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y
+ else x)
+ in if (Set.member v vars)
+ then doRename (TAbs (TVar v) t) v (findSafe v vars)
+ else TAbs (TVar v) t
+
+
+typeOf :: Term -> Type
+typeOf (TConst _ ty) = ty
+typeOf (TVar v) = varTy v
+typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t)
+typeOf (TApp f _) =
+ -- type of f is of the form [[a,b], "->"]
+ last . aType . typeOf $ f
+
+
+typeVarsInTerm :: Term -> Set.Set Type
+typeVarsInTerm (TConst _ ty) = typeVarsInType ty
+typeVarsInTerm (TVar v) = typeVarsInType . varTy $ v
+typeVarsInTerm (TAbs v t) = Set.union (typeVarsInType . varTy . tVar $ v) (typeVarsInTerm t)
+typeVarsInTerm (TApp f x) = Set.union (typeVarsInTerm f) (typeVarsInTerm x)
+
+
+mkEquals :: Term -> Term -> Term
+mkEquals lhs rhs =
+ let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs))
+ in TApp (TApp eqConst lhs) rhs
+
+
+getlhs :: Term -> Term
+getlhs (TApp (TApp eq lhs) _)
+ | (isEq eq) = lhs
+
+
+getrhs :: Term -> Term
+getrhs (TApp (TApp eq _) rhs)
+ | (isEq eq) = rhs
+
+
+isEq :: Term -> Bool
+isEq (TConst (Const (Name [] "=")) _) = True
+isEq _ = False
diff --git a/Library/TermNet.hs b/Library/TermNet.hs
new file mode 100644
index 0000000..4d0b107
--- /dev/null
+++ b/Library/TermNet.hs
@@ -0,0 +1,27 @@
+module Library.TermNet(
+ TermNet,
+ empty,
+ addThm
+ ) where
+
+
+
+import Library.ProofGraph
+import Library.Object
+import Library.Theorem
+
+
+
+data TermNet = Empty | Leaf Object Node | Branch String [TermNet]
+
+
+
+empty :: TermNet
+empty = Empty
+
+
+
+addThm :: TermNet -> PGraph -> Node -> (TermNet, [(Theorem, Node)])
+addThm net graph node =
+
+
diff --git a/Library/Theorem.hs b/Library/Theorem.hs
new file mode 100644
index 0000000..fc66cc2
--- /dev/null
+++ b/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/Library/TypeVar.hs b/Library/TypeVar.hs
new file mode 100644
index 0000000..fbb06a6
--- /dev/null
+++ b/Library/TypeVar.hs
@@ -0,0 +1,77 @@
+module Library.TypeVar (
+ Number,
+
+ Name(..),
+
+ TypeOp(..),
+
+ Type(..),
+
+ Const(..),
+
+ Var(..),
+
+ mkEqualsType,
+ typeFunc,
+ typeBool,
+ typeVarsInType
+ ) where
+
+
+
+import Data.List
+import qualified Data.Set as Set
+
+
+
+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) = "typeVar " ++ (show tyVar)
+ 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
diff --git a/Library/WriteProof.hs b/Library/WriteProof.hs
new file mode 100644
index 0000000..0f4f80f
--- /dev/null
+++ b/Library/WriteProof.hs
@@ -0,0 +1,241 @@
+module Library.WriteProof (
+ write,
+ writeAll,
+ doWriteProof,
+ singleCommands,
+
+ ) 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.List
+import Library.Stack( Stack, at, (<:>) )
+import qualified Library.Stack as Stack
+import Library.Parse( isNumber, fst3, snd3, thd3 )
+
+
+
+output :: Gr String (Int,Int) -> Node -> Int
+output graph node =
+ let label = fromJust (Graph.lab graph node)
+ in case label of
+ "thm" -> 0
+ "pop" -> 0
+ "defineConst" -> 2
+ "defineTypeOp" -> 5
+ x -> 1
+
+
+
+reuse :: Gr String (Int,Int) -> Node -> Int
+reuse graph node =
+ let labels = map snd (Graph.lpre graph node)
+ f = (\x y -> length (filter (\z -> fst y == fst z) x))
+ reuseList = map (f labels) labels
+ in maximum reuseList
+
+
+
+cost :: Gr String (Int,Int) -> Node -> Int
+cost graph node =
+ length (subGraph graph node)
+
+
+
+next :: Int -> Gr String (Int,Int) -> [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 [])
+
+
+
+subGraph :: Gr a b -> Node -> [Node]
+subGraph graph node =
+ let sucList = nub (Graph.suc graph node)
+ in nub (node : (foldl' (++) [] (map (subGraph graph) sucList)))
+
+
+
+orderNodes :: Gr String (Int,Int) -> [Node] -> [Node]
+orderNodes graph nodeList = nodeList
+--placeholder
+
+
+
+removeOverlap :: Gr String (Int,Int) -> Node -> [Node] -> [Node]
+removeOverlap graph node list =
+ let nubFunc = (\x y -> (getArg graph node x) == (getArg graph node y))
+ in nubBy nubFunc list
+
+
+
+--rightmostEdge :: Gr String (Int,Int) -> LEdge (Int,Int) -> Bool
+--rightmostEdge graph edge =
+
+
+
+
+--crossEdge :: Gr String (Int,Int) -> LEdge (Int,Int) -> Bool
+
+
+
+--multiCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+--multiCommands graph nodeList =
+-- let trace = (\g n cn ca ->)
+--
+-- r = (\g n p -> let g' = if ((output g n) <= 1)
+-- then g
+-- else let (argToUseDict, (place, placeArg)) = trace g n n 1
+-- edgesToRemove =
+-- edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) g edgesToRemove
+-- defSubGraph =
+-- edgesToRef =
+-- new =
+-- refsToAdd =
+-- done = foldl' insertSubGraph edgesRemoved refsToAdd
+-- in done
+-- in f g' n)
+--
+-- f = (\g n -> let argList = (removeOverlap g) . reverse $ [1 .. (Graph.outdeg g n)]
+-- in foldl' (\x y -> r x (getArg x n y) n) g argList)
+--
+-- in foldl' f graph nodeList
+
+
+
+multiCommandsSimple :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+multiCommandsSimple graph nodeList =
+ let r = (\g n p -> let g' = if ((output g n) <= 1)
+ then g
+ else let ou = output g n
+ index = next ou g
+ new = Graph.newNodes (5 * ou + 2) g -- 3 for num/def/pop, 2 for num/ref, per output plus an extra num/ref
+ (defNew,refNew) = splitAt (3 * ou + 2) new
+
+ edgeCheck x y = compare (snd . thd3 $ x) (snd . thd3 $ y)
+
+ oldEdge = maximumBy edgeCheck (filter (\x -> fst3 x == p) (Graph.inn g n))
+ toConvert = delete oldEdge (Graph.inn g n)
+
+ defNodeGen = (\i j x lim -> if (x >= lim)
+ then []
+ else [(j!!(x*3), i!!x), (j!!(x*3+1), "def"),
+ (j!!(x*3+2), "pop")] ++ (defNodeGen i j (x+1) lim))
+ defNodes = (defNodeGen index defNew 0 ou) ++ [(defNew!!(3*ou), index!!((snd . thd3 $ oldEdge)-1)), (defNew!!(3*ou+1), "ref")]
+ defEdgeGen = (\x b -> let x' = [(fst b, fst . snd $ x, (1,1))] ++ (fst x)
+ in (x',b))
+ defEdges = [(p, (fst . last $ defNodes), thd3 oldEdge), ((fst . head $ defNodes), n, (1,1))] ++
+ (fst (foldl' defEdgeGen ([], head defNodes) (tail defNodes)))
+ defAdded = (Graph.insEdges defEdges) . (Graph.insNodes defNodes) . (Graph.delLEdge oldEdge) $ g
+
+ refGen = (\i lab -> [(i!!(2*(lab-1)), index!!(lab-1)), (i!!(2*(lab-1)+1), "ref")])
+ refNodes = map (refGen refNew) [1 .. (ou)]
+ refEdges = map (\[x,y] -> (fst y, fst x,(1,1))) refNodes
+ refAdded = (Graph.insEdges refEdges) . (Graph.insNodes (concat refNodes)) $ defAdded
+
+ convertEdge = (\g e -> let new = (fst3 e, fst . last $ (refNodes!!(snd . thd3 $ e)), thd3 e)
+ in (Graph.insEdge new) . (Graph.delLEdge e) $ g)
+
+ done = foldl' convertEdge refAdded toConvert
+ in done
+ in f g' n)
+
+ f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)]
+ in foldl' (\x y -> r x (getArg x n y) n) g argList)
+
+ in foldl' f graph nodeList
+
+
+
+singleCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+singleCommands graph nodeList =
+ let r = (\g n p -> let g' = if (((output g n) /= 1) || ((Graph.indeg g n) == 1) || ((cost g n) < 3) || ((cost g n) == 3 && (Graph.indeg g n) < 3))
+ then g
+ else let index = head (next 1 g)
+ new = Graph.newNodes 4 g -- 2 new nodes for def and 2 new nodes for ref
+
+ oldEdge = head $ (filter (\x -> fst3 x == p) (Graph.inn g n))
+ defNodes = [(new!!0, "def"), (new!!1, index)]
+ defEdges = [(p, fst (defNodes!!0), (fst . thd3 $ oldEdge, 1)),
+ (fst (defNodes!!0), fst (defNodes!!1), (1,1)),
+ (fst (defNodes!!1), n, (1,1))]
+ defAdded = (Graph.insEdges defEdges) . (Graph.insNodes defNodes) . (Graph.delLEdge oldEdge) $ g
+
+ refNodes = [(new!!2, "ref"), (new!!3, index)]
+ refEdge = (fst (refNodes!!0), fst (refNodes!!1), (1,1))
+ refAdded = (Graph.insEdge refEdge) . (Graph.insNodes refNodes) $ defAdded
+ convertEdge = (\g e -> let new = (fst3 e, fst (refNodes!!0), thd3 e)
+ in (Graph.insEdge new) . (Graph.delLEdge e) $ g)
+ done = foldl' convertEdge refAdded (filter (\x -> fst3 x /= fst (defNodes!!1)) (Graph.inn refAdded n))
+ in done
+ in f g' n)
+
+ f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)]
+ in foldl' (\x y -> r x (getArg x n y) n) g argList)
+
+ in foldl' f graph nodeList
+
+
+
+removeUnused :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+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 :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+resolve graph nodeList =
+ foldl' (\g f -> f g nodeList) graph [removeUnused, singleCommands, multiCommandsSimple]
+
+
+
+getArg :: Gr String (Int,Int) -> Node -> Int -> Node
+getArg graph node arg =
+ snd3 . head $ (filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node))
+
+
+
+writeGraph :: Gr String (Int,Int) -> Node -> [String]
+writeGraph graph node =
+ let label = fromJust (Graph.lab graph node)
+ argList = [1 .. (Graph.outdeg graph node)]
+ in foldl' (\s a -> (writeGraph graph (getArg graph node a)) ++ s) [label] argList
+
+
+
+write :: Gr String (Int,Int) -> Node -> [String]
+write graph node =
+ writeGraph (resolve graph [node]) node
+
+
+
+writeAll :: Gr String (Int,Int) -> [Node] -> [String]
+writeAll graph nodeList =
+ let ordered = orderNodes graph nodeList
+ graph' = resolve graph ordered
+ f = (\g n -> if (n == [])
+ then []
+ else (writeGraph g (head n)) ++ (f g (tail n)))
+ in f graph' ordered
+
+
+-- metric relates to minimum amount of work done not-on-top of the stack
+
+
+doWriteProof :: Gr String (Int,Int) -> [String]
+doWriteProof graph =
+ let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph)
+ in writeAll graph initList
+
generated by cgit (git 2.30.0) at 2024-12-22 23:36:43 +0000