src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 35079 592edca1dfb3
parent 35028 108662d50512
parent 35070 96136eb6218f
child 35190 ce653cc27a94
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Feb 09 13:54:27 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Feb 09 17:06:05 2010 +0100
     1.3 @@ -8,10 +8,10 @@
     1.4  signature NITPICK_MONO =
     1.5  sig
     1.6    datatype sign = Plus | Minus
     1.7 -  type extended_context = Nitpick_HOL.extended_context
     1.8 +  type hol_context = Nitpick_HOL.hol_context
     1.9  
    1.10    val formulas_monotonic :
    1.11 -    extended_context -> typ -> sign -> term list -> term list -> term -> bool
    1.12 +    hol_context -> typ -> sign -> term list -> term list -> term -> bool
    1.13  end;
    1.14  
    1.15  structure Nitpick_Mono : NITPICK_MONO =
    1.16 @@ -35,7 +35,7 @@
    1.17    CRec of string * typ list
    1.18  
    1.19  type cdata =
    1.20 -  {ext_ctxt: extended_context,
    1.21 +  {hol_ctxt: hol_context,
    1.22     alpha_T: typ,
    1.23     max_fresh: int Unsynchronized.ref,
    1.24     datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
    1.25 @@ -114,9 +114,9 @@
    1.26    | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
    1.27    | flatten_ctype C = [C]
    1.28  
    1.29 -(* extended_context -> typ -> cdata *)
    1.30 -fun initial_cdata ext_ctxt alpha_T =
    1.31 -  ({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
    1.32 +(* hol_context -> typ -> cdata *)
    1.33 +fun initial_cdata hol_ctxt alpha_T =
    1.34 +  ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
    1.35      datatype_cache = Unsynchronized.ref [],
    1.36      constr_cache = Unsynchronized.ref []} : cdata)
    1.37  
    1.38 @@ -188,7 +188,7 @@
    1.39    in List.app repair_one (!constr_cache) end
    1.40  
    1.41  (* cdata -> typ -> ctype *)
    1.42 -fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh,
    1.43 +fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh,
    1.44                             datatype_cache, constr_cache, ...} : cdata) =
    1.45    let
    1.46      (* typ -> typ -> ctype *)
    1.47 @@ -217,7 +217,7 @@
    1.48            | NONE =>
    1.49              let
    1.50                val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
    1.51 -              val xs = datatype_constrs ext_ctxt T
    1.52 +              val xs = datatype_constrs hol_ctxt T
    1.53                val (all_Cs, constr_Cs) =
    1.54                  fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
    1.55                               let
    1.56 @@ -264,7 +264,7 @@
    1.57    end
    1.58  
    1.59  (* cdata -> styp -> ctype *)
    1.60 -fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache,
    1.61 +fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
    1.62                                  ...}) (x as (_, T)) =
    1.63    if could_exist_alpha_sub_ctype thy alpha_T T then
    1.64      case AList.lookup (op =) (!constr_cache) x of
    1.65 @@ -278,8 +278,8 @@
    1.66                   AList.lookup (op =) (!constr_cache) x |> the)
    1.67    else
    1.68      fresh_ctype_for_type cdata T
    1.69 -fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
    1.70 -  x |> boxed_constr_for_sel ext_ctxt |> ctype_for_constr cdata
    1.71 +fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
    1.72 +  x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
    1.73      |> sel_ctype_from_constr_ctype s
    1.74  
    1.75  (* literal list -> ctype -> ctype *)
    1.76 @@ -549,7 +549,7 @@
    1.77    handle List.Empty => initial_gamma
    1.78  
    1.79  (* cdata -> term -> accumulator -> ctype * accumulator *)
    1.80 -fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
    1.81 +fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
    1.82                               max_fresh, ...}) =
    1.83    let
    1.84      (* typ -> ctype *)
    1.85 @@ -806,7 +806,7 @@
    1.86    in do_term end
    1.87  
    1.88  (* cdata -> sign -> term -> accumulator -> accumulator *)
    1.89 -fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) =
    1.90 +fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
    1.91    let
    1.92      (* typ -> ctype *)
    1.93      val ctype_for = fresh_ctype_for_type cdata
    1.94 @@ -895,7 +895,7 @@
    1.95    not (is_harmless_axiom t) ? consider_general_formula cdata sn t
    1.96  
    1.97  (* cdata -> term -> accumulator -> accumulator *)
    1.98 -fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
    1.99 +fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
   1.100    if not (is_constr_pattern_formula thy t) then
   1.101      consider_nondefinitional_axiom cdata Plus t
   1.102    else if is_harmless_axiom t then
   1.103 @@ -945,13 +945,13 @@
   1.104    map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
   1.105    |> cat_lines |> print_g
   1.106  
   1.107 -(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
   1.108 -fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
   1.109 +(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
   1.110 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
   1.111                         core_t =
   1.112    let
   1.113      val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
   1.114                       Syntax.string_of_typ ctxt alpha_T)
   1.115 -    val cdata as {max_fresh, ...} = initial_cdata ext_ctxt alpha_T
   1.116 +    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
   1.117      val (gamma, cset) =
   1.118        (initial_gamma, slack)
   1.119        |> fold (consider_definitional_axiom cdata) def_ts