make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
authorblanchet
Wed Feb 17 20:46:50 2010 +0100 (2010-02-17)
changeset 35190ce653cc27a94
parent 35189 250fe9541fb2
child 35191 69fa4c39dab2
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     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" ^
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 14:11:41 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 20:46:50 2010 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4    val strip_any_connective : term -> term list * term
     2.5    val conjuncts_of : term -> term list
     2.6    val disjuncts_of : term -> term list
     2.7 -  val unbit_and_unbox_type : typ -> typ
     2.8 +  val unarize_and_unbox_type : typ -> typ
     2.9    val string_for_type : Proof.context -> typ -> string
    2.10    val prefix_name : string -> string -> string
    2.11    val shortest_name : string -> string
    2.12 @@ -117,11 +117,14 @@
    2.13    val is_sel : string -> bool
    2.14    val is_sel_like_and_no_discr : string -> bool
    2.15    val box_type : hol_context -> boxability -> typ -> typ
    2.16 +  val binarize_nat_and_int_in_type : typ -> typ
    2.17 +  val binarize_nat_and_int_in_term : term -> term
    2.18    val discr_for_constr : styp -> styp
    2.19    val num_sels_for_constr_type : typ -> int
    2.20    val nth_sel_name_for_constr_name : string -> int -> string
    2.21    val nth_sel_for_constr : styp -> int -> styp
    2.22 -  val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
    2.23 +  val binarized_and_boxed_nth_sel_for_constr :
    2.24 +    hol_context -> bool -> styp -> int -> styp
    2.25    val sel_no_from_name : string -> int
    2.26    val close_form : term -> term
    2.27    val eta_expand : typ list -> term -> int -> term
    2.28 @@ -132,10 +135,11 @@
    2.29    val register_codatatype : typ -> string -> styp list -> theory -> theory
    2.30    val unregister_codatatype : typ -> theory -> theory
    2.31    val datatype_constrs : hol_context -> typ -> styp list
    2.32 -  val boxed_datatype_constrs : hol_context -> typ -> styp list
    2.33 +  val binarized_and_boxed_datatype_constrs :
    2.34 +    hol_context -> bool -> typ -> styp list
    2.35    val num_datatype_constrs : hol_context -> typ -> int
    2.36    val constr_name_for_sel_like : string -> string
    2.37 -  val boxed_constr_for_sel : hol_context -> styp -> styp
    2.38 +  val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
    2.39    val discriminate_value : hol_context -> styp -> term -> term
    2.40    val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
    2.41    val construct_value : theory -> styp -> term list -> term
    2.42 @@ -176,8 +180,8 @@
    2.43    val equational_fun_axioms : hol_context -> styp -> term list
    2.44    val is_equational_fun_surely_complete : hol_context -> styp -> bool
    2.45    val merge_type_vars_in_terms : term list -> term list
    2.46 -  val ground_types_in_type : hol_context -> typ -> typ list
    2.47 -  val ground_types_in_terms : hol_context -> term list -> typ list
    2.48 +  val ground_types_in_type : hol_context -> bool -> typ -> typ list
    2.49 +  val ground_types_in_terms : hol_context -> bool -> term list -> typ list
    2.50    val format_type : int list -> int list -> typ -> typ
    2.51    val format_term_type :
    2.52      theory -> const_table -> (term option * int list) list -> term -> typ
    2.53 @@ -376,23 +380,23 @@
    2.54     (@{const_name ord_fun_inst.less_eq_fun}, 2)]
    2.55  
    2.56  (* typ -> typ *)
    2.57 -fun unbit_type @{typ "unsigned_bit word"} = nat_T
    2.58 -  | unbit_type @{typ "signed_bit word"} = int_T
    2.59 -  | unbit_type @{typ bisim_iterator} = nat_T
    2.60 -  | unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts)
    2.61 -  | unbit_type T = T
    2.62 -fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
    2.63 -    unbit_and_unbox_type (Type ("fun", Ts))
    2.64 -  | unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
    2.65 -    Type ("*", map unbit_and_unbox_type Ts)
    2.66 -  | unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T
    2.67 -  | unbit_and_unbox_type @{typ "signed_bit word"} = int_T
    2.68 -  | unbit_and_unbox_type @{typ bisim_iterator} = nat_T
    2.69 -  | unbit_and_unbox_type (Type (s, Ts as _ :: _)) =
    2.70 -    Type (s, map unbit_and_unbox_type Ts)
    2.71 -  | unbit_and_unbox_type T = T
    2.72 +fun unarize_type @{typ "unsigned_bit word"} = nat_T
    2.73 +  | unarize_type @{typ "signed_bit word"} = int_T
    2.74 +  | unarize_type @{typ bisim_iterator} = nat_T
    2.75 +  | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
    2.76 +  | unarize_type T = T
    2.77 +fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
    2.78 +    unarize_and_unbox_type (Type ("fun", Ts))
    2.79 +  | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
    2.80 +    Type ("*", map unarize_and_unbox_type Ts)
    2.81 +  | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
    2.82 +  | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
    2.83 +  | unarize_and_unbox_type @{typ bisim_iterator} = nat_T
    2.84 +  | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
    2.85 +    Type (s, map unarize_and_unbox_type Ts)
    2.86 +  | unarize_and_unbox_type T = T
    2.87  (* Proof.context -> typ -> string *)
    2.88 -fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type
    2.89 +fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
    2.90  
    2.91  (* string -> string -> string *)
    2.92  val prefix_name = Long_Name.qualify o Long_Name.base_name
    2.93 @@ -692,7 +696,7 @@
    2.94    member (op =) [@{const_name FunBox}, @{const_name PairBox},
    2.95                   @{const_name Quot}, @{const_name Zero_Rep},
    2.96                   @{const_name Suc_Rep}] s orelse
    2.97 -  let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
    2.98 +  let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
    2.99      Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
   2.100      (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
   2.101      x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
   2.102 @@ -703,7 +707,7 @@
   2.103    not (is_coconstr thy x)
   2.104  fun is_constr thy (x as (_, T)) =
   2.105    is_constr_like thy x andalso
   2.106 -  not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso
   2.107 +  not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
   2.108    not (is_stale_constr thy x)
   2.109  (* string -> bool *)
   2.110  val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   2.111 @@ -757,6 +761,15 @@
   2.112                             else InPair)) Ts)
   2.113    | _ => T
   2.114  
   2.115 +(* typ -> typ *)
   2.116 +fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
   2.117 +  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
   2.118 +  | binarize_nat_and_int_in_type (Type (s, Ts)) =
   2.119 +    Type (s, map binarize_nat_and_int_in_type Ts)
   2.120 +  | binarize_nat_and_int_in_type T = T
   2.121 +(* term -> term *)
   2.122 +val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
   2.123 +
   2.124  (* styp -> styp *)
   2.125  fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
   2.126  
   2.127 @@ -773,9 +786,10 @@
   2.128    | nth_sel_for_constr (s, T) n =
   2.129      (nth_sel_name_for_constr_name s n,
   2.130       body_type T --> nth (maybe_curried_binder_types T) n)
   2.131 -(* hol_context -> styp -> int -> styp *)
   2.132 -fun boxed_nth_sel_for_constr hol_ctxt =
   2.133 -  apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
   2.134 +(* hol_context -> bool -> styp -> int -> styp *)
   2.135 +fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
   2.136 +  apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
   2.137 +  oo nth_sel_for_constr
   2.138  
   2.139  (* string -> int *)
   2.140  fun sel_no_from_name s =
   2.141 @@ -876,8 +890,10 @@
   2.142      let val xs = uncached_datatype_constrs thy T in
   2.143        (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   2.144      end
   2.145 -fun boxed_datatype_constrs hol_ctxt =
   2.146 -  map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
   2.147 +(* hol_context -> bool -> typ -> styp list *)
   2.148 +fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
   2.149 +  map (apsnd ((binarize ? binarize_nat_and_int_in_type)
   2.150 +              o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
   2.151  (* hol_context -> typ -> int *)
   2.152  val num_datatype_constrs = length oo datatype_constrs
   2.153  
   2.154 @@ -885,10 +901,12 @@
   2.155  fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   2.156    | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
   2.157    | constr_name_for_sel_like s' = original_name s'
   2.158 -(* hol_context -> styp -> styp *)
   2.159 -fun boxed_constr_for_sel hol_ctxt (s', T') =
   2.160 +(* hol_context -> bool -> styp -> styp *)
   2.161 +fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
   2.162    let val s = constr_name_for_sel_like s' in
   2.163 -    AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
   2.164 +    AList.lookup (op =)
   2.165 +        (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
   2.166 +        s
   2.167      |> the |> pair s
   2.168    end
   2.169  
   2.170 @@ -2013,28 +2031,33 @@
   2.171        | coalesce T = T
   2.172    in map (map_types (map_atyps coalesce)) ts end
   2.173  
   2.174 -(* hol_context -> typ -> typ list -> typ list *)
   2.175 -fun add_ground_types hol_ctxt T accum =
   2.176 -  case T of
   2.177 -    Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   2.178 -  | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   2.179 -  | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
   2.180 -  | Type (_, Ts) =>
   2.181 -    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
   2.182 -      accum
   2.183 -    else
   2.184 -      T :: accum
   2.185 -      |> fold (add_ground_types hol_ctxt)
   2.186 -              (case boxed_datatype_constrs hol_ctxt T of
   2.187 -                 [] => Ts
   2.188 -               | xs => map snd xs)
   2.189 -  | _ => insert (op =) T accum
   2.190 +(* hol_context -> bool -> typ -> typ list -> typ list *)
   2.191 +fun add_ground_types hol_ctxt binarize =
   2.192 +  let
   2.193 +    fun aux T accum =
   2.194 +      case T of
   2.195 +        Type ("fun", Ts) => fold aux Ts accum
   2.196 +      | Type ("*", Ts) => fold aux Ts accum
   2.197 +      | Type (@{type_name itself}, [T1]) => aux T1 accum
   2.198 +      | Type (_, Ts) =>
   2.199 +        if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
   2.200 +                  T then
   2.201 +          accum
   2.202 +        else
   2.203 +          T :: accum
   2.204 +          |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
   2.205 +                                                                 binarize T of
   2.206 +                         [] => Ts
   2.207 +                       | xs => map snd xs)
   2.208 +      | _ => insert (op =) T accum
   2.209 +  in aux end
   2.210  
   2.211 -(* hol_context -> typ -> typ list *)
   2.212 -fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
   2.213 +(* hol_context -> bool -> typ -> typ list *)
   2.214 +fun ground_types_in_type hol_ctxt binarize T =
   2.215 +  add_ground_types hol_ctxt binarize T []
   2.216  (* hol_context -> term list -> typ list *)
   2.217 -fun ground_types_in_terms hol_ctxt ts =
   2.218 -  fold (fold_types (add_ground_types hol_ctxt)) ts []
   2.219 +fun ground_types_in_terms hol_ctxt binarize ts =
   2.220 +  fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
   2.221  
   2.222  (* theory -> const_table -> styp -> int list *)
   2.223  fun const_format thy def_table (x as (s, T)) =
   2.224 @@ -2082,7 +2105,7 @@
   2.225  (* int list -> int list -> typ -> typ *)
   2.226  fun format_type default_format format T =
   2.227    let
   2.228 -    val T = unbit_and_unbox_type T
   2.229 +    val T = unarize_and_unbox_type T
   2.230      val format = format |> filter (curry (op <) 0)
   2.231    in
   2.232      if forall (curry (op =) 1) format then
   2.233 @@ -2121,7 +2144,7 @@
   2.234             (* term -> term *)
   2.235             val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
   2.236             val (x' as (_, T'), js, ts) =
   2.237 -             AList.find (op =) (!special_funs) (s, unbit_and_unbox_type T)
   2.238 +             AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
   2.239               |> the_single
   2.240             val max_j = List.last js
   2.241             val Ts = List.take (binder_types T', max_j + 1)
   2.242 @@ -2211,7 +2234,7 @@
   2.243           let val t = Const (original_name s, T) in
   2.244             (t, format_term_type thy def_table formats t)
   2.245           end)
   2.246 -      |>> map_types unbit_and_unbox_type
   2.247 +      |>> map_types unarize_and_unbox_type
   2.248        |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   2.249    in do_const end
   2.250  
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 14:11:41 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 20:46:50 2010 +0100
     3.3 @@ -33,7 +33,7 @@
     3.4    val merge_bounds : Kodkod.bound list -> Kodkod.bound list
     3.5    val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
     3.6    val declarative_axioms_for_datatypes :
     3.7 -    hol_context -> int -> int Typtab.table -> kodkod_constrs
     3.8 +    hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
     3.9      -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
    3.10    val kodkod_formula_from_nut :
    3.11      int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
    3.12 @@ -742,12 +742,14 @@
    3.13  (* nut NameTable.table -> styp -> KK.rel_expr *)
    3.14  fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
    3.15  
    3.16 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    3.17 -   -> styp -> int -> nfa_transition list *)
    3.18 -fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
    3.19 -                            rel_table (dtypes : dtype_spec list) constr_x n =
    3.20 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
    3.21 +   -> dtype_spec list -> styp -> int -> nfa_transition list *)
    3.22 +fun nfa_transitions_for_sel hol_ctxt binarize
    3.23 +                            ({kk_project, ...} : kodkod_constrs) rel_table
    3.24 +                            (dtypes : dtype_spec list) constr_x n =
    3.25    let
    3.26 -    val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
    3.27 +    val x as (_, T) =
    3.28 +      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
    3.29      val (r, R, arity) = const_triple rel_table x
    3.30      val type_schema = type_schema_of_rep T R
    3.31    in
    3.32 @@ -756,19 +758,21 @@
    3.33                     else SOME (kk_project r (map KK.Num [0, j]), T))
    3.34                 (index_seq 1 (arity - 1) ~~ tl type_schema)
    3.35    end
    3.36 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    3.37 -   -> styp -> nfa_transition list *)
    3.38 -fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
    3.39 -  maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
    3.40 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
    3.41 +   -> dtype_spec list -> styp -> nfa_transition list *)
    3.42 +fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
    3.43 +                               (x as (_, T)) =
    3.44 +  maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
    3.45         (index_seq 0 (num_sels_for_constr_type T))
    3.46 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    3.47 -   -> dtype_spec -> nfa_entry option *)
    3.48 -fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    3.49 -  | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE
    3.50 -  | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
    3.51 -  | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
    3.52 -    SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
    3.53 -                     o #const) constrs)
    3.54 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
    3.55 +   -> dtype_spec list -> dtype_spec -> nfa_entry option *)
    3.56 +fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    3.57 +  | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
    3.58 +  | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
    3.59 +  | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
    3.60 +                           {typ, constrs, ...} =
    3.61 +    SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
    3.62 +                                                dtypes o #const) constrs)
    3.63  
    3.64  val empty_rel = KK.Product (KK.None, KK.None)
    3.65  
    3.66 @@ -825,23 +829,25 @@
    3.67  fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
    3.68    #kk_no kk (#kk_intersect kk
    3.69                   (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
    3.70 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    3.71 -   -> KK.formula list *)
    3.72 -fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
    3.73 -  map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
    3.74 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
    3.75 +   -> dtype_spec list -> KK.formula list *)
    3.76 +fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =
    3.77 +  map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
    3.78 +             dtypes
    3.79    |> strongly_connected_sub_nfas
    3.80    |> maps (fn nfa =>
    3.81                map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
    3.82  
    3.83 -(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
    3.84 -   -> constr_spec -> int -> KK.formula *)
    3.85 -fun sel_axiom_for_sel hol_ctxt j0
    3.86 +(* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
    3.87 +   -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
    3.88 +fun sel_axiom_for_sel hol_ctxt binarize j0
    3.89          (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
    3.90                  kk_join, ...}) rel_table dom_r
    3.91          ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
    3.92          n =
    3.93    let
    3.94 -    val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
    3.95 +    val x as (_, T) =
    3.96 +      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
    3.97      val (r, R, arity) = const_triple rel_table x
    3.98      val R2 = dest_Func R |> snd
    3.99      val z = (epsilon - delta, delta + j0)
   3.100 @@ -855,9 +861,9 @@
   3.101                                (kk_n_ary_function kk R2 r') (kk_no r'))
   3.102        end
   3.103    end
   3.104 -(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
   3.105 +(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
   3.106     -> constr_spec -> KK.formula list *)
   3.107 -fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
   3.108 +fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
   3.109          (constr as {const, delta, epsilon, explicit_max, ...}) =
   3.110    let
   3.111      val honors_explicit_max =
   3.112 @@ -879,19 +885,19 @@
   3.113                               " too small for \"max\"")
   3.114        in
   3.115          max_axiom ::
   3.116 -        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr)
   3.117 +        map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
   3.118              (index_seq 0 (num_sels_for_constr_type (snd const)))
   3.119        end
   3.120    end
   3.121 -(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
   3.122 +(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
   3.123     -> dtype_spec -> KK.formula list *)
   3.124 -fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
   3.125 +fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
   3.126                              ({constrs, ...} : dtype_spec) =
   3.127 -  maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
   3.128 +  maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
   3.129  
   3.130 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
   3.131 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> constr_spec
   3.132     -> KK.formula list *)
   3.133 -fun uniqueness_axiom_for_constr hol_ctxt
   3.134 +fun uniqueness_axiom_for_constr hol_ctxt binarize
   3.135          ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
   3.136           : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
   3.137    let
   3.138 @@ -899,9 +905,10 @@
   3.139      fun conjunct_for_sel r =
   3.140        kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
   3.141      val num_sels = num_sels_for_constr_type (snd const)
   3.142 -    val triples = map (const_triple rel_table
   3.143 -                       o boxed_nth_sel_for_constr hol_ctxt const)
   3.144 -                      (~1 upto num_sels - 1)
   3.145 +    val triples =
   3.146 +      map (const_triple rel_table
   3.147 +           o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
   3.148 +          (~1 upto num_sels - 1)
   3.149      val j0 = case triples |> hd |> #2 of
   3.150                 Func (Atom (_, j0), _) => j0
   3.151               | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
   3.152 @@ -916,11 +923,11 @@
   3.153                    (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
   3.154                    (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
   3.155    end
   3.156 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
   3.157 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> dtype_spec
   3.158     -> KK.formula list *)
   3.159 -fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
   3.160 +fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
   3.161                                     ({constrs, ...} : dtype_spec) =
   3.162 -  map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
   3.163 +  map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
   3.164  
   3.165  (* constr_spec -> int *)
   3.166  fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
   3.167 @@ -937,22 +944,24 @@
   3.168         kk_disjoint_sets kk rs]
   3.169      end
   3.170  
   3.171 -(* hol_context -> int -> int Typtab.table -> kodkod_constrs
   3.172 +(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
   3.173     -> nut NameTable.table -> dtype_spec -> KK.formula list *)
   3.174 -fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
   3.175 -  | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
   3.176 +fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
   3.177 +  | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
   3.178                                (dtype as {typ, ...}) =
   3.179      let val j0 = offset_of_type ofs typ in
   3.180 -      sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
   3.181 -      uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
   3.182 +      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
   3.183 +      uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
   3.184        partition_axioms_for_datatype j0 kk rel_table dtype
   3.185      end
   3.186  
   3.187 -(* hol_context -> int -> int Typtab.table -> kodkod_constrs
   3.188 +(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
   3.189     -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
   3.190 -fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
   3.191 -  acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
   3.192 -  maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
   3.193 +fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table
   3.194 +                                     dtypes =
   3.195 +  acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @
   3.196 +  maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
   3.197 +       dtypes
   3.198  
   3.199  (* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
   3.200  fun kodkod_formula_from_nut bits ofs
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 17 14:11:41 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 17 20:46:50 2010 +0100
     4.3 @@ -110,23 +110,23 @@
     4.4    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
     4.5  
     4.6  (* term -> term *)
     4.7 -fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
     4.8 -    unbit_and_unbox_term t1
     4.9 -  | unbit_and_unbox_term (Const (@{const_name PairBox},
    4.10 -                          Type ("fun", [T1, Type ("fun", [T2, T3])]))
    4.11 -                          $ t1 $ t2) =
    4.12 -    let val Ts = map unbit_and_unbox_type [T1, T2] in
    4.13 +fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
    4.14 +    unarize_and_unbox_term t1
    4.15 +  | unarize_and_unbox_term (Const (@{const_name PairBox},
    4.16 +                                   Type ("fun", [T1, Type ("fun", [T2, T3])]))
    4.17 +                            $ t1 $ t2) =
    4.18 +    let val Ts = map unarize_and_unbox_type [T1, T2] in
    4.19        Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
    4.20 -      $ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
    4.21 +      $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
    4.22      end
    4.23 -  | unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T)
    4.24 -  | unbit_and_unbox_term (t1 $ t2) =
    4.25 -    unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
    4.26 -  | unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T)
    4.27 -  | unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T)
    4.28 -  | unbit_and_unbox_term (Bound j) = Bound j
    4.29 -  | unbit_and_unbox_term (Abs (s, T, t')) =
    4.30 -    Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t')
    4.31 +  | unarize_and_unbox_term (Const (s, T)) = Const (s, unarize_and_unbox_type T)
    4.32 +  | unarize_and_unbox_term (t1 $ t2) =
    4.33 +    unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
    4.34 +  | unarize_and_unbox_term (Free (s, T)) = Free (s, unarize_and_unbox_type T)
    4.35 +  | unarize_and_unbox_term (Var (x, T)) = Var (x, unarize_and_unbox_type T)
    4.36 +  | unarize_and_unbox_term (Bound j) = Bound j
    4.37 +  | unarize_and_unbox_term (Abs (s, T, t')) =
    4.38 +    Abs (s, unarize_and_unbox_type T, unarize_and_unbox_term t')
    4.39  
    4.40  (* typ -> typ -> (typ * typ) * (typ * typ) *)
    4.41  fun factor_out_types (T1 as Type ("*", [T11, T12]))
    4.42 @@ -264,8 +264,8 @@
    4.43     -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
    4.44     -> typ -> rep -> int list list -> term *)
    4.45  fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
    4.46 -        ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
    4.47 -         : scope) sel_names rel_table bounds =
    4.48 +        ({hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits, datatypes,
    4.49 +          ofs, ...} : scope) sel_names rel_table bounds =
    4.50    let
    4.51      val for_auto = (maybe_name = "")
    4.52      (* int list list -> int *)
    4.53 @@ -356,10 +356,10 @@
    4.54      fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
    4.55        ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
    4.56                   |> make_plain_fun maybe_opt T1 T2
    4.57 -                 |> unbit_and_unbox_term
    4.58 -                 |> typecast_fun (unbit_and_unbox_type T')
    4.59 -                                 (unbit_and_unbox_type T1)
    4.60 -                                 (unbit_and_unbox_type T2)
    4.61 +                 |> unarize_and_unbox_term
    4.62 +                 |> typecast_fun (unarize_and_unbox_type T')
    4.63 +                                 (unarize_and_unbox_type T1)
    4.64 +                                 (unarize_and_unbox_type T2)
    4.65      (* (typ * int) list -> typ -> typ -> int -> term *)
    4.66      fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
    4.67          let
    4.68 @@ -418,8 +418,10 @@
    4.69                              else NONE)
    4.70                          (discr_jsss ~~ constrs) |> the
    4.71              val arg_Ts = curried_binder_types constr_T
    4.72 -            val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
    4.73 -                             (index_seq 0 (length arg_Ts))
    4.74 +            val sel_xs =
    4.75 +              map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
    4.76 +                                                          constr_x)
    4.77 +                  (index_seq 0 (length arg_Ts))
    4.78              val sel_Rs =
    4.79                map (fn x => get_first
    4.80                                 (fn ConstName (s', T', R) =>
    4.81 @@ -550,7 +552,7 @@
    4.82          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
    4.83                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
    4.84                     string_of_int (length jss))
    4.85 -  in polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] end
    4.86 +  in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end
    4.87  
    4.88  (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
    4.89     -> nut -> term *)
    4.90 @@ -618,7 +620,7 @@
    4.91                         nondef_table, user_nondefs, simp_table, psimp_table,
    4.92                         intro_table, ground_thm_table, ersatz_table, skolems,
    4.93                         special_funs, unrolled_preds, wf_cache, constr_cache},
    4.94 -         card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    4.95 +         binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    4.96          formats all_frees free_names sel_names nonsel_names rel_table bounds =
    4.97    let
    4.98      val pool = Unsynchronized.ref []
    4.99 @@ -638,9 +640,9 @@
   4.100         ersatz_table = ersatz_table, skolems = skolems,
   4.101         special_funs = special_funs, unrolled_preds = unrolled_preds,
   4.102         wf_cache = wf_cache, constr_cache = constr_cache}
   4.103 -    val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
   4.104 -                 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
   4.105 -                 ofs = ofs}
   4.106 +    val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
   4.107 +                 card_assigns = card_assigns, bits = bits,
   4.108 +                 bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
   4.109      (* bool -> typ -> typ -> rep -> int list list -> term *)
   4.110      fun term_for_rep unfold =
   4.111        reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
   4.112 @@ -677,7 +679,7 @@
   4.113          val (oper, (t1, T'), T) =
   4.114            case name of
   4.115              FreeName (s, T, _) =>
   4.116 -            let val t = Free (s, unbit_and_unbox_type T) in
   4.117 +            let val t = Free (s, unarize_and_unbox_type T) in
   4.118                ("=", (t, format_term_type thy def_table formats t), T)
   4.119              end
   4.120            | ConstName (s, T, _) =>
   4.121 @@ -699,7 +701,7 @@
   4.122      (* dtype_spec -> Pretty.T *)
   4.123      fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
   4.124        Pretty.block (Pretty.breaks
   4.125 -          [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
   4.126 +          [Syntax.pretty_typ ctxt (unarize_and_unbox_type typ), Pretty.str "=",
   4.127             Pretty.enum "," "{" "}"
   4.128                 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
   4.129                  (if complete then [] else [Pretty.str unrep]))])
   4.130 @@ -742,8 +744,8 @@
   4.131      val free_names =
   4.132        map (fn x as (s, T) =>
   4.133                case filter (curry (op =) x
   4.134 -                           o pairf nickname_of (unbit_and_unbox_type o type_of))
   4.135 -                          free_names of
   4.136 +                       o pairf nickname_of (unarize_and_unbox_type o type_of))
   4.137 +                       free_names of
   4.138                  [name] => name
   4.139                | [] => FreeName (s, T, Any)
   4.140                | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Feb 17 14:11:41 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Feb 17 20:46:50 2010 +0100
     5.3 @@ -11,7 +11,7 @@
     5.4    type hol_context = Nitpick_HOL.hol_context
     5.5  
     5.6    val formulas_monotonic :
     5.7 -    hol_context -> typ -> sign -> term list -> term list -> term -> bool
     5.8 +    hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
     5.9  end;
    5.10  
    5.11  structure Nitpick_Mono : NITPICK_MONO =
    5.12 @@ -36,6 +36,7 @@
    5.13  
    5.14  type cdata =
    5.15    {hol_ctxt: hol_context,
    5.16 +   binarize: bool,
    5.17     alpha_T: typ,
    5.18     max_fresh: int Unsynchronized.ref,
    5.19     datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
    5.20 @@ -114,10 +115,10 @@
    5.21    | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
    5.22    | flatten_ctype C = [C]
    5.23  
    5.24 -(* hol_context -> typ -> cdata *)
    5.25 -fun initial_cdata hol_ctxt alpha_T =
    5.26 -  ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
    5.27 -    datatype_cache = Unsynchronized.ref [],
    5.28 +(* hol_context -> bool -> typ -> cdata *)
    5.29 +fun initial_cdata hol_ctxt binarize alpha_T =
    5.30 +  ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
    5.31 +    max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
    5.32      constr_cache = Unsynchronized.ref []} : cdata)
    5.33  
    5.34  (* typ -> typ -> bool *)
    5.35 @@ -278,9 +279,9 @@
    5.36                   AList.lookup (op =) (!constr_cache) x |> the)
    5.37    else
    5.38      fresh_ctype_for_type cdata T
    5.39 -fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
    5.40 -  x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
    5.41 -    |> sel_ctype_from_constr_ctype s
    5.42 +fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
    5.43 +  x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
    5.44 +    |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
    5.45  
    5.46  (* literal list -> ctype -> ctype *)
    5.47  fun instantiate_ctype lits =
    5.48 @@ -945,13 +946,14 @@
    5.49    map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
    5.50    |> cat_lines |> print_g
    5.51  
    5.52 -(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
    5.53 -fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
    5.54 -                       core_t =
    5.55 +(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
    5.56 +   -> bool *)
    5.57 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
    5.58 +                       nondef_ts core_t =
    5.59    let
    5.60      val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
    5.61                       Syntax.string_of_typ ctxt alpha_T)
    5.62 -    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
    5.63 +    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
    5.64      val (gamma, cset) =
    5.65        (initial_gamma, slack)
    5.66        |> fold (consider_definitional_axiom cdata) def_ts
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 14:11:41 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 20:46:50 2010 +0100
     6.3 @@ -747,10 +747,10 @@
     6.4  
     6.5  (* scope -> styp -> int -> nut list * rep NameTable.table
     6.6     -> nut list * rep NameTable.table *)
     6.7 -fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
     6.8 -                                      (vs, table) =
     6.9 +fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
    6.10 +                                      (x as (_, T)) n (vs, table) =
    6.11    let
    6.12 -    val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
    6.13 +    val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
    6.14      val R' = if n = ~1 orelse is_word_type (body_type T) orelse
    6.15                  (is_fun_type (range_type T') andalso
    6.16                   is_boolean_type (body_type T')) then
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 14:11:41 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 20:46:50 2010 +0100
     7.3 @@ -9,7 +9,8 @@
     7.4  sig
     7.5    type hol_context = Nitpick_HOL.hol_context
     7.6    val preprocess_term :
     7.7 -    hol_context -> term -> ((term list * term list) * (bool * bool)) * term
     7.8 +    hol_context -> term
     7.9 +    -> ((term list * term list) * (bool * bool)) * term * bool
    7.10  end
    7.11  
    7.12  structure Nitpick_Preproc : NITPICK_PREPROC =
    7.13 @@ -54,15 +55,6 @@
    7.14    | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
    7.15    | should_use_binary_ints _ = false
    7.16  
    7.17 -(* typ -> typ *)
    7.18 -fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
    7.19 -  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
    7.20 -  | binarize_nat_and_int_in_type (Type (s, Ts)) =
    7.21 -    Type (s, map binarize_nat_and_int_in_type Ts)
    7.22 -  | binarize_nat_and_int_in_type T = T
    7.23 -(* term -> term *)
    7.24 -val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
    7.25 -
    7.26  (** Uncurrying **)
    7.27  
    7.28  (* theory -> term -> int Termtab.tab -> int Termtab.tab *)
    7.29 @@ -1383,7 +1375,8 @@
    7.30  
    7.31  (** Preprocessor entry point **)
    7.32  
    7.33 -(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
    7.34 +(* hol_context -> term
    7.35 +   -> ((term list * term list) * (bool * bool)) * term * bool *)
    7.36  fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
    7.37                                    skolemize, uncurry, ...}) t =
    7.38    let
    7.39 @@ -1424,7 +1417,7 @@
    7.40    in
    7.41      (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
    7.42        (got_all_mono_user_axioms, no_poly_user_axioms)),
    7.43 -     do_rest false true core_t)
    7.44 +     do_rest false true core_t, binarize)
    7.45    end
    7.46  
    7.47  end;
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Feb 17 14:11:41 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Feb 17 20:46:50 2010 +0100
     8.3 @@ -30,6 +30,7 @@
     8.4  
     8.5    type scope = {
     8.6      hol_ctxt: hol_context,
     8.7 +    binarize: bool,
     8.8      card_assigns: (typ * int) list,
     8.9      bits: int,
    8.10      bisim_depth: int,
    8.11 @@ -48,7 +49,7 @@
    8.12    val scopes_equivalent : scope -> scope -> bool
    8.13    val scope_less_eq : scope -> scope -> bool
    8.14    val all_scopes :
    8.15 -    hol_context -> int -> (typ option * int list) list
    8.16 +    hol_context -> bool -> int -> (typ option * int list) list
    8.17      -> (styp option * int list) list -> (styp option * int list) list
    8.18      -> int list -> int list -> typ list -> typ list -> typ list
    8.19      -> int * scope list
    8.20 @@ -80,6 +81,7 @@
    8.21  
    8.22  type scope = {
    8.23    hol_ctxt: hol_context,
    8.24 +  binarize: bool,
    8.25    card_assigns: (typ * int) list,
    8.26    bits: int,
    8.27    bisim_depth: int,
    8.28 @@ -242,9 +244,10 @@
    8.29  
    8.30  val max_bits = 31 (* Kodkod limit *)
    8.31  
    8.32 -(* hol_context -> (typ option * int list) list -> (styp option * int list) list
    8.33 -   -> (styp option * int list) list -> int list -> int list -> typ -> block *)
    8.34 -fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
    8.35 +(* hol_context -> bool -> (typ option * int list) list
    8.36 +   -> (styp option * int list) list -> (styp option * int list) list -> int list
    8.37 +   -> int list -> typ -> block *)
    8.38 +fun block_for_type (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
    8.39                     iters_assigns bitss bisim_depths T =
    8.40    if T = @{typ unsigned_bit} then
    8.41      [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
    8.42 @@ -262,18 +265,18 @@
    8.43                                              (const_for_iterator_type T)))]
    8.44    else
    8.45      (Card T, lookup_type_ints_assign thy cards_assigns T) ::
    8.46 -    (case datatype_constrs hol_ctxt T of
    8.47 +    (case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
    8.48         [_] => []
    8.49       | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
    8.50  
    8.51 -(* hol_context -> (typ option * int list) list -> (styp option * int list) list
    8.52 -   -> (styp option * int list) list -> int list -> int list -> typ list
    8.53 -   -> typ list -> block list *)
    8.54 -fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
    8.55 -                     bisim_depths mono_Ts nonmono_Ts =
    8.56 +(* hol_context -> bool -> (typ option * int list) list
    8.57 +   -> (styp option * int list) list -> (styp option * int list) list -> int list
    8.58 +   -> int list -> typ list -> typ list -> block list *)
    8.59 +fun blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
    8.60 +                     bitss bisim_depths mono_Ts nonmono_Ts =
    8.61    let
    8.62      (* typ -> block *)
    8.63 -    val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
    8.64 +    val block_for = block_for_type hol_ctxt binarize cards_assigns maxes_assigns
    8.65                                     iters_assigns bitss bisim_depths
    8.66      val mono_block = maps block_for mono_Ts
    8.67      val nonmono_blocks = map block_for nonmono_Ts
    8.68 @@ -314,10 +317,10 @@
    8.69  
    8.70  type scope_desc = (typ * int) list * (styp * int) list
    8.71  
    8.72 -(* hol_context -> scope_desc -> typ * int -> bool *)
    8.73 -fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
    8.74 -                                       (T, k) =
    8.75 -  case datatype_constrs hol_ctxt T of
    8.76 +(* hol_context -> bool -> scope_desc -> typ * int -> bool *)
    8.77 +fun is_surely_inconsistent_card_assign hol_ctxt binarize
    8.78 +                                       (card_assigns, max_assigns) (T, k) =
    8.79 +  case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
    8.80      [] => false
    8.81    | xs =>
    8.82      let
    8.83 @@ -330,21 +333,22 @@
    8.84          | effective_max card max = Int.min (card, max)
    8.85        val max = map2 effective_max dom_cards maxes |> Integer.sum
    8.86      in max < k end
    8.87 -(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
    8.88 -   -> bool *)
    8.89 -fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
    8.90 -  exists (is_surely_inconsistent_card_assign hol_ctxt
    8.91 +(* hol_context -> bool -> (typ * int) list -> (typ * int) list
    8.92 +   -> (styp * int) list -> bool *)
    8.93 +fun is_surely_inconsistent_scope_description hol_ctxt binarize seen rest
    8.94 +                                             max_assigns =
    8.95 +  exists (is_surely_inconsistent_card_assign hol_ctxt binarize
    8.96                                               (seen @ rest, max_assigns)) seen
    8.97  
    8.98 -(* hol_context -> scope_desc -> (typ * int) list option *)
    8.99 -fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
   8.100 +(* hol_context -> bool -> scope_desc -> (typ * int) list option *)
   8.101 +fun repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) =
   8.102    let
   8.103      (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
   8.104      fun aux seen [] = SOME seen
   8.105        | aux seen ((T, 0) :: _) = NONE
   8.106        | aux seen ((T, k) :: rest) =
   8.107 -        (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
   8.108 -                                                     rest max_assigns then
   8.109 +        (if is_surely_inconsistent_scope_description hol_ctxt binarize
   8.110 +                ((T, k) :: seen) rest max_assigns then
   8.111             raise SAME ()
   8.112           else
   8.113             case aux ((T, k) :: seen) rest of
   8.114 @@ -375,13 +379,14 @@
   8.115  (* block -> scope_desc *)
   8.116  fun scope_descriptor_from_block block =
   8.117    fold_rev add_row_to_scope_descriptor block ([], [])
   8.118 -(* hol_context -> block list -> int list -> scope_desc option *)
   8.119 -fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
   8.120 +(* hol_context -> bool -> block list -> int list -> scope_desc option *)
   8.121 +fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) binarize blocks
   8.122 +                                      columns =
   8.123    let
   8.124      val (card_assigns, max_assigns) =
   8.125        maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
   8.126 -    val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
   8.127 -                       |> the
   8.128 +    val card_assigns =
   8.129 +      repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) |> the
   8.130    in
   8.131      SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
   8.132            max_assigns)
   8.133 @@ -462,14 +467,14 @@
   8.134      card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
   8.135    end
   8.136  
   8.137 -(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
   8.138 -fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
   8.139 -                                        (desc as (card_assigns, _)) (T, card) =
   8.140 +(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
   8.141 +fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) binarize
   8.142 +        deep_dataTs (desc as (card_assigns, _)) (T, card) =
   8.143    let
   8.144      val deep = member (op =) deep_dataTs T
   8.145      val co = is_codatatype thy T
   8.146      val standard = is_standard_datatype hol_ctxt T
   8.147 -    val xs = boxed_datatype_constrs hol_ctxt T
   8.148 +    val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
   8.149      val self_recs = map (is_self_recursive_constr_type o snd) xs
   8.150      val (num_self_recs, num_non_self_recs) =
   8.151        List.partition I self_recs |> pairself length
   8.152 @@ -496,21 +501,21 @@
   8.153      min_bits_for_nat_value (fold Integer.max
   8.154          (map snd card_assigns @ map snd max_assigns) 0)
   8.155  
   8.156 -(* hol_context -> int -> typ list -> scope_desc -> scope *)
   8.157 -fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
   8.158 -                          (desc as (card_assigns, _)) =
   8.159 +(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
   8.160 +fun scope_from_descriptor (hol_ctxt as {thy, ...}) binarize sym_break
   8.161 +                          deep_dataTs (desc as (card_assigns, _)) =
   8.162    let
   8.163      val datatypes =
   8.164 -      map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
   8.165 -          (filter (is_datatype thy o fst) card_assigns)
   8.166 +      map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
   8.167 +               desc) (filter (is_datatype thy o fst) card_assigns)
   8.168      val bits = card_of_type card_assigns @{typ signed_bit} - 1
   8.169                 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   8.170                        card_of_type card_assigns @{typ unsigned_bit}
   8.171                        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
   8.172      val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
   8.173    in
   8.174 -    {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
   8.175 -     bits = bits, bisim_depth = bisim_depth,
   8.176 +    {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
   8.177 +     datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
   8.178       ofs = if sym_break <= 0 then Typtab.empty
   8.179             else offset_table_for_card_assigns thy card_assigns datatypes}
   8.180    end
   8.181 @@ -520,7 +525,7 @@
   8.182  fun repair_cards_assigns_wrt_boxing _ _ [] = []
   8.183    | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
   8.184      (if is_fun_type T orelse is_pair_type T then
   8.185 -       Ts |> filter (curry (type_match thy o swap) T o unbit_and_unbox_type)
   8.186 +       Ts |> filter (curry (type_match thy o swap) T o unarize_and_unbox_type)
   8.187            |> map (rpair ks o SOME)
   8.188       else
   8.189         [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
   8.190 @@ -530,26 +535,29 @@
   8.191  val max_scopes = 4096
   8.192  val distinct_threshold = 512
   8.193  
   8.194 -(* hol_context -> int -> (typ option * int list) list
   8.195 +(* hol_context -> bool -> int -> (typ option * int list) list
   8.196     -> (styp option * int list) list -> (styp option * int list) list -> int list
   8.197     -> typ list -> typ list -> typ list -> int * scope list *)
   8.198 -fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
   8.199 -               iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
   8.200 +fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
   8.201 +               maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
   8.202 +               deep_dataTs =
   8.203    let
   8.204      val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
   8.205                                                          cards_assigns
   8.206 -    val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
   8.207 +    val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
   8.208                                    iters_assigns bitss bisim_depths mono_Ts
   8.209                                    nonmono_Ts
   8.210      val ranks = map rank_of_block blocks
   8.211      val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
   8.212      val head = take max_scopes all
   8.213 -    val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
   8.214 -                           head
   8.215 +    val descs =
   8.216 +      map_filter (scope_descriptor_from_combination hol_ctxt binarize blocks)
   8.217 +                 head
   8.218    in
   8.219      (length all - length head,
   8.220       descs |> length descs <= distinct_threshold ? distinct (op =)
   8.221 -           |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
   8.222 +           |> map (scope_from_descriptor hol_ctxt binarize sym_break
   8.223 +                                         deep_dataTs))
   8.224    end
   8.225  
   8.226  end;