src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 35190 ce653cc27a94
parent 35079 592edca1dfb3
child 35219 15a5f213ef5b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Feb 17 14:11:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Feb 17 20:46:50 2010 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    type hol_context = Nitpick_HOL.hol_context
     1.5  
     1.6    val formulas_monotonic :
     1.7 -    hol_context -> typ -> sign -> term list -> term list -> term -> bool
     1.8 +    hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
     1.9  end;
    1.10  
    1.11  structure Nitpick_Mono : NITPICK_MONO =
    1.12 @@ -36,6 +36,7 @@
    1.13  
    1.14  type cdata =
    1.15    {hol_ctxt: hol_context,
    1.16 +   binarize: bool,
    1.17     alpha_T: typ,
    1.18     max_fresh: int Unsynchronized.ref,
    1.19     datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
    1.20 @@ -114,10 +115,10 @@
    1.21    | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
    1.22    | flatten_ctype C = [C]
    1.23  
    1.24 -(* hol_context -> typ -> cdata *)
    1.25 -fun initial_cdata hol_ctxt alpha_T =
    1.26 -  ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
    1.27 -    datatype_cache = Unsynchronized.ref [],
    1.28 +(* hol_context -> bool -> typ -> cdata *)
    1.29 +fun initial_cdata hol_ctxt binarize alpha_T =
    1.30 +  ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
    1.31 +    max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
    1.32      constr_cache = Unsynchronized.ref []} : cdata)
    1.33  
    1.34  (* typ -> typ -> bool *)
    1.35 @@ -278,9 +279,9 @@
    1.36                   AList.lookup (op =) (!constr_cache) x |> the)
    1.37    else
    1.38      fresh_ctype_for_type cdata T
    1.39 -fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
    1.40 -  x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
    1.41 -    |> sel_ctype_from_constr_ctype s
    1.42 +fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
    1.43 +  x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
    1.44 +    |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
    1.45  
    1.46  (* literal list -> ctype -> ctype *)
    1.47  fun instantiate_ctype lits =
    1.48 @@ -945,13 +946,14 @@
    1.49    map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
    1.50    |> cat_lines |> print_g
    1.51  
    1.52 -(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
    1.53 -fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
    1.54 -                       core_t =
    1.55 +(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
    1.56 +   -> bool *)
    1.57 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
    1.58 +                       nondef_ts core_t =
    1.59    let
    1.60      val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
    1.61                       Syntax.string_of_typ ctxt alpha_T)
    1.62 -    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
    1.63 +    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
    1.64      val (gamma, cset) =
    1.65        (initial_gamma, slack)
    1.66        |> fold (consider_definitional_axiom cdata) def_ts