author  blanchet 
Fri, 08 Sep 2017 00:02:52 +0200  
changeset 66632  6950d3da13f8 
parent 66627  4145169ae609 
child 66646  383d8e388d1b 
permissions  rwrr 
64389  1 
(* Title: HOL/Nunchaku/Tools/nunchaku.ML 
66614
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 12 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 12 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, 

66627  25 
min_bound: int, 
26 
max_bound: int option, 

66625  27 
bound_increment: int, 
64389  28 
cards: (typ option * (int option * int option)) list, 
29 
monos: (typ option * bool option) list} 

30 

31 
type output_format_params = 

32 
{verbose: bool, 

33 
debug: bool, 

34 
max_potential: int, 

35 
max_genuine: int, 

36 
evals: term list, 

37 
atomss: (typ option * string list) list} 

38 

39 
type optimization_params = 

40 
{specialize: bool, 

41 
multithread: bool} 

42 

43 
type timeout_params = 

44 
{timeout: Time.time, 

45 
wf_timeout: Time.time} 

46 

47 
type params = 

48 
{mode_of_operation_params: mode_of_operation_params, 

49 
scope_of_search_params: scope_of_search_params, 

50 
output_format_params: output_format_params, 

51 
optimization_params: optimization_params, 

52 
timeout_params: timeout_params} 

53 

54 
val genuineN: string 

55 
val quasi_genuineN: string 

56 
val potentialN: string 

57 
val noneN: string 

58 
val unknownN: string 

59 
val no_nunchakuN: string 

60 

61 
val run_chaku_on_prop: Proof.state > params > mode > int > term list > term > 

62 
string * isa_model option 

63 
val run_chaku_on_subgoal: Proof.state > params > mode > int > string * isa_model option 

64 
end; 

65 

66 
structure Nunchaku : NUNCHAKU = 

67 
struct 

68 

69 
open Nunchaku_Util; 

70 
open Nunchaku_Collect; 

71 
open Nunchaku_Problem; 

72 
open Nunchaku_Translate; 

73 
open Nunchaku_Model; 

74 
open Nunchaku_Reconstruct; 

75 
open Nunchaku_Display; 

76 
open Nunchaku_Tool; 

77 

78 
datatype mode = Auto_Try  Try  Normal; 

79 

80 
type mode_of_operation_params = 

66163  81 
{solvers: string list, 
82 
falsify: bool, 

64389  83 
assms: bool, 
84 
spy: bool, 

85 
overlord: bool, 

86 
expect: string}; 

87 

88 
type scope_of_search_params = 

89 
{wfs: ((string * typ) option * bool option) list, 

90 
whacks: (term option * bool) list, 

66627  91 
min_bound: int, 
92 
max_bound: int option, 

66625  93 
bound_increment: int, 
64389  94 
cards: (typ option * (int option * int option)) list, 
95 
monos: (typ option * bool option) list}; 

96 

97 
type output_format_params = 

98 
{verbose: bool, 

99 
debug: bool, 

100 
max_potential: int, 

101 
max_genuine: int, 

102 
evals: term list, 

103 
atomss: (typ option * string list) list}; 

104 

105 
type optimization_params = 

106 
{specialize: bool, 

107 
multithread: bool}; 

108 

109 
type timeout_params = 

110 
{timeout: Time.time, 

111 
wf_timeout: Time.time}; 

112 

113 
type params = 

114 
{mode_of_operation_params: mode_of_operation_params, 

115 
scope_of_search_params: scope_of_search_params, 

116 
output_format_params: output_format_params, 

117 
optimization_params: optimization_params, 

118 
timeout_params: timeout_params}; 

119 

120 
val genuineN = "genuine"; 

121 
val quasi_genuineN = "quasi_genuine"; 

122 
val potentialN = "potential"; 

123 
val noneN = "none"; 

124 
val unknownN = "unknown"; 

125 

126 
val no_nunchakuN = "no_nunchaku"; 

127 

128 
fun str_of_mode Auto_Try = "Auto_Try" 

129 
 str_of_mode Try = "Try" 

130 
 str_of_mode Normal = "Normal"; 

131 

132 
fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns; 

133 

134 
fun has_lonely_bool_var (@{const Pure.conjunction} $ (@{const Trueprop} $ Free _) $ _) = true 

135 
 has_lonely_bool_var _ = false; 

136 

137 
val syntactic_sorts = 

138 
@{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ @{sort numeral}; 

139 

140 
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = subset (op =) (S, syntactic_sorts) 

141 
 has_tfree_syntactic_sort _ = false; 

142 

143 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort); 

144 

66617  145 
val unprefix_error = 
66620  146 
perhaps (try (unprefix "failure: ")) 
147 
#> perhaps (try (unprefix "Error: ")); 

66617  148 

64389  149 
(* Give the soft timeout a chance. *) 
150 
val timeout_slack = seconds 1.0; 

151 

152 
fun run_chaku_on_prop state 

