performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers);
--- a/src/Pure/Isar/class.ML Tue Jul 25 12:27:31 2023 +0200
+++ b/src/Pure/Isar/class.ML Tue Jul 25 14:12:26 2023 +0200
@@ -156,10 +156,12 @@
val base_morphism = #base_morph oo the_class_data;
-fun morphism thy class =
- Morphism.set_context thy
- (base_morphism thy class $>
- Morphism.default (Element.eq_morphism (these_defs thy [class])));
+fun morphism ctxt class =
+ let val thy = Proof_Context.theory_of ctxt in
+ Morphism.set_context thy
+ (base_morphism thy class $>
+ Morphism.default (Element.eq_morphism ctxt (these_defs thy [class])))
+ end;
val export_morphism = #export_morph oo the_class_data;
@@ -230,8 +232,8 @@
#> fold (curry Graph.add_edge class) sups;
in Class_Data.map add_class thy end;
-fun activate_defs class thms thy =
- (case Element.eq_morphism thms of
+fun activate_defs context class thms thy =
+ (case Element.eq_morphism (Context.proof_of context) thms of
SOME eq_morph =>
fold (fn cls => fn thy' =>
(Context.theory_map o Locale.amend_registration)
@@ -261,7 +263,7 @@
thy
|> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apfst)
(Item_Net.update sym_thm)
- |> activate_defs class [sym_thm]
+ |> activate_defs (Context.Theory thy) class [sym_thm]
end;
@@ -408,7 +410,7 @@
fun const class ((b, mx), lhs) params lthy =
let
- val phi = morphism (Proof_Context.theory_of lthy) class;
+ val phi = morphism lthy class;
val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params));
in
lthy
@@ -463,7 +465,7 @@
fun abbrev class prmode ((b, mx), rhs) lthy =
let
val thy = Proof_Context.theory_of lthy;
- val phi = morphism thy class;
+ val phi = morphism lthy class;
val rhs_generic =
perhaps (try (Pattern.rewrite_term_top thy (these_unchecks_reversed thy [class]) [])) rhs;
in
@@ -504,7 +506,7 @@
|> Local_Theory.raw_theory
(Axclass.add_classrel classrel
#> Class_Data.map (Graph.add_edge (sub, sup))
- #> activate_defs sub (these_defs thy diff_sort))
+ #> activate_defs (Context.Proof lthy) sub (these_defs thy diff_sort))
|> add_dependency
|> synchronize_class_syntax_target sub
end;
--- a/src/Pure/Isar/class_declaration.ML Tue Jul 25 12:27:31 2023 +0200
+++ b/src/Pure/Isar/class_declaration.ML Tue Jul 25 14:12:26 2023 +0200
@@ -75,7 +75,7 @@
$> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class))
$> Element.satisfy_morphism (the_list some_witn);
val eq_morph =
- Element.eq_morphism (Class.these_defs thy sups)
+ Element.eq_morphism thy_ctxt (Class.these_defs thy sups)
|> Option.map (Morphism.set_context thy);
(* assm_intro *)
--- a/src/Pure/Isar/element.ML Tue Jul 25 12:27:31 2023 +0200
+++ b/src/Pure/Isar/element.ML Tue Jul 25 14:12:26 2023 +0200
@@ -51,8 +51,8 @@
val pretty_witness: Proof.context -> witness -> Pretty.T
val instantiate_normalize_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
val satisfy_morphism: witness list -> morphism
- val eq_term_morphism: term list -> morphism option
- val eq_morphism: thm list -> morphism option
+ val eq_term_morphism: Proof.context -> term list -> morphism option
+ val eq_morphism: Proof.context -> thm list -> morphism option
val init: context_i -> Context.generic -> Context.generic
val activate_i: context_i -> Proof.context -> context_i * Proof.context
val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -398,21 +398,24 @@
(* rewriting with equalities *)
+fun decomp_simp ctxt prop =
+ let
+ val _ = Logic.no_prems prop orelse
+ error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop);
+ in
+ Logic.dest_equals prop handle TERM _ =>
+ error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop)
+ end;
+
(* for activating declarations only *)
-fun eq_term_morphism [] = NONE
- | eq_term_morphism props =
+fun eq_term_morphism _ [] = NONE
+ | eq_term_morphism ctxt0 props =
let
- fun decomp_simp ctxt prop =
- let
- val _ = Logic.no_prems prop orelse
- error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop);
- in
- Logic.dest_equals prop handle TERM _ =>
- error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop)
- end;
+ val simps = map (decomp_simp ctxt0) props;
+
fun rewrite_term thy =
let val ctxt = Proof_Context.init_global thy
- in Pattern.rewrite_term thy (map (decomp_simp ctxt) props) [] end;
+ in Pattern.rewrite_term thy simps [] end;
val phi =
Morphism.morphism "Element.eq_term_morphism"
{binding = [],
@@ -421,14 +424,17 @@
fact = [fn _ => fn _ => error "Illegal application of Element.eq_term_morphism"]};
in SOME phi end;
-fun eq_morphism [] = NONE
- | eq_morphism thms =
+fun eq_morphism _ [] = NONE
+ | eq_morphism ctxt0 thms =
let
- val thms0 = map Thm.trim_context thms;
- fun rewrite_term thy =
- Raw_Simplifier.rewrite_term thy (map (Thm.transfer thy) thms0) [];
- fun rewrite thy =
- Raw_Simplifier.rewrite_rule (Proof_Context.init_global thy) (map (Thm.transfer thy) thms0);
+ val simpset = Raw_Simplifier.simpset_of (Raw_Simplifier.init_simpset thms ctxt0);
+ val simps = map (decomp_simp ctxt0 o Thm.full_prop_of) (Raw_Simplifier.dest_simps simpset);
+
+ fun rewrite_term thy = Pattern.rewrite_term thy simps [];
+ val rewrite =
+ Proof_Context.init_global #>
+ Raw_Simplifier.put_simpset simpset #>
+ Raw_Simplifier.rewrite0_rule;
val phi =
Morphism.morphism "Element.eq_morphism"
{binding = [],
--- a/src/Pure/Isar/expression.ML Tue Jul 25 12:27:31 2023 +0200
+++ b/src/Pure/Isar/expression.ML Tue Jul 25 14:12:26 2023 +0200
@@ -406,7 +406,7 @@
val rewrite_morph = eqns'
|> map (abs_def ctxt')
|> Variable.export_terms ctxt' ctxt
- |> Element.eq_term_morphism
+ |> Element.eq_term_morphism ctxt
|> Morphism.default;
val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
--- a/src/Pure/Isar/interpretation.ML Tue Jul 25 12:27:31 2023 +0200
+++ b/src/Pure/Isar/interpretation.ML Tue Jul 25 14:12:26 2023 +0200
@@ -111,7 +111,7 @@
fun register (dep, eqns) ctxt =
ctxt |> add_registration
{inst = dep,
- mixin = Option.map (rpair true) (Element.eq_morphism (eqns @ eqns')),
+ mixin = Option.map (rpair true) (Element.eq_morphism ctxt (eqns @ eqns')),
export = export};
in ctxt'' |> fold register (deps' ~~ eqnss') end;
--- a/src/Pure/raw_simplifier.ML Tue Jul 25 12:27:31 2023 +0200
+++ b/src/Pure/raw_simplifier.ML Tue Jul 25 14:12:26 2023 +0200
@@ -33,6 +33,7 @@
loopers: string list,
unsafe_solvers: string list,
safe_solvers: string list}
+ val dest_simps: simpset -> thm list
type simproc
val eq_simproc: simproc * simproc -> bool
val cert_simproc: theory -> string ->
@@ -107,7 +108,9 @@
(Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm
val generic_rewrite_goal_tac: bool * bool * bool ->
(Proof.context -> tactic) -> Proof.context -> int -> tactic
+ val rewrite0: Proof.context -> bool -> conv
val rewrite: Proof.context -> bool -> thm list -> conv
+ val rewrite0_rule: Proof.context -> thm -> thm
end;
structure Raw_Simplifier: RAW_SIMPLIFIER =
@@ -294,6 +297,8 @@
unsafe_solvers = map solver_name (#1 solvers),
safe_solvers = map solver_name (#2 solvers)};
+fun dest_simps (Simpset ({rules, ...}, _)) = map #thm (Net.entries rules);
+
(* empty *)
@@ -1366,10 +1371,12 @@
val simple_prover =
SINGLE o (fn ctxt => ALLGOALS (resolve_tac ctxt (prems_of ctxt)));
+fun rewrite0 ctxt full = rewrite_cterm (full, false, false) simple_prover ctxt;
+
fun rewrite _ _ [] = Thm.reflexive
- | rewrite ctxt full thms =
- rewrite_cterm (full, false, false) simple_prover (init_simpset thms ctxt);
+ | rewrite ctxt full thms = rewrite0 (init_simpset thms ctxt) full;
+fun rewrite0_rule ctxt = Conv.fconv_rule (rewrite0 ctxt true);
fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
(*simple term rewriting -- no proof*)