src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 35190 ce653cc27a94
parent 35079 592edca1dfb3
child 35219 15a5f213ef5b
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Feb 17 20:46:50 2010 +0100
@@ -11,7 +11,7 @@
   type hol_context = Nitpick_HOL.hol_context
 
   val formulas_monotonic :
-    hol_context -> typ -> sign -> term list -> term list -> term -> bool
+    hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
 end;
 
 structure Nitpick_Mono : NITPICK_MONO =
@@ -36,6 +36,7 @@
 
 type cdata =
   {hol_ctxt: hol_context,
+   binarize: bool,
    alpha_T: typ,
    max_fresh: int Unsynchronized.ref,
    datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
@@ -114,10 +115,10 @@
   | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
   | flatten_ctype C = [C]
 
-(* hol_context -> typ -> cdata *)
-fun initial_cdata hol_ctxt alpha_T =
-  ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
-    datatype_cache = Unsynchronized.ref [],
+(* hol_context -> bool -> typ -> cdata *)
+fun initial_cdata hol_ctxt binarize alpha_T =
+  ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
+    max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
     constr_cache = Unsynchronized.ref []} : cdata)
 
 (* typ -> typ -> bool *)
@@ -278,9 +279,9 @@
                  AList.lookup (op =) (!constr_cache) x |> the)
   else
     fresh_ctype_for_type cdata T
-fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
-  x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
-    |> sel_ctype_from_constr_ctype s
+fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
+  x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
+    |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
 
 (* literal list -> ctype -> ctype *)
 fun instantiate_ctype lits =
@@ -945,13 +946,14 @@
   map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
   |> cat_lines |> print_g
 
-(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
-fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
-                       core_t =
+(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
+   -> bool *)
+fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
+                       nondef_ts core_t =
   let
     val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
                      Syntax.string_of_typ ctxt alpha_T)
-    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
+    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
     val (gamma, cset) =
       (initial_gamma, slack)
       |> fold (consider_definitional_axiom cdata) def_ts