33192

1 
(* Title: HOL/Nitpick/Tools/nitpick.ML


2 
Author: Jasmin Blanchette, TU Muenchen


3 
Copyright 2008, 2009


4 


5 
Finite model generation for HOL formulas using Kodkod.


6 
*)


7 


8 
signature NITPICK =


9 
sig


10 
type params = {


11 
cards_assigns: (typ option * int list) list,


12 
maxes_assigns: (styp option * int list) list,


13 
iters_assigns: (styp option * int list) list,


14 
bisim_depths: int list,


15 
boxes: (typ option * bool option) list,


16 
monos: (typ option * bool option) list,


17 
wfs: (styp option * bool option) list,


18 
sat_solver: string,


19 
blocking: bool,


20 
falsify: bool,


21 
debug: bool,


22 
verbose: bool,


23 
overlord: bool,


24 
user_axioms: bool option,


25 
assms: bool,


26 
coalesce_type_vars: bool,


27 
destroy_constrs: bool,


28 
specialize: bool,


29 
skolemize: bool,


30 
star_linear_preds: bool,


31 
uncurry: bool,


32 
fast_descrs: bool,


33 
peephole_optim: bool,


34 
timeout: Time.time option,


35 
tac_timeout: Time.time option,


36 
sym_break: int,


37 
sharing_depth: int,


38 
flatten_props: bool,


39 
max_threads: int,


40 
show_skolems: bool,


41 
show_datatypes: bool,


42 
show_consts: bool,


43 
evals: term list,


44 
formats: (term option * int list) list,


45 
max_potential: int,


46 
max_genuine: int,


47 
check_potential: bool,


48 
check_genuine: bool,


49 
batch_size: int,


50 
expect: string}


51 


52 
val register_frac_type : string > (string * string) list > theory > theory


53 
val unregister_frac_type : string > theory > theory


54 
val register_codatatype : typ > string > styp list > theory > theory


55 
val unregister_codatatype : typ > theory > theory


56 
val pick_nits_in_term :


57 
Proof.state > params > bool > term list > term > string * Proof.state


58 
val pick_nits_in_subgoal :


59 
Proof.state > params > bool > int > string * Proof.state


60 
end;


61 


62 
structure Nitpick : NITPICK =


63 
struct


64 


65 
open NitpickUtil


66 
open NitpickHOL


67 
open NitpickMono


68 
open NitpickScope


69 
open NitpickPeephole


70 
open NitpickRep


71 
open NitpickNut


72 
open NitpickKodkod


73 
open NitpickModel


74 


75 
type params = {


76 
cards_assigns: (typ option * int list) list,


77 
maxes_assigns: (styp option * int list) list,


78 
iters_assigns: (styp option * int list) list,


79 
bisim_depths: int list,


80 
boxes: (typ option * bool option) list,


81 
monos: (typ option * bool option) list,


82 
wfs: (styp option * bool option) list,


83 
sat_solver: string,


84 
blocking: bool,


85 
falsify: bool,


86 
debug: bool,


87 
verbose: bool,


88 
overlord: bool,


89 
user_axioms: bool option,


90 
assms: bool,


91 
coalesce_type_vars: bool,


92 
destroy_constrs: bool,


93 
specialize: bool,


94 
skolemize: bool,


95 
star_linear_preds: bool,


96 
uncurry: bool,


97 
fast_descrs: bool,


98 
peephole_optim: bool,


99 
timeout: Time.time option,


100 
tac_timeout: Time.time option,


101 
sym_break: int,


102 
sharing_depth: int,


103 
flatten_props: bool,


104 
max_threads: int,


105 
show_skolems: bool,


106 
show_datatypes: bool,


107 
show_consts: bool,


108 
evals: term list,


109 
formats: (term option * int list) list,


110 
max_potential: int,


111 
max_genuine: int,


112 
check_potential: bool,


113 
check_genuine: bool,


114 
batch_size: int,


115 
expect: string}


116 


117 
type problem_extension = {


118 
free_names: nut list,


119 
sel_names: nut list,


120 
nonsel_names: nut list,


121 
rel_table: nut NameTable.table,


122 
liberal: bool,


123 
scope: scope,


124 
core: Kodkod.formula,


125 
defs: Kodkod.formula list}


126 


127 
type rich_problem = Kodkod.problem * problem_extension


128 


129 
(* Proof.context > string > term list > Pretty.T list *)


130 
fun pretties_for_formulas _ _ [] = []


131 
 pretties_for_formulas ctxt s ts =


