From ea3f1f7736c57747e743a5106b917d2853c62f57 Mon Sep 17 00:00:00 2001
From: Jed Barber <jjbarber@y7mail.com>
Date: Thu, 13 Sep 2012 02:14:04 +1000
Subject: Cleaner directory structure, addition of make clean, grouping of
 library modules into a single package

---
 Library/Command.hs    | 203 ++++++++++++++++++++++++++++
 Library/Generator.hs  |  82 ++++++++++++
 Library/GraphPart.hs  | 186 ++++++++++++++++++++++++++
 Library/Object.hs     | 128 ++++++++++++++++++
 Library/Parse.hs      |  77 +++++++++++
 Library/ProofGraph.hs | 116 ++++++++++++++++
 Library/Semantic.hs   | 358 ++++++++++++++++++++++++++++++++++++++++++++++++++
 Library/Stack.hs      |  39 ++++++
 Library/Term.hs       | 193 +++++++++++++++++++++++++++
 Library/TermNet.hs    |  27 ++++
 Library/Theorem.hs    |  19 +++
 Library/TypeVar.hs    |  77 +++++++++++
 Library/WriteProof.hs | 241 +++++++++++++++++++++++++++++++++
 13 files changed, 1746 insertions(+)
 create mode 100644 Library/Command.hs
 create mode 100644 Library/Generator.hs
 create mode 100644 Library/GraphPart.hs
 create mode 100644 Library/Object.hs
 create mode 100644 Library/Parse.hs
 create mode 100644 Library/ProofGraph.hs
 create mode 100644 Library/Semantic.hs
 create mode 100644 Library/Stack.hs
 create mode 100644 Library/Term.hs
 create mode 100644 Library/TermNet.hs
 create mode 100644 Library/Theorem.hs
 create mode 100644 Library/TypeVar.hs
 create mode 100644 Library/WriteProof.hs

(limited to 'Library')

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
+
-- 
cgit