src/HOL/Tools/Nitpick/nitpick.ML
changeset 35190 ce653cc27a94
parent 35185 9b8f351cced6
child 35220 2bcdae5f4fdb
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 14:11:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 20:46:50 2010 +0100
     1.3 @@ -293,7 +293,7 @@
     1.4      val _ = null (Term.add_tvars assms_t []) orelse
     1.5              raise NOT_SUPPORTED "schematic type variables"
     1.6      val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
     1.7 -         core_t) = preprocess_term hol_ctxt assms_t
     1.8 +         core_t, binarize) = preprocess_term hol_ctxt assms_t
     1.9      val got_all_user_axioms =
    1.10        got_all_mono_user_axioms andalso no_poly_user_axioms
    1.11  
    1.12 @@ -345,12 +345,13 @@
    1.13        case triple_lookup (type_match thy) monos T of
    1.14          SOME (SOME b) => b
    1.15        | _ => is_type_always_monotonic T orelse
    1.16 -             formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
    1.17 +             formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
    1.18      fun is_deep_datatype T =
    1.19        is_datatype thy T andalso
    1.20 -      (is_word_type T orelse
    1.21 +      (not standard orelse is_word_type T orelse
    1.22         exists (curry (op =) T o domain_type o type_of) sel_names)
    1.23 -    val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts)
    1.24 +    val all_Ts = ground_types_in_terms hol_ctxt binarize
    1.25 +                                       (core_t :: def_ts @ nondef_ts)
    1.26                   |> sort TermOrd.typ_ord
    1.27      val _ = if verbose andalso binary_ints = SOME true andalso
    1.28                 exists (member (op =) [nat_T, int_T]) all_Ts then
    1.29 @@ -514,8 +515,9 @@
    1.30          val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
    1.31          val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
    1.32          val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
    1.33 -        val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
    1.34 -                                                            rel_table datatypes
    1.35 +        val dtype_axioms =
    1.36 +          declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk
    1.37 +                                           rel_table datatypes
    1.38          val declarative_axioms = plain_axioms @ dtype_axioms
    1.39          val univ_card = univ_card nat_card int_card main_j0
    1.40                                    (plain_bounds @ sel_bounds) formula
    1.41 @@ -545,9 +547,10 @@
    1.42               if loc = "Nitpick_Kodkod.check_arity" andalso
    1.43                  not (Typtab.is_empty ofs) then
    1.44                 problem_for_scope unsound
    1.45 -                   {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
    1.46 -                    bits = bits, bisim_depth = bisim_depth,
    1.47 -                    datatypes = datatypes, ofs = Typtab.empty}
    1.48 +                   {hol_ctxt = hol_ctxt, binarize = binarize,
    1.49 +                    card_assigns = card_assigns, bits = bits,
    1.50 +                    bisim_depth = bisim_depth, datatypes = datatypes,
    1.51 +                    ofs = Typtab.empty}
    1.52               else if loc = "Nitpick.pick_them_nits_in_term.\
    1.53                             \problem_for_scope" then
    1.54                 NONE
    1.55 @@ -905,8 +908,8 @@
    1.56          end
    1.57  
    1.58      val (skipped, the_scopes) =
    1.59 -      all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
    1.60 -                 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    1.61 +      all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
    1.62 +                 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    1.63      val _ = if skipped > 0 then
    1.64                print_m (fn () => "Too many scopes. Skipping " ^
    1.65                                  string_of_int skipped ^ " scope" ^