132 
[Pretty.str (s ^ plural_s_for_list ts ^ ":"),


133 
Pretty.indent indent_size (Pretty.chunks


134 
(map2 (fn j => fn t =>


135 
Pretty.block [t > shorten_const_names_in_term


136 
> Syntax.pretty_term ctxt,


137 
Pretty.str (if j = 1 then "." else ";")])


138 
(length ts downto 1) ts))]


139 


140 
val max_liberal_delay_ms = 200


141 
val max_liberal_delay_percent = 2


142 


143 
(* Time.time option > int *)


144 
fun liberal_delay_for_timeout NONE = max_liberal_delay_ms


145 
 liberal_delay_for_timeout (SOME timeout) =


146 
Int.max (0, Int.min (max_liberal_delay_ms,


147 
Time.toMilliseconds timeout


148 
* max_liberal_delay_percent div 100))


149 


150 
(* Time.time option > bool *)


151 
fun passed_deadline NONE = false


152 
 passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS


153 


154 
(* ('a * bool option) list > bool *)


155 
fun none_true asgns = forall (not_equal (SOME true) o snd) asgns


156 


157 
val weaselly_sorts =


158 
[@{sort default}, @{sort zero}, @{sort one}, @{sort plus}, @{sort minus},


159 
@{sort uminus}, @{sort times}, @{sort inverse}, @{sort abs}, @{sort sgn},


160 
@{sort ord}, @{sort eq}, @{sort number}]


161 
(* theory > typ > bool *)


162 
fun is_tfree_with_weaselly_sort thy (TFree (_, S)) =


163 
exists (curry (Sign.subsort thy) S) weaselly_sorts


164 
 is_tfree_with_weaselly_sort _ _ = false


165 
(* theory term > bool *)


166 
val has_weaselly_sorts =


167 
exists_type o exists_subtype o is_tfree_with_weaselly_sort


168 


169 
(* Time.time > Proof.state > params > bool > term > string * Proof.state *)


170 
fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts


171 
orig_t =


172 
let


173 
val timer = Timer.startRealTimer ()


174 
val thy = Proof.theory_of state


175 
val ctxt = Proof.context_of state


176 
val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,


177 
monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,


178 
user_axioms, assms, coalesce_type_vars, destroy_constrs, specialize,


179 
skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,


180 
tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,


181 
show_skolems, show_datatypes, show_consts, evals, formats,


182 
max_potential, max_genuine, check_potential, check_genuine, batch_size,


183 
...} =


184 
params


185 
val state_ref = Unsynchronized.ref state


186 
(* Pretty.T > unit *)


187 
val pprint =


188 
if auto then


189 
Unsynchronized.change state_ref o Proof.goal_message o K


190 
o curry Pretty.blk 0 o cons (Pretty.str "") o single


191 
o Pretty.mark Markup.hilite


192 
else


193 
priority o Pretty.string_of


194 
(* (unit > Pretty.T) > unit *)


195 
fun pprint_m f = () > not auto ? pprint o f


196 
fun pprint_v f = () > verbose ? pprint o f


197 
fun pprint_d f = () > debug ? pprint o f


198 
(* string > unit *)


199 
val print = pprint o curry Pretty.blk 0 o pstrs


200 
(* (unit > string) > unit *)


201 
fun print_m f = pprint_m (curry Pretty.blk 0 o pstrs o f)


202 
fun print_v f = pprint_v (curry Pretty.blk 0 o pstrs o f)


203 
fun print_d f = pprint_d (curry Pretty.blk 0 o pstrs o f)


204 


205 
(* unit > unit *)


206 
fun check_deadline () =


207 
if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut


208 
else ()


209 
(* unit > 'a *)


210 
fun do_interrupted () =


211 
if passed_deadline deadline then raise TimeLimit.TimeOut


212 
else raise Interrupt


213 


214 
val _ = print_m (K "Nitpicking...")


215 
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})


216 
else orig_t


217 
val assms_t = if assms orelse auto then


218 
Logic.mk_conjunction_list (neg_t :: orig_assm_ts)


219 
else


220 
neg_t


221 
val (assms_t, evals) =


222 
assms_t :: evals


223 
> coalesce_type_vars ? coalesce_type_vars_in_terms


224 
> hd pairf tl


225 
val original_max_potential = max_potential


226 
val original_max_genuine = max_genuine


227 
(*


228 
val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t)


229 
val _ = List.app (fn t => priority ("*** " ^ Syntax.string_of_term ctxt t))


