src/HOL/Tools/Nitpick/nitpick.ML
changeset 41801 ed77524f3429
parent 41793 c7a2669ae75d
child 41802 7592a165fa0b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 14:02:07 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 15:45:44 2011 +0100
     1.3 @@ -35,6 +35,7 @@
     1.4       specialize: bool,
     1.5       star_linear_preds: bool,
     1.6       peephole_optim: bool,
     1.7 +     fix_datatype_vals: bool,
     1.8       datatype_sym_break: int,
     1.9       kodkod_sym_break: int,
    1.10       timeout: Time.time option,
    1.11 @@ -108,6 +109,7 @@
    1.12     specialize: bool,
    1.13     star_linear_preds: bool,
    1.14     peephole_optim: bool,
    1.15 +   fix_datatype_vals: bool,
    1.16     datatype_sym_break: int,
    1.17     kodkod_sym_break: int,
    1.18     timeout: Time.time option,
    1.19 @@ -209,10 +211,10 @@
    1.20           boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    1.21           verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
    1.22           binary_ints, destroy_constrs, specialize, star_linear_preds,
    1.23 -         peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout,
    1.24 -         max_threads, show_datatypes, show_consts, evals, formats, atomss,
    1.25 -         max_potential, max_genuine, check_potential, check_genuine, batch_size,
    1.26 -         ...} = params
    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      val state_ref = Unsynchronized.ref state
    1.32      val pprint =
    1.33        if auto then
    1.34 @@ -320,8 +322,15 @@
    1.35              handle TYPE (_, Ts, ts) =>
    1.36                     raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
    1.37  
    1.38 -    val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
    1.39 -    val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
    1.40 +    val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
    1.41 +    val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
    1.42 +    val needed_us =
    1.43 +      if fix_datatype_vals then
    1.44 +        [@{term "[A, B, C, A]"}, @{term "[C, B, A]"}]
    1.45 +        |> map (nut_from_term hol_ctxt Eq)
    1.46 +        (* infer_needed_constructs ### *)
    1.47 +      else
    1.48 +        []
    1.49      val (free_names, const_names) =
    1.50        fold add_free_and_const_names (nondef_us @ def_us) ([], [])
    1.51      val (sel_names, nonsel_names) =
    1.52 @@ -548,8 +557,8 @@
    1.53          val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
    1.54          val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
    1.55          val dtype_axioms =
    1.56 -          declarative_axioms_for_datatypes hol_ctxt binarize datatype_sym_break
    1.57 -                                           bits ofs kk rel_table datatypes
    1.58 +          declarative_axioms_for_datatypes hol_ctxt binarize needed_us
    1.59 +              datatype_sym_break bits ofs kk rel_table datatypes
    1.60          val declarative_axioms = plain_axioms @ dtype_axioms
    1.61          val univ_card = Int.max (univ_card nat_card int_card main_j0
    1.62                                       (plain_bounds @ sel_bounds) formula,