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