--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 01 10:31:18 2010 +0200
@@ -242,7 +242,7 @@
*)
val max_bisim_depth = fold Integer.max bisim_depths ~1
val case_names = case_const_names thy stds
- val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
+ val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
val def_table = const_def_table ctxt subst defs
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
@@ -322,8 +322,8 @@
". " ^ extra
end
fun is_type_fundamentally_monotonic T =
- (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
- (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
+ (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso
+ (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
is_number_type thy T orelse is_bit_type T
fun is_type_actually_monotonic T =
formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
@@ -369,7 +369,8 @@
else
()
val (deep_dataTs, shallow_dataTs) =
- all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
+ all_Ts |> filter (is_datatype ctxt stds)
+ |> List.partition is_datatype_deep
val finitizable_dataTs =
shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
|> filter is_shallow_datatype_finitizable
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 10:31:18 2010 +0200
@@ -109,20 +109,19 @@
val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
val is_quot_type : theory -> typ -> bool
val is_codatatype : theory -> typ -> bool
- val is_pure_typedef : theory -> typ -> bool
- val is_univ_typedef : theory -> typ -> bool
- val is_datatype : theory -> (typ option * bool) list -> typ -> bool
+ val is_pure_typedef : Proof.context -> typ -> bool
+ val is_univ_typedef : Proof.context -> typ -> bool
+ val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
val is_record_constr : styp -> bool
val is_record_get : theory -> styp -> bool
val is_record_update : theory -> styp -> bool
- val is_abs_fun : theory -> styp -> bool
- val is_rep_fun : theory -> styp -> bool
+ val is_abs_fun : Proof.context -> styp -> bool
+ val is_rep_fun : Proof.context -> styp -> bool
val is_quot_abs_fun : Proof.context -> styp -> bool
val is_quot_rep_fun : Proof.context -> styp -> bool
- val mate_of_rep_fun : theory -> styp -> styp
- val is_constr_like : theory -> styp -> bool
- val is_stale_constr : theory -> styp -> bool
- val is_constr : theory -> (typ option * bool) list -> styp -> bool
+ val mate_of_rep_fun : Proof.context -> styp -> styp
+ val is_constr_like : Proof.context -> styp -> bool
+ val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
val is_sel : string -> bool
val is_sel_like_and_no_discr : string -> bool
val box_type : hol_context -> boxability -> typ -> typ
@@ -151,9 +150,10 @@
val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
val discriminate_value : hol_context -> styp -> term -> term
val select_nth_constr_arg :
- theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
+ Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
+ -> term
val construct_value :
- theory -> (typ option * bool) list -> styp -> term list -> term
+ Proof.context -> (typ option * bool) list -> styp -> term list -> term
val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
@@ -165,7 +165,7 @@
val abs_var : indexname * typ -> term -> term
val is_funky_typedef : theory -> typ -> bool
val all_axioms_of :
- theory -> (term * term) list -> term list * term list * term list
+ Proof.context -> (term * term) list -> term list * term list * term list
val arity_of_built_in_const :
theory -> (typ option * bool) list -> bool -> styp -> int option
val is_built_in_const :
@@ -186,8 +186,8 @@
val ground_theorem_table : theory -> term list Inttab.table
val ersatz_table : theory -> (string * string) list
val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
- val inverse_axioms_for_rep_fun : theory -> styp -> term list
- val optimized_typedef_axioms : theory -> string * typ list -> term list
+ val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
+ val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
val optimized_quot_type_axioms :
Proof.context -> (typ option * bool) list -> string * typ list -> term list
val def_of_const : theory -> const_table -> styp -> term option
@@ -196,8 +196,8 @@
theory -> const_table -> string * typ -> fixpoint_kind
val is_inductive_pred : hol_context -> styp -> bool
val is_equational_fun : hol_context -> styp -> bool
- val is_constr_pattern_lhs : theory -> term -> bool
- val is_constr_pattern_formula : theory -> term -> bool
+ val is_constr_pattern_lhs : Proof.context -> term -> bool
+ val is_constr_pattern_formula : Proof.context -> term -> bool
val nondef_props_for_const :
theory -> bool -> const_table -> styp -> term list
val is_choice_spec_fun : hol_context -> styp -> bool
@@ -524,22 +524,24 @@
set_def: thm option, prop_of_Rep: thm, set_name: string,
Abs_inverse: thm option, Rep_inverse: thm option}
-fun typedef_info thy s =
- if is_frac_type thy (Type (s, [])) then
- SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
- Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
- set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
- |> Logic.varify_global,
- set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
- else case Typedef.get_info_global thy s of
- (* FIXME handle multiple typedef interpretations (!??) *)
- [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse,
- Rep_inverse, ...})] =>
- SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
- Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
- set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
- Rep_inverse = SOME Rep_inverse}
- | _ => NONE
+fun typedef_info ctxt s =
+ let val thy = ProofContext.theory_of ctxt in
+ if is_frac_type thy (Type (s, [])) then
+ SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
+ Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
+ set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
+ |> Logic.varify_global,
+ set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
+ else case Typedef.get_info ctxt s of
+ (* ### multiple *)
+ [({abs_type, rep_type, Abs_name, Rep_name, ...},
+ {set_def, Rep, Abs_inverse, Rep_inverse, ...})] =>
+ SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
+ Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
+ set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
+ Rep_inverse = SOME Rep_inverse}
+ | _ => NONE
+ end
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
@@ -594,14 +596,16 @@
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
|> Option.map snd |> these))
| is_codatatype _ _ = false
-fun is_pure_typedef thy (T as Type (s, _)) =
- is_typedef thy s andalso
- not (is_real_datatype thy s orelse is_quot_type thy T orelse
- is_codatatype thy T orelse is_record_type T orelse
- is_integer_like_type T)
+fun is_pure_typedef ctxt (T as Type (s, _)) =
+ let val thy = ProofContext.theory_of ctxt in
+ is_typedef ctxt s andalso
+ not (is_real_datatype thy s orelse is_quot_type thy T orelse
+ is_codatatype thy T orelse is_record_type T orelse
+ is_integer_like_type T)
+ end
| is_pure_typedef _ _ = false
-fun is_univ_typedef thy (Type (s, _)) =
- (case typedef_info thy s of
+fun is_univ_typedef ctxt (Type (s, _)) =
+ (case typedef_info ctxt s of
SOME {set_def, prop_of_Rep, ...} =>
let
val t_opt =
@@ -623,9 +627,11 @@
end
| NONE => false)
| is_univ_typedef _ _ = false
-fun is_datatype thy stds (T as Type (s, _)) =
- (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
- is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+fun is_datatype ctxt stds (T as Type (s, _)) =
+ let val thy = ProofContext.theory_of ctxt in
+ (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse
+ is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+ end
| is_datatype _ _ _ = false
fun all_record_fields thy T =
@@ -651,13 +657,13 @@
exists (curry (op =) (unsuffix Record.updateN s) o fst)
(all_record_fields thy (body_type T))
handle TYPE _ => false
-fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
- (case typedef_info thy s' of
+fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) =
+ (case typedef_info ctxt s' of
SOME {Abs_name, ...} => s = Abs_name
| NONE => false)
| is_abs_fun _ _ = false
-fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
- (case typedef_info thy s' of
+fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) =
+ (case typedef_info ctxt s' of
SOME {Rep_name, ...} => s = Rep_name
| NONE => false)
| is_rep_fun _ _ = false
@@ -672,9 +678,9 @@
= SOME (Const x))
| is_quot_rep_fun _ _ = false
-fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
- [T1 as Type (s', _), T2]))) =
- (case typedef_info thy s' of
+fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
+ [T1 as Type (s', _), T2]))) =
+ (case typedef_info ctxt s' of
SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
@@ -700,23 +706,30 @@
(AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
end
handle TYPE ("dest_Type", _, _) => false
-fun is_constr_like thy (s, T) =
+fun is_constr_like ctxt (s, T) =
member (op =) [@{const_name FinFun}, @{const_name FunBox},
@{const_name PairBox}, @{const_name Quot},
@{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
- let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (x as (_, T)) = (s, unarize_unbox_etc_type T)
+ in
Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
- (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
+ (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
is_coconstr thy x
end
-fun is_stale_constr thy (x as (_, T)) =
- is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
- not (is_coconstr thy x)
-fun is_constr thy stds (x as (_, T)) =
- is_constr_like thy x andalso
- not (is_basic_datatype thy stds
+fun is_stale_constr ctxt (x as (_, T)) =
+ let val thy = ProofContext.theory_of ctxt in
+ is_codatatype thy (body_type T) andalso is_constr_like ctxt x andalso
+ not (is_coconstr thy x)
+ end
+fun is_constr ctxt stds (x as (_, T)) =
+ let val thy = ProofContext.theory_of ctxt in
+ is_constr_like ctxt x andalso
+ not (is_basic_datatype thy stds
(fst (dest_Type (unarize_type (body_type T))))) andalso
- not (is_stale_constr thy x)
+ not (is_stale_constr ctxt x)
+ end
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
String.isPrefix sel_prefix orf
@@ -836,12 +849,12 @@
fun zero_const T = Const (@{const_name zero_class.zero}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
+fun uncached_datatype_constrs ({thy, ctxt, stds, ...} : hol_context)
(T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
| _ =>
- if is_datatype thy stds T then
+ if is_datatype ctxt stds T then
case Datatype.get_info thy s of
SOME {index, descr, ...} =>
let
@@ -860,7 +873,7 @@
in [(s', T')] end
else if is_quot_type thy T then
[(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
- else case typedef_info thy s of
+ else case typedef_info ctxt s of
SOME {abs_type, rep_type, Abs_name, ...} =>
[(Abs_name,
varify_and_instantiate_type thy abs_type T rep_type --> T)]
@@ -905,11 +918,11 @@
else
Abs (Name.uu, dataT, @{const True})
end
-fun discriminate_value (hol_ctxt as {thy, ...}) x t =
+fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
case head_of t of
Const x' =>
if x = x' then @{const True}
- else if is_constr_like thy x' then @{const False}
+ else if is_constr_like ctxt x' then @{const False}
else betapply (discr_term_for_constr hol_ctxt x, t)
| _ => betapply (discr_term_for_constr hol_ctxt x, t)
@@ -933,24 +946,26 @@
(List.take (arg_Ts, n)) 0
in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
end
-fun select_nth_constr_arg thy stds x t n res_T =
- (case strip_comb t of
- (Const x', args) =>
- if x = x' then nth args n
- else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
- else raise SAME ()
- | _ => raise SAME())
- handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
+fun select_nth_constr_arg ctxt stds x t n res_T =
+ let val thy = ProofContext.theory_of ctxt in
+ (case strip_comb t of
+ (Const x', args) =>
+ if x = x' then nth args n
+ else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
+ else raise SAME ()
+ | _ => raise SAME())
+ handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
+ end
fun construct_value _ _ x [] = Const x
- | construct_value thy stds (x as (s, _)) args =
+ | construct_value ctxt stds (x as (s, _)) args =
let val args = map Envir.eta_contract args in
case hd args of
Const (s', _) $ t =>
if is_sel_like_and_no_discr s' andalso
constr_name_for_sel_like s' = s andalso
forall (fn (n, t') =>
- select_nth_constr_arg thy stds x t n dummyT = t')
+ select_nth_constr_arg ctxt stds x t n dummyT = t')
(index_seq 0 (length args) ~~ args) then
t
else
@@ -958,9 +973,9 @@
| _ => list_comb (Const x, args)
end
-fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
+fun constr_expand (hol_ctxt as {ctxt, stds, ...}) T t =
(case head_of t of
- Const x => if is_constr_like thy x then t else raise SAME ()
+ Const x => if is_constr_like ctxt x then t else raise SAME ()
| _ => raise SAME ())
handle SAME () =>
let
@@ -973,7 +988,7 @@
datatype_constrs hol_ctxt T |> hd
val arg_Ts = binder_types T'
in
- list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
+ list_comb (Const x', map2 (select_nth_constr_arg ctxt stds x' t)
(index_seq 0 (length arg_Ts)) arg_Ts)
end
@@ -985,7 +1000,7 @@
| _ => t
fun coerce_bound_0_in_term hol_ctxt new_T old_T =
old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
-and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
+and coerce_term (hol_ctxt as {ctxt, stds, fast_descrs, ...}) Ts new_T old_T t =
if old_T = new_T then
t
else
@@ -999,7 +1014,7 @@
|> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
|> Envir.eta_contract
|> new_s <> @{type_name fun}
- ? construct_value thy stds
+ ? construct_value ctxt stds
(if new_s = @{type_name fin_fun} then @{const_name FinFun}
else @{const_name FunBox},
Type (@{type_name fun}, new_Ts) --> new_T)
@@ -1014,12 +1029,12 @@
if new_s = @{type_name fun} then
coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
else
- construct_value thy stds
+ construct_value ctxt stds
(old_s, Type (@{type_name fun}, new_Ts) --> new_T)
[coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
(Type (@{type_name fun}, old_Ts)) t1]
| Const _ $ t1 $ t2 =>
- construct_value thy stds
+ construct_value ctxt stds
(if new_s = @{type_name "*"} then @{const_name Pair}
else @{const_name PairBox}, new_Ts ---> new_T)
(map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
@@ -1145,13 +1160,15 @@
fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
$ Const (@{const_name TYPE}, _)) = true
| is_arity_type_axiom _ = false
-fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
- is_typedef_axiom thy boring t2
- | is_typedef_axiom thy boring
+fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
+ is_typedef_axiom ctxt boring t2
+ | is_typedef_axiom ctxt boring
(@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
$ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
$ Const _ $ _)) =
- boring <> is_funky_typedef_name thy s andalso is_typedef thy s
+ let val thy = ProofContext.theory_of ctxt in
+ boring <> is_funky_typedef_name thy s andalso is_typedef ctxt s
+ end
| is_typedef_axiom _ _ _ = false
val is_class_axiom =
Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
@@ -1160,13 +1177,13 @@
typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
Typedef axioms are uninteresting to Nitpick, because it can retrieve them
using "typedef_info". *)
-fun partition_axioms_by_definitionality thy axioms def_names =
+fun partition_axioms_by_definitionality ctxt axioms def_names =
let
val axioms = sort (fast_string_ord o pairself fst) axioms
val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
val nondefs =
OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
- |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
+ |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
in pairself (map snd) (defs, nondefs) end
(* Ideally we would check against "Complex_Main", not "Refute", but any theory
@@ -1189,8 +1206,9 @@
| do_eq _ = false
in do_eq end
-fun all_axioms_of thy subst =
+fun all_axioms_of ctxt subst =
let
+ val thy = ProofContext.theory_of ctxt
val axioms_of_thys =
maps Thm.axioms_of
#> map (apsnd (subst_atomic subst o prop_of))
@@ -1203,12 +1221,12 @@
val built_in_axioms = axioms_of_thys built_in_thys
val user_axioms = axioms_of_thys user_thys
val (built_in_defs, built_in_nondefs) =
- partition_axioms_by_definitionality thy built_in_axioms def_names
- ||> filter (is_typedef_axiom thy false)
+ partition_axioms_by_definitionality ctxt built_in_axioms def_names
+ ||> filter (is_typedef_axiom ctxt false)
val (user_defs, user_nondefs) =
- partition_axioms_by_definitionality thy user_axioms def_names
+ partition_axioms_by_definitionality ctxt user_axioms def_names
val (built_in_nondefs, user_nondefs) =
- List.partition (is_typedef_axiom thy false) user_nondefs
+ List.partition (is_typedef_axiom ctxt false) user_nondefs
|>> append built_in_nondefs
val defs =
(thy |> PureThy.all_thms_of
@@ -1369,16 +1387,16 @@
| _ => NONE
fun is_constr_pattern _ (Bound _) = true
| is_constr_pattern _ (Var _) = true
- | is_constr_pattern thy t =
+ | is_constr_pattern ctxt t =
case strip_comb t of
(Const x, args) =>
- is_constr_like thy x andalso forall (is_constr_pattern thy) args
+ is_constr_like ctxt x andalso forall (is_constr_pattern ctxt) args
| _ => false
-fun is_constr_pattern_lhs thy t =
- forall (is_constr_pattern thy) (snd (strip_comb t))
-fun is_constr_pattern_formula thy t =
+fun is_constr_pattern_lhs ctxt t =
+ forall (is_constr_pattern ctxt) (snd (strip_comb t))
+fun is_constr_pattern_formula ctxt t =
case lhs_of_equation t of
- SOME t' => is_constr_pattern_lhs thy t'
+ SOME t' => is_constr_pattern_lhs ctxt t'
| NONE => false
(* Similar to "specialize_type" but returns all matches rather than only the
@@ -1439,26 +1457,26 @@
(** Constant unfolding **)
-fun constr_case_body thy stds (j, (x as (_, T))) =
+fun constr_case_body ctxt stds (j, (x as (_, T))) =
let val arg_Ts = binder_types T in
- list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
+ list_comb (Bound j, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
-fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
+fun add_constr_case (hol_ctxt as {ctxt, stds, ...}) res_T (j, x) res_t =
Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
- $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
+ $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body ctxt stds (j, x)
$ res_t
-fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
+fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T =
let
val xs = datatype_constrs hol_ctxt dataT
val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
val (xs', x) = split_last xs
in
- constr_case_body thy stds (1, x)
+ constr_case_body ctxt stds (1, x)
|> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
-fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
+fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
case no_of_record_field thy s rec_T of
~1 => (case rec_T of
@@ -1467,14 +1485,15 @@
val rec_T' = List.last Ts
val j = num_record_fields thy rec_T - 1
in
- select_nth_constr_arg thy stds constr_x t j res_T
+ select_nth_constr_arg ctxt stds constr_x t j res_T
|> optimized_record_get hol_ctxt s rec_T' res_T
end
| _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
[]))
- | j => select_nth_constr_arg thy stds constr_x t j res_T
+ | j => select_nth_constr_arg ctxt stds constr_x t j res_T
end
-fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
+fun optimized_record_update (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T fun_t
+ rec_t =
let
val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
val Ts = binder_types constr_T
@@ -1482,7 +1501,7 @@
val special_j = no_of_record_field thy s rec_T
val ts =
map2 (fn j => fn T =>
- let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
+ let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
if j = special_j then
betapply (fun_t, t)
else if j = n - 1 andalso special_j = ~1 then
@@ -1551,9 +1570,9 @@
| Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
(Abs (Name.uu, body_type T,
- select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
+ select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
| select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
- (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
+ (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
and do_const depth Ts t (x as (s, T)) ts =
case AList.lookup (op =) ersatz_table s of
SOME s' =>
@@ -1573,9 +1592,9 @@
|> do_term (depth + 1) Ts, ts)
end
| _ =>
- if is_constr thy stds x then
+ if is_constr ctxt stds x then
(Const x, ts)
- else if is_stale_constr thy x then
+ else if is_stale_constr ctxt x then
raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
\(\"" ^ s ^ "\")")
else if is_quot_abs_fun ctxt x then
@@ -1606,9 +1625,9 @@
(do_term depth Ts (hd ts))
(do_term depth Ts (nth ts 1)), [])
| n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
- else if is_rep_fun thy x then
- let val x' = mate_of_rep_fun thy x in
- if is_constr thy stds x' then
+ else if is_rep_fun ctxt x then
+ let val x' = mate_of_rep_fun ctxt x in
+ if is_constr ctxt stds x' then
select_nth_constr_arg_with_args depth Ts x' ts 0
(range_type T)
else
@@ -1679,18 +1698,24 @@
Unsynchronized.change simp_table
(Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
-fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
- let val abs_T = domain_type T in
- typedef_info thy (fst (dest_Type abs_T)) |> the
+fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val abs_T = domain_type T
+ in
+ typedef_info ctxt (fst (dest_Type abs_T)) |> the
|> pairf #Abs_inverse #Rep_inverse
|> pairself (specialize_type thy x o prop_of o the)
||> single |> op ::
end
-fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
- let val abs_T = Type abs_z in
- if is_univ_typedef thy abs_T then
+fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val abs_T = Type abs_z
+ in
+ if is_univ_typedef ctxt abs_T then
[]
- else case typedef_info thy abs_s of
+ else case typedef_info ctxt abs_s of
SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
let
val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
@@ -1718,7 +1743,7 @@
val x_var = Var (("x", 0), rep_T)
val y_var = Var (("y", 0), rep_T)
val x = (@{const_name Quot}, rep_T --> abs_T)
- val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
+ val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
val normal_x = normal_t $ x_var
val normal_y = normal_t $ y_var
@@ -1736,7 +1761,7 @@
HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
end
-fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
+fun codatatype_bisim_axioms (hol_ctxt as {ctxt, thy, stds, ...}) T =
let
val xs = datatype_constrs hol_ctxt T
val set_T = T --> bool_T
@@ -1753,8 +1778,8 @@
fun nth_sub_bisim x n nth_T =
(if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
else HOLogic.eq_const nth_T)
- $ select_nth_constr_arg thy stds x x_var n nth_T
- $ select_nth_constr_arg thy stds x y_var n nth_T
+ $ select_nth_constr_arg ctxt stds x x_var n nth_T
+ $ select_nth_constr_arg ctxt stds x y_var n nth_T
fun case_func (x as (_, T)) =
let
val arg_Ts = binder_types T
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 10:31:18 2010 +0200
@@ -319,7 +319,7 @@
end
in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
- (scope as {hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns,
+ (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
bits, datatypes, ofs, ...}) sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
@@ -536,7 +536,7 @@
| _ => raise TERM ("Nitpick_Model.reconstruct_term.\
\term_for_atom (Abs_Frac)", ts)
else if not for_auto andalso
- (is_abs_fun thy constr_x orelse
+ (is_abs_fun ctxt constr_x orelse
constr_s = @{const_name Quot}) then
Const (abs_name, constr_T) $ the_single ts
else
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jun 01 10:31:18 2010 +0200
@@ -162,8 +162,8 @@
| could_exist_alpha_subtype alpha_T T = (T = alpha_T)
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
could_exist_alpha_subtype alpha_T T
- | could_exist_alpha_sub_mtype thy alpha_T T =
- (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
+ | could_exist_alpha_sub_mtype ctxt alpha_T T =
+ (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
fun exists_alpha_sub_mtype MAlpha = true
| exists_alpha_sub_mtype (MFun (M1, _, M2)) =
@@ -243,7 +243,7 @@
else
S Minus
in (M1, a, M2) end
-and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
+and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
datatype_mcache, constr_mcache, ...})
all_minus =
let
@@ -255,7 +255,7 @@
MFun (fresh_mfun_for_fun_type mdata false T1 T2)
| Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
| Type (z as (s, _)) =>
- if could_exist_alpha_sub_mtype thy alpha_T T then
+ if could_exist_alpha_sub_mtype ctxt alpha_T T then
case AList.lookup (op =) (!datatype_mcache) z of
SOME M => M
| NONE =>
@@ -304,9 +304,9 @@
case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
end
-fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
+fun mtype_for_constr (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, constr_mcache,
...}) (x as (_, T)) =
- if could_exist_alpha_sub_mtype thy alpha_T T then
+ if could_exist_alpha_sub_mtype ctxt alpha_T T then
case AList.lookup (op =) (!constr_mcache) x of
SOME M => M
| NONE => if T = alpha_T then
@@ -741,7 +741,7 @@
do_robust_set_operation T accum
else if is_sel s then
(mtype_for_sel mdata x, accum)
- else if is_constr thy stds x then
+ else if is_constr ctxt stds x then
(mtype_for_constr mdata x, accum)
else if is_built_in_const thy stds fast_descrs x then
(fresh_mtype_for_type mdata true T, accum)
@@ -924,8 +924,8 @@
if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
else consider_general_formula mdata Plus t
-fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
- if not (is_constr_pattern_formula thy t) then
+fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
+ if not (is_constr_pattern_formula ctxt t) then
consider_nondefinitional_axiom mdata t
else if is_harmless_axiom mdata t then
pair (MRaw (t, dummy_M))
@@ -1027,7 +1027,8 @@
fun fin_fun_constr T1 T2 =
(@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
-fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
+fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
+ ...})
binarize finitizes alpha_T tsp =
case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
SOME (lits, msp, constr_mtypes) =>
@@ -1085,7 +1086,7 @@
Const (s, T')
else if is_built_in_const thy stds fast_descrs x then
coerce_term hol_ctxt Ts T' T t
- else if is_constr thy stds x then
+ else if is_constr ctxt stds x then
Const (finitize_constr x)
else if is_sel s then
let
@@ -1112,7 +1113,7 @@
case T1 of
Type (s, [T11, T12]) =>
(if s = @{type_name fin_fun} then
- select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1
+ select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
0 (T11 --> T12)
else
t1, T11)
@@ -1127,7 +1128,7 @@
in
Abs (s, T, t')
|> should_finitize (T --> T') a
- ? construct_value thy stds (fin_fun_constr T T') o single
+ ? construct_value ctxt stds (fin_fun_constr T T') o single
end
in
Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 01 10:31:18 2010 +0200
@@ -439,7 +439,7 @@
maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
-fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
let
fun aux eq ss Ts t =
let
@@ -565,7 +565,7 @@
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
| (Const (x as (s as @{const_name Suc}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Suc, T, Any)
- else if is_constr thy stds x then do_construct x []
+ else if is_constr ctxt stds x then do_construct x []
else ConstName (s, T, Any)
| (Const (@{const_name finite}, T), [t1]) =>
(if is_finite_type hol_ctxt (domain_type T) then
@@ -576,7 +576,7 @@
| (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
| (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
- else if is_constr thy stds x then do_construct x []
+ else if is_constr ctxt stds x then do_construct x []
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name one_class.one}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
@@ -653,7 +653,7 @@
[t1, t2]) =>
Op2 (Union, T1, Any, sub t1, sub t2)
| (t0 as Const (x as (s, T)), ts) =>
- if is_constr thy stds x then
+ if is_constr ctxt stds x then
do_construct x ts
else if String.isPrefix numeral_prefix s then
Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
@@ -687,13 +687,13 @@
val R = best_non_opt_set_rep_for_type scope (type_of v)
val v = modify_name_rep v R
in (v :: vs, NameTable.update (v, R) table) end
-fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
+fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
(vs, table) =
let
val x as (s, T) = (nickname_of v, type_of v)
- val R = (if is_abs_fun thy x then
+ val R = (if is_abs_fun ctxt x then
rep_for_abs_fun
- else if is_rep_fun thy x then
+ else if is_rep_fun ctxt x then
Func oo best_non_opt_symmetric_reps_for_fun_type
else if all_exact orelse is_skolem_name v orelse
member (op =) [@{const_name undefined_fast_The},
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jun 01 10:31:18 2010 +0200
@@ -65,14 +65,15 @@
(** Uncurrying **)
-fun add_to_uncurry_table thy t =
+fun add_to_uncurry_table ctxt t =
let
+ val thy = ProofContext.theory_of ctxt
fun aux (t1 $ t2) args table =
let val table = aux t2 [] table in aux t1 (t2 :: args) table end
| aux (Abs (_, _, t')) _ table = aux t' [] table
| aux (t as Const (x as (s, _))) args table =
if is_built_in_const thy [(NONE, true)] true x orelse
- is_constr_like thy x orelse
+ is_constr_like ctxt x orelse
is_sel s orelse s = @{const_name Sigma} then
table
else
@@ -121,8 +122,8 @@
(** Boxing **)
-fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
- orig_t =
+fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...})
+ def orig_t =
let
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
Type (@{type_name fun}, map box_relational_operator_type Ts)
@@ -228,10 +229,9 @@
else if is_built_in_const thy stds fast_descrs x orelse
s = @{const_name Sigma} then
T
- else if is_constr_like thy x then
+ else if is_constr_like ctxt x then
box_type hol_ctxt InConstr T
- else if is_sel s
- orelse is_rep_fun thy x then
+ else if is_sel s orelse is_rep_fun ctxt x then
box_type hol_ctxt InSel T
else
box_type hol_ctxt InExpr T)
@@ -248,7 +248,7 @@
betapply (if s1 = @{type_name fun} then
t1
else
- select_nth_constr_arg thy stds
+ select_nth_constr_arg ctxt stds
(@{const_name FunBox},
Type (@{type_name fun}, Ts1) --> T1) t1 0
(Type (@{type_name fun}, Ts1)), t2)
@@ -265,7 +265,7 @@
betapply (if s1 = @{type_name fun} then
t1
else
- select_nth_constr_arg thy stds
+ select_nth_constr_arg ctxt stds
(@{const_name FunBox},
Type (@{type_name fun}, Ts1) --> T1) t1 0
(Type (@{type_name fun}, Ts1)), t2)
@@ -293,12 +293,12 @@
| aux _ = true
in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
-fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
+fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t
args seen =
let val t_comb = list_comb (t, args) in
case t of
Const x =>
- if not relax andalso is_constr thy stds x andalso
+ if not relax andalso is_constr ctxt stds x andalso
not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
has_heavy_bounds_or_vars Ts t_comb andalso
not (loose_bvar (t_comb, level)) then
@@ -397,7 +397,7 @@
$ t $ abs_var z (incr_boundvars 1 (f (Var z)))
end
-fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
+fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =
let
val num_occs_of_var =
fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
@@ -432,7 +432,7 @@
val n = length arg_Ts
in
if length args = n andalso
- (is_constr thy stds x orelse s = @{const_name Pair} orelse
+ (is_constr ctxt stds x orelse s = @{const_name Pair} orelse
x = (@{const_name Suc}, nat_T --> nat_T)) andalso
(not careful orelse not (is_Var t1) orelse
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
@@ -449,7 +449,7 @@
else t0 $ aux false t2 $ aux false t1
and sel_eq x t n nth_T nth_t =
HOLogic.eq_const nth_T $ nth_t
- $ select_nth_constr_arg thy stds x t n nth_T
+ $ select_nth_constr_arg ctxt stds x t n nth_T
|> aux false
in aux axiom t end
@@ -484,7 +484,7 @@
aux (t1 :: prems) (Term.add_vars t1 zs) t2
in aux [] [] end
-fun find_bound_assign thy stds j =
+fun find_bound_assign ctxt stds j =
let
fun do_term _ [] = NONE
| do_term seen (t :: ts) =
@@ -497,8 +497,9 @@
| Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
if j' = j andalso
s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
- SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
- [t2], ts @ seen)
+ SOME (construct_value ctxt stds
+ (@{const_name FunBox}, T2 --> T1) [t2],
+ ts @ seen)
else
raise SAME ()
| _ => raise SAME ())
@@ -523,11 +524,11 @@
| aux _ = raise SAME ()
in aux (t, j) handle SAME () => t end
-fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
+fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) =
let
fun kill [] [] ts = foldr1 s_conj ts
| kill (s :: ss) (T :: Ts) ts =
- (case find_bound_assign thy stds (length ss) [] ts of
+ (case find_bound_assign ctxt stds (length ss) [] ts of
SOME (_, []) => @{const True}
| SOME (arg_t, ts) =>
kill ss Ts (map (subst_one_bound (length ss)
@@ -893,7 +894,7 @@
(if head_of t <> @{const "==>"} then add_def_axiom
else add_nondef_axiom) depth t
and add_eq_axiom depth t =
- (if is_constr_pattern_formula thy t then add_def_axiom
+ (if is_constr_pattern_formula ctxt t then add_def_axiom
else add_nondef_axiom) depth t
and add_axioms_for_term depth t (accum as (xs, axs)) =
case t of
@@ -921,7 +922,7 @@
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
accum
end
- else if is_constr thy stds x then
+ else if is_constr ctxt stds x then
accum
else if is_equational_fun hol_ctxt x then
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
@@ -929,7 +930,7 @@
else if is_choice_spec_fun hol_ctxt x then
fold (add_nondef_axiom depth)
(nondef_props_for_const thy true choice_spec_table x) accum
- else if is_abs_fun thy x then
+ else if is_abs_fun ctxt x then
if is_quot_type thy (range_type T) then
raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
else
@@ -940,7 +941,7 @@
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
(extra_table def_table s) x)
- else if is_rep_fun thy x then
+ else if is_rep_fun ctxt x then
if is_quot_type thy (domain_type T) then
raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
else
@@ -952,9 +953,9 @@
(nondef_props_for_const thy true
(extra_table def_table s) x)
|> add_axioms_for_term depth
- (Const (mate_of_rep_fun thy x))
+ (Const (mate_of_rep_fun ctxt x))
|> fold (add_def_axiom depth)
- (inverse_axioms_for_rep_fun thy x)
+ (inverse_axioms_for_rep_fun ctxt x)
else if s = @{const_name TYPE} then
accum
else
@@ -979,8 +980,8 @@
| TVar (_, S) => add_axioms_for_sort depth T S
| Type (z as (_, Ts)) =>
fold (add_axioms_for_type depth) Ts
- #> (if is_pure_typedef thy T then
- fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
+ #> (if is_pure_typedef ctxt T then
+ fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)
else if is_quot_type thy T then
fold (add_def_axiom depth)
(optimized_quot_type_axioms ctxt stds z)
@@ -1020,7 +1021,7 @@
(** Simplification of constructor/selector terms **)
-fun simplify_constrs_and_sels thy t =
+fun simplify_constrs_and_sels ctxt t =
let
fun is_nth_sel_on t' n (Const (s, _) $ t) =
(t = t' andalso is_sel_like_and_no_discr s andalso
@@ -1032,7 +1033,7 @@
$ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
| do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
| do_term (t as Const (x as (s, T))) (args as _ :: _) =
- ((if is_constr_like thy x then
+ ((if is_constr_like ctxt x then
if length args = num_binder_types T then
case hd args of
Const (_, T') $ t' =>
@@ -1048,7 +1049,7 @@
else if is_sel_like_and_no_discr s then
case strip_comb (hd args) of
(Const (x' as (s', T')), ts') =>
- if is_constr_like thy x' andalso
+ if is_constr_like ctxt x' andalso
constr_name_for_sel_like s = s' andalso
not (exists is_pair_type (binder_types T')) then
list_comb (nth ts' (sel_no_from_name s), tl args)
@@ -1230,7 +1231,7 @@
val max_skolem_depth = 4
-fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
+fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
boxes, ...}) finitizes monos t =
let
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
@@ -1250,7 +1251,7 @@
val box = exists (not_equal (SOME false) o snd) boxes
val table =
Termtab.empty
- |> box ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
+ |> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)
fun do_rest def =
binarize ? binarize_nat_and_int_in_term
#> box ? uncurry_term table
@@ -1261,7 +1262,7 @@
#> curry_assms
#> destroy_universal_equalities
#> destroy_existential_equalities hol_ctxt
- #> simplify_constrs_and_sels thy
+ #> simplify_constrs_and_sels ctxt
#> distribute_quantifiers
#> push_quantifiers_inward
#> close_form
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Jun 01 10:31:18 2010 +0200
@@ -135,7 +135,7 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
fun quintuple_for_scope quote
- ({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+ ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
datatypes, ...} : scope) =
let
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@@ -144,8 +144,8 @@
card_assigns |> filter_out (member (op =) boring_Ts o fst)
|> List.partition (is_fp_iterator_type o fst)
val (secondary_card_assigns, primary_card_assigns) =
- card_assigns |> List.partition ((is_integer_type orf is_datatype thy stds)
- o fst)
+ card_assigns
+ |> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst)
val cards =
map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
string_of_int k)
@@ -458,13 +458,13 @@
concrete = concrete, deep = deep, constrs = constrs}
end
-fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize deep_dataTs
+fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
finitizable_dataTs (desc as (card_assigns, _)) =
let
val datatypes =
map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
finitizable_dataTs desc)
- (filter (is_datatype thy stds o fst) card_assigns)
+ (filter (is_datatype ctxt stds o fst) card_assigns)
val bits = card_of_type card_assigns @{typ signed_bit} - 1
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
card_of_type card_assigns @{typ unsigned_bit}