230 
orig_assm_ts


231 
*)


232 
val max_bisim_depth = fold Integer.max bisim_depths ~1


233 
val case_names = case_const_names thy


234 
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy


235 
val def_table = const_def_table ctxt defs


236 
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)


237 
val simp_table = Unsynchronized.ref (const_simp_table ctxt)


238 
val psimp_table = const_psimp_table ctxt


239 
val intro_table = inductive_intro_table ctxt def_table


240 
val ground_thm_table = ground_theorem_table thy


241 
val ersatz_table = ersatz_table thy


242 
val (ext_ctxt as {skolems, special_funs, wf_cache, ...}) =


243 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,


244 
user_axioms = user_axioms, debug = debug, wfs = wfs,


245 
destroy_constrs = destroy_constrs, specialize = specialize,


246 
skolemize = skolemize, star_linear_preds = star_linear_preds,


247 
uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout,


248 
evals = evals, case_names = case_names, def_table = def_table,


249 
nondef_table = nondef_table, user_nondefs = user_nondefs,


250 
simp_table = simp_table, psimp_table = psimp_table,


251 
intro_table = intro_table, ground_thm_table = ground_thm_table,


252 
ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],


253 
special_funs = Unsynchronized.ref [],


254 
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}


255 
val frees = Term.add_frees assms_t []


256 
val _ = null (Term.add_tvars assms_t [])


257 
orelse raise NOT_SUPPORTED "schematic type variables"


258 
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),


259 
core_t) = preprocess_term ext_ctxt assms_t


260 
val got_all_user_axioms =


261 
got_all_mono_user_axioms andalso no_poly_user_axioms


262 


263 
(* styp * (bool * bool) > unit *)


264 
fun print_wf (x, (gfp, wf)) =


265 
pprint (Pretty.blk (0,


266 
pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")


267 
@ Syntax.pretty_term ctxt (Const x) ::


268 
pstrs (if wf then


269 
"\" was proved wellfounded. Nitpick can compute it \


270 
\efficiently."


271 
else


272 
"\" could not be proved wellfounded. Nitpick might need to \


273 
\unroll it.")))


274 
val _ = if verbose then List.app print_wf (!wf_cache) else ()


275 
val _ =


276 
pprint_d (fn () =>


277 
Pretty.chunks


278 
(pretties_for_formulas ctxt "Preprocessed formula" [core_t] @


279 
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @


280 
pretties_for_formulas ctxt "Relevant nondefinitional axiom"


281 
nondef_ts))


282 
val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts)


283 
handle TYPE (_, Ts, ts) =>


284 
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)


285 


286 
val unique_scope = forall (equal 1 o length o snd) cards_assigns


287 
(* typ > bool *)


288 
fun is_free_type_monotonic T =


289 
unique_scope orelse


290 
case triple_lookup (type_match thy) monos T of


291 
SOME (SOME b) => b


292 
 _ => formulas_monotonic ext_ctxt T def_ts nondef_ts core_t


293 
fun is_datatype_monotonic T =


294 
unique_scope orelse


295 
case triple_lookup (type_match thy) monos T of


296 
SOME (SOME b) => b


297 
 _ =>


298 
not (is_pure_typedef thy T) orelse is_univ_typedef thy T


299 
orelse is_number_type thy T


300 
orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t


301 
val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)


302 
> sort TermOrd.typ_ord


303 
val (all_dataTs, all_free_Ts) =


304 
List.partition (is_integer_type orf is_datatype thy) Ts


305 
val (mono_dataTs, nonmono_dataTs) =


306 
List.partition is_datatype_monotonic all_dataTs


307 
val (mono_free_Ts, nonmono_free_Ts) =


308 
List.partition is_free_type_monotonic all_free_Ts


309 


310 
val _ =


311 
if not unique_scope andalso not (null mono_free_Ts) then


312 
print_v (fn () =>


313 
let


314 
val ss = map (quote o string_for_type ctxt) mono_free_Ts


315 
in


316 
"The type" ^ plural_s_for_list ss ^ " " ^


317 
space_implode " " (serial_commas "and" ss) ^ " " ^


318 
(if none_true monos then


319 
"passed the monotonicity test"


320 
else


321 
(if length ss = 1 then "is" else "are") ^


322 
" considered monotonic") ^


323 
". Nitpick might be able to skip some scopes."


324 
end)


325 
else


326 
()


327 
val mono_Ts = mono_dataTs @ mono_free_Ts


328 
val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts


