30 assms: bool, |
30 assms: bool, |
31 merge_type_vars: bool, |
31 merge_type_vars: bool, |
32 binary_ints: bool option, |
32 binary_ints: bool option, |
33 destroy_constrs: bool, |
33 destroy_constrs: bool, |
34 specialize: bool, |
34 specialize: bool, |
35 skolemize: bool, |
|
36 star_linear_preds: bool, |
35 star_linear_preds: bool, |
37 fast_descrs: bool, |
36 fast_descrs: bool, |
38 peephole_optim: bool, |
37 peephole_optim: bool, |
39 timeout: Time.time option, |
38 timeout: Time.time option, |
40 tac_timeout: Time.time option, |
39 tac_timeout: Time.time option, |
102 assms: bool, |
101 assms: bool, |
103 merge_type_vars: bool, |
102 merge_type_vars: bool, |
104 binary_ints: bool option, |
103 binary_ints: bool option, |
105 destroy_constrs: bool, |
104 destroy_constrs: bool, |
106 specialize: bool, |
105 specialize: bool, |
107 skolemize: bool, |
|
108 star_linear_preds: bool, |
106 star_linear_preds: bool, |
109 fast_descrs: bool, |
107 fast_descrs: bool, |
110 peephole_optim: bool, |
108 peephole_optim: bool, |
111 timeout: Time.time option, |
109 timeout: Time.time option, |
112 tac_timeout: Time.time option, |
110 tac_timeout: Time.time option, |
190 error "You must import the theory \"Nitpick\" to use Nitpick" |
188 error "You must import the theory \"Nitpick\" to use Nitpick" |
191 *) |
189 *) |
192 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, |
190 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, |
193 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, |
191 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, |
194 verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints, |
192 verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints, |
195 destroy_constrs, specialize, skolemize, star_linear_preds, fast_descrs, |
193 destroy_constrs, specialize, star_linear_preds, fast_descrs, |
196 peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes, |
194 peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes, |
197 show_consts, evals, formats, max_potential, max_genuine, |
195 show_consts, evals, formats, max_potential, max_genuine, |
198 check_potential, check_genuine, batch_size, ...} = |
196 check_potential, check_genuine, batch_size, ...} = |
199 params |
197 params |
200 val state_ref = Unsynchronized.ref state |
198 val state_ref = Unsynchronized.ref state |
260 val ersatz_table = ersatz_table thy |
258 val ersatz_table = ersatz_table thy |
261 val (hol_ctxt as {wf_cache, ...}) = |
259 val (hol_ctxt as {wf_cache, ...}) = |
262 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, |
260 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, |
263 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, |
261 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, |
264 binary_ints = binary_ints, destroy_constrs = destroy_constrs, |
262 binary_ints = binary_ints, destroy_constrs = destroy_constrs, |
265 specialize = specialize, skolemize = skolemize, |
263 specialize = specialize, star_linear_preds = star_linear_preds, |
266 star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, |
264 fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, |
267 tac_timeout = tac_timeout, evals = evals, case_names = case_names, |
265 case_names = case_names, def_table = def_table, |
268 def_table = def_table, nondef_table = nondef_table, |
266 nondef_table = nondef_table, user_nondefs = user_nondefs, |
269 user_nondefs = user_nondefs, simp_table = simp_table, |
267 simp_table = simp_table, psimp_table = psimp_table, |
270 psimp_table = psimp_table, choice_spec_table = choice_spec_table, |
268 choice_spec_table = choice_spec_table, intro_table = intro_table, |
271 intro_table = intro_table, ground_thm_table = ground_thm_table, |
269 ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, |
272 ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], |
270 skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], |
273 special_funs = Unsynchronized.ref [], |
|
274 unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], |
271 unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], |
275 constr_cache = Unsynchronized.ref []} |
272 constr_cache = Unsynchronized.ref []} |
276 val frees = Term.add_frees assms_t [] |
273 val frees = Term.add_frees assms_t [] |
277 val _ = null (Term.add_tvars assms_t []) orelse |
274 val _ = null (Term.add_tvars assms_t []) orelse |
278 raise NOT_SUPPORTED "schematic type variables" |
275 raise NOT_SUPPORTED "schematic type variables" |