Reorganising source code

16 files changed, 0 insertions, 2378 deletions

diff --git a/Library/Command.hs b/Library/Command.hs
deleted file mode 100644
index 47f0537..0000000
--- a/Library/Command.hs
+++ /dev/null
@@ -1,203 +0,0 @@
-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/Cost.hs b/Library/Cost.hs
deleted file mode 100644
index 86cabdc..0000000
--- a/Library/Cost.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-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/Library/Generator.hs b/Library/Generator.hs
deleted file mode 100644
index ef9dfe2..0000000
--- a/Library/Generator.hs
+++ /dev/null
@@ -1,82 +0,0 @@
-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
deleted file mode 100644
index 02a95c0..0000000
--- a/Library/GraphPart.hs
+++ /dev/null
@@ -1,161 +0,0 @@
-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/Library/Object.hs b/Library/Object.hs
deleted file mode 100644
index dd65ded..0000000
--- a/Library/Object.hs
+++ /dev/null
@@ -1,128 +0,0 @@
-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
deleted file mode 100644
index 7494822..0000000
--- a/Library/Parse.hs
+++ /dev/null
@@ -1,75 +0,0 @@
-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
deleted file mode 100644
index 0e7e80a..0000000
--- a/Library/ProofGraph.hs
+++ /dev/null
@@ -1,159 +0,0 @@
-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/Library/Semantic.hs b/Library/Semantic.hs
deleted file mode 100644
index 0f08d52..0000000
--- a/Library/Semantic.hs
+++ /dev/null
@@ -1,360 +0,0 @@
-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/Library/Stack.hs b/Library/Stack.hs
deleted file mode 100644
index 99cd8e1..0000000
--- a/Library/Stack.hs
+++ /dev/null
@@ -1,50 +0,0 @@
-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/Library/Term.hs b/Library/Term.hs
deleted file mode 100644
index be9e53b..0000000
--- a/Library/Term.hs
+++ /dev/null
@@ -1,193 +0,0 @@
-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/Library/TermNet.hs b/Library/TermNet.hs
deleted file mode 100644
index 16b5446..0000000
--- a/Library/TermNet.hs
+++ /dev/null
@@ -1,214 +0,0 @@
-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/Library/Theorem.hs b/Library/Theorem.hs
deleted file mode 100644
index fc66cc2..0000000
--- a/Library/Theorem.hs
+++ /dev/null
@@ -1,19 +0,0 @@
-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
deleted file mode 100644
index d2915e6..0000000
--- a/Library/TypeVar.hs
+++ /dev/null
@@ -1,99 +0,0 @@
-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/Library/Usage.hs b/Library/Usage.hs
deleted file mode 100644
index a307274..0000000
--- a/Library/Usage.hs
+++ /dev/null
@@ -1,80 +0,0 @@
-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/Library/WriteProof.hs b/Library/WriteProof.hs
deleted file mode 100644
index 2c15b74..0000000
--- a/Library/WriteProof.hs
+++ /dev/null
@@ -1,211 +0,0 @@
-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/Library/alternate_multi_command.hs b/Library/alternate_multi_command.hs
deleted file mode 100644
index da49a7d..0000000
--- a/Library/alternate_multi_command.hs
+++ /dev/null
@@ -1,315 +0,0 @@
-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