1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon May 31 18:51:06 2010 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 01 10:31:18 2010 +0200
1.3 @@ -242,7 +242,7 @@
1.4 *)
1.5 val max_bisim_depth = fold Integer.max bisim_depths ~1
1.6 val case_names = case_const_names thy stds
1.7 - val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
1.8 + val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
1.9 val def_table = const_def_table ctxt subst defs
1.10 val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
1.11 val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
1.12 @@ -322,8 +322,8 @@
1.13 ". " ^ extra
1.14 end
1.15 fun is_type_fundamentally_monotonic T =
1.16 - (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
1.17 - (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
1.18 + (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso
1.19 + (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
1.20 is_number_type thy T orelse is_bit_type T
1.21 fun is_type_actually_monotonic T =
1.22 formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
1.23 @@ -369,7 +369,8 @@
1.24 else
1.25 ()
1.26 val (deep_dataTs, shallow_dataTs) =
1.27 - all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
1.28 + all_Ts |> filter (is_datatype ctxt stds)
1.29 + |> List.partition is_datatype_deep
1.30 val finitizable_dataTs =
1.31 shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
1.32 |> filter is_shallow_datatype_finitizable
2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon May 31 18:51:06 2010 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 10:31:18 2010 +0200
2.3 @@ -109,20 +109,19 @@
2.4 val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
2.5 val is_quot_type : theory -> typ -> bool
2.6 val is_codatatype : theory -> typ -> bool
2.7 - val is_pure_typedef : theory -> typ -> bool
2.8 - val is_univ_typedef : theory -> typ -> bool
2.9 - val is_datatype : theory -> (typ option * bool) list -> typ -> bool
2.10 + val is_pure_typedef : Proof.context -> typ -> bool
2.11 + val is_univ_typedef : Proof.context -> typ -> bool
2.12 + val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
2.13 val is_record_constr : styp -> bool
2.14 val is_record_get : theory -> styp -> bool
2.15 val is_record_update : theory -> styp -> bool
2.16 - val is_abs_fun : theory -> styp -> bool
2.17 - val is_rep_fun : theory -> styp -> bool
2.18 + val is_abs_fun : Proof.context -> styp -> bool
2.19 + val is_rep_fun : Proof.context -> styp -> bool
2.20 val is_quot_abs_fun : Proof.context -> styp -> bool
2.21 val is_quot_rep_fun : Proof.context -> styp -> bool
2.22 - val mate_of_rep_fun : theory -> styp -> styp
2.23 - val is_constr_like : theory -> styp -> bool
2.24 - val is_stale_constr : theory -> styp -> bool
2.25 - val is_constr : theory -> (typ option * bool) list -> styp -> bool
2.26 + val mate_of_rep_fun : Proof.context -> styp -> styp
2.27 + val is_constr_like : Proof.context -> styp -> bool
2.28 + val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
2.29 val is_sel : string -> bool
2.30 val is_sel_like_and_no_discr : string -> bool
2.31 val box_type : hol_context -> boxability -> typ -> typ
2.32 @@ -151,9 +150,10 @@
2.33 val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
2.34 val discriminate_value : hol_context -> styp -> term -> term
2.35 val select_nth_constr_arg :
2.36 - theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
2.37 + Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
2.38 + -> term
2.39 val construct_value :
2.40 - theory -> (typ option * bool) list -> styp -> term list -> term
2.41 + Proof.context -> (typ option * bool) list -> styp -> term list -> term
2.42 val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
2.43 val card_of_type : (typ * int) list -> typ -> int
2.44 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
2.45 @@ -165,7 +165,7 @@
2.46 val abs_var : indexname * typ -> term -> term
2.47 val is_funky_typedef : theory -> typ -> bool
2.48 val all_axioms_of :
2.49 - theory -> (term * term) list -> term list * term list * term list
2.50 + Proof.context -> (term * term) list -> term list * term list * term list
2.51 val arity_of_built_in_const :
2.52 theory -> (typ option * bool) list -> bool -> styp -> int option
2.53 val is_built_in_const :
2.54 @@ -186,8 +186,8 @@
2.55 val ground_theorem_table : theory -> term list Inttab.table
2.56 val ersatz_table : theory -> (string * string) list
2.57 val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
2.58 - val inverse_axioms_for_rep_fun : theory -> styp -> term list
2.59 - val optimized_typedef_axioms : theory -> string * typ list -> term list
2.60 + val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
2.61 + val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
2.62 val optimized_quot_type_axioms :
2.63 Proof.context -> (typ option * bool) list -> string * typ list -> term list
2.64 val def_of_const : theory -> const_table -> styp -> term option
2.65 @@ -196,8 +196,8 @@
2.66 theory -> const_table -> string * typ -> fixpoint_kind
2.67 val is_inductive_pred : hol_context -> styp -> bool
2.68 val is_equational_fun : hol_context -> styp -> bool
2.69 - val is_constr_pattern_lhs : theory -> term -> bool
2.70 - val is_constr_pattern_formula : theory -> term -> bool
2.71 + val is_constr_pattern_lhs : Proof.context -> term -> bool
2.72 + val is_constr_pattern_formula : Proof.context -> term -> bool
2.73 val nondef_props_for_const :
2.74 theory -> bool -> const_table -> styp -> term list
2.75 val is_choice_spec_fun : hol_context -> styp -> bool
2.76 @@ -524,22 +524,24 @@
2.77 set_def: thm option, prop_of_Rep: thm, set_name: string,
2.78 Abs_inverse: thm option, Rep_inverse: thm option}
2.79
2.80 -fun typedef_info thy s =
2.81 - if is_frac_type thy (Type (s, [])) then
2.82 - SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
2.83 - Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
2.84 - set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
2.85 - |> Logic.varify_global,
2.86 - set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
2.87 - else case Typedef.get_info_global thy s of
2.88 - (* FIXME handle multiple typedef interpretations (!??) *)
2.89 - [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse,
2.90 - Rep_inverse, ...})] =>
2.91 - SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
2.92 - Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
2.93 - set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
2.94 - Rep_inverse = SOME Rep_inverse}
2.95 - | _ => NONE
2.96 +fun typedef_info ctxt s =
2.97 + let val thy = ProofContext.theory_of ctxt in
2.98 + if is_frac_type thy (Type (s, [])) then
2.99 + SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
2.100 + Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
2.101 + set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
2.102 + |> Logic.varify_global,
2.103 + set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
2.104 + else case Typedef.get_info ctxt s of
2.105 + (* ### multiple *)
2.106 + [({abs_type, rep_type, Abs_name, Rep_name, ...},
2.107 + {set_def, Rep, Abs_inverse, Rep_inverse, ...})] =>
2.108 + SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
2.109 + Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
2.110 + set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
2.111 + Rep_inverse = SOME Rep_inverse}
2.112 + | _ => NONE
2.113 + end
2.114
2.115 val is_typedef = is_some oo typedef_info
2.116 val is_real_datatype = is_some oo Datatype.get_info
2.117 @@ -594,14 +596,16 @@
2.118 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
2.119 |> Option.map snd |> these))
2.120 | is_codatatype _ _ = false
2.121 -fun is_pure_typedef thy (T as Type (s, _)) =
2.122 - is_typedef thy s andalso
2.123 - not (is_real_datatype thy s orelse is_quot_type thy T orelse
2.124 - is_codatatype thy T orelse is_record_type T orelse
2.125 - is_integer_like_type T)
2.126 +fun is_pure_typedef ctxt (T as Type (s, _)) =
2.127 + let val thy = ProofContext.theory_of ctxt in
2.128 + is_typedef ctxt s andalso
2.129 + not (is_real_datatype thy s orelse is_quot_type thy T orelse
2.130 + is_codatatype thy T orelse is_record_type T orelse
2.131 + is_integer_like_type T)
2.132 + end
2.133 | is_pure_typedef _ _ = false
2.134 -fun is_univ_typedef thy (Type (s, _)) =
2.135 - (case typedef_info thy s of
2.136 +fun is_univ_typedef ctxt (Type (s, _)) =
2.137 + (case typedef_info ctxt s of
2.138 SOME {set_def, prop_of_Rep, ...} =>
2.139 let
2.140 val t_opt =
2.141 @@ -623,9 +627,11 @@
2.142 end
2.143 | NONE => false)
2.144 | is_univ_typedef _ _ = false
2.145 -fun is_datatype thy stds (T as Type (s, _)) =
2.146 - (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
2.147 - is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
2.148 +fun is_datatype ctxt stds (T as Type (s, _)) =
2.149 + let val thy = ProofContext.theory_of ctxt in
2.150 + (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse
2.151 + is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
2.152 + end
2.153 | is_datatype _ _ _ = false
2.154
2.155 fun all_record_fields thy T =
2.156 @@ -651,13 +657,13 @@
2.157 exists (curry (op =) (unsuffix Record.updateN s) o fst)
2.158 (all_record_fields thy (body_type T))
2.159 handle TYPE _ => false
2.160 -fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
2.161 - (case typedef_info thy s' of
2.162 +fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) =
2.163 + (case typedef_info ctxt s' of
2.164 SOME {Abs_name, ...} => s = Abs_name
2.165 | NONE => false)
2.166 | is_abs_fun _ _ = false
2.167 -fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
2.168 - (case typedef_info thy s' of
2.169 +fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) =
2.170 + (case typedef_info ctxt s' of
2.171 SOME {Rep_name, ...} => s = Rep_name
2.172 | NONE => false)
2.173 | is_rep_fun _ _ = false
2.174 @@ -672,9 +678,9 @@
2.175 = SOME (Const x))
2.176 | is_quot_rep_fun _ _ = false
2.177
2.178 -fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
2.179 - [T1 as Type (s', _), T2]))) =
2.180 - (case typedef_info thy s' of
2.181 +fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
2.182 + [T1 as Type (s', _), T2]))) =
2.183 + (case typedef_info ctxt s' of
2.184 SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
2.185 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
2.186 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
2.187 @@ -700,23 +706,30 @@
2.188 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
2.189 end
2.190 handle TYPE ("dest_Type", _, _) => false
2.191 -fun is_constr_like thy (s, T) =
2.192 +fun is_constr_like ctxt (s, T) =
2.193 member (op =) [@{const_name FinFun}, @{const_name FunBox},
2.194 @{const_name PairBox}, @{const_name Quot},
2.195 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
2.196 - let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
2.197 + let
2.198 + val thy = ProofContext.theory_of ctxt
2.199 + val (x as (_, T)) = (s, unarize_unbox_etc_type T)
2.200 + in
2.201 Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
2.202 - (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
2.203 + (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
2.204 is_coconstr thy x
2.205 end
2.206 -fun is_stale_constr thy (x as (_, T)) =
2.207 - is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
2.208 - not (is_coconstr thy x)
2.209 -fun is_constr thy stds (x as (_, T)) =
2.210 - is_constr_like thy x andalso
2.211 - not (is_basic_datatype thy stds
2.212 +fun is_stale_constr ctxt (x as (_, T)) =
2.213 + let val thy = ProofContext.theory_of ctxt in
2.214 + is_codatatype thy (body_type T) andalso is_constr_like ctxt x andalso
2.215 + not (is_coconstr thy x)
2.216 + end
2.217 +fun is_constr ctxt stds (x as (_, T)) =
2.218 + let val thy = ProofContext.theory_of ctxt in
2.219 + is_constr_like ctxt x andalso
2.220 + not (is_basic_datatype thy stds
2.221 (fst (dest_Type (unarize_type (body_type T))))) andalso
2.222 - not (is_stale_constr thy x)
2.223 + not (is_stale_constr ctxt x)
2.224 + end
2.225 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
2.226 val is_sel_like_and_no_discr =
2.227 String.isPrefix sel_prefix orf
2.228 @@ -836,12 +849,12 @@
2.229 fun zero_const T = Const (@{const_name zero_class.zero}, T)
2.230 fun suc_const T = Const (@{const_name Suc}, T --> T)
2.231
2.232 -fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
2.233 +fun uncached_datatype_constrs ({thy, ctxt, stds, ...} : hol_context)
2.234 (T as Type (s, Ts)) =
2.235 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
2.236 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
2.237 | _ =>
2.238 - if is_datatype thy stds T then
2.239 + if is_datatype ctxt stds T then
2.240 case Datatype.get_info thy s of
2.241 SOME {index, descr, ...} =>
2.242 let
2.243 @@ -860,7 +873,7 @@
2.244 in [(s', T')] end
2.245 else if is_quot_type thy T then
2.246 [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
2.247 - else case typedef_info thy s of
2.248 + else case typedef_info ctxt s of
2.249 SOME {abs_type, rep_type, Abs_name, ...} =>
2.250 [(Abs_name,
2.251 varify_and_instantiate_type thy abs_type T rep_type --> T)]
2.252 @@ -905,11 +918,11 @@
2.253 else
2.254 Abs (Name.uu, dataT, @{const True})
2.255 end
2.256 -fun discriminate_value (hol_ctxt as {thy, ...}) x t =
2.257 +fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
2.258 case head_of t of
2.259 Const x' =>
2.260 if x = x' then @{const True}
2.261 - else if is_constr_like thy x' then @{const False}
2.262 + else if is_constr_like ctxt x' then @{const False}
2.263 else betapply (discr_term_for_constr hol_ctxt x, t)
2.264 | _ => betapply (discr_term_for_constr hol_ctxt x, t)
2.265
2.266 @@ -933,24 +946,26 @@
2.267 (List.take (arg_Ts, n)) 0
2.268 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
2.269 end
2.270 -fun select_nth_constr_arg thy stds x t n res_T =
2.271 - (case strip_comb t of
2.272 - (Const x', args) =>
2.273 - if x = x' then nth args n
2.274 - else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
2.275 - else raise SAME ()
2.276 - | _ => raise SAME())
2.277 - handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
2.278 +fun select_nth_constr_arg ctxt stds x t n res_T =
2.279 + let val thy = ProofContext.theory_of ctxt in
2.280 + (case strip_comb t of
2.281 + (Const x', args) =>
2.282 + if x = x' then nth args n
2.283 + else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
2.284 + else raise SAME ()
2.285 + | _ => raise SAME())
2.286 + handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
2.287 + end
2.288
2.289 fun construct_value _ _ x [] = Const x
2.290 - | construct_value thy stds (x as (s, _)) args =
2.291 + | construct_value ctxt stds (x as (s, _)) args =
2.292 let val args = map Envir.eta_contract args in
2.293 case hd args of
2.294 Const (s', _) $ t =>
2.295 if is_sel_like_and_no_discr s' andalso
2.296 constr_name_for_sel_like s' = s andalso
2.297 forall (fn (n, t') =>
2.298 - select_nth_constr_arg thy stds x t n dummyT = t')
2.299 + select_nth_constr_arg ctxt stds x t n dummyT = t')
2.300 (index_seq 0 (length args) ~~ args) then
2.301 t
2.302 else
2.303 @@ -958,9 +973,9 @@
2.304 | _ => list_comb (Const x, args)
2.305 end
2.306
2.307 -fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
2.308 +fun constr_expand (hol_ctxt as {ctxt, stds, ...}) T t =
2.309 (case head_of t of
2.310 - Const x => if is_constr_like thy x then t else raise SAME ()
2.311 + Const x => if is_constr_like ctxt x then t else raise SAME ()
2.312 | _ => raise SAME ())
2.313 handle SAME () =>
2.314 let
2.315 @@ -973,7 +988,7 @@
2.316 datatype_constrs hol_ctxt T |> hd
2.317 val arg_Ts = binder_types T'
2.318 in
2.319 - list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
2.320 + list_comb (Const x', map2 (select_nth_constr_arg ctxt stds x' t)
2.321 (index_seq 0 (length arg_Ts)) arg_Ts)
2.322 end
2.323
2.324 @@ -985,7 +1000,7 @@
2.325 | _ => t
2.326 fun coerce_bound_0_in_term hol_ctxt new_T old_T =
2.327 old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
2.328 -and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
2.329 +and coerce_term (hol_ctxt as {ctxt, stds, fast_descrs, ...}) Ts new_T old_T t =
2.330 if old_T = new_T then
2.331 t
2.332 else
2.333 @@ -999,7 +1014,7 @@
2.334 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
2.335 |> Envir.eta_contract
2.336 |> new_s <> @{type_name fun}
2.337 - ? construct_value thy stds
2.338 + ? construct_value ctxt stds
2.339 (if new_s = @{type_name fin_fun} then @{const_name FinFun}
2.340 else @{const_name FunBox},
2.341 Type (@{type_name fun}, new_Ts) --> new_T)
2.342 @@ -1014,12 +1029,12 @@
2.343 if new_s = @{type_name fun} then
2.344 coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
2.345 else
2.346 - construct_value thy stds
2.347 + construct_value ctxt stds
2.348 (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
2.349 [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
2.350 (Type (@{type_name fun}, old_Ts)) t1]
2.351 | Const _ $ t1 $ t2 =>
2.352 - construct_value thy stds
2.353 + construct_value ctxt stds
2.354 (if new_s = @{type_name "*"} then @{const_name Pair}
2.355 else @{const_name PairBox}, new_Ts ---> new_T)
2.356 (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
2.357 @@ -1145,13 +1160,15 @@
2.358 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
2.359 $ Const (@{const_name TYPE}, _)) = true
2.360 | is_arity_type_axiom _ = false
2.361 -fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
2.362 - is_typedef_axiom thy boring t2
2.363 - | is_typedef_axiom thy boring
2.364 +fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
2.365 + is_typedef_axiom ctxt boring t2
2.366 + | is_typedef_axiom ctxt boring
2.367 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
2.368 $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
2.369 $ Const _ $ _)) =
2.370 - boring <> is_funky_typedef_name thy s andalso is_typedef thy s
2.371 + let val thy = ProofContext.theory_of ctxt in
2.372 + boring <> is_funky_typedef_name thy s andalso is_typedef ctxt s
2.373 + end
2.374 | is_typedef_axiom _ _ _ = false
2.375 val is_class_axiom =
2.376 Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
2.377 @@ -1160,13 +1177,13 @@
2.378 typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
2.379 Typedef axioms are uninteresting to Nitpick, because it can retrieve them
2.380 using "typedef_info". *)
2.381 -fun partition_axioms_by_definitionality thy axioms def_names =
2.382 +fun partition_axioms_by_definitionality ctxt axioms def_names =
2.383 let
2.384 val axioms = sort (fast_string_ord o pairself fst) axioms
2.385 val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
2.386 val nondefs =
2.387 OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
2.388 - |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
2.389 + |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
2.390 in pairself (map snd) (defs, nondefs) end
2.391
2.392 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
2.393 @@ -1189,8 +1206,9 @@
2.394 | do_eq _ = false
2.395 in do_eq end
2.396
2.397 -fun all_axioms_of thy subst =
2.398 +fun all_axioms_of ctxt subst =
2.399 let
2.400 + val thy = ProofContext.theory_of ctxt
2.401 val axioms_of_thys =
2.402 maps Thm.axioms_of
2.403 #> map (apsnd (subst_atomic subst o prop_of))
2.404 @@ -1203,12 +1221,12 @@
2.405 val built_in_axioms = axioms_of_thys built_in_thys
2.406 val user_axioms = axioms_of_thys user_thys
2.407 val (built_in_defs, built_in_nondefs) =
2.408 - partition_axioms_by_definitionality thy built_in_axioms def_names
2.409 - ||> filter (is_typedef_axiom thy false)
2.410 + partition_axioms_by_definitionality ctxt built_in_axioms def_names
2.411 + ||> filter (is_typedef_axiom ctxt false)
2.412 val (user_defs, user_nondefs) =
2.413 - partition_axioms_by_definitionality thy user_axioms def_names
2.414 + partition_axioms_by_definitionality ctxt user_axioms def_names
2.415 val (built_in_nondefs, user_nondefs) =
2.416 - List.partition (is_typedef_axiom thy false) user_nondefs
2.417 + List.partition (is_typedef_axiom ctxt false) user_nondefs
2.418 |>> append built_in_nondefs
2.419 val defs =
2.420 (thy |> PureThy.all_thms_of
2.421 @@ -1369,16 +1387,16 @@
2.422 | _ => NONE
2.423 fun is_constr_pattern _ (Bound _) = true
2.424 | is_constr_pattern _ (Var _) = true
2.425 - | is_constr_pattern thy t =
2.426 + | is_constr_pattern ctxt t =
2.427 case strip_comb t of
2.428 (Const x, args) =>
2.429 - is_constr_like thy x andalso forall (is_constr_pattern thy) args
2.430 + is_constr_like ctxt x andalso forall (is_constr_pattern ctxt) args
2.431 | _ => false
2.432 -fun is_constr_pattern_lhs thy t =
2.433 - forall (is_constr_pattern thy) (snd (strip_comb t))
2.434 -fun is_constr_pattern_formula thy t =
2.435 +fun is_constr_pattern_lhs ctxt t =
2.436 + forall (is_constr_pattern ctxt) (snd (strip_comb t))
2.437 +fun is_constr_pattern_formula ctxt t =
2.438 case lhs_of_equation t of
2.439 - SOME t' => is_constr_pattern_lhs thy t'
2.440 + SOME t' => is_constr_pattern_lhs ctxt t'
2.441 | NONE => false
2.442
2.443 (* Similar to "specialize_type" but returns all matches rather than only the
2.444 @@ -1439,26 +1457,26 @@
2.445
2.446 (** Constant unfolding **)
2.447
2.448 -fun constr_case_body thy stds (j, (x as (_, T))) =
2.449 +fun constr_case_body ctxt stds (j, (x as (_, T))) =
2.450 let val arg_Ts = binder_types T in
2.451 - list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
2.452 + list_comb (Bound j, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
2.453 (index_seq 0 (length arg_Ts)) arg_Ts)
2.454 end
2.455 -fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
2.456 +fun add_constr_case (hol_ctxt as {ctxt, stds, ...}) res_T (j, x) res_t =
2.457 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
2.458 - $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
2.459 + $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body ctxt stds (j, x)
2.460 $ res_t
2.461 -fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
2.462 +fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T =
2.463 let
2.464 val xs = datatype_constrs hol_ctxt dataT
2.465 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
2.466 val (xs', x) = split_last xs
2.467 in
2.468 - constr_case_body thy stds (1, x)
2.469 + constr_case_body ctxt stds (1, x)
2.470 |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
2.471 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
2.472 end
2.473 -fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
2.474 +fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
2.475 let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
2.476 case no_of_record_field thy s rec_T of
2.477 ~1 => (case rec_T of
2.478 @@ -1467,14 +1485,15 @@
2.479 val rec_T' = List.last Ts
2.480 val j = num_record_fields thy rec_T - 1
2.481 in
2.482 - select_nth_constr_arg thy stds constr_x t j res_T
2.483 + select_nth_constr_arg ctxt stds constr_x t j res_T
2.484 |> optimized_record_get hol_ctxt s rec_T' res_T
2.485 end
2.486 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
2.487 []))
2.488 - | j => select_nth_constr_arg thy stds constr_x t j res_T
2.489 + | j => select_nth_constr_arg ctxt stds constr_x t j res_T
2.490 end
2.491 -fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
2.492 +fun optimized_record_update (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T fun_t
2.493 + rec_t =
2.494 let
2.495 val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
2.496 val Ts = binder_types constr_T
2.497 @@ -1482,7 +1501,7 @@
2.498 val special_j = no_of_record_field thy s rec_T
2.499 val ts =
2.500 map2 (fn j => fn T =>
2.501 - let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
2.502 + let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
2.503 if j = special_j then
2.504 betapply (fun_t, t)
2.505 else if j = n - 1 andalso special_j = ~1 then
2.506 @@ -1551,9 +1570,9 @@
2.507 | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
2.508 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
2.509 (Abs (Name.uu, body_type T,
2.510 - select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
2.511 + select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
2.512 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
2.513 - (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
2.514 + (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
2.515 and do_const depth Ts t (x as (s, T)) ts =
2.516 case AList.lookup (op =) ersatz_table s of
2.517 SOME s' =>
2.518 @@ -1573,9 +1592,9 @@
2.519 |> do_term (depth + 1) Ts, ts)
2.520 end
2.521 | _ =>
2.522 - if is_constr thy stds x then
2.523 + if is_constr ctxt stds x then
2.524 (Const x, ts)
2.525 - else if is_stale_constr thy x then
2.526 + else if is_stale_constr ctxt x then
2.527 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
2.528 \(\"" ^ s ^ "\")")
2.529 else if is_quot_abs_fun ctxt x then
2.530 @@ -1606,9 +1625,9 @@
2.531 (do_term depth Ts (hd ts))
2.532 (do_term depth Ts (nth ts 1)), [])
2.533 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
2.534 - else if is_rep_fun thy x then
2.535 - let val x' = mate_of_rep_fun thy x in
2.536 - if is_constr thy stds x' then
2.537 + else if is_rep_fun ctxt x then
2.538 + let val x' = mate_of_rep_fun ctxt x in
2.539 + if is_constr ctxt stds x' then
2.540 select_nth_constr_arg_with_args depth Ts x' ts 0
2.541 (range_type T)
2.542 else
2.543 @@ -1679,18 +1698,24 @@
2.544 Unsynchronized.change simp_table
2.545 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
2.546
2.547 -fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
2.548 - let val abs_T = domain_type T in
2.549 - typedef_info thy (fst (dest_Type abs_T)) |> the
2.550 +fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) =
2.551 + let
2.552 + val thy = ProofContext.theory_of ctxt
2.553 + val abs_T = domain_type T
2.554 + in
2.555 + typedef_info ctxt (fst (dest_Type abs_T)) |> the
2.556 |> pairf #Abs_inverse #Rep_inverse
2.557 |> pairself (specialize_type thy x o prop_of o the)
2.558 ||> single |> op ::
2.559 end
2.560 -fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
2.561 - let val abs_T = Type abs_z in
2.562 - if is_univ_typedef thy abs_T then
2.563 +fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
2.564 + let
2.565 + val thy = ProofContext.theory_of ctxt
2.566 + val abs_T = Type abs_z
2.567 + in
2.568 + if is_univ_typedef ctxt abs_T then
2.569 []
2.570 - else case typedef_info thy abs_s of
2.571 + else case typedef_info ctxt abs_s of
2.572 SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
2.573 let
2.574 val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
2.575 @@ -1718,7 +1743,7 @@
2.576 val x_var = Var (("x", 0), rep_T)
2.577 val y_var = Var (("y", 0), rep_T)
2.578 val x = (@{const_name Quot}, rep_T --> abs_T)
2.579 - val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
2.580 + val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
2.581 val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
2.582 val normal_x = normal_t $ x_var
2.583 val normal_y = normal_t $ y_var
2.584 @@ -1736,7 +1761,7 @@
2.585 HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
2.586 end
2.587
2.588 -fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
2.589 +fun codatatype_bisim_axioms (hol_ctxt as {ctxt, thy, stds, ...}) T =
2.590 let
2.591 val xs = datatype_constrs hol_ctxt T
2.592 val set_T = T --> bool_T
2.593 @@ -1753,8 +1778,8 @@
2.594 fun nth_sub_bisim x n nth_T =
2.595 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
2.596 else HOLogic.eq_const nth_T)
2.597 - $ select_nth_constr_arg thy stds x x_var n nth_T
2.598 - $ select_nth_constr_arg thy stds x y_var n nth_T
2.599 + $ select_nth_constr_arg ctxt stds x x_var n nth_T
2.600 + $ select_nth_constr_arg ctxt stds x y_var n nth_T
2.601 fun case_func (x as (_, T)) =
2.602 let
2.603 val arg_Ts = binder_types T
3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon May 31 18:51:06 2010 +0200
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 10:31:18 2010 +0200
3.3 @@ -319,7 +319,7 @@
3.4 end
3.5 in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
3.6 and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
3.7 - (scope as {hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns,
3.8 + (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
3.9 bits, datatypes, ofs, ...}) sel_names rel_table bounds =
3.10 let
3.11 val for_auto = (maybe_name = "")
3.12 @@ -536,7 +536,7 @@
3.13 | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
3.14 \term_for_atom (Abs_Frac)", ts)
3.15 else if not for_auto andalso
3.16 - (is_abs_fun thy constr_x orelse
3.17 + (is_abs_fun ctxt constr_x orelse
3.18 constr_s = @{const_name Quot}) then
3.19 Const (abs_name, constr_T) $ the_single ts
3.20 else
4.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon May 31 18:51:06 2010 +0200
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jun 01 10:31:18 2010 +0200
4.3 @@ -162,8 +162,8 @@
4.4 | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
4.5 fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
4.6 could_exist_alpha_subtype alpha_T T
4.7 - | could_exist_alpha_sub_mtype thy alpha_T T =
4.8 - (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
4.9 + | could_exist_alpha_sub_mtype ctxt alpha_T T =
4.10 + (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
4.11
4.12 fun exists_alpha_sub_mtype MAlpha = true
4.13 | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
4.14 @@ -243,7 +243,7 @@
4.15 else
4.16 S Minus
4.17 in (M1, a, M2) end
4.18 -and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
4.19 +and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
4.20 datatype_mcache, constr_mcache, ...})
4.21 all_minus =
4.22 let
4.23 @@ -255,7 +255,7 @@
4.24 MFun (fresh_mfun_for_fun_type mdata false T1 T2)
4.25 | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
4.26 | Type (z as (s, _)) =>
4.27 - if could_exist_alpha_sub_mtype thy alpha_T T then
4.28 + if could_exist_alpha_sub_mtype ctxt alpha_T T then
4.29 case AList.lookup (op =) (!datatype_mcache) z of
4.30 SOME M => M
4.31 | NONE =>
4.32 @@ -304,9 +304,9 @@
4.33 case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
4.34 end
4.35
4.36 -fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
4.37 +fun mtype_for_constr (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, constr_mcache,
4.38 ...}) (x as (_, T)) =
4.39 - if could_exist_alpha_sub_mtype thy alpha_T T then
4.40 + if could_exist_alpha_sub_mtype ctxt alpha_T T then
4.41 case AList.lookup (op =) (!constr_mcache) x of
4.42 SOME M => M
4.43 | NONE => if T = alpha_T then
4.44 @@ -741,7 +741,7 @@
4.45 do_robust_set_operation T accum
4.46 else if is_sel s then
4.47 (mtype_for_sel mdata x, accum)
4.48 - else if is_constr thy stds x then
4.49 + else if is_constr ctxt stds x then
4.50 (mtype_for_constr mdata x, accum)
4.51 else if is_built_in_const thy stds fast_descrs x then
4.52 (fresh_mtype_for_type mdata true T, accum)
4.53 @@ -924,8 +924,8 @@
4.54 if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
4.55 else consider_general_formula mdata Plus t
4.56
4.57 -fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
4.58 - if not (is_constr_pattern_formula thy t) then
4.59 +fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
4.60 + if not (is_constr_pattern_formula ctxt t) then
4.61 consider_nondefinitional_axiom mdata t
4.62 else if is_harmless_axiom mdata t then
4.63 pair (MRaw (t, dummy_M))
4.64 @@ -1027,7 +1027,8 @@
4.65 fun fin_fun_constr T1 T2 =
4.66 (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
4.67
4.68 -fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
4.69 +fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
4.70 + ...})
4.71 binarize finitizes alpha_T tsp =
4.72 case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
4.73 SOME (lits, msp, constr_mtypes) =>
4.74 @@ -1085,7 +1086,7 @@
4.75 Const (s, T')
4.76 else if is_built_in_const thy stds fast_descrs x then
4.77 coerce_term hol_ctxt Ts T' T t
4.78 - else if is_constr thy stds x then
4.79 + else if is_constr ctxt stds x then
4.80 Const (finitize_constr x)
4.81 else if is_sel s then
4.82 let
4.83 @@ -1112,7 +1113,7 @@
4.84 case T1 of
4.85 Type (s, [T11, T12]) =>
4.86 (if s = @{type_name fin_fun} then
4.87 - select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1
4.88 + select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
4.89 0 (T11 --> T12)
4.90 else
4.91 t1, T11)
4.92 @@ -1127,7 +1128,7 @@
4.93 in
4.94 Abs (s, T, t')
4.95 |> should_finitize (T --> T') a
4.96 - ? construct_value thy stds (fin_fun_constr T T') o single
4.97 + ? construct_value ctxt stds (fin_fun_constr T T') o single
4.98 end
4.99 in
4.100 Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon May 31 18:51:06 2010 +0200
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 01 10:31:18 2010 +0200
5.3 @@ -439,7 +439,7 @@
5.4 maps factorize [mk_fst z, mk_snd z]
5.5 | factorize z = [z]
5.6
5.7 -fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
5.8 +fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
5.9 let
5.10 fun aux eq ss Ts t =
5.11 let
5.12 @@ -565,7 +565,7 @@
5.13 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
5.14 | (Const (x as (s as @{const_name Suc}, T)), []) =>
5.15 if is_built_in_const thy stds false x then Cst (Suc, T, Any)
5.16 - else if is_constr thy stds x then do_construct x []
5.17 + else if is_constr ctxt stds x then do_construct x []
5.18 else ConstName (s, T, Any)
5.19 | (Const (@{const_name finite}, T), [t1]) =>
5.20 (if is_finite_type hol_ctxt (domain_type T) then
5.21 @@ -576,7 +576,7 @@
5.22 | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
5.23 | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
5.24 if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
5.25 - else if is_constr thy stds x then do_construct x []
5.26 + else if is_constr ctxt stds x then do_construct x []
5.27 else ConstName (s, T, Any)
5.28 | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
5.29 if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
5.30 @@ -653,7 +653,7 @@
5.31 [t1, t2]) =>
5.32 Op2 (Union, T1, Any, sub t1, sub t2)
5.33 | (t0 as Const (x as (s, T)), ts) =>
5.34 - if is_constr thy stds x then
5.35 + if is_constr ctxt stds x then
5.36 do_construct x ts
5.37 else if String.isPrefix numeral_prefix s then
5.38 Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
5.39 @@ -687,13 +687,13 @@
5.40 val R = best_non_opt_set_rep_for_type scope (type_of v)
5.41 val v = modify_name_rep v R
5.42 in (v :: vs, NameTable.update (v, R) table) end
5.43 -fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
5.44 +fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
5.45 (vs, table) =
5.46 let
5.47 val x as (s, T) = (nickname_of v, type_of v)
5.48 - val R = (if is_abs_fun thy x then
5.49 + val R = (if is_abs_fun ctxt x then
5.50 rep_for_abs_fun
5.51 - else if is_rep_fun thy x then
5.52 + else if is_rep_fun ctxt x then
5.53 Func oo best_non_opt_symmetric_reps_for_fun_type
5.54 else if all_exact orelse is_skolem_name v orelse
5.55 member (op =) [@{const_name undefined_fast_The},
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon May 31 18:51:06 2010 +0200
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jun 01 10:31:18 2010 +0200
6.3 @@ -65,14 +65,15 @@
6.4
6.5 (** Uncurrying **)
6.6
6.7 -fun add_to_uncurry_table thy t =
6.8 +fun add_to_uncurry_table ctxt t =
6.9 let
6.10 + val thy = ProofContext.theory_of ctxt
6.11 fun aux (t1 $ t2) args table =
6.12 let val table = aux t2 [] table in aux t1 (t2 :: args) table end
6.13 | aux (Abs (_, _, t')) _ table = aux t' [] table
6.14 | aux (t as Const (x as (s, _))) args table =
6.15 if is_built_in_const thy [(NONE, true)] true x orelse
6.16 - is_constr_like thy x orelse
6.17 + is_constr_like ctxt x orelse
6.18 is_sel s orelse s = @{const_name Sigma} then
6.19 table
6.20 else
6.21 @@ -121,8 +122,8 @@
6.22
6.23 (** Boxing **)
6.24
6.25 -fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
6.26 - orig_t =
6.27 +fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...})
6.28 + def orig_t =
6.29 let
6.30 fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
6.31 Type (@{type_name fun}, map box_relational_operator_type Ts)
6.32 @@ -228,10 +229,9 @@
6.33 else if is_built_in_const thy stds fast_descrs x orelse
6.34 s = @{const_name Sigma} then
6.35 T
6.36 - else if is_constr_like thy x then
6.37 + else if is_constr_like ctxt x then
6.38 box_type hol_ctxt InConstr T
6.39 - else if is_sel s
6.40 - orelse is_rep_fun thy x then
6.41 + else if is_sel s orelse is_rep_fun ctxt x then
6.42 box_type hol_ctxt InSel T
6.43 else
6.44 box_type hol_ctxt InExpr T)
6.45 @@ -248,7 +248,7 @@
6.46 betapply (if s1 = @{type_name fun} then
6.47 t1
6.48 else
6.49 - select_nth_constr_arg thy stds
6.50 + select_nth_constr_arg ctxt stds
6.51 (@{const_name FunBox},
6.52 Type (@{type_name fun}, Ts1) --> T1) t1 0
6.53 (Type (@{type_name fun}, Ts1)), t2)
6.54 @@ -265,7 +265,7 @@
6.55 betapply (if s1 = @{type_name fun} then
6.56 t1
6.57 else
6.58 - select_nth_constr_arg thy stds
6.59 + select_nth_constr_arg ctxt stds
6.60 (@{const_name FunBox},
6.61 Type (@{type_name fun}, Ts1) --> T1) t1 0
6.62 (Type (@{type_name fun}, Ts1)), t2)
6.63 @@ -293,12 +293,12 @@
6.64 | aux _ = true
6.65 in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
6.66
6.67 -fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
6.68 +fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t
6.69 args seen =
6.70 let val t_comb = list_comb (t, args) in
6.71 case t of
6.72 Const x =>
6.73 - if not relax andalso is_constr thy stds x andalso
6.74 + if not relax andalso is_constr ctxt stds x andalso
6.75 not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
6.76 has_heavy_bounds_or_vars Ts t_comb andalso
6.77 not (loose_bvar (t_comb, level)) then
6.78 @@ -397,7 +397,7 @@
6.79 $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
6.80 end
6.81
6.82 -fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
6.83 +fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =
6.84 let
6.85 val num_occs_of_var =
6.86 fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
6.87 @@ -432,7 +432,7 @@
6.88 val n = length arg_Ts
6.89 in
6.90 if length args = n andalso
6.91 - (is_constr thy stds x orelse s = @{const_name Pair} orelse
6.92 + (is_constr ctxt stds x orelse s = @{const_name Pair} orelse
6.93 x = (@{const_name Suc}, nat_T --> nat_T)) andalso
6.94 (not careful orelse not (is_Var t1) orelse
6.95 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
6.96 @@ -449,7 +449,7 @@
6.97 else t0 $ aux false t2 $ aux false t1
6.98 and sel_eq x t n nth_T nth_t =
6.99 HOLogic.eq_const nth_T $ nth_t
6.100 - $ select_nth_constr_arg thy stds x t n nth_T
6.101 + $ select_nth_constr_arg ctxt stds x t n nth_T
6.102 |> aux false
6.103 in aux axiom t end
6.104
6.105 @@ -484,7 +484,7 @@
6.106 aux (t1 :: prems) (Term.add_vars t1 zs) t2
6.107 in aux [] [] end
6.108
6.109 -fun find_bound_assign thy stds j =
6.110 +fun find_bound_assign ctxt stds j =
6.111 let
6.112 fun do_term _ [] = NONE
6.113 | do_term seen (t :: ts) =
6.114 @@ -497,8 +497,9 @@
6.115 | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
6.116 if j' = j andalso
6.117 s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
6.118 - SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
6.119 - [t2], ts @ seen)
6.120 + SOME (construct_value ctxt stds
6.121 + (@{const_name FunBox}, T2 --> T1) [t2],
6.122 + ts @ seen)
6.123 else
6.124 raise SAME ()
6.125 | _ => raise SAME ())
6.126 @@ -523,11 +524,11 @@
6.127 | aux _ = raise SAME ()
6.128 in aux (t, j) handle SAME () => t end
6.129
6.130 -fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
6.131 +fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) =
6.132 let
6.133 fun kill [] [] ts = foldr1 s_conj ts
6.134 | kill (s :: ss) (T :: Ts) ts =
6.135 - (case find_bound_assign thy stds (length ss) [] ts of
6.136 + (case find_bound_assign ctxt stds (length ss) [] ts of
6.137 SOME (_, []) => @{const True}
6.138 | SOME (arg_t, ts) =>
6.139 kill ss Ts (map (subst_one_bound (length ss)
6.140 @@ -893,7 +894,7 @@
6.141 (if head_of t <> @{const "==>"} then add_def_axiom
6.142 else add_nondef_axiom) depth t
6.143 and add_eq_axiom depth t =
6.144 - (if is_constr_pattern_formula thy t then add_def_axiom
6.145 + (if is_constr_pattern_formula ctxt t then add_def_axiom
6.146 else add_nondef_axiom) depth t
6.147 and add_axioms_for_term depth t (accum as (xs, axs)) =
6.148 case t of
6.149 @@ -921,7 +922,7 @@
6.150 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
6.151 accum
6.152 end
6.153 - else if is_constr thy stds x then
6.154 + else if is_constr ctxt stds x then
6.155 accum
6.156 else if is_equational_fun hol_ctxt x then
6.157 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
6.158 @@ -929,7 +930,7 @@
6.159 else if is_choice_spec_fun hol_ctxt x then
6.160 fold (add_nondef_axiom depth)
6.161 (nondef_props_for_const thy true choice_spec_table x) accum
6.162 - else if is_abs_fun thy x then
6.163 + else if is_abs_fun ctxt x then
6.164 if is_quot_type thy (range_type T) then
6.165 raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
6.166 else
6.167 @@ -940,7 +941,7 @@
6.168 ? fold (add_maybe_def_axiom depth)
6.169 (nondef_props_for_const thy true
6.170 (extra_table def_table s) x)
6.171 - else if is_rep_fun thy x then
6.172 + else if is_rep_fun ctxt x then
6.173 if is_quot_type thy (domain_type T) then
6.174 raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
6.175 else
6.176 @@ -952,9 +953,9 @@
6.177 (nondef_props_for_const thy true
6.178 (extra_table def_table s) x)
6.179 |> add_axioms_for_term depth
6.180 - (Const (mate_of_rep_fun thy x))
6.181 + (Const (mate_of_rep_fun ctxt x))
6.182 |> fold (add_def_axiom depth)
6.183 - (inverse_axioms_for_rep_fun thy x)
6.184 + (inverse_axioms_for_rep_fun ctxt x)
6.185 else if s = @{const_name TYPE} then
6.186 accum
6.187 else
6.188 @@ -979,8 +980,8 @@
6.189 | TVar (_, S) => add_axioms_for_sort depth T S
6.190 | Type (z as (_, Ts)) =>
6.191 fold (add_axioms_for_type depth) Ts
6.192 - #> (if is_pure_typedef thy T then
6.193 - fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
6.194 + #> (if is_pure_typedef ctxt T then
6.195 + fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)
6.196 else if is_quot_type thy T then
6.197 fold (add_def_axiom depth)
6.198 (optimized_quot_type_axioms ctxt stds z)
6.199 @@ -1020,7 +1021,7 @@
6.200
6.201 (** Simplification of constructor/selector terms **)
6.202
6.203 -fun simplify_constrs_and_sels thy t =
6.204 +fun simplify_constrs_and_sels ctxt t =
6.205 let
6.206 fun is_nth_sel_on t' n (Const (s, _) $ t) =
6.207 (t = t' andalso is_sel_like_and_no_discr s andalso
6.208 @@ -1032,7 +1033,7 @@
6.209 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
6.210 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
6.211 | do_term (t as Const (x as (s, T))) (args as _ :: _) =
6.212 - ((if is_constr_like thy x then
6.213 + ((if is_constr_like ctxt x then
6.214 if length args = num_binder_types T then
6.215 case hd args of
6.216 Const (_, T') $ t' =>
6.217 @@ -1048,7 +1049,7 @@
6.218 else if is_sel_like_and_no_discr s then
6.219 case strip_comb (hd args) of
6.220 (Const (x' as (s', T')), ts') =>
6.221 - if is_constr_like thy x' andalso
6.222 + if is_constr_like ctxt x' andalso
6.223 constr_name_for_sel_like s = s' andalso
6.224 not (exists is_pair_type (binder_types T')) then
6.225 list_comb (nth ts' (sel_no_from_name s), tl args)
6.226 @@ -1230,7 +1231,7 @@
6.227
6.228 val max_skolem_depth = 4
6.229
6.230 -fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
6.231 +fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
6.232 boxes, ...}) finitizes monos t =
6.233 let
6.234 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
6.235 @@ -1250,7 +1251,7 @@
6.236 val box = exists (not_equal (SOME false) o snd) boxes
6.237 val table =
6.238 Termtab.empty
6.239 - |> box ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
6.240 + |> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)
6.241 fun do_rest def =
6.242 binarize ? binarize_nat_and_int_in_term
6.243 #> box ? uncurry_term table
6.244 @@ -1261,7 +1262,7 @@
6.245 #> curry_assms
6.246 #> destroy_universal_equalities
6.247 #> destroy_existential_equalities hol_ctxt
6.248 - #> simplify_constrs_and_sels thy
6.249 + #> simplify_constrs_and_sels ctxt
6.250 #> distribute_quantifiers
6.251 #> push_quantifiers_inward
6.252 #> close_form
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon May 31 18:51:06 2010 +0200
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Jun 01 10:31:18 2010 +0200
7.3 @@ -135,7 +135,7 @@
7.4 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
7.5
7.6 fun quintuple_for_scope quote
7.7 - ({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
7.8 + ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
7.9 datatypes, ...} : scope) =
7.10 let
7.11 val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
7.12 @@ -144,8 +144,8 @@
7.13 card_assigns |> filter_out (member (op =) boring_Ts o fst)
7.14 |> List.partition (is_fp_iterator_type o fst)
7.15 val (secondary_card_assigns, primary_card_assigns) =
7.16 - card_assigns |> List.partition ((is_integer_type orf is_datatype thy stds)
7.17 - o fst)
7.18 + card_assigns
7.19 + |> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst)
7.20 val cards =
7.21 map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
7.22 string_of_int k)
7.23 @@ -458,13 +458,13 @@
7.24 concrete = concrete, deep = deep, constrs = constrs}
7.25 end
7.26
7.27 -fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize deep_dataTs
7.28 +fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
7.29 finitizable_dataTs (desc as (card_assigns, _)) =
7.30 let
7.31 val datatypes =
7.32 map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
7.33 finitizable_dataTs desc)
7.34 - (filter (is_datatype thy stds o fst) card_assigns)
7.35 + (filter (is_datatype ctxt stds o fst) card_assigns)
7.36 val bits = card_of_type card_assigns @{typ signed_bit} - 1
7.37 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
7.38 card_of_type card_assigns @{typ unsigned_bit}