66163  153 
({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect}, 
66627  154 
scope_of_search_params = {wfs, whacks, min_bound, max_bound, bound_increment, cards, monos}, 
64389  155 
output_format_params = {verbose, debug, evals, atomss, ...}, 
156 
optimization_params = {specialize, ...}, 

157 
timeout_params = {timeout, wf_timeout}}) 

158 
mode i all_assms subgoal = 

159 
let 

160 
val ctxt = Proof.context_of state; 

161 

162 
val timer = Timer.startRealTimer () 

163 

164 
val print = writeln; 

165 
val print_n = if mode = Normal then writeln else K (); 

166 
fun print_v f = if verbose then writeln (f ()) else (); 

167 
fun print_d f = if debug then writeln (f ()) else (); 

168 

169 
val das_wort_Model = if falsify then "Countermodel" else "Model"; 

170 
val das_wort_model = if falsify then "countermodel" else "model"; 

171 

66163  172 
val tool_params = 
66627  173 
{solvers = solvers, overlord = overlord, min_bound = min_bound, max_bound = max_bound, 
66625  174 
bound_increment = bound_increment, debug = debug, specialize = specialize, 
66163  175 
timeout = timeout}; 
64389  176 

177 
fun run () = 

178 
let 

179 
val outcome as (outcome_code, _) = 

180 
let 

181 
val (poly_axioms, isa_problem as {sound, complete, ...}) = 

182 
isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals 

183 
(if assms then all_assms else []) subgoal; 

184 
val _ = print_d (fn () => "*** Isabelle problem ***\n" ^ 

185 
str_of_isa_problem ctxt isa_problem); 

186 
val ugly_nun_problem = nun_problem_of_isa ctxt isa_problem; 

187 
val _ = print_d (fn () => "*** Ugly Nunchaku problem ***\n" ^ 

188 
str_of_nun_problem ugly_nun_problem); 

189 
val (nice_nun_problem, pool) = nice_nun_problem ugly_nun_problem; 

190 
val _ = print_d (fn () => "*** Nice Nunchaku problem ***\n" ^ 

191 
str_of_nun_problem nice_nun_problem); 

192 

193 
fun print_any_hints () = 

194 
if has_lonely_bool_var subgoal then 

195 
print "Hint: Maybe you forgot a colon after the lemma's name?" 

196 
else if has_syntactic_sorts subgoal then 

197 
print "Hint: Maybe you forgot a type constraint?" 

198 
else 

199 
(); 

200 

201 
fun get_isa_model_opt output = 

202 
let 

203 
val nice_nun_model = nun_model_of_str output; 

204 
val _ = print_d (fn () => "*** Nice Nunchaku model ***\n" ^ 

205 
str_of_nun_model nice_nun_model); 

206 
val ugly_nun_model = ugly_nun_model pool nice_nun_model; 

207 
val _ = print_d (fn () => "*** Ugly Nunchaku model ***\n" ^ 

208 
str_of_nun_model ugly_nun_model); 

209 

210 
val pat_completes = pat_completes_of_isa_problem isa_problem; 

66623  211 
val raw_isa_model = isa_model_of_nun ctxt pat_completes atomss ugly_nun_model; 
212 
val _ = print_d (fn () => "*** Raw Isabelle model ***\n" ^ 

213 
str_of_isa_model ctxt raw_isa_model); 

214 

215 
val cleaned_isa_model = clean_up_isa_model ctxt raw_isa_model; 

216 
val _ = print_d (fn () => "*** Cleanedup Isabelle model ***\n" ^ 

217 
str_of_isa_model ctxt cleaned_isa_model); 

64389  218 
in 
66623  219 
cleaned_isa_model 
64389  220 
end; 
221 

222 
fun isa_model_opt output = 

223 
if debug then SOME (get_isa_model_opt output) else try get_isa_model_opt output; 

224 

225 
val model_str = isa_model_opt #> pretty_of_isa_model_opt ctxt #> Pretty.string_of; 

226 

227 
fun unsat_means_theorem () = 

228 
null whacks andalso null cards andalso null monos; 

229 

230 
fun unknown () = 

66617  231 
(print_n ("No " ^ das_wort_model ^ " found"); (unknownN, NONE)); 
64389  232 

66620  233 
fun unsat_or_unknown solver complete = 
64389  234 
if complete then 
66620  235 
(print_n ("No " ^ das_wort_model ^ " exists (according to " ^ solver ^ ")" ^ 
64407  236 
(if falsify andalso unsat_means_theorem () then "\nThe goal is a theorem" 
237 
else "")); 

64389  238 
(noneN, NONE)) 
239 
else 

240 
unknown (); 

241 

