src/HOL/Tools/Nitpick/nitpick.ML
author wenzelm
Thu May 27 18:10:37 2010 +0200 (2010-05-27)
changeset 37146 f652333bbf8e
parent 36913 0010f08e288e
child 37213 efcad7594872
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
     1 (*  Title:      HOL/Tools/Nitpick/nitpick.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009, 2010
     4 
     5 Finite model generation for HOL formulas using Kodkod.
     6 *)
     7 
     8 signature NITPICK =
     9 sig
    10   type styp = Nitpick_Util.styp
    11   type term_postprocessor = Nitpick_Model.term_postprocessor
    12   type params =
    13     {cards_assigns: (typ option * int list) list,
    14      maxes_assigns: (styp option * int list) list,
    15      iters_assigns: (styp option * int list) list,
    16      bitss: int list,
    17      bisim_depths: int list,
    18      boxes: (typ option * bool option) list,
    19      finitizes: (typ option * bool option) list,
    20      monos: (typ option * bool option) list,
    21      stds: (typ option * bool) list,
    22      wfs: (styp option * bool option) list,
    23      sat_solver: string,
    24      blocking: bool,
    25      falsify: bool,
    26      debug: bool,
    27      verbose: bool,
    28      overlord: bool,
    29      user_axioms: bool option,
    30      assms: bool,
    31      merge_type_vars: bool,
    32      binary_ints: bool option,
    33      destroy_constrs: bool,
    34      specialize: bool,
    35      star_linear_preds: bool,
    36      fast_descrs: bool,
    37      peephole_optim: bool,
    38      timeout: Time.time option,
    39      tac_timeout: Time.time option,
    40      max_threads: int,
    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 register_term_postprocessor :
    57     typ -> term_postprocessor -> theory -> theory
    58   val unregister_term_postprocessor : typ -> theory -> theory
    59   val pick_nits_in_term :
    60     Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
    61     -> term list -> term -> string * Proof.state
    62   val pick_nits_in_subgoal :
    63     Proof.state -> params -> bool -> int -> int -> string * Proof.state
    64 end;
    65 
    66 structure Nitpick : NITPICK =
    67 struct
    68 
    69 open Nitpick_Util
    70 open Nitpick_HOL
    71 open Nitpick_Preproc
    72 open Nitpick_Mono
    73 open Nitpick_Scope
    74 open Nitpick_Peephole
    75 open Nitpick_Rep
    76 open Nitpick_Nut
    77 open Nitpick_Kodkod
    78 open Nitpick_Model
    79 
    80 structure KK = Kodkod
    81 
    82 type params =
    83   {cards_assigns: (typ option * int list) list,
    84    maxes_assigns: (styp option * int list) list,
    85    iters_assigns: (styp option * int list) list,
    86    bitss: int list,
    87    bisim_depths: int list,
    88    boxes: (typ option * bool option) list,
    89    finitizes: (typ option * bool option) list,
    90    monos: (typ option * bool option) list,
    91    stds: (typ option * bool) list,
    92    wfs: (styp option * bool option) list,
    93    sat_solver: string,
    94    blocking: bool,
    95    falsify: bool,
    96    debug: bool,
    97    verbose: bool,
    98    overlord: bool,
    99    user_axioms: bool option,
   100    assms: bool,
   101    merge_type_vars: bool,
   102    binary_ints: bool option,
   103    destroy_constrs: bool,
   104    specialize: bool,
   105    star_linear_preds: bool,
   106    fast_descrs: bool,
   107    peephole_optim: bool,
   108    timeout: Time.time option,
   109    tac_timeout: Time.time option,
   110    max_threads: int,
   111    show_datatypes: bool,
   112    show_consts: bool,
   113    evals: term list,
   114    formats: (term option * int list) list,
   115    max_potential: int,
   116    max_genuine: int,
   117    check_potential: bool,
   118    check_genuine: bool,
   119    batch_size: int,
   120    expect: string}
   121 
   122 type problem_extension =
   123   {free_names: nut list,
   124    sel_names: nut list,
   125    nonsel_names: nut list,
   126    rel_table: nut NameTable.table,
   127    unsound: bool,
   128    scope: scope}
   129  
   130 type rich_problem = KK.problem * problem_extension
   131 
   132 fun pretties_for_formulas _ _ [] = []
   133   | pretties_for_formulas ctxt s ts =
   134     [Pretty.str (s ^ plural_s_for_list ts ^ ":"),
   135      Pretty.indent indent_size (Pretty.chunks
   136          (map2 (fn j => fn t =>
   137                    Pretty.block [t |> shorten_names_in_term
   138                                    |> Syntax.pretty_term ctxt,
   139                                  Pretty.str (if j = 1 then "." else ";")])
   140                (length ts downto 1) ts))]
   141 
   142 fun install_java_message () =
   143   "Nitpick requires a Java 1.5 virtual machine called \"java\"."
   144 fun install_kodkodi_message () =
   145   "Nitpick requires the external Java program Kodkodi. To install it, download \
   146   \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
   147   \directory's full path to \"" ^
   148   Path.implode (Path.expand (Path.appends
   149       (Path.variable "ISABELLE_HOME_USER" ::
   150        map Path.basic ["etc", "components"]))) ^ "\" on a line of its own."
   151 
   152 val max_unsound_delay_ms = 200
   153 val max_unsound_delay_percent = 2
   154 
   155 fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
   156   | unsound_delay_for_timeout (SOME timeout) =
   157     Int.max (0, Int.min (max_unsound_delay_ms,
   158                          Time.toMilliseconds timeout
   159                          * max_unsound_delay_percent div 100))
   160 
   161 fun passed_deadline NONE = false
   162   | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
   163 
   164 fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
   165 
   166 val syntactic_sorts =
   167   @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
   168   @{sort number}
   169 fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
   170     subset (op =) (S, syntactic_sorts)
   171   | has_tfree_syntactic_sort _ = false
   172 val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)
   173 
   174 fun plazy f = Pretty.blk (0, pstrs (f ()))
   175 
   176 fun pick_them_nits_in_term deadline state (params : params) auto i n step
   177                            subst orig_assm_ts orig_t =
   178   let
   179     val timer = Timer.startRealTimer ()
   180     val thy = Proof.theory_of state
   181     val ctxt = Proof.context_of state
   182 (* FIXME: reintroduce code before new release:
   183 
   184     val nitpick_thy = ThyInfo.get_theory "Nitpick"
   185     val _ = Theory.subthy (nitpick_thy, thy) orelse
   186             error "You must import the theory \"Nitpick\" to use Nitpick"
   187 *)
   188     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
   189          boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
   190          verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
   191          destroy_constrs, specialize, star_linear_preds, fast_descrs,
   192          peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
   193          evals, formats, max_potential, max_genuine, check_potential,
   194          check_genuine, batch_size, ...} = params
   195     val state_ref = Unsynchronized.ref state
   196     val pprint =
   197       if auto then
   198         Unsynchronized.change state_ref o Proof.goal_message o K
   199         o Pretty.chunks o cons (Pretty.str "") o single
   200         o Pretty.mark Markup.hilite
   201       else
   202         (fn s => (priority s; if debug then tracing s else ()))
   203         o Pretty.string_of
   204     fun pprint_m f = () |> not auto ? pprint o f
   205     fun pprint_v f = () |> verbose ? pprint o f
   206     fun pprint_d f = () |> debug ? pprint o f
   207     val print = pprint o curry Pretty.blk 0 o pstrs
   208     val print_g = pprint o Pretty.str
   209     val print_m = pprint_m o K o plazy
   210     val print_v = pprint_v o K o plazy
   211 
   212     fun check_deadline () =
   213       if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
   214       else ()
   215     fun do_interrupted () =
   216       if passed_deadline deadline then raise TimeLimit.TimeOut
   217       else raise Interrupt
   218 
   219     val orig_assm_ts = if assms orelse auto then orig_assm_ts else []
   220     val _ =
   221       if step = 0 then
   222         print_m (fn () => "Nitpicking formula...")
   223       else
   224         pprint_m (fn () => Pretty.chunks (
   225             pretties_for_formulas ctxt ("Nitpicking " ^
   226                 (if i <> 1 orelse n <> 1 then
   227                    "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
   228                  else
   229                    "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
   230     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
   231                 else orig_t
   232     val assms_t = Logic.mk_conjunction_list (neg_t :: orig_assm_ts)
   233     val (assms_t, evals) =
   234       assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms
   235                        |> pairf hd tl
   236     val original_max_potential = max_potential
   237     val original_max_genuine = max_genuine
   238 (*
   239     val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t)
   240     val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t))
   241                      orig_assm_ts
   242 *)
   243     val max_bisim_depth = fold Integer.max bisim_depths ~1
   244     val case_names = case_const_names thy stds
   245     val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
   246     val def_table = const_def_table ctxt subst defs
   247     val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
   248     val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
   249     val psimp_table = const_psimp_table ctxt subst
   250     val choice_spec_table = const_choice_spec_table ctxt subst
   251     val user_nondefs =
   252       user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
   253     val intro_table = inductive_intro_table ctxt subst def_table
   254     val ground_thm_table = ground_theorem_table thy
   255     val ersatz_table = ersatz_table thy
   256     val (hol_ctxt as {wf_cache, ...}) =
   257       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
   258        stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
   259        binary_ints = binary_ints, destroy_constrs = destroy_constrs,
   260        specialize = specialize, star_linear_preds = star_linear_preds,
   261        fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
   262        case_names = case_names, def_table = def_table,
   263        nondef_table = nondef_table, user_nondefs = user_nondefs,
   264        simp_table = simp_table, psimp_table = psimp_table,
   265        choice_spec_table = choice_spec_table, intro_table = intro_table,
   266        ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
   267        skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
   268        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
   269        constr_cache = Unsynchronized.ref []}
   270     val frees = Term.add_frees assms_t []
   271     val _ = null (Term.add_tvars assms_t []) orelse
   272             raise NOT_SUPPORTED "schematic type variables"
   273     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
   274          binarize) = preprocess_term hol_ctxt finitizes monos assms_t
   275     val got_all_user_axioms =
   276       got_all_mono_user_axioms andalso no_poly_user_axioms
   277 
   278     fun print_wf (x, (gfp, wf)) =
   279       pprint (Pretty.blk (0,
   280           pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
   281           @ Syntax.pretty_term ctxt (Const x) ::
   282           pstrs (if wf then
   283                    "\" was proved well-founded. Nitpick can compute it \
   284                    \efficiently."
   285                  else
   286                    "\" could not be proved well-founded. Nitpick might need to \
   287                    \unroll it.")))
   288     val _ = if verbose then List.app print_wf (!wf_cache) else ()
   289     val _ =
   290       pprint_d (fn () => Pretty.chunks
   291           (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
   292            pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
   293            pretties_for_formulas ctxt "Relevant nondefinitional axiom"
   294                                  (tl nondef_ts)))
   295     val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts)
   296             handle TYPE (_, Ts, ts) =>
   297                    raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
   298 
   299     val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
   300     val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
   301     val (free_names, const_names) =
   302       fold add_free_and_const_names (nondef_us @ def_us) ([], [])
   303     val (sel_names, nonsel_names) =
   304       List.partition (is_sel o nickname_of) const_names
   305     val sound_finitizes =
   306       none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
   307                           | _ => false) finitizes)
   308     val standard = forall snd stds
   309 (*
   310     val _ = List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us)
   311 *)
   312 
   313     val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
   314     fun monotonicity_message Ts extra =
   315       let val ss = map (quote o string_for_type ctxt) Ts 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") ^ " considered monotonic") ^
   322         ". " ^ extra
   323       end
   324     fun is_type_fundamentally_monotonic T =
   325       (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
   326        (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
   327       is_number_type thy T orelse is_bit_type T
   328     fun is_type_actually_monotonic T =
   329       formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
   330     fun is_type_kind_of_monotonic T =
   331       case triple_lookup (type_match thy) monos T of
   332         SOME (SOME false) => false
   333       | _ => is_type_actually_monotonic T
   334     fun is_type_monotonic T =
   335       unique_scope orelse
   336       case triple_lookup (type_match thy) monos T of
   337         SOME (SOME b) => b
   338       | _ => is_type_fundamentally_monotonic T orelse
   339              is_type_actually_monotonic T
   340     fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
   341         is_type_kind_of_monotonic T
   342       | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
   343         is_type_kind_of_monotonic T
   344       | is_shallow_datatype_finitizable T =
   345         case triple_lookup (type_match thy) finitizes T of
   346           SOME (SOME b) => b
   347         | _ => is_type_kind_of_monotonic T
   348     fun is_datatype_deep T =
   349       not standard orelse T = nat_T orelse is_word_type T orelse
   350       exists (curry (op =) T o domain_type o type_of) sel_names
   351     val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
   352                  |> sort Term_Ord.typ_ord
   353     val _ = if verbose andalso binary_ints = SOME true andalso
   354                exists (member (op =) [nat_T, int_T]) all_Ts then
   355               print_v (K "The option \"binary_ints\" will be ignored because \
   356                          \of the presence of rationals, reals, \"Suc\", \
   357                          \\"gcd\", or \"lcm\" in the problem or because of the \
   358                          \\"non_std\" option.")
   359             else
   360               ()
   361     val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
   362     val _ =
   363       if verbose andalso not unique_scope then
   364         case filter_out is_type_fundamentally_monotonic mono_Ts of
   365           [] => ()
   366         | interesting_mono_Ts =>
   367           print_v (K (monotonicity_message interesting_mono_Ts
   368                          "Nitpick might be able to skip some scopes."))
   369       else
   370         ()
   371     val (deep_dataTs, shallow_dataTs) =
   372       all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
   373     val finitizable_dataTs =
   374       shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
   375                      |> filter is_shallow_datatype_finitizable
   376     val _ =
   377       if verbose andalso not (null finitizable_dataTs) then
   378         print_v (K (monotonicity_message finitizable_dataTs
   379                         "Nitpick can use a more precise finite encoding."))
   380       else
   381         ()
   382     (* This detection code is an ugly hack. Fortunately, it is used only to
   383        provide a hint to the user. *)
   384     fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
   385       not (null fixes) andalso
   386       exists (String.isSuffix ".hyps" o fst) assumes andalso
   387       exists (exists (curry (op =) name o shortest_name o fst)
   388               o datatype_constrs hol_ctxt) deep_dataTs
   389     val likely_in_struct_induct_step =
   390       exists is_struct_induct_step (ProofContext.cases_of ctxt)
   391     val _ = if standard andalso likely_in_struct_induct_step then
   392               pprint_m (fn () => Pretty.blk (0,
   393                   pstrs "Hint: To check that the induction hypothesis is \
   394                         \general enough, try this command: " @
   395                   [Pretty.mark Markup.sendback (Pretty.blk (0,
   396                        pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
   397             else
   398               ()
   399 (*
   400     val _ = print_g "Monotonic types:"
   401     val _ = List.app (print_g o string_for_type ctxt) mono_Ts
   402     val _ = print_g "Nonmonotonic types:"
   403     val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts
   404 *)
   405 
   406     val incremental = Int.max (max_potential, max_genuine) >= 2
   407     val actual_sat_solver =
   408       if sat_solver <> "smart" then
   409         if incremental andalso
   410            not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
   411                        sat_solver) then
   412           (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
   413                        \be used instead of " ^ quote sat_solver ^ "."));
   414            "SAT4J")
   415         else
   416           sat_solver
   417       else
   418         Kodkod_SAT.smart_sat_solver_name incremental
   419     val _ =
   420       if sat_solver = "smart" then
   421         print_v (fn () =>
   422             "Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^
   423             (if incremental then " incremental " else " ") ^
   424             "solvers are configured: " ^
   425             commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".")
   426       else
   427         ()
   428 
   429     val too_big_scopes = Unsynchronized.ref []
   430 
   431     fun problem_for_scope unsound
   432             (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
   433       let
   434         val _ = not (exists (fn other => scope_less_eq other scope)
   435                             (!too_big_scopes)) orelse
   436                 raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
   437                                  \problem_for_scope", "too large scope")
   438 (*
   439         val _ = print_g "Offsets:"
   440         val _ = List.app (fn (T, j0) =>
   441                              print_g (string_for_type ctxt T ^ " = " ^
   442                                     string_of_int j0))
   443                          (Typtab.dest ofs)
   444 *)
   445         val all_exact = forall (is_exact_type datatypes true) all_Ts
   446         val repify_consts = choose_reps_for_consts scope all_exact
   447         val main_j0 = offset_of_type ofs bool_T
   448         val (nat_card, nat_j0) = spec_of_type scope nat_T
   449         val (int_card, int_j0) = spec_of_type scope int_T
   450         val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse
   451                 raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope",
   452                            "bad offsets")
   453         val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
   454         val (free_names, rep_table) =
   455           choose_reps_for_free_vars scope free_names NameTable.empty
   456         val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
   457         val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table
   458         val min_highest_arity =
   459           NameTable.fold (Integer.max o arity_of_rep o snd) rep_table 1
   460         val min_univ_card =
   461           NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table
   462                          (univ_card nat_card int_card main_j0 [] KK.True)
   463         val _ = check_arity min_univ_card min_highest_arity
   464 
   465         val def_us = map (choose_reps_in_nut scope unsound rep_table true)
   466                          def_us
   467         val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
   468                             nondef_us
   469 (*
   470         val _ = List.app (print_g o string_for_nut ctxt)
   471                          (free_names @ sel_names @ nonsel_names @
   472                           nondef_us @ def_us)
   473 *)
   474         val (free_rels, pool, rel_table) =
   475           rename_free_vars free_names initial_pool NameTable.empty
   476         val (sel_rels, pool, rel_table) =
   477           rename_free_vars sel_names pool rel_table
   478         val (other_rels, pool, rel_table) =
   479           rename_free_vars nonsel_names pool rel_table
   480         val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
   481         val def_us = map (rename_vars_in_nut pool rel_table) def_us
   482         val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
   483         val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
   484         val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
   485         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
   486                       Print_Mode.setmp [] multiline_string_for_scope scope
   487         val kodkod_sat_solver =
   488           Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
   489         val bit_width = if bits = 0 then 16 else bits + 1
   490         val delay =
   491           if unsound then
   492             Option.map (fn time => Time.- (time, Time.now ())) deadline
   493             |> unsound_delay_for_timeout
   494           else
   495             0
   496         val settings = [("solver", commas_quote kodkod_sat_solver),
   497                         ("skolem_depth", "-1"),
   498                         ("bit_width", string_of_int bit_width),
   499                         ("symmetry_breaking", "20"),
   500                         ("sharing", "3"),
   501                         ("flatten", "false"),
   502                         ("delay", signed_string_of_int delay)]
   503         val plain_rels = free_rels @ other_rels
   504         val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
   505         val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
   506         val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
   507         val dtype_axioms =
   508           declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk
   509                                            rel_table datatypes
   510         val declarative_axioms = plain_axioms @ dtype_axioms
   511         val univ_card = Int.max (univ_card nat_card int_card main_j0
   512                                      (plain_bounds @ sel_bounds) formula,
   513                                  main_j0 |> bits > 0 ? Integer.add (bits + 1))
   514         val built_in_bounds = bounds_for_built_in_rels_in_formula debug
   515                                   univ_card nat_card int_card main_j0 formula
   516         val bounds = built_in_bounds @ plain_bounds @ sel_bounds
   517                      |> not debug ? merge_bounds
   518         val highest_arity =
   519           fold Integer.max (map (fst o fst) (maps fst bounds)) 0
   520         val formula = fold_rev s_and declarative_axioms formula
   521         val _ = if bits = 0 then () else check_bits bits formula
   522         val _ = if formula = KK.False then ()
   523                 else check_arity univ_card highest_arity
   524       in
   525         SOME ({comment = comment, settings = settings, univ_card = univ_card,
   526                tuple_assigns = [], bounds = bounds,
   527                int_bounds = if bits = 0 then sequential_int_bounds univ_card
   528                             else pow_of_two_int_bounds bits main_j0,
   529                expr_assigns = [], formula = formula},
   530               {free_names = free_names, sel_names = sel_names,
   531                nonsel_names = nonsel_names, rel_table = rel_table,
   532                unsound = unsound, scope = scope})
   533       end
   534       handle TOO_LARGE (loc, msg) =>
   535              if loc = "Nitpick_Kodkod.check_arity" andalso
   536                 not (Typtab.is_empty ofs) then
   537                problem_for_scope unsound
   538                    {hol_ctxt = hol_ctxt, binarize = binarize,
   539                     card_assigns = card_assigns, bits = bits,
   540                     bisim_depth = bisim_depth, datatypes = datatypes,
   541                     ofs = Typtab.empty}
   542              else if loc = "Nitpick.pick_them_nits_in_term.\
   543                            \problem_for_scope" then
   544                NONE
   545              else
   546                (Unsynchronized.change too_big_scopes (cons scope);
   547                 print_v (fn () => ("Limit reached: " ^ msg ^
   548                                    ". Skipping " ^ (if unsound then "potential"
   549                                                     else "genuine") ^
   550                                    " component of scope."));
   551                 NONE)
   552            | TOO_SMALL (_, msg) =>
   553              (print_v (fn () => ("Limit reached: " ^ msg ^
   554                                  ". Skipping " ^ (if unsound then "potential"
   555                                                   else "genuine") ^
   556                                  " component of scope."));
   557               NONE)
   558 
   559     val das_wort_model =
   560       (if falsify then "counterexample" else "model")
   561       |> not standard ? prefix "nonstandard "
   562 
   563     val scopes = Unsynchronized.ref []
   564     val generated_scopes = Unsynchronized.ref []
   565     val generated_problems = Unsynchronized.ref ([] : rich_problem list)
   566     val checked_problems = Unsynchronized.ref (SOME [])
   567     val met_potential = Unsynchronized.ref 0
   568 
   569     fun update_checked_problems problems =
   570       List.app (Unsynchronized.change checked_problems o Option.map o cons
   571                 o nth problems)
   572     fun show_kodkod_warning "" = ()
   573       | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".")
   574 
   575     fun print_and_check_model genuine bounds
   576             ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
   577              : problem_extension) =
   578       let
   579         val (reconstructed_model, codatatypes_ok) =
   580           reconstruct_hol_model {show_datatypes = show_datatypes,
   581                                  show_consts = show_consts}
   582               scope formats frees free_names sel_names nonsel_names rel_table
   583               bounds
   584         val genuine_means_genuine =
   585           got_all_user_axioms andalso none_true wfs andalso
   586           sound_finitizes andalso codatatypes_ok
   587       in
   588         (pprint (Pretty.chunks
   589              [Pretty.blk (0,
   590                   (pstrs ("Nitpick found a" ^
   591                           (if not genuine then " potential "
   592                            else if genuine_means_genuine then " "
   593                            else " quasi genuine ") ^ das_wort_model) @
   594                    (case pretties_for_scope scope verbose of
   595                       [] => []
   596                     | pretties => pstrs " for " @ pretties) @
   597                    [Pretty.str ":\n"])),
   598               Pretty.indent indent_size reconstructed_model]);
   599          if genuine then
   600            (if check_genuine andalso standard then
   601               case prove_hol_model scope tac_timeout free_names sel_names
   602                                    rel_table bounds assms_t of
   603                 SOME true =>
   604                 print ("Confirmation by \"auto\": The above " ^
   605                        das_wort_model ^ " is really genuine.")
   606               | SOME false =>
   607                 if genuine_means_genuine then
   608                   error ("A supposedly genuine " ^ das_wort_model ^ " was \
   609                          \shown to be spurious by \"auto\".\nThis should never \
   610                          \happen.\nPlease send a bug report to blanchet\
   611                          \te@in.tum.de.")
   612                  else
   613                    print ("Refutation by \"auto\": The above " ^
   614                           das_wort_model ^ " is spurious.")
   615                | NONE => print "No confirmation by \"auto\"."
   616             else
   617               ();
   618             if not standard andalso likely_in_struct_induct_step then
   619               print "The existence of a nonstandard model suggests that the \
   620                     \induction hypothesis is not general enough or may even be \
   621                     \wrong. See the Nitpick manual's \"Inductive Properties\" \
   622                     \section for details (\"isabelle doc nitpick\")."
   623             else
   624               ();
   625             if has_syntactic_sorts orig_t then
   626               print "Hint: Maybe you forgot a type constraint?"
   627             else
   628               ();
   629             if not genuine_means_genuine then
   630               if no_poly_user_axioms then
   631                 let
   632                   val options =
   633                     [] |> not got_all_mono_user_axioms
   634                           ? cons ("user_axioms", "\"true\"")
   635                        |> not (none_true wfs)
   636                           ? cons ("wf", "\"smart\" or \"false\"")
   637                        |> not sound_finitizes
   638                           ? cons ("finitize", "\"smart\" or \"false\"")
   639                        |> not codatatypes_ok
   640                           ? cons ("bisim_depth", "a nonnegative value")
   641                   val ss =
   642                     map (fn (name, value) => quote name ^ " set to " ^ value)
   643                         options
   644                 in
   645                   print ("Try again with " ^
   646                          space_implode " " (serial_commas "and" ss) ^
   647                          " to confirm that the " ^ das_wort_model ^
   648                          " is genuine.")
   649                 end
   650               else
   651                 print ("Nitpick is unable to guarantee the authenticity of \
   652                        \the " ^ das_wort_model ^ " in the presence of \
   653                        \polymorphic axioms.")
   654             else
   655               ();
   656             NONE)
   657          else
   658            if not genuine then
   659              (Unsynchronized.inc met_potential;
   660               if check_potential then
   661                 let
   662                   val status = prove_hol_model scope tac_timeout free_names
   663                                               sel_names rel_table bounds assms_t
   664                 in
   665                   (case status of
   666                      SOME true => print ("Confirmation by \"auto\": The \
   667                                          \above " ^ das_wort_model ^
   668                                          " is genuine.")
   669                    | SOME false => print ("Refutation by \"auto\": The above " ^
   670                                           das_wort_model ^ " is spurious.")
   671                    | NONE => print "No confirmation by \"auto\".");
   672                   status
   673                 end
   674               else
   675                 NONE)
   676            else
   677              NONE)
   678         |> pair genuine_means_genuine
   679       end
   680     fun solve_any_problem (found_really_genuine, max_potential, max_genuine,
   681                            donno) first_time problems =
   682       let
   683         val max_potential = Int.max (0, max_potential)
   684         val max_genuine = Int.max (0, max_genuine)
   685         fun print_and_check genuine (j, bounds) =
   686           print_and_check_model genuine bounds (snd (nth problems j))
   687         val max_solutions = max_potential + max_genuine
   688                             |> not incremental ? Integer.min 1
   689       in
   690         if max_solutions <= 0 then
   691           (found_really_genuine, 0, 0, donno)
   692         else
   693           case KK.solve_any_problem overlord deadline max_threads max_solutions
   694                                     (map fst problems) of
   695             KK.JavaNotInstalled =>
   696             (print_m install_java_message;
   697              (found_really_genuine, max_potential, max_genuine, donno + 1))
   698           | KK.KodkodiNotInstalled =>
   699             (print_m install_kodkodi_message;
   700              (found_really_genuine, max_potential, max_genuine, donno + 1))
   701           | KK.Normal ([], unsat_js, s) =>
   702             (update_checked_problems problems unsat_js; show_kodkod_warning s;
   703              (found_really_genuine, max_potential, max_genuine, donno))
   704           | KK.Normal (sat_ps, unsat_js, s) =>
   705             let
   706               val (lib_ps, con_ps) =
   707                 List.partition (#unsound o snd o nth problems o fst) sat_ps
   708             in
   709               update_checked_problems problems (unsat_js @ map fst lib_ps);
   710               show_kodkod_warning s;
   711               if null con_ps then
   712                 let
   713                   val genuine_codes =
   714                     lib_ps |> take max_potential
   715                            |> map (print_and_check false)
   716                            |> filter (curry (op =) (SOME true) o snd)
   717                   val found_really_genuine =
   718                     found_really_genuine orelse exists fst genuine_codes
   719                   val num_genuine = length genuine_codes
   720                   val max_genuine = max_genuine - num_genuine
   721                   val max_potential = max_potential
   722                                       - (length lib_ps - num_genuine)
   723                 in
   724                   if max_genuine <= 0 then
   725                     (found_really_genuine, 0, 0, donno)
   726                   else
   727                     let
   728                       (* "co_js" is the list of sound problems whose unsound
   729                          pendants couldn't be satisfied and hence that most
   730                          probably can't be satisfied themselves. *)
   731                       val co_js =
   732                         map (fn j => j - 1) unsat_js
   733                         |> filter (fn j =>
   734                                       j >= 0 andalso
   735                                       scopes_equivalent
   736                                           (#scope (snd (nth problems j)),
   737                                            #scope (snd (nth problems (j + 1)))))
   738                       val bye_js = sort_distinct int_ord (map fst sat_ps @
   739                                                           unsat_js @ co_js)
   740                       val problems =
   741                         problems |> filter_out_indices bye_js
   742                                  |> max_potential <= 0
   743                                     ? filter_out (#unsound o snd)
   744                     in
   745                       solve_any_problem (found_really_genuine, max_potential,
   746                                          max_genuine, donno) false problems
   747                     end
   748                 end
   749               else
   750                 let
   751                   val genuine_codes =
   752                     con_ps |> take max_genuine
   753                            |> map (print_and_check true)
   754                   val max_genuine = max_genuine - length genuine_codes
   755                   val found_really_genuine =
   756                     found_really_genuine orelse exists fst genuine_codes
   757                 in
   758                   if max_genuine <= 0 orelse not first_time then
   759                     (found_really_genuine, 0, max_genuine, donno)
   760                   else
   761                     let
   762                       val bye_js = sort_distinct int_ord
   763                                                  (map fst sat_ps @ unsat_js)
   764                       val problems =
   765                         problems |> filter_out_indices bye_js
   766                                  |> filter_out (#unsound o snd)
   767                     in
   768                       solve_any_problem (found_really_genuine, 0, max_genuine,
   769                                          donno) false problems
   770                     end
   771                 end
   772             end
   773           | KK.TimedOut unsat_js =>
   774             (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
   775           | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ())
   776           | KK.Interrupted (SOME unsat_js) =>
   777             (update_checked_problems problems unsat_js; do_interrupted ())
   778           | KK.Error (s, unsat_js) =>
   779             (update_checked_problems problems unsat_js;
   780              print_v (K ("Kodkod error: " ^ s ^ "."));
   781              (found_really_genuine, max_potential, max_genuine, donno + 1))
   782       end
   783 
   784     fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine,
   785                               donno) =
   786       let
   787         val _ =
   788           if null scopes then
   789             print_m (K "The scope specification is inconsistent.")
   790           else if verbose then
   791             pprint (Pretty.chunks
   792                 [Pretty.blk (0,
   793                      pstrs ((if n > 1 then
   794                                "Batch " ^ string_of_int (j + 1) ^ " of " ^
   795                                signed_string_of_int n ^ ": "
   796                              else
   797                                "") ^
   798                             "Trying " ^ string_of_int (length scopes) ^
   799                             " scope" ^ plural_s_for_list scopes ^ ":")),
   800                  Pretty.indent indent_size
   801                      (Pretty.chunks (map2
   802                           (fn j => fn scope =>
   803                               Pretty.block (
   804                                   (case pretties_for_scope scope true of
   805                                      [] => [Pretty.str "Empty"]
   806                                    | pretties => pretties) @
   807                                   [Pretty.str (if j = 1 then "." else ";")]))
   808                           (length scopes downto 1) scopes))])
   809           else
   810             ()
   811         fun add_problem_for_scope (scope, unsound) (problems, donno) =
   812           (check_deadline ();
   813            case problem_for_scope unsound scope of
   814              SOME problem =>
   815              (problems
   816               |> (null problems orelse
   817                   not (KK.problems_equivalent (fst problem, fst (hd problems))))
   818                   ? cons problem, donno)
   819            | NONE => (problems, donno + 1))
   820         val (problems, donno) =
   821           fold add_problem_for_scope
   822                (map_product pair scopes
   823                     ((if max_genuine > 0 then [false] else []) @
   824                      (if max_potential > 0 then [true] else [])))
   825                ([], donno)
   826         val _ = Unsynchronized.change generated_problems (append problems)
   827         val _ = Unsynchronized.change generated_scopes (append scopes)
   828         val _ =
   829           if j + 1 = n then
   830             let
   831               val (unsound_problems, sound_problems) =
   832                 List.partition (#unsound o snd) (!generated_problems)
   833             in
   834               if not (null sound_problems) andalso
   835                  forall (KK.is_problem_trivially_false o fst)
   836                         sound_problems then
   837                 print_m (fn () =>
   838                     "Warning: The conjecture either trivially holds for the \
   839                     \given scopes or lies outside Nitpick's supported \
   840                     \fragment." ^
   841                     (if exists (not o KK.is_problem_trivially_false o fst)
   842                                unsound_problems then
   843                        " Only potential " ^ das_wort_model ^ "s may be found."
   844                      else
   845                        ""))
   846               else
   847                 ()
   848             end
   849           else
   850             ()
   851       in
   852         solve_any_problem (found_really_genuine, max_potential, max_genuine,
   853                            donno) true (rev problems)
   854       end
   855 
   856     fun scope_count (problems : rich_problem list) scope =
   857       length (filter (curry scopes_equivalent scope o #scope o snd) problems)
   858     fun excipit did_so_and_so =
   859       let
   860         val do_filter =
   861           if !met_potential = max_potential then filter_out (#unsound o snd)
   862           else I
   863         val total = length (!scopes)
   864         val unsat =
   865           fold (fn scope =>
   866                    case scope_count (do_filter (!generated_problems)) scope of
   867                      0 => I
   868                    | n =>
   869                      scope_count (do_filter (these (!checked_problems)))
   870                                  scope = n
   871                      ? Integer.add 1) (!generated_scopes) 0
   872       in
   873         "Nitpick " ^ did_so_and_so ^
   874         (if is_some (!checked_problems) andalso total > 0 then
   875            " " ^ string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
   876            string_of_int total ^ " scope" ^ plural_s total
   877          else
   878            "") ^ "."
   879       end
   880 
   881     fun run_batches _ _ []
   882                     (found_really_genuine, max_potential, max_genuine, donno) =
   883         if donno > 0 andalso max_genuine > 0 then
   884           (print_m (fn () => excipit "checked"); "unknown")
   885         else if max_genuine = original_max_genuine then
   886           if max_potential = original_max_potential then
   887             (print_m (fn () =>
   888                  "Nitpick found no " ^ das_wort_model ^ "." ^
   889                  (if not standard andalso likely_in_struct_induct_step then
   890                     " This suggests that the induction hypothesis might be \
   891                     \general enough to prove this subgoal."
   892                   else
   893                     "")); "none")
   894           else
   895             (print_m (fn () =>
   896                  "Nitpick could not find a" ^
   897                  (if max_genuine = 1 then " better " ^ das_wort_model ^ "."
   898                   else "ny better " ^ das_wort_model ^ "s.")); "potential")
   899         else if found_really_genuine then
   900           "genuine"
   901         else
   902           "quasi_genuine"
   903       | run_batches j n (batch :: batches) z =
   904         let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in
   905           run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
   906         end
   907 
   908     val (skipped, the_scopes) =
   909       all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
   910                  bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
   911                  finitizable_dataTs
   912     val _ = if skipped > 0 then
   913               print_m (fn () => "Too many scopes. Skipping " ^
   914                                 string_of_int skipped ^ " scope" ^
   915                                 plural_s skipped ^
   916                                 ". (Consider using \"mono\" or \
   917                                 \\"merge_type_vars\" to prevent this.)")
   918             else
   919               ()
   920     val _ = scopes := the_scopes
   921 
   922     val batches = batch_list batch_size (!scopes)
   923     val outcome_code =
   924       (run_batches 0 (length batches) batches
   925                    (false, max_potential, max_genuine, 0)
   926        handle Exn.Interrupt => do_interrupted ())
   927       handle TimeLimit.TimeOut =>
   928              (print_m (fn () => excipit "ran out of time after checking");
   929               if !met_potential > 0 then "potential" else "unknown")
   930            | Exn.Interrupt =>
   931              if auto orelse debug then raise Interrupt
   932              else error (excipit "was interrupted after checking")
   933     val _ = print_v (fn () => "Total time: " ^
   934                               signed_string_of_int (Time.toMilliseconds
   935                                     (Timer.checkRealTimer timer)) ^ " ms.")
   936   in (outcome_code, !state_ref) end
   937   handle Exn.Interrupt =>
   938          if auto orelse #debug params then
   939            raise Interrupt
   940          else
   941            if passed_deadline deadline then
   942              (priority "Nitpick ran out of time."; ("unknown", state))
   943            else
   944              error "Nitpick was interrupted."
   945 
   946 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
   947                       step subst orig_assm_ts orig_t =
   948   if getenv "KODKODI" = "" then
   949     (if auto then ()
   950      else warning (Pretty.string_of (plazy install_kodkodi_message));
   951      ("unknown", state))
   952   else
   953     let
   954       val deadline = Option.map (curry Time.+ (Time.now ())) timeout
   955       val outcome as (outcome_code, _) =
   956         time_limit (if debug then NONE else timeout)
   957             (pick_them_nits_in_term deadline state params auto i n step subst
   958                                     orig_assm_ts) orig_t
   959     in
   960       if expect = "" orelse outcome_code = expect then outcome
   961       else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   962     end
   963 
   964 fun is_fixed_equation fixes
   965                       (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
   966     member (op =) fixes s
   967   | is_fixed_equation _ _ = false
   968 fun extract_fixed_frees ctxt (assms, t) =
   969   let
   970     val fixes = Variable.fixes_of ctxt |> map snd
   971     val (subst, other_assms) =
   972       List.partition (is_fixed_equation fixes) assms
   973       |>> map Logic.dest_equals
   974   in (subst, other_assms, subst_atomic subst t) end
   975 
   976 fun pick_nits_in_subgoal state params auto i step =
   977   let
   978     val ctxt = Proof.context_of state
   979     val t = state |> Proof.raw_goal |> #goal |> prop_of
   980   in
   981     case Logic.count_prems t of
   982       0 => (priority "No subgoal!"; ("none", state))
   983     | n =>
   984       let
   985         val t = Logic.goal_params t i |> fst
   986         val assms = map term_of (Assumption.all_assms_of ctxt)
   987         val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
   988       in pick_nits_in_term state params auto i n step subst assms t end
   989   end
   990 
   991 end;