329 


330 
(*


331 
val _ = priority "Monotonic datatypes:"


332 
val _ = List.app (priority o string_for_type ctxt) mono_dataTs


333 
val _ = priority "Nonmonotonic datatypes:"


334 
val _ = List.app (priority o string_for_type ctxt) nonmono_dataTs


335 
val _ = priority "Monotonic free types:"


336 
val _ = List.app (priority o string_for_type ctxt) mono_free_Ts


337 
val _ = priority "Nonmonotonic free types:"


338 
val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts


339 
*)


340 


341 
val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t


342 
val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)


343 
def_ts


344 
val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)


345 
nondef_ts


346 
val (free_names, const_names) =


347 
fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])


348 
val nonsel_names = filter_out (is_sel o nickname_of) const_names


349 
val would_be_genuine = got_all_user_axioms andalso none_true wfs


350 
(*


351 
val _ = List.app (priority o string_for_nut ctxt)


352 
(core_u :: def_us @ nondef_us)


353 
*)


354 
val need_incremental = Int.max (max_potential, max_genuine) >= 2


355 
val effective_sat_solver =


356 
if sat_solver <> "smart" then


357 
if need_incremental andalso


358 
not (sat_solver mem KodkodSAT.configured_sat_solvers true) then


359 
(print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \


360 
\be used instead of " ^ quote sat_solver ^ "."));


361 
"SAT4J")


362 
else


363 
sat_solver


364 
else


365 
KodkodSAT.smart_sat_solver_name need_incremental


366 
val _ =


367 
if sat_solver = "smart" then


368 
print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^


369 
". The following" ^


370 
(if need_incremental then " incremental " else " ") ^


371 
"solvers are configured: " ^


372 
commas (map quote (KodkodSAT.configured_sat_solvers


373 
need_incremental)) ^ ".")


374 
else


375 
()


376 


377 
val too_big_scopes = Unsynchronized.ref []


378 


379 
(* bool > scope > rich_problem option *)


380 
fun problem_for_scope liberal


381 
(scope as {card_assigns, bisim_depth, datatypes, ofs, ...}) =


382 
let


383 
val _ = not (exists (fn other => scope_less_eq other scope)


384 
(!too_big_scopes))


