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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
import System.Environment( getArgs )
import Text.Printf
import Parse
import ProofGraph
import GraphPart
import TermNet( TermNet )
import qualified TermNet as TermNet
import qualified Data.Graph.Inductive.Graph as Graph
data Step = Step { from :: Node
, to :: Node
, sub :: Substitution }
createSubst :: Theorem -> Theorem -> Maybe Substitution
createSubst one two =
let alreadyMatched = (\x y m -> (Map.member x m || y `elem` Map.elems m) && Map.lookup x m /= Just y)
f = (\x y tymap varmap ->
case (x,y) of
(TConst a1 ty1, TConst a2 ty2) ->
if (alreadyMatch ty1 ty2 tymap || a1 /= a2)
then Nothing
else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
in Just (tymap', varmap')
(TApp a1 b1, TApp a2 b2) ->
do (tymap', varmap') <- f a1 a2 tymap varmap
f b1 b2 tymap' varmap'
(TAbs (TVar (Var n1 ty1)) b1, TAbs (TVar (Var n2 ty2)) b2) ->
if (alreadyMatched ty1 ty2 tymap || alreadyMatched n1 n2 varmap)
then Nothing
else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
varmap' = if (n1 == n2) then varmap else Map.insert n1 n2 varmap
in f b1 b2 tymap' varmap'
(TVar (Var n1 ty1), TVar (Var n2 ty2)) ->
if (alreadyMatched ty1 ty2 tymap || alreadyMatched n1 n2 varmap)
then Nothing
else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
varmap' = if (n1 == n2) then varmap else Map.insert n1 n2 varmap
in Just (tymap', varmap')
(other, combination) -> Nothing)
g = (\x y tymap varmap ->
let (hyp1,hyp2) = (Set.fromList . thmHyp $ x, Set.fromList . thmHyp $ y)
if (hyp1 == [])
then f (thmCon x) (thmCon y) tymap varmap
else do (tymap', varmap') <- f (head hyp1) (head hyp2) tymap varmap
g (Theorem (Set.fromList . tail $ hyp1) (thmCon x))
(Theorem (Set.fromList . tail $ hyp2) (thmCon y))
tymap' varmap')
maps = g one two Map.empty Map.empty
in if (Set.size . thmHyp $ one /= Set.size . thmHyp $ two || isNothing maps)
then Nothing
else do (t,v) <- maps
return (Map.toList t, Map.toList v)
checkNode :: PGraph -> TermNet -> Node -> (TermNet, Maybe (GraphPart, GraphPart))
checkNode graph termnet node =
let (termnet', list) = TermNet.addThm termnet graph node
(working, possibles) = partition (\x -> snd x == node) list
canBeSubbed = (\inn out ->
if (inn == [])
then out
else let sub = createSubst (fst working) (fst . head $ inn)
out' = if (isNothing sub)
then out
else (Step (snd working) (snd . head $ inn) (fromJust sub)) : out
in canBeSubbed (tail inn) out'
maxPositiveBenefit = (\list ->
let sortVal = (\x -> (size . snd x) - (addedSize (fst x) graph) - (overlap (fst x) (snd x)))
sorted = sortBy (\x y -> compare (sortVal x) (sortVal y)) list
check = head sorted
in if (sortVal check > 0) then check else Nothing)
step = maxPositiveBenefit . (map (stepGen graph)) $ (canBeSubbed possibles [])
in (termnet', step)
stepGen :: PGraph -> Step -> (GraphPart, GraphPart)
stepGen graph step =
let unused = graphPart (findUnused graph (Graph.suc graph (to step))) [] Nothing Nothing
base = doGraphGen (substitutionGen . sub $ step)
num = Graph.newNodes 1 base
node = (num, "subst")
cons = head (filter (\x -> Graph.indeg base x == 0) (Graph.nodes base))
edge = (num, cons, (2,1))
substGraph = (Graph.insEdge edge) . (Graph.insNode node) $ base
subst = makeGraphPart substGraph (Just (node,1)) (Just (node,1))
in (subst, unused)
findUnused :: PGraph -> [Node] -> [Node]
findUnused graph nodeList =
let nextLayer = concat . (map (Graph.suc graph)) $ nodeList
unused = filter (\x -> all (\y -> y `elem` nodeList) (Graph.pre graph x)) nextLayer
in nodeList ++ (findUnused graph usused)
doMeaningSubst :: PGraph -> PGraph
doMeaningSubst graph =
let f = (\g termnet nodeList ->
if (nodeList == [])
then g
else let working = head nodeList
(termnet', step) = checkNode g termnet working
(g', nodeList') = if (isNothing step)
then (g, nodeList)
else let (subst, unused) = fromJust step
in ((graphAdd subst () ()) . (graphDel unused) $ g, nodeList \\ (nodes unused))
in f g' termnet' nodeList')
in f graph TermNet.empty (Graph.nodes graph)
main = do
args <- getArgs
list <- getLines (head args)
let graph = doGraphGen (map stripReturn list)
result = doMeaningSubst graph
printf $ (show result) ++ "\n"
|
