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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
open Lang
open Tactical
open Definitions
module L = Qed.Logic
let named l = {
vid = l.l_name ;
title = l.l_name ;
descr = Pretty_utils.to_string F.pp_pred l.l_lemma ;
value = l ;
}
class browser ?on_cluster f cluster =
object(self)
inherit Definitions.visitor cluster
method section _ = ()
method on_library _ = ()
method on_type _ _ = ()
method on_comp _ _ = ()
method on_icomp _ _ = ()
method on_dfun _ = ()
method! vtypes = ()
method! vsymbols = ()
method! vself = self#vlemmas
method on_cluster c =
match on_cluster with
| None -> (new browser ~on_cluster:self#vcluster f c)#vlemmas
| Some visitor -> visitor c
method on_dlemma l = f (named l)
end
let browse f s =
if WpContext.is_defined () then
begin
let main = Definitions.cluster ~id:"browser" () in
let visitor = new browser f main in
let selection = Tactical.selected s in
visitor#vterm selection
end
type env = {
feedback : Tactical.feedback ;
lemma : F.pred ;
descr : string ;
}
type lemma = Definitions.dlemma Tactical.named
let find thm = named (Definitions.find_name thm)
let search,psearch =
Tactical.search ~id:"lemma" ~title:"Lemma" ~descr:"Lemma to Instantiate"
~browse ~find ()
let fresh pool { l_forall ; l_lemma } =
let vars = List.map (F.alpha pool) l_forall in
let sigma = Lang.subst l_forall (List.map F.e_var vars) in
vars , F.p_subst sigma l_lemma
class instance =
object(self)
inherit Tactical.make ~id:"Wp.lemma"
~title:"Lemma"
~descr:"Search & Instantiate Lemma"
~params:(psearch :: TacInstance.params)
method private hide (feedback : Tactical.feedback) fields =
List.iter
(fun fd -> feedback#update_field ~enabled:false fd)
fields
method private wrap env vars fields =
match vars , fields with
| x::xs , fd::fields ->
let title = Pretty_utils.to_string F.pp_var x in
let value = self#get_field fd in
let tau = F.tau_of_var x in
env.feedback#update_field ~enabled:true
~title ~tooltip:env.descr
~range:(match tau with L.Int -> true | _ -> false)
~filter:(TacInstance.filter tau) fd ;
let bindings,lemma = self#wrap env xs fields in
(x,value)::bindings , lemma
| _ ->
self#hide env.feedback fields ;
[] , F.p_forall vars env.lemma
method select feedback = function
| Empty -> Not_applicable
| selection ->
begin match self#get_field search with
| None ->
self#hide feedback TacInstance.fields ;
Not_configured
| Some Tactical.{ title ; value = dlem } ->
let fields = TacInstance.fields in
let vars,lemma = fresh feedback#pool dlem in
let descr = Pretty_utils.to_string F.pp_pred lemma in
let bindings,lemma =
self#wrap { feedback ; descr ; lemma } vars fields in
match TacInstance.cardinal 1000 bindings with
| Some n ->
if n > 1 then
feedback#set_descr "Generates %d instances" n ;
let at = Tactical.at selection in
Applicable
(TacInstance.instance_have ~title ?at bindings lemma)
| None ->
feedback#set_error "More than 1,000 instances" ;
Not_configured
end
end
let tactical = Tactical.export (new instance)
let strategy ?(priority=1.0) ?(at = Tactical.int 0) lemma values =
Strategy.{
priority ; tactical ; selection = at ;
arguments =
arg search (try Some (find lemma) with Not_found -> None) ::
TacInstance.wrap TacInstance.fields values ;
}