385 
orelse raise LIMIT ("Nitpick.pick_them_nits_in_term.\


386 
\problem_for_scope", "too big scope")


387 
(*


388 
val _ = priority "Offsets:"


389 
val _ = List.app (fn (T, j0) =>


390 
priority (string_for_type ctxt T ^ " = " ^


391 
string_of_int j0))


392 
(Typtab.dest ofs)


393 
*)


394 
val all_precise = forall (is_precise_type datatypes) Ts


395 
(* nut list > rep NameTable.table > nut list * rep NameTable.table *)


396 
val repify_consts = choose_reps_for_consts scope all_precise


397 
val main_j0 = offset_of_type ofs bool_T


398 
val (nat_card, nat_j0) = spec_of_type scope nat_T


399 
val (int_card, int_j0) = spec_of_type scope int_T


400 
val _ = forall (equal main_j0) [nat_j0, int_j0]


401 
orelse raise BAD ("Nitpick.pick_them_nits_in_term.\


402 
\problem_for_scope", "bad offsets")


403 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0


404 
val (free_names, rep_table) =


405 
choose_reps_for_free_vars scope free_names NameTable.empty


406 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table


407 
val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table


408 
val min_highest_arity =


409 
NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1


410 
val min_univ_card =


411 
NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table


412 
(univ_card nat_card int_card main_j0 [] Kodkod.True)


413 
val _ = check_arity min_univ_card min_highest_arity


414 


415 
val core_u = choose_reps_in_nut scope liberal rep_table false core_u


416 
val def_us = map (choose_reps_in_nut scope liberal rep_table true)


417 
def_us


418 
val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)


419 
nondef_us


420 
(*


421 
val _ = List.app (priority o string_for_nut ctxt)


422 
(free_names @ sel_names @ nonsel_names @


423 
core_u :: def_us @ nondef_us)


424 
*)


425 
val (free_rels, pool, rel_table) =


426 
rename_free_vars free_names initial_pool NameTable.empty


427 
val (sel_rels, pool, rel_table) =


428 
rename_free_vars sel_names pool rel_table


429 
val (other_rels, pool, rel_table) =


430 
rename_free_vars nonsel_names pool rel_table


431 
val core_u = rename_vars_in_nut pool rel_table core_u


432 
val def_us = map (rename_vars_in_nut pool rel_table) def_us


433 
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us


434 
(* nut > Kodkod.formula *)


435 
val to_f = kodkod_formula_from_nut ofs liberal kk


436 
val core_f = to_f core_u


437 
val def_fs = map to_f def_us


438 
val nondef_fs = map to_f nondef_us


439 
val formula = fold (fold s_and) [def_fs, nondef_fs] core_f


440 
val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^


441 
PrintMode.setmp [] multiline_string_for_scope scope


442 
val kodkod_sat_solver = KodkodSAT.sat_solver_spec effective_sat_solver


443 
> snd


444 
val delay = if liberal then


445 
Option.map (fn time => Time. (time, Time.now ()))


446 
deadline


447 
> liberal_delay_for_timeout


448 
else


449 
0


450 
val settings = [("solver", commas (map quote kodkod_sat_solver)),


451 
("skolem_depth", "1"),


452 
("bit_width", "16"),


453 
("symmetry_breaking", signed_string_of_int sym_break),


454 
("sharing", signed_string_of_int sharing_depth),


455 
("flatten", Bool.toString flatten_props),


456 
("delay", signed_string_of_int delay)]


457 
val plain_rels = free_rels @ other_rels


458 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels


459 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels


460 
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels


461 
val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt ofs kk


462 
rel_table datatypes


463 
val declarative_axioms = plain_axioms @ dtype_axioms


464 
val univ_card = univ_card nat_card int_card main_j0


465 
(plain_bounds @ sel_bounds) formula


466 
val built_in_bounds = bounds_for_built_in_rels_in_formula debug


467 
univ_card nat_card int_card main_j0 formula


468 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds


469 
> not debug ? merge_bounds


470 
val highest_arity =


471 
fold Integer.max (map (fst o fst) (maps fst bounds)) 0


472 
val formula = fold_rev s_and declarative_axioms formula


473 
val _ = if formula = Kodkod.False then ()


474 
else check_arity univ_card highest_arity


475 
in


476 
SOME ({comment = comment, settings = settings, univ_card = univ_card,


477 
tuple_assigns = [], bounds = bounds,


478 
int_bounds = sequential_int_bounds univ_card,


479 
expr_assigns = [], formula = formula},


480 
{free_names = free_names, sel_names = sel_names,


481 
nonsel_names = nonsel_names, rel_table = rel_table,


482 
liberal = liberal, scope = scope, core = core_f,


483 
defs = nondef_fs @ def_fs @ declarative_axioms})


484 
end


485 
handle LIMIT (loc, msg) =>


486 
if loc = "NitpickKodkod.check_arity"


487 
andalso not (Typtab.is_empty ofs) then


488 
problem_for_scope liberal


489 
{ext_ctxt = ext_ctxt, card_assigns = card_assigns,


490 
bisim_depth = bisim_depth, datatypes = datatypes,


491 
ofs = Typtab.empty}


492 
else if loc = "Nitpick.pick_them_nits_in_term.\


493 
\problem_for_scope" then


494 
NONE


495 
else


496 
(Unsynchronized.change too_big_scopes (cons scope);


497 
print_v (fn () => ("Limit reached: " ^ msg ^


498 
". Dropping " ^ (if liberal then "potential"


499 
else "genuine") ^


500 
" component of scope."));


501 
NONE)


502 


503 
(* int > (''a * int list list) list > ''a > Kodkod.tuple_set *)


504 
fun tuple_set_for_rel univ_card =


505 
Kodkod.TupleSet o map (kk_tuple debug univ_card) o the


506 
oo AList.lookup (op =)


507 


508 
val word_model = if falsify then "counterexample" else "model"


509 


510 
val scopes = Unsynchronized.ref []


511 
val generated_scopes = Unsynchronized.ref []


512 
val generated_problems = Unsynchronized.ref []


513 
val checked_problems = Unsynchronized.ref (SOME [])


514 
val met_potential = Unsynchronized.ref 0


515 


516 
(* rich_problem list > int list > unit *)


517 
fun update_checked_problems problems =


518 
List.app (Unsynchronized.change checked_problems o Option.map o cons


519 
o nth problems)


520 


521 
(* bool > Kodkod.raw_bound list > problem_extension > bool option *)


522 
fun print_and_check_model genuine bounds


523 
({free_names, sel_names, nonsel_names, rel_table, scope, ...}


524 
: problem_extension) =


525 
let


526 
val (reconstructed_model, codatatypes_ok) =


527 
reconstruct_hol_model {show_skolems = show_skolems,


528 
show_datatypes = show_datatypes,


529 
show_consts = show_consts}


530 
scope formats frees free_names sel_names nonsel_names rel_table


531 
bounds


532 
val would_be_genuine = would_be_genuine andalso codatatypes_ok


533 
in


534 
pprint (Pretty.chunks


535 
[Pretty.blk (0,


536 
(pstrs ("Nitpick found a" ^


537 
(if not genuine then " potential "


538 
else if would_be_genuine then " "


539 
else " likely genuine ") ^ word_model) @


540 
(case pretties_for_scope scope verbose of


541 
[] => []


542 
 pretties => pstrs " for " @ pretties) @


543 
[Pretty.str ":\n"])),


544 
Pretty.indent indent_size reconstructed_model]);


545 
if genuine then


546 
(if check_genuine then


547 
(case prove_hol_model scope tac_timeout free_names sel_names


548 
rel_table bounds assms_t of


549 
SOME true => print ("Confirmation by \"auto\": The above " ^


550 
word_model ^ " is really genuine.")


551 
 SOME false =>


552 
if would_be_genuine then


553 
error ("A supposedly genuine " ^ word_model ^ " was shown to\


554 
\be spurious by \"auto\".\nThis should never happen.\n\


555 
\Please send a bug report to blanchet\


556 
\te@in.tum.de.")


557 
else


558 
print ("Refutation by \"auto\": The above " ^ word_model ^


559 
" is spurious.")


560 
 NONE => print "No confirmation by \"auto\".")


561 
else


562 
();


563 
if has_weaselly_sorts thy orig_t then


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


565 
else


566 
();


567 
if not would_be_genuine then


568 
if no_poly_user_axioms then


569 
let


570 
val options =


571 
[] > not got_all_mono_user_axioms


572 
? cons ("user_axioms", "\"true\"")


573 
> not (none_true wfs)


574 
? cons ("wf", "\"smart\" or \"false\"")


575 
> not codatatypes_ok


576 
? cons ("bisim_depth", "a nonnegative value")


577 
val ss =


578 
map (fn (name, value) => quote name ^ " set to " ^ value)


579 
options


580 
in


581 
print ("Try again with " ^


582 
space_implode " " (serial_commas "and" ss) ^


583 
" to confirm that the " ^ word_model ^ " is genuine.")


584 
end


585 
else


586 
print ("Nitpick is unable to guarantee the authenticity of \


587 
\the " ^ word_model ^ " in the presence of polymorphic \


588 
\axioms.")


589 
else


590 
();


591 
NONE)


592 
else


593 
if not genuine then


594 
(Unsynchronized.inc met_potential;


595 
if check_potential then


596 
let


597 
val status = prove_hol_model scope tac_timeout free_names


598 
sel_names rel_table bounds assms_t


599 
in


600 
(case status of


601 
SOME true => print ("Confirmation by \"auto\": The above " ^


602 
word_model ^ " is genuine.")


603 
 SOME false => print ("Refutation by \"auto\": The above " ^


604 
word_model ^ " is spurious.")


605 
 NONE => print "No confirmation by \"auto\".");


606 
status


607 
end


608 
else


609 
NONE)


610 
else


611 
NONE


612 
end


613 
(* int > int > int > bool > rich_problem list > int * int * int *)


614 
fun solve_any_problem max_potential max_genuine donno first_time problems =


615 
let


616 
val max_potential = Int.max (0, max_potential)


617 
val max_genuine = Int.max (0, max_genuine)


618 
(* bool > int * Kodkod.raw_bound list > bool option *)


619 
fun print_and_check genuine (j, bounds) =


620 
print_and_check_model genuine bounds (snd (nth problems j))


621 
val max_solutions = max_potential + max_genuine


622 
> not need_incremental ? curry Int.min 1


623 
in


624 
if max_solutions <= 0 then


625 
(0, 0, donno)


626 
else


627 
case Kodkod.solve_any_problem overlord deadline max_threads


628 
max_solutions (map fst problems) of


629 
Kodkod.Normal ([], unsat_js) =>


630 
(update_checked_problems problems unsat_js;


631 
(max_potential, max_genuine, donno))


632 
 Kodkod.Normal (sat_ps, unsat_js) =>


633 
let


634 
val (lib_ps, con_ps) =


635 
List.partition (#liberal o snd o nth problems o fst) sat_ps


636 
in


637 
update_checked_problems problems (unsat_js @ map fst lib_ps);


638 
if null con_ps then


639 
let


640 
val num_genuine = Library.take (max_potential, lib_ps)


641 
> map (print_and_check false)


642 
> filter (equal (SOME true)) > length


643 
val max_genuine = max_genuine  num_genuine


644 
val max_potential = max_potential


645 
 (length lib_ps  num_genuine)


646 
in


647 
if max_genuine <= 0 then


648 
(0, 0, donno)


649 
else


650 
let


651 
(* "co_js" is the list of conservative problems whose


652 
liberal pendants couldn't be satisfied and hence that


653 
most probably can't be satisfied themselves. *)


654 
val co_js =


655 
map (fn j => j  1) unsat_js


656 
> filter (fn j =>


657 
j >= 0 andalso


658 
scopes_equivalent


659 
(#scope (snd (nth problems j)))


660 
(#scope (snd (nth problems (j + 1)))))


661 
val bye_js = sort_distinct int_ord (map fst sat_ps @


662 
unsat_js @ co_js)


663 
val problems =


664 
problems > filter_out_indices bye_js


665 
> max_potential <= 0


666 
? filter_out (#liberal o snd)


667 
in


668 
solve_any_problem max_potential max_genuine donno false


669 
problems


670 
end


671 
end


672 
else


673 
let


674 
val _ = Library.take (max_genuine, con_ps)


675 
> List.app (ignore o print_and_check true)


676 
val max_genuine = max_genuine  length con_ps


677 
in


678 
if max_genuine <= 0 orelse not first_time then


679 
(0, max_genuine, donno)


680 
else


681 
let


682 
val bye_js = sort_distinct int_ord


683 
(map fst sat_ps @ unsat_js)


684 
val problems =


685 
problems > filter_out_indices bye_js


686 
> filter_out (#liberal o snd)


687 
in solve_any_problem 0 max_genuine donno false problems end


688 
end


689 
end


690 
 Kodkod.TimedOut unsat_js =>


691 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)


692 
 Kodkod.Interrupted NONE =>


693 
(checked_problems := NONE; do_interrupted ())


694 
 Kodkod.Interrupted (SOME unsat_js) =>


695 
(update_checked_problems problems unsat_js; do_interrupted ())


696 
 Kodkod.Error (s, unsat_js) =>


697 
(update_checked_problems problems unsat_js;


698 
print_v (K ("Kodkod error: " ^ s ^ "."));


699 
(max_potential, max_genuine, donno + 1))


700 
end


701 


702 
(* int > int > scope list > int * int * int > int * int * int *)


703 
fun run_batch j n scopes (max_potential, max_genuine, donno) =


704 
let


705 
val _ =


706 
if null scopes then


707 
print_m (K "The scope specification is inconsistent.")


708 
else if verbose then


709 
pprint (Pretty.chunks


710 
[Pretty.blk (0,


711 
pstrs ((if n > 1 then


712 
"Batch " ^ string_of_int (j + 1) ^ " of " ^


713 
signed_string_of_int n ^ ": "


714 
else


715 
"") ^


716 
"Trying " ^ string_of_int (length scopes) ^


717 
" scope" ^ plural_s_for_list scopes ^ ":")),


718 
Pretty.indent indent_size


719 
(Pretty.chunks (map2


720 
(fn j => fn scope =>


721 
Pretty.block (


722 
(case pretties_for_scope scope true of


723 
[] => [Pretty.str "Empty"]


724 
 pretties => pretties) @


725 
[Pretty.str (if j = 1 then "." else ";")]))


726 
(length scopes downto 1) scopes))])


727 
else


728 
()


729 
(* scope * bool > rich_problem list * bool


730 
> rich_problem list * bool *)


731 
fun add_problem_for_scope (scope as {datatypes, ...}, liberal)


732 
(problems, donno) =


733 
(check_deadline ();


734 
case problem_for_scope liberal scope of


735 
SOME problem =>


736 
(problems


737 
> (null problems orelse


738 
not (Kodkod.problems_equivalent (fst problem)


739 
(fst (hd problems))))


740 
? cons problem, donno)


741 
 NONE => (problems, donno + 1))


742 
val (problems, donno) =


743 
fold add_problem_for_scope


744 
(map_product pair scopes


745 
((if max_genuine > 0 then [false] else []) @


746 
(if max_potential > 0 then [true] else [])))


747 
([], donno)


748 
val _ = Unsynchronized.change generated_problems (append problems)


749 
val _ = Unsynchronized.change generated_scopes (append scopes)


750 
in


751 
solve_any_problem max_potential max_genuine donno true (rev problems)


752 
end


753 


754 
(* rich_problem list > scope > int *)


755 
fun scope_count (problems : rich_problem list) scope =


756 
length (filter (scopes_equivalent scope o #scope o snd) problems)


757 
(* string > string *)


758 
fun excipit did_so_and_so =


759 
let


760 
(* rich_problem list > rich_problem list *)


761 
val do_filter =


762 
if !met_potential = max_potential then filter_out (#liberal o snd)


763 
else I


764 
val total = length (!scopes)


765 
val unsat =


766 
fold (fn scope =>


767 
case scope_count (do_filter (!generated_problems)) scope of


768 
0 => I


769 
 n =>


770 
if scope_count (do_filter (these (!checked_problems)))


771 
scope = n then


772 
Integer.add 1


773 
else


774 
I) (!generated_scopes) 0


775 
in


776 
"Nitpick " ^ did_so_and_so ^


777 
(if is_some (!checked_problems) andalso total > 0 then


778 
" after checking " ^


779 
string_of_int (Int.min (total  1, unsat)) ^ " of " ^


780 
string_of_int total ^ " scope" ^ plural_s total


781 
else


782 
"") ^ "."


783 
end


784 


785 
(* int > int > scope list > int * int * int > Kodkod.outcome *)


786 
fun run_batches _ _ [] (max_potential, max_genuine, donno) =


787 
if donno > 0 andalso max_genuine > 0 then


788 
(print_m (fn () => excipit "ran out of resources"); "unknown")


789 
else if max_genuine = original_max_genuine then


790 
if max_potential = original_max_potential then


791 
(print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")


792 
else


793 
(print_m (K ("Nitpick could not find " ^


794 
(if max_genuine = 1 then "a better " ^ word_model ^ "."


795 
else "any better " ^ word_model ^ "s.")));


796 
"potential")


797 
else


798 
if would_be_genuine then "genuine" else "likely_genuine"


799 
 run_batches j n (batch :: batches) z =


800 
let val (z as (_, max_genuine, _)) = run_batch j n batch z in


801 
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z


802 
end


803 


804 
val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns


805 
iters_assigns bisim_depths mono_Ts nonmono_Ts


806 
val batches = batch_list batch_size (!scopes)


807 
val outcome_code =


808 
(run_batches 0 (length batches) batches (max_potential, max_genuine, 0)


809 
handle Exn.Interrupt => do_interrupted ())


810 
handle TimeLimit.TimeOut =>


811 
(print_m (fn () => excipit "ran out of time");


812 
if !met_potential > 0 then "potential" else "unknown")


813 
 Exn.Interrupt => if auto orelse debug then raise Interrupt


814 
else error (excipit "was interrupted")


815 
val _ = print_v (fn () => "Total time: " ^


816 
signed_string_of_int (Time.toMilliseconds


817 
(Timer.checkRealTimer timer)) ^ " ms.")


818 
in (outcome_code, !state_ref) end


819 
handle Exn.Interrupt =>


820 
if auto orelse #debug params then


821 
raise Interrupt


822 
else


823 
if passed_deadline deadline then


824 
(priority "Nitpick ran out of time."; ("unknown", state))


825 
else


826 
error "Nitpick was interrupted."


827 


828 
(* Proof.state > params > bool > term > string * Proof.state *)


829 
fun pick_nits_in_term state (params as {debug, timeout, expect, ...})


830 
auto orig_assm_ts orig_t =


831 
let


832 
val deadline = Option.map (curry Time.+ (Time.now ())) timeout


833 
val outcome as (outcome_code, _) =


834 
time_limit (if debug then NONE else timeout)


835 
(pick_them_nits_in_term deadline state params auto orig_assm_ts)


836 
orig_t


837 
in


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


839 
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")


840 
end


841 


842 
(* Proof.state > params > thm > int > string * Proof.state *)


843 
fun pick_nits_in_subgoal state params auto subgoal =


844 
let


845 
val ctxt = Proof.context_of state


846 
val t = state > Proof.get_goal > snd > snd > prop_of


847 
in


848 
if Logic.count_prems t = 0 then


849 
(priority "No subgoal!"; ("none", state))


850 
else


851 
let


852 
val assms = map term_of (Assumption.all_assms_of ctxt)


853 
val (t, frees) = Logic.goal_params t subgoal


854 
in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end


855 
end


856 


857 
end;
