src/HOL/Tools/Nitpick/nitpick.ML
changeset 41803 ef13e3b7cbaf
parent 41802 7592a165fa0b
child 41856 7244589c8ccc
     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