more work on "fix_datatype_vals" optimization (renamed "preconstruct")
authorblanchet
Mon Feb 21 17:36:32 2011 +0100 (2011-02-21)
changeset 41803ef13e3b7cbaf
parent 41802 7592a165fa0b
child 41804 90dd5291afd8
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 16:33:21 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 17:36:32 2011 +0100
     1.3 @@ -34,8 +34,8 @@
     1.4       destroy_constrs: bool,
     1.5       specialize: bool,
     1.6       star_linear_preds: bool,
     1.7 +     preconstrs: (term option * bool option) list,
     1.8       peephole_optim: bool,
     1.9 -     fix_datatype_vals: bool,
    1.10       datatype_sym_break: int,
    1.11       kodkod_sym_break: int,
    1.12       timeout: Time.time option,
    1.13 @@ -108,8 +108,8 @@
    1.14     destroy_constrs: bool,
    1.15     specialize: bool,
    1.16     star_linear_preds: bool,
    1.17 +   preconstrs: (term option * bool option) list,
    1.18     peephole_optim: bool,
    1.19 -   fix_datatype_vals: bool,
    1.20     datatype_sym_break: int,
    1.21     kodkod_sym_break: int,
    1.22     timeout: Time.time option,
    1.23 @@ -211,10 +211,10 @@
    1.24           boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    1.25           verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
    1.26           binary_ints, destroy_constrs, specialize, star_linear_preds,
    1.27 -         peephole_optim, fix_datatype_vals, datatype_sym_break,
    1.28 -         kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
    1.29 -         show_consts, evals, formats, atomss, max_potential, max_genuine,
    1.30 -         check_potential, check_genuine, batch_size, ...} = params
    1.31 +         preconstrs, peephole_optim, datatype_sym_break, kodkod_sym_break,
    1.32 +         tac_timeout, max_threads, show_datatypes, show_consts, evals, formats,
    1.33 +         atomss, max_potential, max_genuine, check_potential, check_genuine,
    1.34 +         batch_size, ...} = params
    1.35      val state_ref = Unsynchronized.ref state
    1.36      val pprint =
    1.37        if auto then
    1.38 @@ -282,21 +282,23 @@
    1.39         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    1.40         whacks = whacks, binary_ints = binary_ints,
    1.41         destroy_constrs = destroy_constrs, specialize = specialize,
    1.42 -       star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
    1.43 -       evals = evals, case_names = case_names, def_tables = def_tables,
    1.44 -       nondef_table = nondef_table, user_nondefs = user_nondefs,
    1.45 -       simp_table = simp_table, psimp_table = psimp_table,
    1.46 -       choice_spec_table = choice_spec_table, intro_table = intro_table,
    1.47 -       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    1.48 -       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    1.49 +       star_linear_preds = star_linear_preds, preconstrs = preconstrs,
    1.50 +       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
    1.51 +       def_tables = def_tables, nondef_table = nondef_table,
    1.52 +       user_nondefs = user_nondefs, simp_table = simp_table,
    1.53 +       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    1.54 +       intro_table = intro_table, ground_thm_table = ground_thm_table,
    1.55 +       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    1.56 +       special_funs = Unsynchronized.ref [],
    1.57         unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    1.58         constr_cache = Unsynchronized.ref []}
    1.59      val pseudo_frees = []
    1.60      val real_frees = fold Term.add_frees (neg_t :: assm_ts) []
    1.61      val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
    1.62              raise NOT_SUPPORTED "schematic type variables"
    1.63 -    val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
    1.64 -         binarize) = preprocess_formulas hol_ctxt assm_ts neg_t
    1.65 +    val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
    1.66 +         no_poly_user_axioms, binarize) =
    1.67 +      preprocess_formulas hol_ctxt assm_ts neg_t
    1.68      val got_all_user_axioms =
    1.69        got_all_mono_user_axioms andalso no_poly_user_axioms
    1.70  
    1.71 @@ -324,13 +326,7 @@
    1.72  
    1.73      val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
    1.74      val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
    1.75 -    val needed_us =
    1.76 -      if fix_datatype_vals then
    1.77 -        [@{term "[A, B, C, A]"}, @{term "[C, B, A]"}]
    1.78 -        |> map (nut_from_term hol_ctxt Eq)
    1.79 -        (* infer_needed_constructs ### *)
    1.80 -      else
    1.81 -        []
    1.82 +    val preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq)
    1.83      val (free_names, const_names) =
    1.84        fold add_free_and_const_names (nondef_us @ def_us) ([], [])
    1.85      val (sel_names, nonsel_names) =
    1.86 @@ -519,8 +515,8 @@
    1.87            def_us |> map (choose_reps_in_nut scope unsound rep_table true)
    1.88          val nondef_us =
    1.89            nondef_us |> map (choose_reps_in_nut scope unsound rep_table false)
    1.90 -        val needed_us =
    1.91 -          needed_us |> map (choose_reps_in_nut scope unsound rep_table false)
    1.92 +        val preconstr_us =
    1.93 +          preconstr_us |> map (choose_reps_in_nut scope unsound rep_table false)
    1.94  (*
    1.95          val _ = List.app (print_g o string_for_nut ctxt)
    1.96                           (free_names @ sel_names @ nonsel_names @
    1.97 @@ -534,7 +530,8 @@
    1.98            rename_free_vars nonsel_names pool rel_table
    1.99          val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table)
   1.100          val def_us = def_us |> map (rename_vars_in_nut pool rel_table)
   1.101 -        val needed_us = needed_us |> map (rename_vars_in_nut pool rel_table)
   1.102 +        val preconstr_us =
   1.103 +          preconstr_us |> map (rename_vars_in_nut pool rel_table)
   1.104          val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
   1.105          val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
   1.106          val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
   1.107 @@ -560,7 +557,7 @@
   1.108          val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
   1.109          val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
   1.110          val dtype_axioms =
   1.111 -          declarative_axioms_for_datatypes hol_ctxt binarize needed_us
   1.112 +          declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
   1.113                datatype_sym_break bits ofs kk rel_table datatypes
   1.114          val declarative_axioms = plain_axioms @ dtype_axioms
   1.115          val univ_card = Int.max (univ_card nat_card int_card main_j0
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 16:33:21 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 17:36:32 2011 +0100
     2.3 @@ -27,6 +27,7 @@
     2.4       destroy_constrs: bool,
     2.5       specialize: bool,
     2.6       star_linear_preds: bool,
     2.7 +     preconstrs: (term option * bool option) list,
     2.8       tac_timeout: Time.time option,
     2.9       evals: term list,
    2.10       case_names: (string * int) list,
    2.11 @@ -257,6 +258,7 @@
    2.12     destroy_constrs: bool,
    2.13     specialize: bool,
    2.14     star_linear_preds: bool,
    2.15 +   preconstrs: (term option * bool option) list,
    2.16     tac_timeout: Time.time option,
    2.17     evals: term list,
    2.18     case_names: (string * int) list,
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Feb 21 16:33:21 2011 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Feb 21 17:36:32 2011 +0100
     3.3 @@ -58,8 +58,8 @@
     3.4     ("destroy_constrs", "true"),
     3.5     ("specialize", "true"),
     3.6     ("star_linear_preds", "true"),
     3.7 +   ("preconstr", "smart"),
     3.8     ("peephole_optim", "true"),
     3.9 -   ("fix_datatype_vals", "true"),
    3.10     ("datatype_sym_break", "5"),
    3.11     ("kodkod_sym_break", "15"),
    3.12     ("timeout", "30"),
    3.13 @@ -91,8 +91,8 @@
    3.14     ("dont_destroy_constrs", "destroy_constrs"),
    3.15     ("dont_specialize", "specialize"),
    3.16     ("dont_star_linear_preds", "star_linear_preds"),
    3.17 +   ("dont_preconstr", "preconstr"),
    3.18     ("no_peephole_optim", "peephole_optim"),
    3.19 -   ("fix_datatype_vals", "dont_fix_datatype_vals"),
    3.20     ("no_debug", "debug"),
    3.21     ("quiet", "verbose"),
    3.22     ("no_overlord", "overlord"),
    3.23 @@ -104,11 +104,11 @@
    3.24  fun is_known_raw_param s =
    3.25    AList.defined (op =) default_default_params s orelse
    3.26    AList.defined (op =) negated_params s orelse
    3.27 -  member (op =) ["max", "show_all", "whack", "atoms", "eval", "expect"] s orelse
    3.28 +  member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse
    3.29    exists (fn p => String.isPrefix (p ^ " ") s)
    3.30           ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
    3.31 -          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
    3.32 -          "atoms"]
    3.33 +          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr",
    3.34 +          "dont_preconstr", "format", "atoms"]
    3.35  
    3.36  fun check_raw_param (s, _) =
    3.37    if is_known_raw_param s then ()
    3.38 @@ -253,8 +253,9 @@
    3.39      val destroy_constrs = lookup_bool "destroy_constrs"
    3.40      val specialize = lookup_bool "specialize"
    3.41      val star_linear_preds = lookup_bool "star_linear_preds"
    3.42 +    val preconstrs =
    3.43 +      lookup_bool_option_assigns read_term_polymorphic "preconstr"
    3.44      val peephole_optim = lookup_bool "peephole_optim"
    3.45 -    val fix_datatype_vals = lookup_bool "fix_datatype_vals"
    3.46      val datatype_sym_break = lookup_int "datatype_sym_break"
    3.47      val kodkod_sym_break = lookup_int "kodkod_sym_break"
    3.48      val timeout = if auto then NONE else lookup_time "timeout"
    3.49 @@ -262,9 +263,9 @@
    3.50      val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
    3.51      val show_datatypes = debug orelse lookup_bool "show_datatypes"
    3.52      val show_consts = debug orelse lookup_bool "show_consts"
    3.53 +    val evals = lookup_term_list_polymorphic "eval"
    3.54      val formats = lookup_ints_assigns read_term_polymorphic "format" 0
    3.55      val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
    3.56 -    val evals = lookup_term_list_polymorphic "eval"
    3.57      val max_potential =
    3.58        if auto then 0 else Int.max (0, lookup_int "max_potential")
    3.59      val max_genuine = Int.max (0, lookup_int "max_genuine")
    3.60 @@ -284,13 +285,12 @@
    3.61       user_axioms = user_axioms, assms = assms, whacks = whacks,
    3.62       merge_type_vars = merge_type_vars, binary_ints = binary_ints,
    3.63       destroy_constrs = destroy_constrs, specialize = specialize,
    3.64 -     star_linear_preds = star_linear_preds, peephole_optim = peephole_optim,
    3.65 -     fix_datatype_vals = fix_datatype_vals,
    3.66 -     datatype_sym_break = datatype_sym_break,
    3.67 +     star_linear_preds = star_linear_preds, preconstrs = preconstrs,
    3.68 +     peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
    3.69       kodkod_sym_break = kodkod_sym_break, timeout = timeout,
    3.70       tac_timeout = tac_timeout, max_threads = max_threads,
    3.71       show_datatypes = show_datatypes, show_consts = show_consts,
    3.72 -     formats = formats, atomss = atomss, evals = evals,
    3.73 +     evals = evals, formats = formats, atomss = atomss,
    3.74       max_potential = max_potential, max_genuine = max_genuine,
    3.75       check_potential = check_potential, check_genuine = check_genuine,
    3.76       batch_size = batch_size, expect = expect}
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Feb 21 16:33:21 2011 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Feb 21 17:36:32 2011 +0100
     4.3 @@ -1478,8 +1478,8 @@
     4.4                        "malformed Kodkod formula")
     4.5    end
     4.6  
     4.7 -fun needed_value_axioms_for_datatype [] _ _ _ = []
     4.8 -  | needed_value_axioms_for_datatype needed_us ofs kk
     4.9 +fun preconstructed_value_axioms_for_datatype [] _ _ _ = []
    4.10 +  | preconstructed_value_axioms_for_datatype preconstr_us ofs kk
    4.11          ({typ, card, constrs, ...} : datatype_spec) =
    4.12      let
    4.13        fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
    4.14 @@ -1507,9 +1507,10 @@
    4.15                   else
    4.16                     accum)
    4.17          | aux u =
    4.18 -          raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
    4.19 +          raise NUT ("Nitpick_Kodkod.preconstructed_value_axioms_for_datatype\
    4.20 +                     \.aux", [u])
    4.21      in
    4.22 -      case SOME (index_seq 0 card, []) |> fold aux needed_us of
    4.23 +      case SOME (index_seq 0 card, []) |> fold aux preconstr_us of
    4.24          SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)
    4.25        | NONE => [KK.False]
    4.26      end
    4.27 @@ -1653,33 +1654,34 @@
    4.28                                                nfas dtypes)
    4.29    end
    4.30  
    4.31 -fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
    4.32 -    T = T' orelse exists (is_datatype_in_needed_value T) us
    4.33 -  | is_datatype_in_needed_value _ _ = false
    4.34 +fun is_datatype_in_preconstructed_value T (Construct (_, T', _, us)) =
    4.35 +    T = T' orelse exists (is_datatype_in_preconstructed_value T) us
    4.36 +  | is_datatype_in_preconstructed_value _ _ = false
    4.37  
    4.38  val min_sym_break_card = 7
    4.39  
    4.40 -fun sym_break_axioms_for_datatypes hol_ctxt binarize needed_us
    4.41 +fun sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
    4.42                                     datatype_sym_break kk rel_table nfas dtypes =
    4.43    if datatype_sym_break = 0 then
    4.44      []
    4.45    else
    4.46 -    maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas
    4.47 -                                        dtypes)
    4.48 -         (dtypes |> filter is_datatype_acyclic
    4.49 -                 |> filter (fn {constrs = [_], ...} => false
    4.50 -                             | {card, constrs, ...} =>
    4.51 -                               card >= min_sym_break_card andalso
    4.52 -                               forall (forall (not o is_higher_order_type)
    4.53 -                                       o binder_types o snd o #const) constrs)
    4.54 -                 |> filter_out (fn {typ, ...} =>
    4.55 -                                   exists (is_datatype_in_needed_value typ)
    4.56 -                                          needed_us)
    4.57 -                 |> (fn dtypes' =>
    4.58 -                        dtypes'
    4.59 -                        |> length dtypes' > datatype_sym_break
    4.60 -                           ? (sort (datatype_ord o swap)
    4.61 -                              #> take datatype_sym_break)))
    4.62 +    dtypes |> filter is_datatype_acyclic
    4.63 +           |> filter (fn {constrs = [_], ...} => false
    4.64 +                       | {card, constrs, ...} =>
    4.65 +                         card >= min_sym_break_card andalso
    4.66 +                         forall (forall (not o is_higher_order_type)
    4.67 +                                 o binder_types o snd o #const) constrs)
    4.68 +           |> filter_out
    4.69 +                  (fn {typ, ...} =>
    4.70 +                      exists (is_datatype_in_preconstructed_value typ)
    4.71 +                             preconstr_us)
    4.72 +           |> (fn dtypes' =>
    4.73 +                  dtypes' |> length dtypes' > datatype_sym_break
    4.74 +                             ? (sort (datatype_ord o swap)
    4.75 +                                #> take datatype_sym_break))
    4.76 +           |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
    4.77 +                                                  nfas dtypes)
    4.78 +
    4.79  
    4.80  fun sel_axiom_for_sel hol_ctxt binarize j0
    4.81          (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
    4.82 @@ -1777,7 +1779,7 @@
    4.83        partition_axioms_for_datatype j0 kk rel_table dtype
    4.84      end
    4.85  
    4.86 -fun declarative_axioms_for_datatypes hol_ctxt binarize needed_us
    4.87 +fun declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
    4.88          datatype_sym_break bits ofs kk rel_table dtypes =
    4.89    let
    4.90      val nfas =
    4.91 @@ -1786,8 +1788,8 @@
    4.92               |> strongly_connected_sub_nfas
    4.93    in
    4.94      acyclicity_axioms_for_datatypes kk nfas @
    4.95 -    maps (needed_value_axioms_for_datatype needed_us ofs kk) dtypes @
    4.96 -    sym_break_axioms_for_datatypes hol_ctxt binarize needed_us
    4.97 +    maps (preconstructed_value_axioms_for_datatype preconstr_us ofs kk) dtypes @
    4.98 +    sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
    4.99          datatype_sym_break kk rel_table nfas dtypes @
   4.100      maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
   4.101           dtypes
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 21 16:33:21 2011 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 21 17:36:32 2011 +0100
     5.3 @@ -862,12 +862,12 @@
     5.4  fun reconstruct_hol_model {show_datatypes, show_consts}
     5.5          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
     5.6                        debug, whacks, binary_ints, destroy_constrs, specialize,
     5.7 -                      star_linear_preds, tac_timeout, evals, case_names,
     5.8 -                      def_tables, nondef_table, user_nondefs, simp_table,
     5.9 -                      psimp_table, choice_spec_table, intro_table,
    5.10 +                      star_linear_preds, preconstrs, tac_timeout, evals,
    5.11 +                      case_names, def_tables, nondef_table, user_nondefs,
    5.12 +                      simp_table, psimp_table, choice_spec_table, intro_table,
    5.13                        ground_thm_table, ersatz_table, skolems, special_funs,
    5.14 -                      unrolled_preds, wf_cache, constr_cache},
    5.15 -         binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    5.16 +                      unrolled_preds, wf_cache, constr_cache}, binarize,
    5.17 +                      card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    5.18          formats atomss real_frees pseudo_frees free_names sel_names nonsel_names
    5.19          rel_table bounds =
    5.20    let
    5.21 @@ -879,15 +879,15 @@
    5.22         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    5.23         whacks = whacks, binary_ints = binary_ints,
    5.24         destroy_constrs = destroy_constrs, specialize = specialize,
    5.25 -       star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
    5.26 -       evals = evals, case_names = case_names, def_tables = def_tables,
    5.27 -       nondef_table = nondef_table, user_nondefs = user_nondefs,
    5.28 -       simp_table = simp_table, psimp_table = psimp_table,
    5.29 -       choice_spec_table = choice_spec_table, intro_table = intro_table,
    5.30 -       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    5.31 -       skolems = skolems, special_funs = special_funs,
    5.32 -       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
    5.33 -       constr_cache = constr_cache}
    5.34 +       star_linear_preds = star_linear_preds, preconstrs = preconstrs,
    5.35 +       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
    5.36 +       def_tables = def_tables, nondef_table = nondef_table,
    5.37 +       user_nondefs = user_nondefs, simp_table = simp_table,
    5.38 +       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    5.39 +       intro_table = intro_table, ground_thm_table = ground_thm_table,
    5.40 +       ersatz_table = ersatz_table, skolems = skolems,
    5.41 +       special_funs = special_funs, unrolled_preds = unrolled_preds,
    5.42 +       wf_cache = wf_cache, constr_cache = constr_cache}
    5.43      val scope =
    5.44        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    5.45         bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 21 16:33:21 2011 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 21 17:36:32 2011 +0100
     6.3 @@ -10,7 +10,7 @@
     6.4    type hol_context = Nitpick_HOL.hol_context
     6.5    val preprocess_formulas :
     6.6      hol_context -> term list -> term
     6.7 -    -> term list * term list * bool * bool * bool
     6.8 +    -> term list * term list * term list * bool * bool * bool
     6.9  end;
    6.10  
    6.11  structure Nitpick_Preproc : NITPICK_PREPROC =
    6.12 @@ -1246,7 +1246,7 @@
    6.13  
    6.14  fun preprocess_formulas
    6.15          (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
    6.16 -                      ...}) assm_ts neg_t =
    6.17 +                      preconstrs, ...}) assm_ts neg_t =
    6.18    let
    6.19      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
    6.20        neg_t |> unfold_defs_in_term hol_ctxt
    6.21 @@ -1266,13 +1266,14 @@
    6.22      val table =
    6.23        Termtab.empty
    6.24        |> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)
    6.25 -    fun do_rest def =
    6.26 +    fun do_middle def =
    6.27        binarize ? binarize_nat_and_int_in_term
    6.28        #> box ? uncurry_term table
    6.29        #> box ? box_fun_and_pair_in_term hol_ctxt def
    6.30 -      #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
    6.31 -                            #> pull_out_existential_constrs hol_ctxt
    6.32 -                            #> destroy_pulled_out_constrs hol_ctxt def)
    6.33 +    fun do_tail def =
    6.34 +      destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
    6.35 +                         #> pull_out_existential_constrs hol_ctxt
    6.36 +                         #> destroy_pulled_out_constrs hol_ctxt def)
    6.37        #> curry_assms
    6.38        #> destroy_universal_equalities
    6.39        #> destroy_existential_equalities hol_ctxt
    6.40 @@ -1281,10 +1282,17 @@
    6.41        #> push_quantifiers_inward
    6.42        #> close_form
    6.43        #> Term.map_abs_vars shortest_name
    6.44 -    val nondef_ts = map (do_rest false) nondef_ts
    6.45 -    val def_ts = map (do_rest true) def_ts
    6.46 +    val nondef_ts = nondef_ts |> map (do_middle false)
    6.47 +    val preconstr_ts =
    6.48 +      (* FIXME: Implement preconstruction inference. *)
    6.49 +      preconstrs
    6.50 +      |> map_filter (fn (SOME t, SOME true) => SOME (t |> do_middle false)
    6.51 +                      | _ => NONE)
    6.52 +    val nondef_ts = nondef_ts |> map (do_tail false)
    6.53 +    val def_ts = def_ts |> map (do_middle true #> do_tail true)
    6.54    in
    6.55 -    (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
    6.56 +    (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
    6.57 +     no_poly_user_axioms, binarize)
    6.58    end
    6.59  
    6.60  end;