Reorganising source code

16 files changed, 2378 insertions, 0 deletions

diff --git a/src/Library/Command.hs b/src/Library/Command.hs
new file mode 100644
index 0000000..47f0537
--- /dev/null
+++ b/src/Library/Command.hs
@@ -0,0 +1,203 @@
+module Library.Command (
+	name,
+	number,
+	absTerm,
+	absThm,
+	appTerm,
+	appThm,
+	assume,
+	axiom,
+	betaConv,
+	constant,
+	constTerm,
+	deductAntisym,
+	defineConst,
+	defineTypeOp,
+	eqMp,
+	opType,
+	refl,
+	subst,
+	thm,
+	typeOp,
+	var,
+	varTerm,
+	varType
+    ) where
+
+-- deliberately not included:
+-- cons, nil, def, ref, remove, pop
+
+-- all functions here deal exclusively with arguments
+-- and results from/to the stack
+
+import Control.Monad
+import Data.List
+import Data.Maybe
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+import Library.TypeVar
+import Library.Term
+import Library.Theorem
+import Library.Object
+import Library.Parse
+
+
+name :: String -> Maybe Name
+name str =
+	do guard (isName str)
+	   let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str
+	   return (Name (init wordlist) (last wordlist))
+
+
+number :: String -> Maybe Number
+number num =
+	do guard (isNumber num)
+	   return (read num)
+
+
+absTerm :: Term -> Var -> Term
+absTerm term var =
+	TAbs (TVar var) term
+
+
+absThm :: Theorem -> Var -> Maybe Theorem
+absThm thm var =
+	do guard (not (Set.member (TVar var) (thmHyp thm)))
+	   return (Theorem (thmHyp thm) (mkEquals (TAbs (TVar var) (getlhs . thmCon $ thm))
+	   	                                      (TAbs (TVar var) (getrhs . thmCon $ thm))))
+
+
+appTerm :: Term -> Term -> Term
+appTerm term1 term2 =
+	TApp term2 term1
+
+
+appThm :: Theorem -> Theorem -> Theorem
+appThm thm1 thm2 =
+	Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
+	        (mkEquals (TApp (getlhs . thmCon $ thm2) (getlhs . thmCon $ thm1))
+                      (TApp (getrhs . thmCon $ thm2) (getrhs . thmCon $ thm1)))
+
+
+assume :: Term -> Maybe Theorem
+assume term =
+	do guard (typeOf term == typeBool)
+	   return (Theorem (Set.singleton term) term)
+
+
+axiom :: Term -> [Term] -> Maybe Theorem
+axiom term termlist =
+	do guard (all ((== typeBool) . typeOf) termlist)
+	   return (Theorem (Set.fromList termlist) term)
+
+
+betaConv :: Term -> Theorem
+betaConv term =
+	Theorem (Set.empty)
+            (mkEquals term
+                      (substitute ([], [(tVar . tAbsVar . tAppLeft $ term, tAppRight $ term)])
+                                  (tAbsTerm . tAppLeft $ term)))
+
+
+constant :: Name -> Const
+constant name =
+	Const name
+
+
+constTerm :: Type -> Const -> Term
+constTerm ty c =
+	TConst c ty
+
+
+deductAntisym :: Theorem -> Theorem -> Theorem
+deductAntisym x y =
+	Theorem (Set.union (Set.delete (thmCon $ x) (thmHyp $ y))
+                       (Set.delete (thmCon $ y) (thmHyp $ x)))
+            (mkEquals (thmCon $ y) (thmCon $ x))
+
+
+defineConst :: Term -> Name -> Maybe (Theorem, Const)
+defineConst term name =
+	do guard ((freeVars term == Set.empty) && (typeVarsInTerm term == typeVarsInType (typeOf term)))
+	   let constant = Const name
+	       constTerm = TConst constant (typeOf term)
+	       theorem = Theorem Set.empty (mkEquals constTerm term)
+	   return (theorem, constant)
+
+
+defineTypeOp :: Theorem -> [Name] -> Name -> Name -> Name -> Maybe (Theorem, Theorem, Const, Const, TypeOp)
+defineTypeOp thm namelist r a n =
+	do guard ((typeVarsInTerm . tAppLeft . thmCon $ thm) == (Set.fromList . map (TypeVar) $ namelist) &&
+		      (length namelist) == (length . nub $ namelist))
+	   let rep = Const r
+	       abst = Const a
+	       op = TypeOp n
+	       rtype = typeOf . tAppRight . thmCon $ thm
+	       atype = AType (map (TypeVar) namelist) op
+	       r' = TVar (Var (Name [] "r'") rtype)
+	       a' = TVar (Var (Name [] "a'") atype)
+	       reptype = typeFunc atype rtype
+	       abstype = typeFunc rtype atype
+	       repTerm = TConst rep reptype
+	       absTerm = TConst abst abstype
+	       rthm = Theorem Set.empty
+	                      (mkEquals (TApp (tAppLeft . thmCon $ thm) r')
+	                      	        (mkEquals (TApp repTerm (TApp absTerm r')) r'))
+	       athm = Theorem Set.empty
+	                      (mkEquals (TApp absTerm (TApp repTerm a')) a')
+	   return (rthm, athm, rep, abst, op)
+
+
+eqMp :: Theorem -> Theorem -> Maybe Theorem
+eqMp thm1 thm2 =
+	do guard (thmCon thm1 == (getlhs . thmCon $ thm2))
+	   return (Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
+	   	               (getrhs . thmCon $ thm2))
+
+
+opType :: [Type] -> TypeOp -> Type
+opType typelist tyOp =
+	AType typelist tyOp
+
+
+refl :: Term -> Theorem
+refl term =
+	Theorem Set.empty (mkEquals term term)
+
+
+subst :: Theorem -> [Object] -> Maybe Theorem
+subst thm list =
+	do s <- makeSubst list
+	   return (Theorem (Set.map (substitute s) (thmHyp thm))
+                       (substitute s (thmCon thm)))
+
+
+thm :: Term -> [Term] -> Theorem -> Maybe Theorem
+thm term termlist oldthm =
+	do guard ((term == thmCon oldthm) && (Set.fromList termlist == thmHyp oldthm))
+	   return (Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ oldthm) termlist))
+	   	               (alphaConvert (thmCon oldthm) term))
+
+
+typeOp :: Name -> TypeOp
+typeOp name =
+	TypeOp name
+
+
+var :: Type -> Name -> Maybe Var
+var ty name =
+    do guard ((nameSpace name) == [])
+       return (Var name ty)
+
+
+varTerm :: Var -> Term
+varTerm var =
+	TVar var
+
+
+varType :: Name -> Maybe Type
+varType name =
+    do guard ((nameSpace name) == [])
+       return (TypeVar name)
+
+
diff --git a/src/Library/Cost.hs b/src/Library/Cost.hs
new file mode 100644
index 0000000..86cabdc
--- /dev/null
+++ b/src/Library/Cost.hs
@@ -0,0 +1,29 @@
+module Library.Cost(
+	cost,
+	nodeCost,
+	listCost
+	) where
+
+
+
+import Data.Maybe
+import Data.Graph.Inductive.Graph( Node )
+import qualified Data.Graph.Inductive.Graph as Graph
+import Library.ProofGraph
+
+
+
+cost :: String -> Int
+cost x = 1
+
+
+nodeCost :: PGraph -> Node -> Int
+nodeCost graph node =
+	let label = fromJust (Graph.lab graph node)
+	    nextCostLayer = map (nodeCost graph) (Graph.suc graph node)
+	in (cost label) + (sum nextCostLayer)
+
+
+listCost :: [String] -> Int
+listCost = sum . (map cost)
+
diff --git a/src/Library/Generator.hs b/src/Library/Generator.hs
new file mode 100644
index 0000000..ef9dfe2
--- /dev/null
+++ b/src/Library/Generator.hs
@@ -0,0 +1,82 @@
+module Library.Generator (
+    listGen,
+    substitutionGen,
+    termGen,
+    varGen,
+    typeGen,
+    typeOpGen,
+    constGen,
+    nameGen
+    ) where
+
+
+import Data.List
+import Library.Term
+import Library.TypeVar
+
+
+
+listGen :: (a -> [String]) -> [a] -> [String]
+listGen f list =
+    concat (map f list) ++ ["nil"] ++ replicate (length list) "cons"
+
+
+
+substitutionGen :: Substitution -> [String]
+substitutionGen sub =
+    let varTermList = listGen varTermPair (snd sub)
+        nameTypeList = listGen nameTypePair (fst sub)
+    in nameTypeList ++ varTermList ++ ["nil", "cons", "cons"]
+
+
+
+varTermPair :: (Var, Term) -> [String]
+varTermPair (var, term) =
+    (varGen var) ++ (termGen term) ++ ["nil", "cons", "cons"]
+
+
+
+nameTypePair :: (Name, Type) -> [String]
+nameTypePair (name, ty) =
+    (nameGen name) ++ (typeGen ty) ++ ["nil", "cons", "cons"]
+
+
+
+termGen :: Term -> [String]
+termGen (TVar v) = (varGen v) ++ ["varTerm"]
+termGen (TConst c ty) = (constGen c) ++ (typeGen ty) ++ ["constTerm"]
+termGen (TApp h x) = (termGen h) ++ (termGen x) ++ ["appTerm"]
+termGen (TAbs x t) = (termGen x) ++ (termGen t) ++ ["absTerm"]
+
+
+
+varGen :: Var -> [String]
+varGen var =
+    (nameGen . varName $ var) ++ (typeGen . varTy $ var) ++ ["var"]
+
+
+
+typeGen :: Type -> [String]
+typeGen (TypeVar v) = (nameGen v) ++ ["varType"]
+typeGen (AType ty op) = 
+    let list = listGen typeGen ty
+    in (typeOpGen op) ++ list ++ ["opType"]
+
+
+
+typeOpGen :: TypeOp -> [String]
+typeOpGen op = 
+    (nameGen . tyOp $ op) ++ ["typeOp"]
+
+
+
+constGen :: Const -> [String]
+constGen c =
+    (nameGen . constName $ c) ++ ["const"]
+
+
+
+nameGen :: Name -> [String]
+nameGen name =
+    ["\"" ++ intercalate "." (nameSpace name ++ [nameId name]) ++ "\""]
+
diff --git a/src/Library/GraphPart.hs b/src/Library/GraphPart.hs
new file mode 100644
index 0000000..02a95c0
--- /dev/null
+++ b/src/Library/GraphPart.hs
@@ -0,0 +1,161 @@
+module Library.GraphPart (
+	GraphPart,
+	
+	graphPart,
+	makeGraphPart,
+
+	nodes,
+	edges,
+	inputNode,
+	outputNode,
+	inputLab,
+	outputLab,
+
+	graphAdd,
+	graphAddList,
+	graphDel,
+	size,
+	addedSize,
+	overlap,
+	join
+    ) where
+
+
+
+import Data.Maybe
+import Data.List
+import Data.Map( Map )
+import qualified Data.Map as Map
+import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge )
+import qualified Data.Graph.Inductive.Graph as Graph
+import Data.Graph.Inductive.Tree
+import Library.ProofGraph
+
+
+data GraphPart = GraphPart { getGraph :: Gr String (Int,Int)
+                           , getInput :: Maybe (Node,Int)
+                           , getOutput :: Maybe (Node,Int) }
+
+
+graphPart :: [LNode String] -> [LEdge (Int,Int)] -> Maybe (Node,Int) -> Maybe (Node,Int) -> GraphPart
+graphPart nodes edges =
+	let graph = checkDupe (Graph.mkGraph nodes edges)
+	in GraphPart graph
+
+
+makeGraphPart :: PGraph -> Maybe (Node,Int) -> Maybe (Node,Int) -> GraphPart
+makeGraphPart = GraphPart
+
+
+nodes :: GraphPart -> [LNode String]
+nodes = Graph.labNodes . getGraph
+
+
+edges :: GraphPart -> [LEdge (Int,Int)]
+edges = Graph.labEdges . getGraph
+
+
+inputNode :: GraphPart -> Maybe Node
+inputNode gpart = do
+	input <- getInput gpart
+	return (fst input)
+
+
+outputNode :: GraphPart -> Maybe Node
+outputNode gpart = do
+	output <- getOutput gpart
+	return (fst output)
+
+
+inputLab :: GraphPart -> Maybe Int
+inputLab gpart = do
+	input <- getInput gpart
+	return (snd input)
+
+
+outputLab :: GraphPart -> Maybe Int
+outputLab gpart = do
+	output <- getOutput gpart
+	return (snd output)
+
+
+
+graphAddImp :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph
+graphAddImp gpart i o graph =
+	let (resolved, dict) = resolveNodeClash graph (getGraph gpart)
+	    base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) $ graph
+
+	    inputAdded = if (isNothing i || isNothing (getInput gpart))
+	    	         then base
+	    	         else Graph.insEdge (fromJust (Map.lookup (fst . fromJust . getInput $ gpart) dict),
+	    	         	                 fst . fromJust $ i,
+	    	         	                 (snd . fromJust . getInput $ gpart, snd . fromJust $ i)) base
+
+	    outputAdded = if (o == [] || isNothing (getOutput gpart))
+	    	          then inputAdded
+	    	          else let outEdge = map (\(x,y) -> (x, fromJust (Map.lookup (fst . fromJust . getOutput $ gpart) dict),
+	    	          	                                    (y, snd . fromJust . getOutput $ gpart))) o
+	    	               in Graph.insEdges outEdge inputAdded
+
+	    graph' = outputAdded
+	in graph'
+
+
+
+graphAdd :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph
+graphAdd gpart i o graph =
+	let graph' = graphAddImp gpart i o graph
+	in checkDupe graph'
+
+
+
+graphAddList :: [(GraphPart, Maybe (Node,Int), [(Node,Int)])] -> PGraph -> PGraph
+graphAddList partList graph =
+	let graph' = foldl' (\g (x,y,z) -> graphAddImp x y z g) graph partList
+	in checkDupe graph'
+
+
+
+graphDel :: GraphPart -> PGraph -> PGraph
+graphDel gpart graph =
+	let n = map fst . nodes $ gpart
+	    e = map (\(a,b,_) -> (a,b)) . edges $ gpart
+	in (Graph.delNodes n) . (Graph.delEdges e) $ graph
+
+
+
+size :: GraphPart -> Int
+size = Graph.noNodes . getGraph
+
+
+
+addedSize :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> Int
+addedSize gpart i o graph =
+	let oldSize = Graph.noNodes graph
+	    newSize = Graph.noNodes (graphAdd gpart i o graph)
+	in newSize - oldSize
+
+
+
+overlap :: GraphPart -> GraphPart -> Int
+overlap one two =
+	let added = Graph.noNodes (graphAdd one Nothing [] (getGraph two))
+	    total = Graph.noNodes (getGraph one) + Graph.noNodes (getGraph two)
+	in total - added
+
+
+
+join :: GraphPart -> GraphPart -> GraphPart
+join one two | (isJust (getOutput one) && isJust (getInput two)) =
+	let (resolved, dict) = resolveNodeClash (getGraph one) (getGraph two)
+	    base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) . getGraph $ one
+
+	    from = (\(x,y) -> (fromJust (Map.lookup x dict), y)) . fromJust . getInput $ two
+	    to = fromJust . getOutput $ one
+	    ioEdge = (fst from, fst to, (snd from, snd to))
+
+	    newOutput = (\(x,y) -> (fromJust (Map.lookup x dict), y)) . fromJust . getOutput $ two
+
+	in makeGraphPart (checkDupe (Graph.insEdge ioEdge base)) (getInput one) (Just newOutput)
+
+
diff --git a/src/Library/Object.hs b/src/Library/Object.hs
new file mode 100644
index 0000000..dd65ded
--- /dev/null
+++ b/src/Library/Object.hs
@@ -0,0 +1,128 @@
+module Library.Object (
+	Object(..),
+    objNum,
+    objName,
+    objList,
+    objTyOp,
+    objType,
+    objConst,
+    objVar,
+    objTerm,
+    objThm,
+
+	List,
+
+    makeSubst
+	) where
+
+
+
+import Data.Maybe
+import Data.List
+import Library.TypeVar
+import Library.Term
+import Library.Theorem
+
+
+
+data Object = ObjNum Number
+            | ObjName Name
+            | ObjList List
+            | ObjTyOp TypeOp
+            | ObjType Type
+            | ObjConst Const
+            | ObjVar Var
+            | ObjTerm Term
+            | ObjThm Theorem deriving (Eq, Ord)
+
+type List = [Object]
+
+
+
+instance Show Object where
+    show (ObjNum a)    =   show a
+    show (ObjName a)   =   show a
+    show (ObjList a)   =   show a
+    show (ObjTyOp a)   =   show a
+    show (ObjType a)   =   show a
+    show (ObjConst a)  =   show a
+    show (ObjVar a)    =   show a
+    show (ObjTerm a)   =   show a
+    show (ObjThm a)    =   show a
+
+
+
+makeSubst :: [Object] -> Maybe Substitution
+makeSubst l =
+    let list = (map (mapMaybe objList)) . (mapMaybe objList) $ l
+        f g h x = (g . head $ x, h . last $ x)
+        check = f (map (f objName objType)) (map (f objVar objTerm)) list
+        g = all (\x -> (isJust . fst $ x) && (isJust . snd $ x))
+        h x = (fromJust . fst $ x, fromJust . snd $ x)
+    in if ((g . fst $ check) && (g . snd $ check))
+       then Just (map h (fst check), map h (snd check))
+       else Nothing
+
+
+objNum :: Object -> Maybe Number
+objNum obj =
+    case (obj) of
+        (ObjNum n) -> Just n
+        (_) -> Nothing
+
+
+objName :: Object -> Maybe Name
+objName obj =
+    case (obj) of
+        (ObjName n) -> Just n
+        (_) -> Nothing
+
+
+objList :: Object -> Maybe List
+objList obj =
+    case (obj) of
+        (ObjList l) -> Just l
+        (_) -> Nothing
+
+
+objTyOp :: Object -> Maybe TypeOp
+objTyOp obj =
+    case (obj) of
+        (ObjTyOp tyop) -> Just tyop
+        (_) -> Nothing
+
+
+objType :: Object -> Maybe Type
+objType obj =
+    case (obj) of
+        (ObjType ty) -> Just ty
+        (_) -> Nothing
+
+
+objConst :: Object -> Maybe Const
+objConst obj =
+    case (obj) of
+        (ObjConst c) -> Just c
+        (_) -> Nothing
+
+
+objVar :: Object -> Maybe Var
+objVar obj =
+    case (obj) of
+        (ObjVar var) -> Just var
+        (_) -> Nothing
+
+
+objTerm :: Object -> Maybe Term
+objTerm obj =
+    case (obj) of
+        (ObjTerm term) -> Just term
+        (_) -> Nothing
+
+
+objThm :: Object -> Maybe Theorem
+objThm obj =
+    case (obj) of
+        (ObjThm thm) -> Just thm
+        (_) -> Nothing
+
diff --git a/src/Library/Parse.hs b/src/Library/Parse.hs
new file mode 100644
index 0000000..7494822
--- /dev/null
+++ b/src/Library/Parse.hs
@@ -0,0 +1,75 @@
+module Library.Parse (
+	getLines,
+	stripReturn,
+	removeEscChars,
+	removeQuotes,
+	separateBy,
+	isComment,
+	isNumber,
+	isName,
+	output,
+	fst3,
+	snd3,
+	thd3
+	) where
+
+import Control.Monad( liftM )
+import qualified Data.Char as Char
+
+
+getLines :: FilePath -> IO [String]
+getLines = liftM lines . readFile
+
+
+stripReturn :: String -> String
+stripReturn s = if (last s == '\r') then init s else s
+
+
+removeEscChars :: String -> String
+removeEscChars [] = []
+removeEscChars (x:[]) = [x]
+removeEscChars x = if (head x == '\\')
+                   then (x!!1) : (removeEscChars . (drop 2) $ x)
+                   else (head x) : (removeEscChars . tail $ x)
+
+
+removeQuotes :: String -> String
+removeQuotes = init . tail
+
+
+separateBy :: Char -> String -> [String]
+separateBy char list =
+	let f x = if (x == char) then ' ' else x
+	in words . (map f) $ list
+
+
+isComment :: String -> Bool
+isComment = (==) '#' . head
+
+
+isNumber :: String -> Bool
+isNumber ('0':[]) = True
+isNumber ('-':ns)
+         | (ns /= [] && head ns /= '0') = isNumber ns
+isNumber n = all (Char.isNumber) n
+
+
+isName :: String -> Bool
+isName s = all ((==) '"') [head s, last s]
+
+
+output :: [String] -> IO ()
+output [] = return ()
+output list = do
+	putStrLn (head list)
+	output (tail list)
+
+
+fst3 :: (a,b,c) -> a
+fst3 (a,_,_) = a
+
+snd3 :: (a,b,c) -> b
+snd3 (_,b,_) = b
+
+thd3 :: (a,b,c) -> c
+thd3 (_,_,c) = c
diff --git a/src/Library/ProofGraph.hs b/src/Library/ProofGraph.hs
new file mode 100644
index 0000000..0e7e80a
--- /dev/null
+++ b/src/Library/ProofGraph.hs
@@ -0,0 +1,159 @@
+module Library.ProofGraph (
+    PGraph,
+    doGraphGen,
+
+    checkDupe,
+    nodeEquals,
+    resolveNodeClash,
+
+    argMap
+    ) where
+
+
+
+import Data.Maybe
+import Data.List
+import Data.Set( Set )
+import qualified Data.Set as Set
+import Data.Map( Map, (!) )
+import qualified Data.Map as Map
+
+import Data.Graph.Inductive.Graph( Node, LNode, LEdge, (&) )
+import qualified Data.Graph.Inductive.Graph as Graph
+import Data.Graph.Inductive.Tree
+
+import Library.Stack( Stack, at, (<:>) )
+import qualified Library.Stack as Stack
+import Library.Parse( isNumber, isName )
+
+
+
+type PGraph = Gr String (Int,Int)
+type PStack = Stack (Int, LNode String)
+type PMap = Map Int (Int, LNode String)
+
+
+data CommandIO = IO { args :: Int
+                    , results :: Int }
+
+
+argMap :: String -> CommandIO
+argMap "absTerm" = IO 2 1
+argMap "absThm" = IO 2 1
+argMap "appTerm" = IO 2 1
+argMap "appThm" = IO 2 1
+argMap "assume" = IO 1 1
+argMap "axiom" = IO 2 1
+argMap "betaConv" = IO 1 1
+argMap "cons" = IO 2 1
+argMap "const" = IO 1 1
+argMap "constTerm" = IO 2 1
+argMap "deductAntisym" = IO 2 1
+argMap "defineConst" = IO 2 2
+argMap "defineTypeOp" = IO 5 5
+argMap "eqMp" = IO 2 1
+argMap "nil" = IO 0 1
+argMap "opType" = IO 2 1
+argMap "refl" = IO 1 1
+argMap "subst" = IO 2 1
+argMap "thm" = IO 3 0
+argMap "typeOp" = IO 1 1
+argMap "var" = IO 2 1
+argMap "varTerm" = IO 1 1
+argMap "varType" = IO 1 1
+argMap x | (isName x) = IO 0 1
+
+
+
+process :: String -> CommandIO -> PGraph -> PStack -> (PGraph, PStack)
+process str io graph stack =
+    let argList = map (\x -> fromJust (stack `at` x)) [0..((args io) - 1)]
+        nextNum = head (Graph.newNodes 1 graph)
+        node = (nextNum, str)
+        edgeList = map (\x -> (nextNum, (fst . snd . snd $ x), (fst x, fst . snd $ x))) (zip [1..(args io)] argList)
+        graph' = (Graph.insEdges edgeList) . (Graph.insNode node) $ graph
+        nodeList = map (\x -> (x, node)) [1..(results io)]
+        stack' = foldr (<:>) (Stack.pop (args io) stack) nodeList
+    in (graph', stack')
+
+
+
+parse :: (PGraph,PStack,PMap) -> String -> (PGraph,PStack,PMap)
+parse gs@(graph,stack,dictionary) str =
+    case str of
+        "def" -> let num = fst . fromJust $ stack `at` 0
+                     node = fromJust $ stack `at` 1
+                     dictionary' = Map.insert num node dictionary
+                     stack' = Stack.pop 1 stack
+                 in (graph, stack', dictionary')
+
+        "ref" -> let num = fst . fromJust $ stack `at` 0
+                     node = fromJust (Map.lookup num dictionary)
+                     stack' = node <:> (Stack.pop 1 stack)
+                 in (graph, stack', dictionary)
+
+        "remove" -> let num = fst . fromJust $ stack `at` 0
+                        node = fromJust (Map.lookup num dictionary)
+                        stack' = node <:> (Stack.pop 1 stack)
+                        dictionary' = Map.delete num dictionary
+                    in (graph, stack', dictionary')
+
+        "pop" -> (graph, (Stack.pop 1 stack), dictionary)
+
+        '#':rest -> gs
+
+        n | (isNumber n) -> let node = (read n, (0,""))
+                                stack' = node <:> stack
+                            in (graph, stack', dictionary)
+
+        x -> let (graph', stack') = process x (argMap x) graph stack
+             in (graph', stack', dictionary)
+
+
+
+checkDupe :: PGraph -> PGraph
+checkDupe graph =
+    let f g n = let list = filter (\x -> (x /= n) && (nodeEquals g n x)) (Graph.nodes g)
+                in if (list == []) then g else merge g n (head list)
+
+        merge g n r = 
+                let edgesFixed = map (\(a,b,c) -> (a,r,c)) (Graph.inn g n)
+                in (Graph.insEdges edgesFixed) . (Graph.delNode n) $ g
+
+    in foldl' f graph (Graph.nodes graph)
+
+
+
+nodeEquals :: Gr String (Int,Int) -> Node -> Node -> Bool
+nodeEquals graph one two =
+    let edgesOne = sortBy sortFunc (Graph.out graph one)
+        edgesTwo = sortBy sortFunc (Graph.out graph two)
+        sortFunc = (\(_,_,x) (_,_,y) -> compare x y)
+        paired = zip (map (\(_,x,_) -> x) edgesOne) (map (\(_,x,_) -> x) edgesTwo)
+
+    in (Graph.gelem one graph) &&
+       (Graph.gelem two graph) &&
+       (Graph.lab graph one == Graph.lab graph two) &&
+       (length edgesOne == length edgesTwo) &&
+       (all (\x -> nodeEquals graph (fst x) (snd x)) paired)
+
+
+
+resolveNodeClash :: Gr String (Int,Int) -> Gr String (Int,Int) -> (Gr String (Int,Int), Map Int Int)
+resolveNodeClash ref graph =
+    let dict = Map.fromList (zip (Graph.nodes graph) (Graph.newNodes (Graph.noNodes graph) ref))
+        nodeList = map (\(x,y) -> (fromJust (Map.lookup x dict), y)) (Graph.labNodes graph)
+        edgeList = map (\(x,y,z) -> (fromJust (Map.lookup x dict),
+                                     fromJust (Map.lookup y dict), z)) (Graph.labEdges graph)
+    in (Graph.mkGraph nodeList edgeList, dict)
+
+
+
+doGraphGen :: [String] -> PGraph
+doGraphGen list =
+    let graph = Graph.empty
+        stack = Stack.empty
+        dictionary = Map.empty
+        result = foldl' parse (graph,stack,dictionary) list
+    in case result of (g,s,d) -> checkDupe g
+
diff --git a/src/Library/Semantic.hs b/src/Library/Semantic.hs
new file mode 100644
index 0000000..0f08d52
--- /dev/null
+++ b/src/Library/Semantic.hs
@@ -0,0 +1,360 @@
+module Library.Semantic (
+    MachineState,
+    machineToString,
+    eval,
+    doSemanticCheck
+    ) where
+
+
+
+import Data.List
+import Data.Maybe
+import Data.Set( Set )
+import qualified Data.Set as Set
+import Data.Map( Map, (!) )
+import qualified Data.Map as Map
+import Library.TypeVar
+import Library.Term
+import Library.Theorem
+import Library.Object
+import Library.Parse
+import Library.Stack( Stack, at, (<:>) )
+import qualified Library.Stack as Stack
+import qualified Library.Command as Com
+
+
+
+type MachineState = Maybe (Stack Object,
+                           Map Int Object, --dictionary
+                           Set Theorem, --assumptions
+                           Set Theorem) --theorems
+
+
+machineToString :: MachineState -> Maybe String
+machineToString x =
+    do (s,d,a,t) <- x
+       let s' = show s
+           d' = "Dictionary:\n" ++ intercalate "\n" (map (show) (Map.toList d)) ++ "\n\n"
+           a' = "Assumptions:\n" ++ intercalate "\n" (map (show) (Set.toList a)) ++ "\n\n"
+           t' = "Theorems:\n" ++ intercalate "\n" (map (show) (Set.toList t)) ++ "\n\n"
+       return (s' ++ d' ++ a' ++ t')
+
+
+data ArticleLine = Comment { commentString :: String }
+                 | Command { commandFunc :: (MachineState -> MachineState) }
+
+
+
+parse :: String -> ArticleLine
+parse "absTerm" = Command absTerm
+parse "absThm" = Command absThm
+parse "appTerm" = Command appTerm
+parse "appThm" = Command appThm
+parse "assume" = Command assume
+parse "axiom" = Command axiom
+parse "betaConv" = Command betaConv
+parse "cons" = Command cons
+parse "const" = Command constant
+parse "constTerm" = Command constTerm
+parse "deductAntisym" = Command deductAntisym
+parse "def" = Command def
+parse "defineConst" = Command defineConst
+parse "defineTypeOp" = Command defineTypeOp
+parse "eqMp" = Command eqMp
+parse "nil" = Command nil
+parse "opType" = Command opType
+parse "pop" = Command pop
+parse "ref" = Command ref
+parse "refl" = Command refl
+parse "remove" = Command remove
+parse "subst" = Command subst
+parse "thm" = Command thm
+parse "typeOp" = Command typeOp
+parse "var" = Command var
+parse "varTerm" = Command varTerm
+parse "varType" = Command varType
+parse s@('#':rest) = Comment s
+parse s@('"':rest) = Command (name s)
+parse n = Command (number n)
+
+
+
+name :: String -> (MachineState -> MachineState)
+name str x =
+    do (s,d,a,t) <- x
+       n <- Com.name str
+       let s' = (ObjName n) <:> s
+       return (s',d,a,t)
+
+
+number :: String -> (MachineState -> MachineState)
+number n x =
+    do (s,d,a,t) <- x
+       num <- Com.number n
+       let s' = (ObjNum num) <:> s
+       return (s',d,a,t)
+
+
+absTerm :: MachineState -> MachineState
+absTerm x =
+    do (s,d,a,t) <- x
+       te <- (s `at` 0) >>= objTerm; v <- (s `at` 1) >>= objVar
+       let term = Com.absTerm te v
+           s' = (ObjTerm term) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+absThm :: MachineState -> MachineState
+absThm x =
+    do (s,d,a,t) <- x
+       th <- (s `at` 0) >>= objThm; v <- (s `at` 1) >>= objVar
+       thm <- Com.absThm th v
+       let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+appTerm :: MachineState -> MachineState
+appTerm x =
+    do (s,d,a,t) <- x
+       f <- (s `at` 0) >>= objTerm; x <- (s `at` 1) >>= objTerm
+       let term = Com.appTerm f x
+           s' = (ObjTerm term) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+appThm :: MachineState -> MachineState
+appThm x =
+    do (s,d,a,t) <- x
+       t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+       let thm = Com.appThm t1 t2
+           s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+assume :: MachineState -> MachineState
+assume x =
+    do (s,d,a,t) <- x
+       te <- (s `at` 0) >>= objTerm
+       thm <- Com.assume te
+       let s' = (ObjThm thm) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
+
+
+axiom :: MachineState -> MachineState
+axiom x =
+    do (s,d,a,t) <- x
+       te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList
+       thm <- Com.axiom te (mapMaybe objTerm l)
+       let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+           a' = Set.insert thm a
+       return (s',d,a',t)
+
+
+betaConv :: MachineState -> MachineState
+betaConv x =
+    do (s,d,a,t) <- x
+       te <- (s `at` 0) >>= objTerm
+       let thm = Com.betaConv te
+           s' = (ObjThm thm) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
+
+
+cons :: MachineState -> MachineState
+cons x =
+    do (s,d,a,t) <- x
+       l <- (s `at` 0) >>= objList; h <- (s `at` 1)
+       let s' = (ObjList $ h : l) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+constant :: MachineState -> MachineState
+constant x =
+    do (s,d,a,t) <- x
+       n <- (s `at` 0) >>= objName
+       let constant = Com.constant n
+           s' = (ObjConst constant) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
+
+
+constTerm :: MachineState -> MachineState
+constTerm x =
+    do (s,d,a,t) <- x
+       ty <- (s `at` 0) >>= objType; c <- (s `at` 1) >>= objConst
+       let term = Com.constTerm ty c
+           s' = (ObjTerm term) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+deductAntisym :: MachineState -> MachineState
+deductAntisym x =
+    do (s,d,a,t) <- x
+       t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+       let thm = Com.deductAntisym t1 t2
+           s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+def :: MachineState -> MachineState
+def x =
+    do (s,d,a,t) <- x
+       num <- (s `at` 0) >>= objNum; obj <- (s `at` 1)
+       let d' = Map.insert num obj d
+           s' = Stack.pop 1 s
+       return (s',d',a,t)
+
+
+defineConst :: MachineState -> MachineState
+defineConst x =
+    do (s,d,a,t) <- x
+       te <- (s `at` 0) >>= objTerm; n <- (s `at` 1) >>= objName
+       (thm, constant) <- Com.defineConst te n
+       let s' = (ObjThm thm) <:> (ObjConst constant) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+defineTypeOp :: MachineState -> MachineState
+defineTypeOp x =
+    do (s,d,a,t) <- x
+       th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList; r <- (s `at` 2) >>= objName
+       ab <- (s `at` 3) >>= objName; y <- (s `at` 4) >>= objName
+       (rthm, athm, rep, abst, n) <- Com.defineTypeOp th (mapMaybe objName l) r ab y
+       let s' = (ObjThm rthm) <:> (ObjThm athm) <:> (ObjConst rep) <:> (ObjConst abst) <:> (ObjTyOp n) <:> (Stack.pop 5 s)
+       return (s',d,a,t)
+
+
+eqMp :: MachineState -> MachineState
+eqMp x =
+    do (s,d,a,t) <- x
+       t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm
+       thm <- Com.eqMp t1 t2
+       let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+nil :: MachineState -> MachineState
+nil x =
+    do (s,d,a,t) <- x
+       return (ObjList [] <:> s, d, a, t)
+
+
+opType :: MachineState -> MachineState
+opType x =
+    do (s,d,a,t) <- x
+       l <- (s `at` 0) >>= objList; to <- (s `at` 1) >>= objTyOp
+       let newType = Com.opType (mapMaybe objType l) to
+           s' = (ObjType newType) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+pop :: MachineState -> MachineState
+pop x = 
+    do (s,d,a,t) <- x
+       return ((Stack.pop 1 s),d,a,t)
+
+
+ref :: MachineState -> MachineState
+ref x =
+    do (s,d,a,t) <- x
+       n <- (s `at` 0) >>= objNum
+       let object = d ! n
+           s' = object <:> (Stack.pop 1 s)
+       return (s',d,a,t)
+
+
+refl :: MachineState -> MachineState
+refl x =
+    do (s,d,a,t) <- x
+       te <- (s `at` 0) >>= objTerm
+       let thm = Com.refl te
+           s' = (ObjThm thm) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
+
+
+remove :: MachineState -> MachineState
+remove x =
+    do (s,d,a,t) <- x
+       n <- (s `at` 0) >>= objNum
+       let object = d ! n
+           s' = object <:> (Stack.pop 1 s)
+           d' = Map.delete n d
+       return (s',d',a,t)
+
+
+subst :: MachineState -> MachineState
+subst x =
+    do (s,d,a,t) <- x
+       th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList
+       thm <- Com.subst th l
+       let s' = (ObjThm thm) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+thm :: MachineState -> MachineState
+thm x =
+    do (s,d,a,t) <- x
+       te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList; th <- (s `at` 2) >>= objThm
+       thm <- Com.thm te (mapMaybe objTerm l) th
+       let s' = Stack.pop 3 s
+           t' = Set.insert thm t
+       return (s',d,a,t')
+
+
+typeOp :: MachineState -> MachineState
+typeOp x =
+    do (s,d,a,t) <- x
+       n <- (s `at` 0) >>= objName
+       let typeOp = Com.typeOp n
+           s' = (ObjTyOp typeOp) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
+
+
+var :: MachineState -> MachineState
+var x =
+    do (s,d,a,t) <- x
+       ty <- (s `at` 0) >>= objType; n <- (s `at` 1) >>= objName
+       v <- Com.var ty n
+       let s' = (ObjVar v) <:> (Stack.pop 2 s)
+       return (s',d,a,t)
+
+
+varTerm :: MachineState -> MachineState
+varTerm x =
+    do (s,d,a,t) <- x
+       v <- (s `at` 0) >>= objVar
+       let term = Com.varTerm v
+           s' = (ObjTerm term) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
+
+
+varType :: MachineState -> MachineState
+varType x =
+    do (s,d,a,t) <- x
+       n <- (s `at` 0) >>= objName
+       newType <- Com.varType n
+       let s' = (ObjType newType) <:> (Stack.pop 1 s)
+       return (s',d,a,t)
+
+
+
+eval :: [String] -> MachineState
+eval list =
+    let s = Stack.empty
+        d = Map.empty
+        a = Set.empty
+        t = Set.empty
+        op = (\x y -> case y of (Comment _) -> x
+                                (Command z) -> z x)
+
+        -- important to use foldl here so commands get applied in the correct order
+        result = (foldl' (op) (Just (s,d,a,t))) . (map (parse)) $ list
+
+    in result
+
+
+
+doSemanticCheck :: [String] -> String
+doSemanticCheck list =
+    case (machineToString (eval list)) of
+           Just x -> x
+           Nothing -> "Error\n"
+
diff --git a/src/Library/Stack.hs b/src/Library/Stack.hs
new file mode 100644
index 0000000..99cd8e1
--- /dev/null
+++ b/src/Library/Stack.hs
@@ -0,0 +1,50 @@
+module Library.Stack (
+	Stack,
+    empty,
+    at,
+    pop,
+    (<:>),
+    size,
+    diff
+    ) where
+
+
+import Data.List
+
+
+data Stack a = Stack [a] deriving (Eq)
+
+
+instance Show a => Show (Stack a) where
+    show (Stack x)   =   "Stack:\n" ++ intercalate "\n" (map (show) x) ++ "\n\n"
+
+
+infixr 9 <:>
+
+
+empty :: Stack a
+empty = Stack []
+
+
+at :: Stack a -> Int -> Maybe a
+at (Stack list) index =
+    if (index < length list && index >= 0)
+    then Just (list!!index)
+    else Nothing
+
+
+pop :: Int -> Stack a -> Stack a
+pop n (Stack list) = Stack (drop n list)
+
+
+(<:>) :: a -> Stack a -> Stack a
+x <:> (Stack list) = Stack (x : list)
+
+
+size :: Stack a -> Int
+size (Stack list) = length list
+
+
+diff :: (Eq a) => Stack a -> Stack a -> Stack a
+diff (Stack one) (Stack two) = Stack (one \\ two)
+
diff --git a/src/Library/Term.hs b/src/Library/Term.hs
new file mode 100644
index 0000000..be9e53b
--- /dev/null
+++ b/src/Library/Term.hs
@@ -0,0 +1,193 @@
+module Library.Term (
+    Term(..),
+    Substitution,
+
+    alphaEquiv,
+    alphaConvert,
+    alphaConvertList,
+    substitute,
+    boundVars,
+    freeVars,
+    rename,
+    typeOf,
+    typeVarsInTerm,
+    mkEquals,
+    isEq,
+    getlhs,
+    getrhs
+    ) where
+
+
+
+import Data.List
+import Data.Maybe
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+import Library.TypeVar
+
+
+
+data Term   = TVar { tVar :: Var }
+            | TConst { tConst :: Const
+                     , tConstType :: Type }
+            | TApp { tAppLeft :: Term
+                   , tAppRight :: Term }
+            | TAbs { tAbsVar :: Term
+                   , tAbsTerm :: Term } deriving (Ord)
+
+type Substitution = ( [(Name,Type)], [(Var,Term)] )
+
+
+instance Show Term where
+    show (TVar v)       =   (show v) 
+    show (TConst a _)   =   (show a)
+    show (TApp (TApp eq lhs) rhs)
+            | isEq eq   =   "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")"
+    show (TApp a b)     =   "(" ++ (show a) ++ " " ++ (show b) ++ ")"
+    show (TAbs a b)     =   "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")"
+
+
+instance Eq Term where
+    a == b   =   a `alphaEquiv` b
+
+
+
+alphaEquiv :: Term -> Term -> Bool
+alphaEquiv a b =
+    let equiv term1 term2 varmap1 varmap2 depth =
+            case (term1,term2) of
+                (TConst a1 b1, TConst a2 b2) ->
+                    a1 == a2 && b1 == b2
+
+                (TApp a1 b1, TApp a2 b2) ->
+                    equiv a1 a2 varmap1 varmap2 depth &&
+                    equiv b1 b2 varmap1 varmap2 depth
+
+                (TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) ->
+                    equiv b1 b2 newmap1 newmap2 (depth+1)
+                    where newmap1 = Map.insert (Var name1 type1) depth varmap1
+                          newmap2 = Map.insert (Var name2 type2) depth varmap2
+
+                (TVar (Var name1 type1), TVar (Var name2 type2)) ->
+                    type1 == type2 && ((name1 == name2 && Map.notMember (Var name1 type1) varmap1 && Map.notMember (Var name2 type2) varmap2) ||
+                    Map.lookup (Var name1 type1) varmap1 == Map.lookup (Var name2 type2) varmap2)
+
+                (_,_) -> False
+                
+    in equiv a b Map.empty Map.empty 0
+
+
+alphaConvert :: Term -> Term -> Term
+alphaConvert (TConst _ _) (TConst a ty) = TConst a ty
+alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2)
+alphaConvert (TVar _) (TVar v) = TVar v
+alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute ([],[(tVar v1,v2)]) (TAbs v1 (alphaConvert a b))
+
+
+alphaConvertList :: [Term] -> [Term] -> [Term]
+alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b)
+
+
+substitute :: Substitution -> Term -> Term
+substitute (t,v) term =
+    let typesub x y =
+                case y of
+                    (TConst a ty) -> TConst a (typeVarSub x ty)
+                    (TApp a b) -> TApp (typesub x a) (typesub x b)
+                    (TAbs (TVar (Var n ty)) a) -> TAbs (TVar (Var n (typeVarSub x ty))) (typesub x a)
+                    (TVar (Var n ty)) -> TVar (Var n (typeVarSub x ty))
+
+        varsub x y =
+                case y of
+                    (TConst a ty) -> TConst a ty
+                    (TApp a b) -> TApp (varsub x a) (varsub x b)
+                    (TVar v) -> if (Map.member v x)
+                                then fromJust (Map.lookup v x)
+                                else TVar v
+                    (TAbs v a) -> let safe = rename (TAbs v a) (Set.union (Map.keysSet x) (Set.unions . (map freeVars) . (Map.elems) $ x))
+                                  in case safe of
+                                         (TAbs m n) -> TAbs m (varsub x n)
+
+        tymap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty t
+        vmap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty v
+
+    in (varsub vmap) . (typesub tymap) $ term
+
+
+boundVars :: Term -> Set.Set Var
+boundVars (TConst a b) = Set.empty
+boundVars (TApp a b) = Set.union (boundVars a) (boundVars b)
+boundVars (TVar a) = Set.empty
+boundVars (TAbs a b) = Set.insert (tVar a) (boundVars b)
+
+
+freeVars :: Term -> Set.Set Var
+freeVars (TConst a b) = Set.empty
+freeVars (TApp a b) = Set.union (freeVars a) (freeVars b)
+freeVars (TVar a) = Set.singleton a
+freeVars (TAbs a b) = Set.delete (tVar a) (freeVars b)
+
+
+rename :: Term -> Set.Set Var -> Term
+rename (TAbs (TVar v) t) vars =
+    let doRename x y z =
+            case x of
+                (TAbs (TVar a) b) ->
+                    if (a == y)
+                    then TAbs (TVar z) (doRename b y z)
+                    else TAbs (TVar a) (doRename b y z)
+                (TConst a b) -> TConst a b
+                (TApp a b) -> TApp (doRename a y z) (doRename b y z)
+                (TVar a) ->
+                    if (a == y)
+                    then TVar z
+                    else TVar a
+
+        findSafe x y =
+            if (Set.member x y)
+            then case x of
+                    (Var a b) ->
+                        case a of
+                            (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y
+            else x
+
+    in if (Set.member v vars)
+       then doRename (TAbs (TVar v) t) v (findSafe v vars)
+       else TAbs (TVar v) t
+
+
+typeOf :: Term -> Type
+typeOf (TConst _ ty) = ty
+typeOf (TVar v) = varTy v
+typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t)
+typeOf (TApp f _) = 
+    -- type of f is of the form [[a,b], "->"]
+    last . aType . typeOf $ f
+
+
+typeVarsInTerm :: Term -> Set.Set Type
+typeVarsInTerm (TConst _ ty) = typeVarsInType ty
+typeVarsInTerm (TVar v) = typeVarsInType . varTy $ v
+typeVarsInTerm (TAbs v t) = Set.union (typeVarsInType . varTy . tVar $ v) (typeVarsInTerm t)
+typeVarsInTerm (TApp f x) = Set.union (typeVarsInTerm f) (typeVarsInTerm x)
+
+
+mkEquals :: Term -> Term -> Term
+mkEquals lhs rhs =
+    let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs))
+    in TApp (TApp eqConst lhs) rhs
+
+
+getlhs :: Term -> Term
+getlhs (TApp (TApp eq lhs) _)
+    | (isEq eq) = lhs
+
+
+getrhs :: Term -> Term
+getrhs (TApp (TApp eq _) rhs)
+    | (isEq eq) = rhs
+
+
+isEq :: Term -> Bool
+isEq (TConst (Const (Name [] "=")) _) = True
+isEq _ = False
diff --git a/src/Library/TermNet.hs b/src/Library/TermNet.hs
new file mode 100644
index 0000000..16b5446
--- /dev/null
+++ b/src/Library/TermNet.hs
@@ -0,0 +1,214 @@
+module Library.TermNet(
+    TermNet,
+
+    empty,
+    getLeafList,
+    getBranchList,
+
+    genThm,
+    termToTermString,
+    thmToTermString,
+
+    addThm,
+    addThmFromNode,
+    matchThm
+    ) where
+
+
+
+import Data.Maybe
+import Data.List
+import qualified Data.Set as Set
+import Data.Graph.Inductive.Graph( Node )
+import qualified Data.Graph.Inductive.Graph as Graph
+import Library.ProofGraph
+import Library.WriteProof
+import Library.Object
+import Library.Theorem
+import Library.Term
+import Library.Parse
+import Library.Semantic
+import Library.Stack( Stack, at, (<:>) )
+import qualified Library.Stack as Stack
+
+
+
+data TermNet = Leaf [(Theorem, Node)] | Branch [(String, TermNet)]
+    deriving (Eq, Show)
+
+
+
+empty :: TermNet
+empty = Branch []
+
+
+
+isLeaf :: TermNet -> Bool
+isLeaf (Leaf _) = True
+isLeaf _ = False
+
+
+
+isBranch :: TermNet -> Bool
+isBranch (Branch _) = True
+isBranch _ = False
+
+
+
+getLeafList :: TermNet -> Maybe [(Theorem, Node)]
+getLeafList net =
+    case net of
+        Leaf list -> Just list
+        Branch list -> Nothing
+
+
+
+getBranchList :: TermNet -> Maybe [(String, TermNet)]
+getBranchList net =
+    case net of 
+        Leaf list -> Nothing
+        Branch list -> Just list
+
+
+
+genThm :: PGraph -> Node -> Theorem
+genThm graph node =
+    let gen g n num = 
+            let edge = filter (\x -> (fst . thd3 $ x) == num) (Graph.out g n)
+                node = (snd3 . head $ edge)
+                listing = write g node
+            in fromJust (((\(a,_,_,_) -> a) . fromJust $ (eval listing)) `at` 0)
+
+        hypList = map (fromJust . objTerm) (fromJust . objList $ (gen graph node 2))
+        con = fromJust . objTerm $ (gen graph node 1)
+
+    in Theorem (Set.fromList hypList) con
+
+
+
+termToTermString :: Term -> [String]
+termToTermString term =
+    case term of
+        (TConst _ _) ->
+            ["const"]
+
+        (TApp func arg) ->
+            ["app"] ++ (termToTermString func) ++ (termToTermString arg)
+
+        (TAbs var body) ->
+            ["abs", "var"] ++ (termToTermString body)
+
+        (TVar var) ->
+            ["var"]
+
+
+
+thmToTermString :: Theorem -> [String]
+thmToTermString theorem =
+    let hypList = Set.toList (thmHyp theorem)
+        f soFar hyp = soFar ++ ["hyp"] ++ (termToTermString hyp)
+    in (foldl' f [] hypList) ++ ["con"] ++ (termToTermString . thmCon $ theorem)
+
+
+
+addThm :: TermNet -> Theorem -> Node -> TermNet
+addThm net theorem node =
+    addThmImp net (theorem,node) (thmToTermString theorem)
+
+
+
+addThmFromNode :: TermNet -> PGraph -> Node -> TermNet
+addThmFromNode net graph node =
+    let theorem = genThm graph node
+    in addThmImp net (theorem,node) (thmToTermString theorem)
+
+
+
+addThmImp :: TermNet -> (Theorem,Node) -> [String] -> TermNet
+addThmImp (Branch branchList) item (x:[]) =
+    let (sameKey, rest) = partition (\(y,z) -> y == x && isLeaf z) branchList
+    in if (sameKey == [])
+       then let leaf' = Leaf [item]
+            in Branch ((x,leaf'):rest)
+       else let leaf = snd . head $ sameKey
+                leafList = fromJust . getLeafList $ leaf
+            in if (item `elem` leafList)
+               then Branch branchList
+               else let leaf' = Leaf (item:leafList)
+                    in Branch ((x,leaf'):rest)
+
+addThmImp (Branch branchList) item (x:xs) =
+    let (sameKey, rest) = partition (\(y,z) -> y == x) branchList
+    in if (sameKey == [])
+       then let net' = addThmImp empty item xs
+            in Branch ((x,net'):rest)
+       else let nextStepDown = snd . head $ sameKey
+                net' = addThmImp nextStepDown item xs
+            in Branch ((x,net'):rest)
+
+
+
+matchThm :: TermNet -> Theorem -> [(Theorem,Node)]
+matchThm net theorem =
+    let hyp = Set.toList (thmHyp theorem)
+        con = thmCon theorem
+        (curPrefix, curTerm) = if (hyp == [])
+                               then ("con", con)
+                               else ("hyp", head hyp)
+
+        r = do a <- matchImp curPrefix net
+               let b = matchTermImp curTerm a
+                   (branches, leaves) = partition (\x -> isBranch x) b
+
+               c <- if (hyp == [])
+                    then getLeafList (foldl' unify (Leaf []) leaves)
+                    else let theorem' = Theorem (Set.fromList (tail hyp)) con
+                         in return (matchThm (foldl' unify empty branches) theorem')
+               return c
+
+    in if (isNothing r) then [] else fromJust r
+
+
+
+matchImp :: String -> TermNet -> Maybe TermNet
+matchImp key net =
+    do list <- getBranchList net
+       let result = filter (\(x,y) -> x == key) list
+       r <- if (result == []) then Nothing else Just (snd . head $ result)
+       return r
+
+
+
+matchTermImp :: Term -> TermNet -> [TermNet]
+matchTermImp term net =
+    let list = getBranchList net
+        var = matchImp "var" net
+        result =
+            case term of
+                (TConst c ty) -> 
+                    do a <- matchImp "const" net
+                       return [a]
+
+                (TApp f x) ->
+                    do a <- matchImp "app" net
+                       let b = matchTermImp f a
+                       return (concat (map (matchTermImp x) b))
+
+                (TAbs v x) ->
+                    do a <- matchImp "abs" net
+                       b <- matchImp "var" a
+                       return (matchTermImp x b)
+
+                (TVar v) -> Nothing --don't need to do anything because variables are already taken care of
+
+        var' = if (isNothing var) then [] else [fromJust var]
+        result' = if (isNothing result) then [] else fromJust result
+
+    in var' ++ result'
+
+
+
+unify :: TermNet -> TermNet -> TermNet
+unify (Branch a) (Branch b) = Branch (a ++ b)
+unify (Leaf a) (Leaf b) = Leaf (a ++ b)
+
diff --git a/src/Library/Theorem.hs b/src/Library/Theorem.hs
new file mode 100644
index 0000000..fc66cc2
--- /dev/null
+++ b/src/Library/Theorem.hs
@@ -0,0 +1,19 @@
+module Library.Theorem (
+	Theorem(..),
+	) where
+
+
+
+import qualified Data.Set as Set
+import Library.TypeVar
+import Library.Term
+
+
+
+data Theorem = Theorem { thmHyp :: Set.Set Term
+                       , thmCon :: Term } deriving (Eq, Ord)
+
+
+
+instance Show Theorem where
+    show a   =   (show . Set.toList . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a)
diff --git a/src/Library/TypeVar.hs b/src/Library/TypeVar.hs
new file mode 100644
index 0000000..d2915e6
--- /dev/null
+++ b/src/Library/TypeVar.hs
@@ -0,0 +1,99 @@
+module Library.TypeVar (
+	Number,
+
+	Name(..),
+
+	TypeOp(..),
+
+	Type(..),
+
+	Const(..),
+
+	Var(..),
+
+	mkEqualsType,
+	typeFunc,
+	typeBool,
+	typeVarsInType,
+	isTypeVar,
+	typeVarSub
+	) where
+
+
+
+import Data.List
+import Data.Maybe
+import qualified Data.Set as Set
+import Data.Map( Map, (!) )
+import qualified Data.Map as Map
+
+
+
+type Number = Int
+
+data Name = Name { nameSpace :: [String]
+                 , nameId :: String } deriving (Eq, Ord)
+
+data TypeOp = TypeOp { tyOp :: Name } deriving (Eq, Ord)
+
+data Type = TypeVar { typeVar :: Name }
+          | AType { aType :: [Type]
+                  , aTypeOp :: TypeOp } deriving (Eq, Ord)
+
+data Const = Const { constName :: Name } deriving (Eq, Ord)
+
+data Var = Var { varName :: Name
+               , varTy :: Type } deriving (Eq, Ord)
+
+
+
+instance Show Name where
+    show a   =   intercalate "." (nameSpace a ++ [nameId a])
+
+instance Show TypeOp where
+    show a   =   "typeOp " ++ (show $ tyOp a)
+
+instance Show Type where
+    show (TypeVar tyVar)   =   "V " ++ (show tyVar)
+    show (AType [] (TypeOp (Name [] "bool"))) = "bool"
+    show (AType [d,r] (TypeOp (Name [] "->"))) = "(" ++ show d ++ " -> " ++ show r ++ ")"
+    show (AType list typeOp) =   "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list)
+
+instance Show Const where
+    show (Const a)   =   show a
+
+instance Show Var where
+    show (Var a _)   =   show a
+
+
+
+mkEqualsType :: Type -> Type
+mkEqualsType ty = typeFunc ty (typeFunc ty typeBool)
+
+
+typeFunc :: Type -> Type -> Type
+typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->"))
+
+
+typeBool :: Type
+typeBool = AType [] (TypeOp (Name [] "bool"))
+
+
+typeVarsInType :: Type -> Set.Set Type
+typeVarsInType (TypeVar t) = Set.singleton (TypeVar t)
+typeVarsInType (AType list _) = Set.unions . (map typeVarsInType) $ list
+
+
+isTypeVar :: Type -> Bool
+isTypeVar (TypeVar _) = True
+isTypeVar _ = False
+
+
+typeVarSub :: Map Name Type -> Type -> Type
+typeVarSub m (TypeVar a) = 
+	if (Map.member a m)
+	then fromJust (Map.lookup a m)
+	else TypeVar a
+typeVarSub m (AType list op) =
+	AType (map (typeVarSub m) list) op
+
diff --git a/src/Library/Usage.hs b/src/Library/Usage.hs
new file mode 100644
index 0000000..a307274
--- /dev/null
+++ b/src/Library/Usage.hs
@@ -0,0 +1,80 @@
+module Library.Usage(
+	UsageMap,
+	usageMap,
+	useSort,
+	nodeOutput,
+	getArg
+	) where
+
+
+
+import Data.Map( Map )
+import qualified Data.Map as Map
+import Data.Set( Set )
+import qualified Data.Set as Set
+import Data.List
+import Data.Maybe
+import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge )
+import qualified Data.Graph.Inductive.Graph as Graph
+import Library.Parse
+import Library.ProofGraph
+
+
+
+type UsageMap = Map Node (Map (LEdge (Int,Int)) (Int,[Int]))
+
+
+-- Takes a graph, a starting list of nodes, a set of nodes of interest, and
+-- follows the starting nodes up the graph to find which edges the starting nodes
+-- will encounter the nodes of interest through.
+usageMap :: PGraph -> [Node] -> Set Node -> UsageMap
+usageMap graph order interest =
+    let unionFunc a b = Map.unionWith min a b
+
+        addFunc index prev umap edge =
+                let node = snd3 edge
+                    curIn = Graph.outdeg graph (fst3 edge)
+                    prev' = (curIn - (fst . thd3 $ edge)):prev
+                    toAdd = Map.singleton node (Map.singleton edge (index,prev'))
+                in if (Set.member node interest)
+                   then Map.unionWith unionFunc toAdd umap
+                   else umap
+
+        f umap (index,node,prev) =
+                let edgeList = Graph.out graph node
+                    sucMapList = map (f Map.empty) (map (\x -> (index, snd3 x, (length edgeList - (fst . thd3 $ x)):prev)) edgeList)
+                    umap' = foldl' (addFunc index prev) umap edgeList
+                in Map.unionsWith unionFunc (umap':sucMapList)
+
+    in foldl' f Map.empty (zip3 [1..] order (repeat []))
+
+
+
+useSort :: (LEdge a, (Int,[Int])) -> (LEdge a, (Int,[Int])) -> Ordering
+useSort (_,(w,x)) (_,(y,z)) =
+	let check = compare w y
+	in if (check == EQ)
+	   then compare (reverse x) (reverse z)
+	   else check
+
+
+
+nodeOutput :: PGraph -> Node -> Int
+nodeOutput graph node =
+    let label = fromJust (Graph.lab graph node)
+    in case label of
+           "thm" -> 0
+           "pop" -> 0
+           "defineConst" -> 2
+           "defineTypeOp" -> 5
+           x -> 1
+
+
+
+getArg :: PGraph -> Node -> Int -> Maybe Node
+getArg graph node arg =
+    let edge = filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node)
+    in if (edge == [])
+       then Nothing
+       else Just (snd3 . head $ edge)
+
diff --git a/src/Library/WriteProof.hs b/src/Library/WriteProof.hs
new file mode 100644
index 0000000..2c15b74
--- /dev/null
+++ b/src/Library/WriteProof.hs
@@ -0,0 +1,211 @@
+module Library.WriteProof (
+    write,
+    writeAll,
+    doWriteProof,
+    singleCommands,
+    next,
+    genPart,
+    writeGraph
+    ) where
+
+
+
+import Data.Maybe
+import Data.Graph.Inductive.Graph( LNode, LEdge, Node, Edge, (&) )
+import qualified Data.Graph.Inductive.Graph as Graph
+import Data.Graph.Inductive.Tree
+import Data.Map( Map, (!) )
+import qualified Data.Map as Map
+import Data.Set( Set )
+import qualified Data.Set as Set
+import Data.List
+import Library.Stack( Stack, at, (<:>) )
+import qualified Library.Stack as Stack
+import Library.Parse( isNumber, fst3, snd3, thd3 )
+import Library.Cost
+import Library.ProofGraph
+import Library.GraphPart
+import Library.Usage
+
+
+
+orderNodes :: PGraph -> [Node] -> [Node]
+orderNodes graph nodeList = nodeList
+--placeholder
+
+
+
+-- buggy
+multiCommandsSimple :: PGraph -> UsageMap -> [Node] -> PGraph
+multiCommandsSimple graph usemap nodeList =
+    let multiNodes = filter (\x -> nodeOutput graph x > 1 && x `notElem` nodeList) (Graph.nodes graph)
+        umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap
+
+        f = (\gr node edgemap ->
+                let out = nodeOutput gr node
+                    index = next out gr
+
+                    edgeList = Map.toList edgemap
+                    edgeToNode = (\x -> (fst3 x, fst . thd3 $ x))
+
+                    sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edgeList
+                    grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted
+
+                    defEdge = fst (minimumBy useSort edgeList)
+                    removeEdges = map (fst . (maximumBy useSort)) grouped
+                    refEdges = map (filter (\x -> x /= defEdge && x `notElem` removeEdges) . (map fst)) grouped
+
+                    usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeEdges)) [1..out]
+
+                    defGen = (\num ->
+                        if (num > out)
+                        then let reqEdges = filter (\x -> (snd . thd3 . fst $ x) == (snd . thd3 $ defEdge) && fst x /= defEdge) edgeList
+                                 refArg = (snd . thd3 $ defEdge) - 1
+                             in if (reqEdges == [])
+                                then [index!!refArg, "ref"] --remove
+                                else [index!!refArg, "ref"]
+                        else if (num == (snd . thd3 $ defEdge) && num == out)
+                             then if (filter (\x -> x /= defEdge && (snd . thd3 $ x) == num) (map fst edgeList) == [])
+                                  then []
+                                  else [index!!(num-1), "def"]
+                             else if (num `elem` usedArgs)
+                                  then [index!!(num-1), "def", "pop"] ++ defGen (num+1)
+                                  else ["pop"] ++ defGen (num+1))
+
+                    defPart = (genPart (defGen 1) True, Just (node,1), [edgeToNode defEdge])
+
+                    removeList = filter (\(x,y) -> y /= defEdge) (zip usedArgs removeEdges)
+                    removeParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, [edgeToNode y])) removeList
+
+                    refList = filter (\(x,y) -> y /= []) (zip usedArgs refEdges)
+                    refParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, map edgeToNode y)) refList
+
+                    partList = defPart:(removeParts ++ refParts)
+                    edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList
+                    partsAdded = graphAddList partList edgesRemoved
+                in partsAdded)
+
+    in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes
+
+
+
+singleCommands :: PGraph -> UsageMap -> [Node] -> PGraph
+singleCommands graph usemap nodeList =
+    let singleNodes = filter (\x -> nodeOutput graph x == 1 && Graph.indeg graph x > 1) (Graph.nodes graph)
+        umap = Map.filterWithKey (\n _ -> n `elem` singleNodes) usemap
+
+        s = (\gr node edgemap ->
+                let index = head (next 1 gr)
+                    edgeList = Map.toList edgemap
+
+                    defEdge = fst (minimumBy useSort edgeList)
+                    removeEdge = fst (maximumBy useSort edgeList)
+                    refEdgeList = filter (\x -> x /= defEdge && x /= removeEdge) (map fst edgeList)
+
+                    defPart = genPart [index, "def"] True
+                    refPart = genPart [index, "ref"] False
+                    removePart = genPart [index, "ref"] False
+
+                    defNode = (fst3 defEdge, fst . thd3 $ defEdge)
+                    removeNode = (fst3 removeEdge, fst . thd3 $ removeEdge)
+                    refNodeList = map (\x -> (fst3 x, fst . thd3 $ x)) refEdgeList
+
+                    partList = [(defPart, Just (node, 1), [defNode]), (removePart, Nothing, [removeNode])]
+                    partList' = if (refNodeList == []) then partList else (refPart, Nothing, refNodeList):partList
+
+                    edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList
+                    partsAdded = graphAddList partList' edgesRemoved
+                in partsAdded)
+
+        f = (\gr node edgemap ->
+                let reuse = Graph.indeg graph node
+                    costToStore = (nodeCost graph node) + (listCost ["def","0"]) + (reuse - 1) * (listCost ["ref","0"])
+                    costToIgnore = reuse * (nodeCost graph node)
+                in if (costToStore >= costToIgnore)
+                   then gr
+                   else s gr node edgemap)
+
+    in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph singleNodes
+
+
+
+genPart :: [String] -> Bool -> GraphPart
+genPart labels hasInput =
+    let nodeList = zip [1..] labels
+        edgeFunc = (\edges nodes ->
+            if (nodes == [] || (tail nodes) == [])
+            then edges
+            else let newEdge = (fst (nodes!!1), fst (nodes!!0), (1,1))
+                 in edgeFunc (newEdge:edges) (tail nodes))
+        edgeList = edgeFunc [] nodeList
+        input = if (hasInput) then Just (1,1) else Nothing
+        output = Just (length labels, 1)
+    in graphPart nodeList edgeList input output
+
+
+
+next :: Int -> PGraph -> [String]
+next num graph =
+    let nodeList = filter (isNumber . snd) (Graph.labNodes graph)
+        numList = nub . (map (read . snd)) $ nodeList
+        f x y = if (x `elem` y) then f (x + 1) y else x
+        g x y = if (x == 0) then y else g (x - 1) (f 0 (y ++ numList) : y)
+    in map show (g num [])
+
+
+
+removeUnused :: PGraph -> [Node] -> PGraph
+removeUnused graph nodeList =
+    let unused = filter (\x -> Graph.indeg graph x == 0 && x `notElem` nodeList) (Graph.nodes graph)
+    in if (unused == [])
+       then graph
+       else removeUnused (Graph.delNodes unused graph) nodeList
+
+
+
+resolve :: PGraph -> [Node] -> PGraph
+resolve graph nodeList =
+    let liveGraph = removeUnused graph nodeList
+        umap = usageMap graph nodeList (Set.fromList (Graph.nodes liveGraph))
+        singlesDone = singleCommands liveGraph umap nodeList
+        multisDone = multiCommandsSimple singlesDone umap nodeList
+    in multisDone
+
+
+
+writeGraph :: PGraph -> Node -> [String]
+writeGraph graph node =
+    let label = fromJust (Graph.lab graph node)
+        argList = [1 .. (Graph.outdeg graph node)]
+        f s a = let arg = getArg graph node a
+                in if (isNothing arg)
+                    then s
+                    else (writeGraph graph (fromJust arg)) ++ s
+    in foldl' f [label] argList
+
+
+
+write :: PGraph -> Node -> [String]
+write graph node =
+    writeGraph (resolve graph [node]) node
+
+
+
+writeAll :: PGraph -> [Node] -> [String]
+writeAll graph nodeList =
+    let ordered = orderNodes graph nodeList
+        resolved = resolve graph ordered
+        f g n = if (n == [])
+                then []
+                else (writeGraph g (head n)) ++ (f g (tail n))
+    in f resolved ordered
+
+
+-- metric relates to minimum amount of work done not-on-top of the stack
+
+
+doWriteProof :: PGraph -> [String]
+doWriteProof graph =
+    let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph)
+    in writeAll graph initList
+
diff --git a/src/Library/alternate_multi_command.hs b/src/Library/alternate_multi_command.hs
new file mode 100644
index 0000000..da49a7d
--- /dev/null
+++ b/src/Library/alternate_multi_command.hs
@@ -0,0 +1,315 @@
+multiCommands :: PGraph -> UsageMap -> [Node] -> PGraph
+multiCommands graph usemap nodeList =
+    let multiNodes = filter (\x -> nodeOutput graph x > 1) (Graph.nodes graph)
+        umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap
+
+        before = (\gr node edgemap arg indexList ->
+                let edges = filter (\x -> snd . thd3 . fst $ x < arg) edgemap
+
+                    -- sorts and groups by which output of the command each edge is using
+                    sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges
+                    grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted
+
+                    -- makes a list of pairs of (maximum, restOfList)
+                    maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped
+
+                    refNodeEdges = map (fst . snd) maxSplit
+                    removeNodeEdges = concat (map (fst . fst) maxSplit)
+
+                    usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeNodeEdges)) [1..(arg-1)]
+
+                    -- creates a graphpart to define and pop all the initial outputs to get to the used one in the middle
+                    defGen = (\num -> 
+                            if (num == arg)
+                            then []
+                            else if (index!!num `elem` usedArgs)
+                                 then [index!!num, "def", "pop"] ++ defGen (num+1)
+                                 else ["pop"] ++ defGen (num+1))
+                    defPart = genPart (defGen 0) True
+
+                    -- creates graphparts for removing all the items stored in the dictionary, including node attachments
+                    removeList = zip usedArgs removeNodeEdges
+                    removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList
+
+                    -- creates graphparts to reference all the items stored in the dictionary, including node attachments
+                    refList = zip usedArgs refNodeEdges
+                    refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList
+
+                in (defPart, refPart ++ removePart))
+
+
+        after = (\gr node edgemap arg indexList ->
+                let -- obtain edges after the cutoff argument
+                    edges = filter (\x -> snd . thd3 . fst $ x > arg) edgemap
+
+                    -- sort and group by which output of the command each edge is using
+                    sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges
+                    grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted
+
+                    mins = map (minimumBy useSort) grouped
+                    initEdge = minimumBy useSort (Map.toList edgemap)
+
+                    usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) mins)) [(arg+1)..(nodeOutput gr node)]
+                    edgeToNode = (\x -> (fst3 x, fst . thd3 $ x))
+
+                    -- finds the argument where you have to pop everything and store it all in the dictionary before
+                    -- proceeding
+                    findAttach = (\x y ->
+                            if (x == [])
+                            then nodeOutput gr node
+                            else let allZero = all (=0) (snd . snd . head $ x)
+                                     headIsMin = (head x) == (minimumBy useSort x)
+                                     headThmLowestStrict = let testList = map (fst . snd) x
+                                                           in all (> head testList) (tail testList)
+                                     nextUsedArg = snd . thd3 . fst . head . tail $ x
+                                 in if (allZero && headIsMin && headThmLowestStrict)
+                                    then findAttach (tail x) nextUsedArg
+                                    else y)
+
+                    argToAttach = findAttach initEdge:mins arg
+
+                    process = (\attach curArg modp ordp ->
+                        case (compare arg argToAttach) of
+                            LT ->
+                            EQ ->
+                            GT ->)
+
+                    (modParts, ordinaryParts) = process argToAttach arg [] []
+
+                    -- calculate the def/pop/ref defPart
+                    afterPartInit = 
+                    afterPart = 
+                        if (argToAttach == arg)
+                        then
+                        else
+
+                    -- calculate def nodes/parts for outputs before the argToAttach
+                    defs =
+                    makeDefList =
+                    defPart = map (\(x,y) -> (genPart [index!!(x-1), "def"] False, Nothing, [edgeToNode y])) makeDefList
+
+                    -- calculate ref and remove nodes/parts
+                    maxes = map (maximumBy useSort) grouped
+                    refs = map (filter (\x -> x `notElem` maxes && x `notElem` defs)) grouped
+
+                    removeList = zip usedArgs maxes
+                    removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList
+
+                    -- creates graphparts to reference all the items stored in the dictionary, including node attachments
+                    refList = zip usedArgs refs
+                    refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList
+
+                in (modParts, ordinaryParts))
+
+        addPreserveNodeParts = (\partList graph ->
+            )
+
+        f = (\gr node edgemap ->
+                let edgeList = Map.toList edgemap
+
+                    out = nodeOutput gr node
+                    index = next (out + 1) gr
+
+                    initEdge = fst (minimumBy useSort edgeList)
+                    initArg = snd . thd3 $ initEdge
+                    (defBefore, beforeParts) = before gr node edgemap initArg (take (initArg-1) index)
+                    (defAfter, afterParts) = after gr node edgemap initArg (drop initArg index)
+                    edgesToRemove = filter (\x -> x /= initEdge) (map fst edgeList)
+
+                    gr' = addPreserveNodeParts defAfter gr
+
+                    edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) gr' edgesToRemove
+                    partsAdded = graphAddList partList edgesRemoved
+                in partsAdded)
+
+    in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes
+
+
+
+
+
+
+
+
+
+
+
+
+
+multiCommands :: PGraph -> PGraph -> UsageMap -> [Node] -> PGraph
+multiCommands graph orig usemap nodeList =
+    let process = (\gr stack dict workmap edge ->
+                let node = snd3 edge
+                    label = fromJust (Graph.lab gr node)
+                in if (label == "def" || label == "ref" || label == "remove" || isNumber label)
+                   then dictProcess gr stack dict workmap edge
+                   else regProcess gr stack dict workmap edge
+
+
+        dictProcess = (\gr stack dict workmap edge ->
+                let node = snd3 edge
+                    label = fromJust (Graph.lab gr node)
+                    index = fromJust (Graph.lab gr (head (Graph.suc gr node)))
+
+                in if (label == "def")
+                   then let dict' = Map.insert index (head stack) dict
+                        in (gr, stack, dict', workmap)
+
+                   else if (label == "ref")
+                        then let stack' = (fromJust (Map.lookup index dict)):stack
+                             in (gr, stack', dict, workmap)
+
+                        else if (label == "remove")
+                             then let stack' = (fromJust (Map.lookup index dict)):stack
+                                      dict' = Map.delete index dict
+                                  in (gr, stack', dict', workmap)
+                             else -- isNumber label
+                                  (gr, stack, dict, workmap)
+
+
+        regProcess = (\gr stack dict workmap edge ->
+                let node = snd3 edge
+                    label = fromJust (Graph.lab gr node)
+
+                    io = argMap label
+                    sortedIns = sortBy (\x y -> compare (fst . thd3 $ x) (fst . thd3 $ y)) (Graph.out orig node)
+                    expectedInput = map (\(a,b,(c,d)) -> (b,d)) sortedIns
+
+                    consume = (\(g,s,d,w) inList ->
+                        if (inList == [])
+                        then if (nodeOutput == 1)
+                             then (g, (node,1):s, d, w)
+                             else initial (g,s,d,w) 
+                        else let i = head inList
+                             in if (head s == i)
+                                then consume (g, tail s, d, w) (tail inList)
+                                else store (g, s, d, w) inList)
+
+                    initial = (\(g,s,d,w) inList ->
+                        let edgemap = Map.toList (fromJust (Map.lookup node usemap))
+                            sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ b)) edgemap
+                            grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted
+                            minimals = map (minimumBy useSort) grouped
+                            usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) minimals)) [1..nodeOutput]
+                            atArg = snd . thd3 $ edge
+                            atArgReuse = length (filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap)
+                            fromStart = fst . snd $ (head (filter (\x -> ((snd . thd3 . fst $ x) == atArg)) minimals))
+                            edgesToRemove = filter (\x -> (snd . thd3 $ x) < upTo) (map fst edgemap)
+
+                            upTo = let shortList = filter (\x -> (snd . thd3 . fst $ x) > atArg && (fst . snd $ x) > fromStart) minimals
+                                   in if (shortList == [])
+                                      then nodeOutput + 1
+                                      else let shortNum = snd . thd3 . fst . head $ shortList
+                                               calc = (\num ->
+                                                    if (filter (\x -> (snd . thd3 . fst $ x) == num - 1) edgemap == [])
+                                                    then calc (num - 1)
+                                                    else num)
+                                               in calc shortNum
+                            index = next upTo g
+
+                            defPartGen = (\num ->
+                                if (num == upTo)
+                                then if (atArg + 1 < upTo)
+                                     then if (atArgReuse > 1)
+                                          then [index!!atArg, "ref"]
+                                          else [index!!atArg, "remove"]
+                                     else []
+                                else if (num `elem` usedArgs)
+                                     then if (num + 1 == atArg &&) 
+                                     else if (num == atArg)
+                                          then if (atArgReuse <= 1 && atArg + 1 == upTo)
+                                               then defPartGen (num+1)
+                                               else if (atArg + 1 < upTo)
+                                                    then [index!!num, "def", "pop"] ++ (defPartGen (num+1))
+                                                    else [index!!num, "def"] ++ (defPartGen (num+1))
+                                          else [index!!num, "def", "pop"] ++ (defPartGen (num+1))
+                                     else ["pop"] ++ (defPartGen (num+1)))
+                            defPart = genPart (defPartGen 1) True
+
+                            maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped
+                            refNodeEdges = map (fst . snd) maxSplit
+                            removeNodeEdges = concat (map (fst . fst) maxSplit)
+
+                            removeList = zip usedArgs removeNodeEdges
+                            removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList
+
+                            refList = zip usedArgs refNodeEdges
+                            refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refPart
+
+                            workingEdge =
+                                let atArgEdges = filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap
+                                    initEdge = fst . head $ (filter (\x -> (snd . thd3 $ x) == atArg &&
+                                                                           (x `notElem` (delete (minimumBy useSort atArgEdges)
+                                                                                                atArgEdges))) (Graph.inn g' node))
+                                    calc = (\e ->
+                                        if (fst3 e == fst3 edge)
+                                        then e
+                                        else calc (head (Graph.inn g' (fst3 e))))
+                                in calc initEdge
+                            w' = Map.insert node workingEdge
+
+                            storedArgs = if (atArgReuse > 1 || atArg + 1 < upTo)
+                                         then filter (< upTo) usedArgs
+                                         else delete atArg (filter (< upTo) usedArgs)
+                            dictAddList = map (\x -> (index!!(x-1), (node,x))) storedArgs
+                            d' = foldl' (\x (y,z) -> Map.insert y z x) d dictAddList
+
+                            stackArgs = atArg:(filter (>= upTo) usedArgs)
+                            stackAddList = map (\x -> (node,x)) stackArgs
+                            s' = stackArgs ++ s
+
+                            edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) g edgesToRemove
+                            g' = graphAddList (defPart:(refPart ++ removePart)) edgesRemoved
+
+                        in (g', s', d', w'))
+
+
+                    store = (\(g,s,d,w) inList ->
+                        let s' = tail s
+                            (node, arg) = head s -- the thing on the stack that shouldnt be there
+                            workEdge = Map.lookup node w
+                            (reqNode, reqArg) = head inList -- what we want on the stack instead
+
+                            index = head (next 1 g)
+                            edgemap = Map.toList (Map.lookup node usemap) -- map of the edges leading into the node
+                            edgesOfArg = filter (\(x,y) -> (snd . thd3 $ x) == arg) edgemap -- edges using the arg we want to get rid of
+                            
+                            removeEdge = maximumBy useSort edgesOfArg
+                            refEdgeList = delete removeEdge edgesOfArg
+
+                            defPart = genPart [index, "def"] True
+                            refPart = genPart [index, "ref"] False
+                            removePart = genPart [index, "remove" False
+                            popPart = genPart ["pop"] True
+
+                        in consume (g', s', d', w') inList
+
+                in consume (gr,stack,dict,workmap) expectedInput)
+
+
+        h = (\gr st di ma edge ->
+                let node = snd3 edge
+                    (gr',st',di',ma') = f gr st di ma node
+                in process gr' st' di' ma' edge)
+
+        f = (\gr st di ma no ->
+                let args = reverse [1..(nodeOutput gr no)]
+                    func = (\(g,s,d,m) a ->
+                        let edge = filter (\x -> fst . thd3 $ x == a) (Graph.out g no)
+                        in if (edge == [])
+                           then (g,s,d,m)
+                           else h gr st di ma (head edge)
+                in foldl' func (gr,st,di,ma) args
+
+        stack = []
+        dictionary = Map.empty
+        workmap = Map.empty
+
+        (graph',stack',dictionary',workmap') =
+            foldl' (\(g,s,d,m) n -> f g s d m n) (graph, stack, dictionary, workmap) nodeList
+
+    in graph'
+
+
+
+    
\ No newline at end of file