1 files changed, 46 insertions, 9 deletions
diff --git a/writetest.hs b/writetest.hs
index 81df3d7..0a05ccb 100644
--- a/writetest.hs
+++ b/writetest.hs
@@ -1,9 +1,20 @@
 import Library.WriteProof
 import Library.ProofGraph
+import Library.GraphPart
+import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge )
+import qualified Data.Graph.Inductive.Graph as Graph
+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.Usage
+import Library.Parse
+
 
 
 list = [-- create a var term, define a constant to it
-        "\"const\"","\"x\"","const","\"t1\"","typeOp","nil","opType","1","def","constTerm","0","def","defineConst",
+        "\"c\"","\"x\"","const","\"t1\"","typeOp","nil","opType","1","def","constTerm","0","def","defineConst",
         
         -- hypothesis list for theorem
         "nil",
@@ -19,7 +30,7 @@ list = [-- create a var term, define a constant to it
         "constTerm",
 
         -- the constant
-        "\"const\"","const","1","remove","constTerm",
+        "\"c\"","const","1","remove","constTerm",
 
         -- construct the equation of constant = variable
         "appTerm",
@@ -28,16 +39,42 @@ list = [-- create a var term, define a constant to it
 
         "thm","pop"]
 
-graph = doGraphGen list
+list2 = ["\"x\"", "const", "\"bool\"", "typeOp", "nil", "opType", "constTerm", "assume", "1", "def", "1", "remove", "deductAntisym"]
+
 
-fst3 :: (a,b,c) -> a
-fst3 (a,_,_) = a
+singleNodes = (\g -> filter (\x -> nodeOutput g x == 1 && Graph.indeg g x > 1) (Graph.nodes g))
+singleNodeSet = (\g -> Set.fromList (singleNodes g))
 
-snd3 :: (a,b,c) -> b
-snd3 (_,b,_) = b
 
-thd3 :: (a,b,c) -> c
-thd3 (_,_,c) = c
+graph = doGraphGen list
+graph2 = doGraphGen list2
+
 
 edgeCheck :: (Ord d) => (a,b,(c,d)) -> (e,f,(g,d)) -> Ordering
 edgeCheck = (\a b -> compare (snd . thd3 $ a) (snd . thd3 $ b))
+
+
+f :: PGraph -> Node -> Map (LEdge (Int,Int)) Int -> PGraph
+f = (\graph node edgemap ->
+        let index = head (next 1 graph)
+            edgeList = Map.toList edgemap
+
+            sortFunc = (\(w,x) (y,z) -> compare x z)
+
+            defEdge = fst (minimumBy sortFunc edgeList)
+            refEdgeList = map fst (filter (\x -> fst x /= defEdge && fst x /= removeEdge) edgeList)
+            removeEdge = fst (maximumBy sortFunc edgeList)
+
+            defPart = genPart [index, "def"] True
+            refPart = genPart [index, "ref"] False
+            removePart = genPart [index, "remove"] False
+
+            defNode = (fst3 defEdge,1)
+            refNodeList = map (\x -> (fst3 x,1)) refEdgeList
+            removeNode = (fst3 removeEdge,1)
+
+            edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) graph edgeList
+            partsAdded = graphAddList [(defPart, Just (node,1) , [defNode]),
+                                       (refPart, Nothing, refNodeList),
+                                       (removePart, Nothing, [removeNode])] edgesRemoved
+        in partsAdded)