66620  242 
fun sat_or_maybe_sat solver sound output = 
64389  243 
let val header = if sound then das_wort_Model else "Potential " ^ das_wort_model in 
244 
(case (null poly_axioms, none_true wfs) of 

245 
(true, true) => 

66620  246 
(print (header ^ " (according to " ^ solver ^ "):\n" ^ 
64389  247 
model_str output); print_any_hints (); 
248 
(genuineN, isa_model_opt output)) 

249 
 (no_poly, no_wf) => 

250 
let 

251 
val ignorings = [] 

252 
> not no_poly ? cons "polymorphic axioms" 

253 
> not no_wf ? cons "unchecked wellfoundedness"; 

254 
in 

66620  255 
(print (header ^ " (according to " ^ solver ^ 
256 
", ignoring " ^ space_implode " and " ignorings ^ "):\n" ^ 

64389  257 
model_str output ^ 
258 
(if no_poly then 

259 
"" 

260 
else 

261 
"\nIgnored axioms:\n" ^ 

262 
cat_lines (map (prefix " " o Syntax.string_of_term ctxt) poly_axioms))); 

263 
print_any_hints (); 

264 
(quasi_genuineN, isa_model_opt output)) 

265 
end) 

266 
end; 

267 
in 

268 
(case solve_nun_problem tool_params nice_nun_problem of 

66620  269 
Unsat solver => unsat_or_unknown solver complete 
270 
 Sat (solver, output, _) => sat_or_maybe_sat solver sound output 

64389  271 
 Unknown NONE => unknown () 
66620  272 
 Unknown (SOME (solver, output, _)) => sat_or_maybe_sat solver false output 
64389  273 
 Timeout => (print_n "Time out"; (unknownN, NONE)) 
274 
 Nunchaku_Var_Not_Set => 

64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset

275 
(print_n ("Variable $" ^ nunchaku_home_env_var ^ " not set"); (unknownN, NONE)) 
64389  276 
 Nunchaku_Cannot_Execute => 
277 
(print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE)) 

278 
 Nunchaku_Not_Found => 

279 
(print_n "External tool \"nunchaku\" not found"; (unknownN, NONE)) 

280 
 CVC4_Cannot_Execute => 

281 
(print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE)) 

282 
 CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE)) 

283 
 Unknown_Error (code, msg) => 

66632  284 
(print_n ("Error: " ^ unprefix_error msg ^ 
64389  285 
(if code = 0 then "" else " (code " ^ string_of_int code ^ ")")); 
286 
(unknownN, NONE))) 

287 
end 

288 
handle 

289 
CYCLIC_DEPS () => 

290 
(print_n "Cyclic dependencies (or bug in Nunchaku)"; (unknownN, NONE)) 

291 
 TOO_DEEP_DEPS () => 

292 
(print_n "Too deep dependencies (or bug in Nunchaku)"; (unknownN, NONE)) 

293 
 TOO_META t => 

294 
(print_n ("Formula too meta for Nunchaku:\n" ^ Syntax.string_of_term ctxt t); 

295 
(unknownN, NONE)) 

296 
 UNEXPECTED_POLYMORPHISM t => 

297 
(print_n ("Unexpected polymorphism in term\n" ^ Syntax.string_of_term ctxt t); 

298 
(unknownN, NONE)) 

299 
 UNEXPECTED_VAR t => 

300 
(print_n ("Unexpected schematic variables in term\n" ^ Syntax.string_of_term ctxt t); 

301 
(unknownN, NONE)) 

302 
 UNSUPPORTED_FUNC t => 

303 
(print_n ("Unsupported lowlevel constant in problem: " ^ Syntax.string_of_term ctxt t); 

304 
(unknownN, NONE)); 

305 
in 

306 
if expect = "" orelse outcome_code = expect then outcome 

307 
else error ("Unexpected outcome: " ^ quote outcome_code) 

308 
end; 

309 

310 
val _ = spying spy (fn () => (state, i, "starting " ^ str_of_mode mode ^ " mode")); 

311 

312 
val outcome as (outcome_code, _) = 

313 
Timeout.apply (Time.+ (timeout, timeout_slack)) run () 

314 
handle Timeout.TIMEOUT _ => (print_n "Time out"; (unknownN, NONE)); 

315 

316 
val _ = print_v (fn () => "Total time: " ^ string_of_time (Timer.checkRealTimer timer)); 

317 

318 
val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code)); 

319 
in 

320 
if expect = "" orelse outcome_code = expect then outcome 

321 
else error ("Unexpected outcome: " ^ quote outcome_code) 

322 
end; 

323 

324 
fun run_chaku_on_subgoal state params mode i = 

325 
let 

326 
val ctxt = Proof.context_of state; 

327 
val goal = Thm.prop_of (#goal (Proof.raw_goal state)); 

328 
in 

329 
if Logic.count_prems goal = 0 then 

330 
(writeln "No subgoal!"; (noneN, NONE)) 

331 
else 

332 
let 

333 
val subgoal = fst (Logic.goal_params goal i); 

334 
val all_assms = map Thm.term_of (Assumption.all_assms_of ctxt); 

335 
in 

336 
run_chaku_on_prop state params mode i all_assms subgoal 

337 
end 

338 
end; 

339 

340 
end; 