author | blanchet |
Mon, 07 Nov 2016 14:55:39 +0100 | |
changeset 64469 | 488d4e627238 |
parent 64407 | 5c5b9d945625 |
child 66163 | 45d3d43abee7 |
permissions | -rw-r--r-- |
64389 | 1 |
(* Title: HOL/Nunchaku/Tools/nunchaku.ML |
2 |
Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII |
|
3 |
Copyright 2015, 2016 |
|
4 |
||
5 |
The core of the Nunchaku integration in Isabelle. |
|
6 |
*) |
|
7 |
||
8 |
signature NUNCHAKU = |
|
9 |
sig |
|
10 |
type isa_model = Nunchaku_Reconstruct.isa_model |
|
11 |
||
12 |
datatype mode = Auto_Try | Try | Normal |
|
13 |
||
14 |
type mode_of_operation_params = |
|
15 |
{falsify: bool, |
|
16 |
assms: bool, |
|
17 |
spy: bool, |
|
18 |
overlord: bool, |
|
19 |
expect: string} |
|
20 |
||
21 |
type scope_of_search_params = |
|
22 |
{wfs: ((string * typ) option * bool option) list, |
|
23 |
whacks: (term option * bool) list, |
|
24 |
cards: (typ option * (int option * int option)) list, |
|
25 |
monos: (typ option * bool option) list} |
|
26 |
||
27 |
type output_format_params = |
|
28 |
{verbose: bool, |
|
29 |
debug: bool, |
|
30 |
max_potential: int, |
|
31 |
max_genuine: int, |
|
32 |
evals: term list, |
|
33 |
atomss: (typ option * string list) list} |
|
34 |
||
35 |
type optimization_params = |
|
36 |
{specialize: bool, |
|
37 |
multithread: bool} |
|
38 |
||
39 |
type timeout_params = |
|
40 |
{timeout: Time.time, |
|
41 |
wf_timeout: Time.time} |
|
42 |
||
43 |
type params = |
|
44 |
{mode_of_operation_params: mode_of_operation_params, |
|
45 |
scope_of_search_params: scope_of_search_params, |
|
46 |
output_format_params: output_format_params, |
|
47 |
optimization_params: optimization_params, |
|
48 |
timeout_params: timeout_params} |
|
49 |
||
50 |
val genuineN: string |
|
51 |
val quasi_genuineN: string |
|
52 |
val potentialN: string |
|
53 |
val noneN: string |
|
54 |
val unknownN: string |
|
55 |
val no_nunchakuN: string |
|
56 |
||
57 |
val run_chaku_on_prop: Proof.state -> params -> mode -> int -> term list -> term -> |
|
58 |
string * isa_model option |
|
59 |
val run_chaku_on_subgoal: Proof.state -> params -> mode -> int -> string * isa_model option |
|
60 |
end; |
|
61 |
||
62 |
structure Nunchaku : NUNCHAKU = |
|
63 |
struct |
|
64 |
||
65 |
open Nunchaku_Util; |
|
66 |
open Nunchaku_Collect; |
|
67 |
open Nunchaku_Problem; |
|
68 |
open Nunchaku_Translate; |
|
69 |
open Nunchaku_Model; |
|
70 |
open Nunchaku_Reconstruct; |
|
71 |
open Nunchaku_Display; |
|
72 |
open Nunchaku_Tool; |
|
73 |
||
74 |
datatype mode = Auto_Try | Try | Normal; |
|
75 |
||
76 |
type mode_of_operation_params = |
|
77 |
{falsify: bool, |
|
78 |
assms: bool, |
|
79 |
spy: bool, |
|
80 |
overlord: bool, |
|
81 |
expect: string}; |
|
82 |
||
83 |
type scope_of_search_params = |
|
84 |
{wfs: ((string * typ) option * bool option) list, |
|
85 |
whacks: (term option * bool) list, |
|
86 |
cards: (typ option * (int option * int option)) list, |
|
87 |
monos: (typ option * bool option) list}; |
|
88 |
||
89 |
type output_format_params = |
|
90 |
{verbose: bool, |
|
91 |
debug: bool, |
|
92 |
max_potential: int, |
|
93 |
max_genuine: int, |
|
94 |
evals: term list, |
|
95 |
atomss: (typ option * string list) list}; |
|
96 |
||
97 |
type optimization_params = |
|
98 |
{specialize: bool, |
|
99 |
multithread: bool}; |
|
100 |
||
101 |
type timeout_params = |
|
102 |
{timeout: Time.time, |
|
103 |
wf_timeout: Time.time}; |
|
104 |
||
105 |
type params = |
|
106 |
{mode_of_operation_params: mode_of_operation_params, |
|
107 |
scope_of_search_params: scope_of_search_params, |
|
108 |
output_format_params: output_format_params, |
|
109 |
optimization_params: optimization_params, |
|
110 |
timeout_params: timeout_params}; |
|
111 |
||
112 |
val genuineN = "genuine"; |
|
113 |
val quasi_genuineN = "quasi_genuine"; |
|
114 |
val potentialN = "potential"; |
|
115 |
val noneN = "none"; |
|
116 |
val unknownN = "unknown"; |
|
117 |
||
118 |
val no_nunchakuN = "no_nunchaku"; |
|
119 |
||
120 |
fun str_of_mode Auto_Try = "Auto_Try" |
|
121 |
| str_of_mode Try = "Try" |
|
122 |
| str_of_mode Normal = "Normal"; |
|
123 |
||
124 |
fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns; |
|
125 |
||
126 |
fun has_lonely_bool_var (@{const Pure.conjunction} $ (@{const Trueprop} $ Free _) $ _) = true |
|
127 |
| has_lonely_bool_var _ = false; |
|
128 |
||
129 |
val syntactic_sorts = |
|
130 |
@{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ @{sort numeral}; |
|
131 |
||
132 |
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = subset (op =) (S, syntactic_sorts) |
|
133 |
| has_tfree_syntactic_sort _ = false; |
|
134 |
||
135 |
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort); |
|
136 |
||
137 |
(* Give the soft timeout a chance. *) |
|
138 |
val timeout_slack = seconds 1.0; |
|
139 |
||
140 |
fun run_chaku_on_prop state |
|
141 |
({mode_of_operation_params = {falsify, assms, spy, overlord, expect}, |
|
142 |
scope_of_search_params = {wfs, whacks, cards, monos}, |
|
143 |
output_format_params = {verbose, debug, evals, atomss, ...}, |
|
144 |
optimization_params = {specialize, ...}, |
|
145 |
timeout_params = {timeout, wf_timeout}}) |
|
146 |
mode i all_assms subgoal = |
|
147 |
let |
|
148 |
val ctxt = Proof.context_of state; |
|
149 |
||
150 |
val timer = Timer.startRealTimer () |
|
151 |
||
152 |
val print = writeln; |
|
153 |
val print_n = if mode = Normal then writeln else K (); |
|
154 |
fun print_v f = if verbose then writeln (f ()) else (); |
|
155 |
fun print_d f = if debug then writeln (f ()) else (); |
|
156 |
||
157 |
val das_wort_Model = if falsify then "Countermodel" else "Model"; |
|
158 |
val das_wort_model = if falsify then "countermodel" else "model"; |
|
159 |
||
160 |
val tool_params = {overlord = overlord, debug = debug, specialize = specialize, |
|
161 |
timeout = timeout}; |
|
162 |
||
163 |
fun run () = |
|
164 |
let |
|
165 |
val outcome as (outcome_code, _) = |
|
166 |
let |
|
167 |
val (poly_axioms, isa_problem as {sound, complete, ...}) = |
|
168 |
isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals |
|
169 |
(if assms then all_assms else []) subgoal; |
|
170 |
val _ = print_d (fn () => "*** Isabelle problem ***\n" ^ |
|
171 |
str_of_isa_problem ctxt isa_problem); |
|
172 |
val ugly_nun_problem = nun_problem_of_isa ctxt isa_problem; |
|
173 |
val _ = print_d (fn () => "*** Ugly Nunchaku problem ***\n" ^ |
|
174 |
str_of_nun_problem ugly_nun_problem); |
|
175 |
val (nice_nun_problem, pool) = nice_nun_problem ugly_nun_problem; |
|
176 |
val _ = print_d (fn () => "*** Nice Nunchaku problem ***\n" ^ |
|
177 |
str_of_nun_problem nice_nun_problem); |
|
178 |
||
179 |
fun print_any_hints () = |
|
180 |
if has_lonely_bool_var subgoal then |
|
181 |
print "Hint: Maybe you forgot a colon after the lemma's name?" |
|
182 |
else if has_syntactic_sorts subgoal then |
|
183 |
print "Hint: Maybe you forgot a type constraint?" |
|
184 |
else |
|
185 |
(); |
|
186 |
||
187 |
fun get_isa_model_opt output = |
|
188 |
let |
|
189 |
val nice_nun_model = nun_model_of_str output; |
|
190 |
val _ = print_d (fn () => "*** Nice Nunchaku model ***\n" ^ |
|
191 |
str_of_nun_model nice_nun_model); |
|
192 |
val ugly_nun_model = ugly_nun_model pool nice_nun_model; |
|
193 |
val _ = print_d (fn () => "*** Ugly Nunchaku model ***\n" ^ |
|
194 |
str_of_nun_model ugly_nun_model); |
|
195 |
||
196 |
val pat_completes = pat_completes_of_isa_problem isa_problem; |
|
197 |
val isa_model = isa_model_of_nun ctxt pat_completes atomss ugly_nun_model; |
|
198 |
val _ = print_d (fn () => "*** Isabelle model ***\n" ^ |
|
199 |
str_of_isa_model ctxt isa_model); |
|
200 |
in |
|
201 |
isa_model |
|
202 |
end; |
|
203 |
||
204 |
fun isa_model_opt output = |
|
205 |
if debug then SOME (get_isa_model_opt output) else try get_isa_model_opt output; |
|
206 |
||
207 |
val model_str = isa_model_opt #> pretty_of_isa_model_opt ctxt #> Pretty.string_of; |
|
208 |
||
209 |
fun unsat_means_theorem () = |
|
210 |
null whacks andalso null cards andalso null monos; |
|
211 |
||
212 |
fun unknown () = |
|
64407 | 213 |
(print_n ("No " ^ das_wort_model ^ " can be found\n\ |
214 |
\The problem lies outside Nunchaku's fragment, or the Nunchaku backends are not \ |
|
215 |
\installed properly"); |
|
64389 | 216 |
(unknownN, NONE)); |
217 |
||
218 |
fun unsat_or_unknown complete = |
|
219 |
if complete then |
|
220 |
(print_n ("No " ^ das_wort_model ^ " exists" ^ |
|
64407 | 221 |
(if falsify andalso unsat_means_theorem () then "\nThe goal is a theorem" |
222 |
else "")); |
|
64389 | 223 |
(noneN, NONE)) |
224 |
else |
|
225 |
unknown (); |
|
226 |
||
227 |
fun sat_or_maybe_sat sound output = |
|
228 |
let val header = if sound then das_wort_Model else "Potential " ^ das_wort_model in |
|
229 |
(case (null poly_axioms, none_true wfs) of |
|
230 |
(true, true) => |
|
231 |
(print (header ^ ":\n" ^ |
|
232 |
model_str output); print_any_hints (); |
|
233 |
(genuineN, isa_model_opt output)) |
|
234 |
| (no_poly, no_wf) => |
|
235 |
let |
|
236 |
val ignorings = [] |
|
237 |
|> not no_poly ? cons "polymorphic axioms" |
|
238 |
|> not no_wf ? cons "unchecked well-foundedness"; |
|
239 |
in |
|
240 |
(print (header ^ " (ignoring " ^ space_implode " and " ignorings ^ "):\n" ^ |
|
241 |
model_str output ^ |
|
242 |
(if no_poly then |
|
243 |
"" |
|
244 |
else |
|
245 |
"\nIgnored axioms:\n" ^ |
|
246 |
cat_lines (map (prefix " " o Syntax.string_of_term ctxt) poly_axioms))); |
|
247 |
print_any_hints (); |
|
248 |
(quasi_genuineN, isa_model_opt output)) |
|
249 |
end) |
|
250 |
end; |
|
251 |
in |
|
252 |
(case solve_nun_problem tool_params nice_nun_problem of |
|
253 |
Unsat => unsat_or_unknown complete |
|
254 |
| Sat (output, _) => sat_or_maybe_sat sound output |
|
255 |
| Unknown NONE => unknown () |
|
256 |
| Unknown (SOME (output, _)) => sat_or_maybe_sat false output |
|
257 |
| Timeout => (print_n "Time out"; (unknownN, NONE)) |
|
258 |
| Nunchaku_Var_Not_Set => |
|
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
259 |
(print_n ("Variable $" ^ nunchaku_home_env_var ^ " not set"); (unknownN, NONE)) |
64389 | 260 |
| Nunchaku_Cannot_Execute => |
261 |
(print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE)) |
|
262 |
| Nunchaku_Not_Found => |
|
263 |
(print_n "External tool \"nunchaku\" not found"; (unknownN, NONE)) |
|
264 |
| CVC4_Cannot_Execute => |
|
265 |
(print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE)) |
|
266 |
| CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE)) |
|
267 |
| Unknown_Error (code, msg) => |
|
268 |
(print_n ("Unknown error: " ^ msg ^ |
|
269 |
(if code = 0 then "" else " (code " ^ string_of_int code ^ ")")); |
|
270 |
(unknownN, NONE))) |
|
271 |
end |
|
272 |
handle |
|
273 |
CYCLIC_DEPS () => |
|
274 |
(print_n "Cyclic dependencies (or bug in Nunchaku)"; (unknownN, NONE)) |
|
275 |
| TOO_DEEP_DEPS () => |
|
276 |
(print_n "Too deep dependencies (or bug in Nunchaku)"; (unknownN, NONE)) |
|
277 |
| TOO_META t => |
|
278 |
(print_n ("Formula too meta for Nunchaku:\n" ^ Syntax.string_of_term ctxt t); |
|
279 |
(unknownN, NONE)) |
|
280 |
| UNEXPECTED_POLYMORPHISM t => |
|
281 |
(print_n ("Unexpected polymorphism in term\n" ^ Syntax.string_of_term ctxt t); |
|
282 |
(unknownN, NONE)) |
|
283 |
| UNEXPECTED_VAR t => |
|
284 |
(print_n ("Unexpected schematic variables in term\n" ^ Syntax.string_of_term ctxt t); |
|
285 |
(unknownN, NONE)) |
|
286 |
| UNSUPPORTED_FUNC t => |
|
287 |
(print_n ("Unsupported low-level constant in problem: " ^ Syntax.string_of_term ctxt t); |
|
288 |
(unknownN, NONE)); |
|
289 |
in |
|
290 |
if expect = "" orelse outcome_code = expect then outcome |
|
291 |
else error ("Unexpected outcome: " ^ quote outcome_code) |
|
292 |
end; |
|
293 |
||
294 |
val _ = spying spy (fn () => (state, i, "starting " ^ str_of_mode mode ^ " mode")); |
|
295 |
||
296 |
val outcome as (outcome_code, _) = |
|
297 |
Timeout.apply (Time.+ (timeout, timeout_slack)) run () |
|
298 |
handle Timeout.TIMEOUT _ => (print_n "Time out"; (unknownN, NONE)); |
|
299 |
||
300 |
val _ = print_v (fn () => "Total time: " ^ string_of_time (Timer.checkRealTimer timer)); |
|
301 |
||
302 |
val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code)); |
|
303 |
in |
|
304 |
if expect = "" orelse outcome_code = expect then outcome |
|
305 |
else error ("Unexpected outcome: " ^ quote outcome_code) |
|
306 |
end; |
|
307 |
||
308 |
fun run_chaku_on_subgoal state params mode i = |
|
309 |
let |
|
310 |
val ctxt = Proof.context_of state; |
|
311 |
val goal = Thm.prop_of (#goal (Proof.raw_goal state)); |
|
312 |
in |
|
313 |
if Logic.count_prems goal = 0 then |
|
314 |
(writeln "No subgoal!"; (noneN, NONE)) |
|
315 |
else |
|
316 |
let |
|
317 |
val subgoal = fst (Logic.goal_params goal i); |
|
318 |
val all_assms = map Thm.term_of (Assumption.all_assms_of ctxt); |
|
319 |
in |
|
320 |
run_chaku_on_prop state params mode i all_assms subgoal |
|
321 |
end |
|
322 |
end; |
|
323 |
||
324 |
end; |