src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 37256 0dca1ec52999
parent 36385 ff5f88702590
child 37260 dde817e6dfb1
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon May 31 18:51:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jun 01 10:31:18 2010 +0200
     1.3 @@ -162,8 +162,8 @@
     1.4    | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
     1.5  fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
     1.6      could_exist_alpha_subtype alpha_T T
     1.7 -  | could_exist_alpha_sub_mtype thy alpha_T T =
     1.8 -    (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
     1.9 +  | could_exist_alpha_sub_mtype ctxt alpha_T T =
    1.10 +    (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
    1.11  
    1.12  fun exists_alpha_sub_mtype MAlpha = true
    1.13    | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
    1.14 @@ -243,7 +243,7 @@
    1.15              else
    1.16                S Minus
    1.17    in (M1, a, M2) end
    1.18 -and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
    1.19 +and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
    1.20                                      datatype_mcache, constr_mcache, ...})
    1.21                           all_minus =
    1.22    let
    1.23 @@ -255,7 +255,7 @@
    1.24          MFun (fresh_mfun_for_fun_type mdata false T1 T2)
    1.25        | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
    1.26        | Type (z as (s, _)) =>
    1.27 -        if could_exist_alpha_sub_mtype thy alpha_T T then
    1.28 +        if could_exist_alpha_sub_mtype ctxt alpha_T T then
    1.29            case AList.lookup (op =) (!datatype_mcache) z of
    1.30              SOME M => M
    1.31            | NONE =>
    1.32 @@ -304,9 +304,9 @@
    1.33            case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
    1.34    end
    1.35  
    1.36 -fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
    1.37 +fun mtype_for_constr (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, constr_mcache,
    1.38                                  ...}) (x as (_, T)) =
    1.39 -  if could_exist_alpha_sub_mtype thy alpha_T T then
    1.40 +  if could_exist_alpha_sub_mtype ctxt alpha_T T then
    1.41      case AList.lookup (op =) (!constr_mcache) x of
    1.42        SOME M => M
    1.43      | NONE => if T = alpha_T then
    1.44 @@ -741,7 +741,7 @@
    1.45                    do_robust_set_operation T accum
    1.46                  else if is_sel s then
    1.47                    (mtype_for_sel mdata x, accum)
    1.48 -                else if is_constr thy stds x then
    1.49 +                else if is_constr ctxt stds x then
    1.50                    (mtype_for_constr mdata x, accum)
    1.51                  else if is_built_in_const thy stds fast_descrs x then
    1.52                    (fresh_mtype_for_type mdata true T, accum)
    1.53 @@ -924,8 +924,8 @@
    1.54    if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
    1.55    else consider_general_formula mdata Plus t
    1.56  
    1.57 -fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
    1.58 -  if not (is_constr_pattern_formula thy t) then
    1.59 +fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
    1.60 +  if not (is_constr_pattern_formula ctxt t) then
    1.61      consider_nondefinitional_axiom mdata t
    1.62    else if is_harmless_axiom mdata t then
    1.63      pair (MRaw (t, dummy_M))
    1.64 @@ -1027,7 +1027,8 @@
    1.65  fun fin_fun_constr T1 T2 =
    1.66    (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
    1.67  
    1.68 -fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
    1.69 +fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
    1.70 +                                ...})
    1.71                    binarize finitizes alpha_T tsp =
    1.72    case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
    1.73      SOME (lits, msp, constr_mtypes) =>
    1.74 @@ -1085,7 +1086,7 @@
    1.75                    Const (s, T')
    1.76                  else if is_built_in_const thy stds fast_descrs x then
    1.77                    coerce_term hol_ctxt Ts T' T t
    1.78 -                else if is_constr thy stds x then
    1.79 +                else if is_constr ctxt stds x then
    1.80                    Const (finitize_constr x)
    1.81                  else if is_sel s then
    1.82                    let
    1.83 @@ -1112,7 +1113,7 @@
    1.84                  case T1 of
    1.85                    Type (s, [T11, T12]) => 
    1.86                    (if s = @{type_name fin_fun} then
    1.87 -                     select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1
    1.88 +                     select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
    1.89                                             0 (T11 --> T12)
    1.90                     else
    1.91                       t1, T11)
    1.92 @@ -1127,7 +1128,7 @@
    1.93              in
    1.94                Abs (s, T, t')
    1.95                |> should_finitize (T --> T') a
    1.96 -                 ? construct_value thy stds (fin_fun_constr T T') o single
    1.97 +                 ? construct_value ctxt stds (fin_fun_constr T T') o single
    1.98              end
    1.99        in
   1.100          Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));