src/HOL/Tools/Nitpick/nitpick.ML
author blanchet
Thu Oct 22 14:51:47 2009 +0200 (2009-10-22 ago)
changeset 33192 08a39a957ed7
child 33232 f93390060bbe
permissions -rw-r--r--
added Nitpick's theory and ML files to Isabelle/HOL;
the examples and the documentation are on their way.
     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 well-founded. Nitpick can compute it \
   270                    \efficiently."
   271                  else
   272                    "\" could not be proved well-founded. 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;