# HG changeset patch # User blanchet # Date 1281107129 -7200 # Node ID a44d108a8d3932c050844e8138f35222138c00c5 # Parent 17d9808ed626b7c1640bd2148dc7f4b818e32f34 local versions of Nitpick.register_xxx functions diff -r 17d9808ed626 -r a44d108a8d39 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 06 11:37:33 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 06 17:05:29 2010 +0200 @@ -127,6 +127,16 @@ batch_size: int, expect: string} +(* TODO: eliminate these historical aliases *) +val register_frac_type = Nitpick_HOL.register_frac_type_global +val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global +val register_codatatype = Nitpick_HOL.register_codatatype_global +val unregister_codatatype = Nitpick_HOL.unregister_codatatype_global +val register_term_postprocessor = + Nitpick_Model.register_term_postprocessor_global +val unregister_term_postprocessor = + Nitpick_Model.unregister_term_postprocessor_global + type problem_extension = {free_names: nut list, sel_names: nut list, @@ -251,7 +261,7 @@ val original_max_potential = max_potential val original_max_genuine = max_genuine val max_bisim_depth = fold Integer.max bisim_depths ~1 - val case_names = case_const_names thy stds + val case_names = case_const_names ctxt stds 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) @@ -262,7 +272,7 @@ user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table) val intro_table = inductive_intro_table ctxt subst def_table val ground_thm_table = ground_theorem_table thy - val ersatz_table = ersatz_table thy + val ersatz_table = ersatz_table ctxt val (hol_ctxt as {wf_cache, ...}) = {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, @@ -337,9 +347,9 @@ ". " ^ extra)) end fun is_type_fundamentally_monotonic T = - (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso + (is_datatype ctxt stds T andalso not (is_quot_type ctxt 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 + is_number_type ctxt T orelse is_bit_type T fun is_type_actually_monotonic T = formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts) fun is_type_kind_of_monotonic T = diff -r 17d9808ed626 -r a44d108a8d39 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:37:33 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 17:05:29 2010 +0200 @@ -102,7 +102,7 @@ val is_word_type : typ -> bool val is_integer_like_type : typ -> bool val is_record_type : typ -> bool - val is_number_type : theory -> typ -> bool + val is_number_type : Proof.context -> typ -> bool val const_for_iterator_type : typ -> styp val strip_n_binders : int -> typ -> typ list * typ val nth_range_type : int -> typ -> typ @@ -113,8 +113,8 @@ val dest_n_tuple : int -> term -> term list val is_real_datatype : theory -> string -> bool val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool - val is_codatatype : theory -> typ -> bool - val is_quot_type : theory -> typ -> bool + val is_codatatype : Proof.context -> typ -> bool + val is_quot_type : Proof.context -> 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 @@ -143,10 +143,18 @@ val close_form : term -> term val eta_expand : typ list -> term -> int -> term val distinctness_formula : typ -> term list -> term - val register_frac_type : string -> (string * string) list -> theory -> theory - val unregister_frac_type : string -> theory -> theory - val register_codatatype : typ -> string -> styp list -> theory -> theory - val unregister_codatatype : typ -> theory -> theory + val register_frac_type : + string -> (string * string) list -> Proof.context -> Proof.context + val register_frac_type_global : + string -> (string * string) list -> theory -> theory + val unregister_frac_type : string -> Proof.context -> Proof.context + val unregister_frac_type_global : string -> theory -> theory + val register_codatatype : + typ -> string -> styp list -> Proof.context -> Proof.context + val register_codatatype_global : + typ -> string -> styp list -> theory -> theory + val unregister_codatatype : typ -> Proof.context -> Proof.context + val unregister_codatatype_global : typ -> theory -> theory val datatype_constrs : hol_context -> typ -> styp list val binarized_and_boxed_datatype_constrs : hol_context -> bool -> typ -> styp list @@ -167,7 +175,7 @@ val is_finite_type : hol_context -> typ -> bool val is_small_finite_type : hol_context -> typ -> bool val special_bounds : term list -> (indexname * typ) list - val is_funky_typedef : theory -> typ -> bool + val is_funky_typedef : Proof.context -> typ -> bool val all_axioms_of : Proof.context -> (term * term) list -> term list * term list * term list val arity_of_built_in_const : @@ -176,7 +184,7 @@ theory -> (typ option * bool) list -> bool -> styp -> bool val term_under_def : term -> term val case_const_names : - theory -> (typ option * bool) list -> (string * int) list + Proof.context -> (typ option * bool) list -> (string * int) list val unfold_defs_in_term : hol_context -> term -> term val const_def_table : Proof.context -> (term * term) list -> term list -> const_table @@ -188,7 +196,7 @@ val inductive_intro_table : Proof.context -> (term * term) list -> const_table -> const_table val ground_theorem_table : theory -> term list Inttab.table - val ersatz_table : theory -> (string * string) list + val ersatz_table : Proof.context -> (string * string) list val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list val optimized_typedef_axioms : Proof.context -> string * typ list -> term list @@ -267,7 +275,7 @@ datatype boxability = InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 -structure Data = Theory_Data( +structure Data = Generic_Data( type T = {frac_types: (string * (string * string) list) list, codatatypes: (string * (string * styp list)) list} val empty = {frac_types = [], codatatypes = []} @@ -531,10 +539,11 @@ | is_word_type _ = false val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type val is_record_type = not o null o Record.dest_recTs -fun is_frac_type thy (Type (s, [])) = - not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s))) +fun is_frac_type ctxt (Type (s, [])) = + s |> AList.lookup (op =) (#frac_types (Data.get (Context.Proof ctxt))) + |> these |> null |> not | is_frac_type _ _ = false -fun is_number_type thy = is_integer_like_type orf is_frac_type thy +fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt fun iterator_type_for_const gfp (s, T) = Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s, @@ -575,24 +584,22 @@ Abs_inverse: thm option, Rep_inverse: thm option} 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 \ Frac"} - |> Logic.varify_global, - set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} - else case Typedef.get_info ctxt s of - (* When several entries are returned, it shouldn't matter much which one - we take (according to Florian Haftmann). *) - ({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 + if is_frac_type ctxt (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 \ Frac"} + |> Logic.varify_global, + set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} + else case Typedef.get_info ctxt s of + (* When several entries are returned, it shouldn't matter much which one + we take (according to Florian Haftmann). *) + ({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 val is_typedef = is_some oo typedef_info val is_real_datatype = is_some oo Datatype.get_info @@ -605,28 +612,39 @@ "Code_Numeral.code_numeral"] s orelse (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T) +(* TODO: use "Term_Subst.instantiateT" instead? *) fun instantiate_type thy T1 T1' T2 = Same.commit (Envir.subst_type_same (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 handle Type.TYPE_MATCH => raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) -fun varify_and_instantiate_type thy T1 T1' T2 = - instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2) +fun varify_and_instantiate_type ctxt T1 T1' T2 = + let val thy = ProofContext.theory_of ctxt in + instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) + end -fun repair_constr_type thy body_T' T = - varify_and_instantiate_type thy (body_type T) body_T' T +fun repair_constr_type ctxt body_T' T = + varify_and_instantiate_type ctxt (body_type T) body_T' T -fun register_frac_type frac_s ersaetze thy = +fun register_frac_type_generic frac_s ersaetze generic = let - val {frac_types, codatatypes} = Data.get thy + val {frac_types, codatatypes} = Data.get generic val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types - in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end -fun unregister_frac_type frac_s = register_frac_type frac_s [] + in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end +val register_frac_type = Context.proof_map oo register_frac_type_generic +val register_frac_type_global = Context.theory_map oo register_frac_type_generic -fun register_codatatype co_T case_name constr_xs thy = +fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s [] +val unregister_frac_type = Context.proof_map o unregister_frac_type_generic +val unregister_frac_type_global = + Context.theory_map o unregister_frac_type_generic + +fun register_codatatype_generic co_T case_name constr_xs generic = let - val {frac_types, codatatypes} = Data.get thy - val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs + val ctxt = Context.proof_of generic + val thy = Context.theory_of generic + val {frac_types, codatatypes} = Data.get generic + val constr_xs = map (apsnd (repair_constr_type ctxt co_T)) constr_xs val (co_s, co_Ts) = dest_Type co_T val _ = if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso @@ -637,23 +655,32 @@ raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) codatatypes - in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end -fun unregister_codatatype co_T = register_codatatype co_T "" [] + in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end +val register_codatatype = Context.proof_map ooo register_codatatype_generic +val register_codatatype_global = + Context.theory_map ooo register_codatatype_generic -fun is_codatatype thy (Type (s, _)) = - not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s - |> Option.map snd |> these)) +fun unregister_codatatype_generic co_T = register_codatatype_generic co_T "" [] +val unregister_codatatype = Context.proof_map o unregister_codatatype_generic +val unregister_codatatype_global = + Context.theory_map o unregister_codatatype_generic + +fun is_codatatype ctxt (Type (s, _)) = + s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) + |> Option.map snd |> these |> null |> not | is_codatatype _ _ = false fun is_real_quot_type thy (Type (s, _)) = is_some (Quotient_Info.quotdata_lookup_raw thy s) | is_real_quot_type _ _ = false -fun is_quot_type thy T = - is_real_quot_type thy T andalso not (is_codatatype thy T) +fun is_quot_type ctxt T = + let val thy = ProofContext.theory_of ctxt in + is_real_quot_type thy T andalso not (is_codatatype ctxt T) + end 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_real_quot_type thy T orelse - is_codatatype thy T orelse is_record_type T orelse + is_codatatype ctxt T orelse is_record_type T orelse is_integer_like_type T) end | is_pure_typedef _ _ = false @@ -682,8 +709,9 @@ | is_univ_typedef _ _ = false 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_real_quot_type thy T) andalso not (is_basic_datatype thy stds s) + (is_typedef ctxt s orelse is_codatatype ctxt T orelse + T = @{typ ind} orelse is_real_quot_type thy T) andalso + not (is_basic_datatype thy stds s) end | is_datatype _ _ _ = false @@ -722,17 +750,13 @@ | is_rep_fun _ _ = false fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun}, [_, abs_T as Type (s', _)]))) = - let val thy = ProofContext.theory_of ctxt in - (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' - = SOME (Const x)) andalso not (is_codatatype thy abs_T) - end + try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' + = SOME (Const x) andalso not (is_codatatype ctxt abs_T) | is_quot_abs_fun _ _ = false fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun}, [abs_T as Type (s', _), _]))) = - let val thy = ProofContext.theory_of ctxt in - (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' - = SOME (Const x)) andalso not (is_codatatype thy abs_T) - end + try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' + = SOME (Const x) andalso not (is_codatatype ctxt abs_T) | is_quot_rep_fun _ _ = false fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun}, @@ -753,16 +777,14 @@ | equiv_relation_for_quot_type _ T = raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) -fun is_coconstr thy (s, T) = - let - val {codatatypes, ...} = Data.get thy - val co_T = body_type T - val co_s = dest_Type co_T |> fst - in - exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T) - (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these) - end - handle TYPE ("dest_Type", _, _) => false +fun is_coconstr ctxt (s, T) = + case body_type T of + co_T as Type (co_s, _) => + let val {codatatypes, ...} = Data.get (Context.Proof ctxt) in + exists (fn (s', T') => s = s' andalso repair_constr_type ctxt co_T T' = T) + (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these) + end + | _ => false fun is_constr_like ctxt (s, T) = member (op =) [@{const_name FinFun}, @{const_name FunBox}, @{const_name PairBox}, @{const_name Quot}, @@ -773,13 +795,11 @@ in is_real_constr thy x orelse is_record_constr x orelse (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse - is_coconstr thy x + is_coconstr ctxt x end 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 + is_codatatype ctxt (body_type T) andalso is_constr_like ctxt x andalso + not (is_coconstr ctxt x) fun is_constr ctxt stds (x as (_, T)) = let val thy = ProofContext.theory_of ctxt in is_constr_like ctxt x andalso @@ -899,8 +919,9 @@ 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' + (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) + s of + SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type ctxt T)) xs' | _ => if is_datatype ctxt stds T then case Datatype.get_info thy s of @@ -924,7 +945,7 @@ 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)] + varify_and_instantiate_type ctxt abs_type T rep_type --> T)] | NONE => if T = @{typ ind} then [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}] @@ -1197,11 +1218,11 @@ fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst) (* FIXME: detect "rep_datatype"? *) -fun is_funky_typedef_name thy s = +fun is_funky_typedef_name ctxt s = member (op =) [@{type_name unit}, @{type_name prod}, @{type_name Sum_Type.sum}, @{type_name int}] s orelse - is_frac_type thy (Type (s, [])) -fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s + is_frac_type ctxt (Type (s, [])) +fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s | is_funky_typedef _ _ = false fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _) $ Const (@{const_name TYPE}, _)) = true @@ -1212,9 +1233,7 @@ (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _) $ Const (_, Type (@{type_name fun}, [Type (s, _), _])) $ Const _ $ _)) = - let val thy = ProofContext.theory_of ctxt in - boring <> is_funky_typedef_name thy s andalso is_typedef ctxt s - end + boring <> is_funky_typedef_name ctxt s andalso is_typedef ctxt s | is_typedef_axiom _ _ _ = false val is_class_axiom = Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class) @@ -1391,15 +1410,17 @@ | NONE => t) | t => t) -fun case_const_names thy stds = - Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => - if is_basic_datatype thy stds dtype_s then - I - else - cons (case_name, AList.lookup (op =) descr index - |> the |> #3 |> length)) - (Datatype.get_all thy) [] @ - map (apsnd length o snd) (#codatatypes (Data.get thy)) +fun case_const_names ctxt stds = + let val thy = ProofContext.theory_of ctxt in + Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => + if is_basic_datatype thy stds dtype_s then + I + else + cons (case_name, AList.lookup (op =) descr index + |> the |> #3 |> length)) + (Datatype.get_all thy) [] @ + map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) + end fun fixpoint_kind_of_const thy table x = if is_built_in_const thy [(NONE, false)] false x then @@ -1596,7 +1617,7 @@ case t of (t0 as Const (@{const_name Int.number_class.number_of}, Type (@{type_name fun}, [_, ran_T]))) $ t1 => - ((if is_number_type thy ran_T then + ((if is_number_type ctxt ran_T then let val j = t1 |> HOLogic.dest_numeral |> ran_T = nat_T ? Integer.max 0 @@ -1712,7 +1733,7 @@ (do_term depth Ts (nth ts 1)), []) | n => (do_term depth Ts (eta_expand Ts t (2 - n)), []) else if is_abs_fun ctxt x andalso - is_quot_type thy (range_type T) then + is_quot_type ctxt (range_type T) then let val abs_T = range_type T val rep_T = domain_type (domain_type T) @@ -1732,7 +1753,7 @@ if is_constr ctxt stds x' then select_nth_constr_arg_with_args depth Ts x' ts 0 (range_type T) - else if is_quot_type thy (domain_type T) then + else if is_quot_type ctxt (domain_type T) then let val abs_T = domain_type T val rep_T = domain_type (range_type T) @@ -1852,8 +1873,9 @@ (@{const_name wf_wfrec}, @{const_name wf_wfrec'}), (@{const_name wfrec}, @{const_name wfrec'})] -fun ersatz_table thy = - fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table +fun ersatz_table ctxt = + basic_ersatz_table + |> fold (append o snd) (#frac_types (Data.get (Context.Proof ctxt))) fun add_simps simp_table s eqs = Unsynchronized.change simp_table @@ -1879,7 +1901,7 @@ 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 + val rep_T = varify_and_instantiate_type ctxt abs_type abs_T rep_type val rep_t = Const (Rep_name, abs_T --> rep_T) val set_t = Const (set_name, rep_T --> bool_T) val set_t' = @@ -1923,7 +1945,7 @@ HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))] end -fun codatatype_bisim_axioms (hol_ctxt as {ctxt, thy, stds, ...}) T = +fun codatatype_bisim_axioms (hol_ctxt as {thy, ctxt, stds, ...}) T = let val xs = datatype_constrs hol_ctxt T val set_T = T --> bool_T @@ -1939,7 +1961,7 @@ fun bisim_const T = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T) fun nth_sub_bisim x n nth_T = - (if is_codatatype thy nth_T then bisim_const nth_T $ n_var_minus_1 + (if is_codatatype ctxt nth_T then bisim_const nth_T $ n_var_minus_1 else HOLogic.eq_const 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 @@ -2242,7 +2264,7 @@ else raw_inductive_pred_axiom hol_ctxt x -fun equational_fun_axioms (hol_ctxt as {ctxt, thy, stds, fast_descrs, def_table, +fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, fast_descrs, def_table, simp_table, psimp_table, ...}) x = case def_props_for_const thy stds fast_descrs (!simp_table) x of [] => (case def_props_for_const thy stds fast_descrs psimp_table x of diff -r 17d9808ed626 -r a44d108a8d39 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Aug 06 11:37:33 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Aug 06 17:05:29 2010 +0200 @@ -25,8 +25,11 @@ val unknown : string val unrep : unit -> string val register_term_postprocessor : + typ -> term_postprocessor -> Proof.context -> Proof.context + val register_term_postprocessor_global : typ -> term_postprocessor -> theory -> theory - val unregister_term_postprocessor : typ -> theory -> theory + val unregister_term_postprocessor : typ -> Proof.context -> Proof.context + val unregister_term_postprocessor_global : typ -> theory -> theory val tuple_list_for_name : nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list val dest_plain_fun : term -> bool * (term list * term list) @@ -59,7 +62,7 @@ type term_postprocessor = Proof.context -> string -> (typ -> term list) -> typ -> term -> term -structure Data = Theory_Data( +structure Data = Generic_Data( type T = (typ * term_postprocessor) list val empty = [] val extend = I @@ -155,8 +158,17 @@ | ord => ord) | _ => Term_Ord.fast_term_ord tp -fun register_term_postprocessor T p = Data.map (cons (T, p)) -fun unregister_term_postprocessor T = Data.map (AList.delete (op =) T) +fun register_term_postprocessor_generic T p = Data.map (cons (T, p)) +val register_term_postprocessor = + Context.proof_map oo register_term_postprocessor_generic +val register_term_postprocessor_global = + Context.theory_map oo register_term_postprocessor_generic + +fun unregister_term_postprocessor_generic T = Data.map (AList.delete (op =) T) +val unregister_term_postprocessor = + Context.proof_map o unregister_term_postprocessor_generic +val unregister_term_postprocessor_global = + Context.theory_map o unregister_term_postprocessor_generic fun tuple_list_for_name rel_table bounds name = the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] @@ -309,8 +321,10 @@ | mk_tuple _ (t :: _) = t | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) -fun varified_type_match thy (candid_T, pat_T) = - strict_type_match thy (candid_T, Logic.varifyT_global pat_T) +fun varified_type_match ctxt (candid_T, pat_T) = + let val thy = ProofContext.theory_of ctxt in + strict_type_match thy (candid_T, varify_type ctxt pat_T) + end fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope) atomss sel_names rel_table bounds card T = @@ -351,11 +365,12 @@ bounds 0 fun postprocess_term (Type (@{type_name fun}, _)) = I | postprocess_term T = - if null (Data.get thy) then - I - else case AList.lookup (varified_type_match thy) (Data.get thy) T of - SOME postproc => postproc ctxt maybe_name all_values T - | NONE => I + case Data.get (Context.Proof ctxt) of + [] => I + | postprocs => + case AList.lookup (varified_type_match ctxt) postprocs T of + SOME postproc => postproc ctxt maybe_name all_values T + | NONE => I fun postprocess_subterms Ts (t1 $ t2) = let val t = postprocess_subterms Ts t1 $ postprocess_subterms Ts t2 in postprocess_term (fastype_of1 (Ts, t)) t diff -r 17d9808ed626 -r a44d108a8d39 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:37:33 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 17:05:29 2010 +0200 @@ -962,7 +962,7 @@ else if is_abs_fun ctxt x then accum |> fold (add_nondef_axiom depth) (nondef_props_for_const thy false nondef_table x) - |> (is_funky_typedef thy (range_type T) orelse + |> (is_funky_typedef ctxt (range_type T) orelse range_type T = nat_T) ? fold (add_maybe_def_axiom depth) (nondef_props_for_const thy true @@ -970,7 +970,7 @@ else if is_rep_fun ctxt x then accum |> fold (add_nondef_axiom depth) (nondef_props_for_const thy false nondef_table x) - |> (is_funky_typedef thy (range_type T) orelse + |> (is_funky_typedef ctxt (range_type T) orelse range_type T = nat_T) ? fold (add_maybe_def_axiom depth) (nondef_props_for_const thy true @@ -1014,10 +1014,10 @@ fold (add_axioms_for_type depth) Ts #> (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 + else if is_quot_type ctxt T then fold (add_def_axiom depth) (optimized_quot_type_axioms ctxt stds z) - else if max_bisim_depth >= 0 andalso is_codatatype thy T then + else if max_bisim_depth >= 0 andalso is_codatatype ctxt T then fold (add_maybe_def_axiom depth) (codatatype_bisim_axioms hol_ctxt T) else diff -r 17d9808ed626 -r a44d108a8d39 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Aug 06 11:37:33 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Aug 06 17:05:29 2010 +0200 @@ -244,25 +244,27 @@ fun block_for_type (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns iters_assigns bitss bisim_depths T = - if T = @{typ unsigned_bit} then + case T of + @{typ unsigned_bit} => [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)] - else if T = @{typ signed_bit} then + | @{typ signed_bit} => [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)] - else if T = @{typ "unsigned_bit word"} then + | @{typ "unsigned_bit word"} => [(Card T, lookup_type_ints_assign thy cards_assigns nat_T)] - else if T = @{typ "signed_bit word"} then + | @{typ "signed_bit word"} => [(Card T, lookup_type_ints_assign thy cards_assigns int_T)] - else if T = @{typ bisim_iterator} then + | @{typ bisim_iterator} => [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)] - else if is_fp_iterator_type T then - [(Card T, map (Integer.add 1 o Integer.max 0) - (lookup_const_ints_assign thy iters_assigns - (const_for_iterator_type T)))] - else - (Card T, lookup_type_ints_assign thy cards_assigns T) :: - (case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of - [_] => [] - | constrs => map_filter (row_for_constr thy maxes_assigns) constrs) + | _ => + if is_fp_iterator_type T then + [(Card T, map (Integer.add 1 o Integer.max 0) + (lookup_const_ints_assign thy iters_assigns + (const_for_iterator_type T)))] + else + (Card T, lookup_type_ints_assign thy cards_assigns T) :: + (case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of + [_] => [] + | constrs => map_filter (row_for_constr thy maxes_assigns) constrs) fun blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts = @@ -331,10 +333,10 @@ handle SAME () => aux seen ((T, k - 1) :: rest) in aux [] (rev card_assigns) end -fun repair_iterator_assign thy assigns (T as Type (_, Ts), k) = +fun repair_iterator_assign ctxt assigns (T as Type (_, Ts), k) = (T, if T = @{typ bisim_iterator} then let - val co_cards = map snd (filter (is_codatatype thy o fst) assigns) + val co_cards = map snd (filter (is_codatatype ctxt o fst) assigns) in Int.min (k, Integer.sum co_cards) end else if is_fp_iterator_type T then case Ts of @@ -350,7 +352,7 @@ | Max x => (card_assigns, (x, the_single ks) :: max_assigns) fun scope_descriptor_from_block block = fold_rev add_row_to_scope_descriptor block ([], []) -fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) binarize blocks +fun scope_descriptor_from_combination (hol_ctxt as {ctxt, ...}) binarize blocks columns = let val (card_assigns, max_assigns) = @@ -358,7 +360,7 @@ val card_assigns = repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) |> the in - SOME (map (repair_iterator_assign thy card_assigns) card_assigns, + SOME (map (repair_iterator_assign ctxt card_assigns) card_assigns, max_assigns) end handle Option.Option => NONE @@ -430,11 +432,12 @@ card_assigns T end -fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize - deep_dataTs finitizable_dataTs (desc as (card_assigns, _)) (T, card) = +fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ctxt, stds, ...}) + binarize deep_dataTs finitizable_dataTs (desc as (card_assigns, _)) + (T, card) = let val deep = member (op =) deep_dataTs T - val co = is_codatatype thy T + val co = is_codatatype ctxt T val standard = is_standard_datatype thy stds T val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T val self_recs = map (is_self_recursive_constr_type o snd) xs @@ -496,11 +499,11 @@ iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs finitizable_dataTs = let - val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts - cards_assigns - val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns - iters_assigns bitss bisim_depths mono_Ts - nonmono_Ts + val cards_assigns = + repair_cards_assigns_wrt_boxing_etc thy mono_Ts cards_assigns + val blocks = + blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns + iters_assigns bitss bisim_depths mono_Ts nonmono_Ts val ranks = map rank_of_block blocks val all = all_combinations_ordered_smartly (map (rpair 0) ranks) val head = take max_scopes all diff -r 17d9808ed626 -r a44d108a8d39 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Aug 06 11:37:33 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Aug 06 17:05:29 2010 +0200 @@ -66,6 +66,7 @@ val get_class_def : theory -> string -> (string * term) option val monomorphic_term : Type.tyenv -> term -> term val specialize_type : theory -> string * typ -> term -> term + val varify_type : Proof.context -> typ -> typ val nat_subscript : int -> string val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b val DETERM_TIMEOUT : Time.time option -> tactic -> tactic @@ -253,6 +254,10 @@ val monomorphic_term = Sledgehammer_Util.monomorphic_term val specialize_type = Sledgehammer_Util.specialize_type +fun varify_type ctxt T = + Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] + |> snd |> the_single |> dest_Const |> snd + val i_subscript = implode o map (prefix "\<^isub>") o explode fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>" fun nat_subscript n =