diff options
Diffstat (limited to 'writetest.hs')
-rw-r--r-- | writetest.hs | 55 |
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) |