1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
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
"\"c\"","\"x\"","const","\"t1\"","typeOp","nil","opType","1","def","constTerm","0","def","defineConst",
-- hypothesis list for theorem
"nil",
-- equals name
"\"=\"","const",
-- equals type
"\"->\"","typeOp","1","ref","\"->\"","typeOp","1","ref","\"bool\"","typeOp","nil","opType","nil","cons","cons","opType",
"nil","cons","cons","opType",
-- equals term
"constTerm",
-- the constant
"\"c\"","const","1","remove","constTerm",
-- construct the equation of constant = variable
"appTerm",
"0","remove",
"appTerm",
"thm","pop"]
list2 = ["\"x\"", "const", "\"bool\"", "typeOp", "nil", "opType", "constTerm", "assume", "1", "def", "1", "remove", "deductAntisym"]
singleNodes = (\g -> filter (\x -> nodeOutput g x == 1 && Graph.indeg g x > 1) (Graph.nodes g))
singleNodeSet = (\g -> Set.fromList (singleNodes g))
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)
|
