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
open Lang
open Lang.F
open Tactical
open Conditions
type lookup = {
target : Lang.F.term ;
mutable marked : Tset.t ;
}
let lookup_term env e =
let rec walk env e =
if e == env.target then raise Exit ;
if not (Tset.mem e env.marked) then
begin
env.marked <- Tset.add e env.marked ;
Lang.F.lc_iter (walk env) e ;
end
in
try walk env e ; false
with Exit -> true
let occurs_x x a = F.Vars.mem x (F.vars a)
let occurs_y x p = F.Vars.mem x (F.varsp p)
let occurs_e a b = lookup_term { target = a ; marked = Tset.empty } b
let occurs_p a p = occurs_e a (F.e_prop p)
let occurs_q p q = occurs_e (F.e_prop p) (F.e_prop q)
let lookup_step env queue s =
match s.condition with
| State _ -> Empty
| Probe(_,t) ->
if t == env.target then Inside(Step s,env.target) else Empty
| When p | Have p | Init p | Core p | Type p ->
let p = Lang.F.e_prop p in
if p == env.target then Clause(Step s) else
if lookup_term env p then Inside(Step s,env.target) else Empty
| Branch(c,sa,sb) ->
let p = Lang.F.e_prop c in
if lookup_term env p then Inside(Step s,env.target) else
( Queue.add sa queue ; Queue.add sb queue ; Empty )
| Either cs ->
List.iter (fun s -> Queue.add s queue) cs ; Empty
exception Found of selection
let lookup_sequence env queue seq =
Conditions.iter
(fun s ->
match lookup_step env queue s with
| Empty -> ()
| sel -> raise (Found sel)
) seq
let select_e (sequence,goal) e =
let g = Lang.F.e_prop goal in
if g == e then Clause(Goal goal) else
let env = { target = e ; marked = Tset.empty } in
if lookup_term env g then Inside(Goal goal,e) else
try
let queue = Queue.create () in
lookup_sequence env queue sequence ;
while not (Queue.is_empty queue) do
lookup_sequence env queue (Queue.pop queue)
done ; Empty
with Found sel -> sel
let select_p seq p = select_e seq (F.e_prop p)
type argument = ARG: 'a field * 'a -> argument
type strategy = {
priority : float ;
tactical : tactical ;
selection : selection ;
arguments : argument list ;
} and t = strategy
let highest a b = Stdlib.compare b.priority a.priority
class pool =
object
val pool : strategy Vector.t = Vector.create ()
method add = Vector.add pool
method sort =
let hs = Vector.to_array pool in
Array.stable_sort highest hs ; hs
end
class type heuristic =
object
method id : string
method title : string
method descr : string
method search : (strategy -> unit) -> sequent -> unit
end
module Tmap = Map.Make(String)
let registry = ref Tmap.empty
let register s =
let id = s#id in
if Tmap.mem id !registry then
Wp_parameters.error "Strategy #%s already registered (skipped)" id
else
registry := Tmap.add id (s :> heuristic) !registry
let export s = register s ; (s :> heuristic)
let lookup ~id = Tmap.find id !registry
let iter f = Tmap.iter (fun _ s -> f s) !registry
let arg fd v = ARG(fd,v)
let set_arg (tactical : #tactical) =
function ARG(fd,v) -> tactical#set_field fd v
let set_args tactical arguments =
List.iter (set_arg tactical) arguments
let make tactical ?(priority=1.0) ?(arguments=[]) selection =
{ priority ; tactical ; selection ; arguments }