summaryrefslogtreecommitdiff
path: root/Graph.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Graph.hs')
-rw-r--r--Graph.hs115
1 files changed, 0 insertions, 115 deletions
diff --git a/Graph.hs b/Graph.hs
deleted file mode 100644
index 7b034bc..0000000
--- a/Graph.hs
+++ /dev/null
@@ -1,115 +0,0 @@
-import System( getArgs )
-import Text.Printf
-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 ProofGraph
-import qualified ProofGraph as Graph
-import Stack( Stack, at, (<:>) )
-import qualified Stack as Stack
-import Parse
-
-
-
-type GraphState = (Graph String,
- Stack (Node String),
- Map Int (Node 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 -> Graph String -> Stack (Node String) -> (Graph String, Stack (Node String))
-process str io graph stack =
- let argList = map (\x -> fromJust (stack `at` x)) [0..((args io) - 1)]
- node = Node str (Set.fromList argList)
- nodeList = replicate (results io) node
- stack' = foldr (<:>) (Stack.pop (args io) stack) nodeList
- graph' = Graph.insert node graph
- in (graph',stack')
-
-
-
-parse :: GraphState -> String -> GraphState
-parse gs@(graph,stack,dictionary) str =
- case str of
- "def" -> let num = read . contents . 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 = read . contents . fromJust $ stack `at` 0
- node = fromJust (Map.lookup num dictionary)
- stack' = node <:> (Stack.pop 1 stack)
- in (graph, stack', dictionary)
-
- "remove" -> let num = read . contents . 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 = Node n Set.empty
- stack' = node <:> stack
- in (graph, stack', dictionary)
-
- x -> let (graph', stack') = process x (argMap x) graph stack
- in (graph', stack', dictionary)
-
-
-
-doGraphGen :: [String] -> Graph String
-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) -> g
-
-
-
-main = do
- args <- getArgs
- list <- getLines $ head args
- let result = doGraphGen (map (stripReturn) list)
- printf $ show result
-