# HG changeset patch # User wenzelm # Date 1684257618 -7200 # Node ID 11d6a1e62841b92d1d7d7bba59d8ea06d2cc1441 # Parent 4e865c45458bf68d5cacb0848876241e76fe60f6 more careful treatment of set_context / reset_context for persistent morphisms; avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition; diff -r 4e865c45458b -r 11d6a1e62841 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue May 16 17:08:31 2023 +0200 +++ b/src/Pure/Isar/class.ML Tue May 16 19:20:18 2023 +0200 @@ -157,8 +157,9 @@ val base_morphism = #base_morph oo the_class_data; fun morphism thy class = - base_morphism thy class $> - Morphism.default (Element.eq_morphism thy (these_defs thy [class])); + Morphism.set_context thy + (base_morphism thy class $> + Morphism.default (Element.eq_morphism (these_defs thy [class]))); val export_morphism = #export_morph oo the_class_data; @@ -230,7 +231,7 @@ in Class_Data.map add_class thy end; fun activate_defs class thms thy = - (case Element.eq_morphism thy thms of + (case Element.eq_morphism thms of SOME eq_morph => fold (fn cls => fn thy' => (Context.theory_map o Locale.amend_registration) @@ -359,7 +360,8 @@ fun target_const class phi0 prmode (b, rhs) lthy = let - val export = Variable.export_morphism lthy (Local_Theory.target_of lthy); + val export = + Morphism.set_context' lthy (Variable.export_morphism lthy (Local_Theory.target_of lthy)); val guess_identity = guess_morphism_identity (b, rhs) export; val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0); in diff -r 4e865c45458b -r 11d6a1e62841 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Tue May 16 17:08:31 2023 +0200 +++ b/src/Pure/Isar/class_declaration.ML Tue May 16 19:20:18 2023 +0200 @@ -74,7 +74,9 @@ val base_morph = inst_morph $> 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 thy (Class.these_defs thy sups |> map Thm.trim_context); + val eq_morph = + Element.eq_morphism (Class.these_defs thy sups) + |> Option.map (Morphism.set_context thy); (* assm_intro *) fun prove_assm_intro thm = diff -r 4e865c45458b -r 11d6a1e62841 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue May 16 17:08:31 2023 +0200 +++ b/src/Pure/Isar/element.ML Tue May 16 19:20:18 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: theory -> term list -> morphism option - val eq_morphism: theory -> thm list -> morphism option + val eq_term_morphism: term list -> morphism option + val eq_morphism: 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 @@ -399,37 +399,42 @@ (* rewriting with equalities *) (* for activating declarations only *) -fun eq_term_morphism _ [] = NONE - | eq_term_morphism thy props = +fun eq_term_morphism [] = NONE + | eq_term_morphism props = let - (* FIXME proper morphism context *) - fun decomp_simp prop = + fun decomp_simp ctxt prop = let - val ctxt = Proof_Context.init_global thy; val _ = Logic.no_prems prop orelse error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop); - val lhsrhs = Logic.dest_equals prop - handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop); - in lhsrhs end; + in + Logic.dest_equals prop handle TERM _ => + error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop) + end; + fun rewrite_term thy = + let val ctxt = Proof_Context.init_global thy + in Pattern.rewrite_term thy (map (decomp_simp ctxt) props) [] end; val phi = Morphism.morphism "Element.eq_term_morphism" {binding = [], typ = [], - term = [K (Pattern.rewrite_term thy (map decomp_simp props) [])], + term = [rewrite_term o Morphism.the_theory], fact = [fn _ => fn _ => error "Illegal application of Element.eq_term_morphism"]}; in SOME phi end; -fun eq_morphism _ [] = NONE - | eq_morphism thy thms = +fun eq_morphism [] = NONE + | eq_morphism thms = let - (* FIXME proper morphism context *) - fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th; + 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 phi = Morphism.morphism "Element.eq_morphism" {binding = [], typ = [], - term = [K (Raw_Simplifier.rewrite_term thy thms [])], - fact = [K (map rewrite)]}; + term = [rewrite_term o Morphism.the_theory], + fact = [map o rewrite o Morphism.the_theory]}; in SOME phi end; diff -r 4e865c45458b -r 11d6a1e62841 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue May 16 17:08:31 2023 +0200 +++ b/src/Pure/Isar/expression.ML Tue May 16 19:20:18 2023 +0200 @@ -406,7 +406,7 @@ val rewrite_morph = eqns' |> map (abs_def ctxt') |> Variable.export_terms ctxt' ctxt - |> Element.eq_term_morphism (Proof_Context.theory_of ctxt) + |> Element.eq_term_morphism |> Morphism.default; val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt; val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns']; diff -r 4e865c45458b -r 11d6a1e62841 src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Tue May 16 17:08:31 2023 +0200 +++ b/src/Pure/Isar/interpretation.ML Tue May 16 19:20:18 2023 +0200 @@ -111,9 +111,7 @@ fun register (dep, eqns) ctxt = ctxt |> add_registration {inst = dep, - mixin = - Option.map (rpair true) - (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')), + mixin = Option.map (rpair true) (Element.eq_morphism (eqns @ eqns')), export = export}; in ctxt'' |> fold register (deps' ~~ eqnss') end; diff -r 4e865c45458b -r 11d6a1e62841 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue May 16 17:08:31 2023 +0200 +++ b/src/Pure/Isar/locale.ML Tue May 16 19:20:18 2023 +0200 @@ -107,8 +107,14 @@ type dep = {name: string, morphisms: morphism * morphism, pos: Position.T, serial: serial}; fun eq_dep (dep1: dep, dep2: dep) = #serial dep1 = #serial dep2; +fun transfer_dep thy ({name, morphisms, pos, serial}: dep) : dep = + {name = name, morphisms = apply2 (Morphism.set_context thy) morphisms, pos = pos, serial = serial}; + fun make_dep (name, morphisms) : dep = - {name = name, morphisms = morphisms, pos = Position.thread_data (), serial = serial ()}; + {name = name, + morphisms = apply2 Morphism.reset_context morphisms, + pos = Position.thread_data (), + serial = serial ()}; (*table of mixin lists, per list mixins in reverse order of declaration; lists indexed by registration/dependency serial, @@ -120,7 +126,8 @@ val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =); -fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ())); +fun insert_mixin serial' (morph, b) : mixins -> mixins = + Inttab.cons_list (serial', ((Morphism.reset_context morph, b), serial ())); fun rename_mixin (old, new) (mixins: mixins) = (case Inttab.lookup mixins old of @@ -216,8 +223,7 @@ map Element.trim_context_ctxt hyp_spec), ((map (fn decl => (decl, serial ())) syntax_decls, map (fn (a, facts) => ((a, map Attrib.trim_context_fact facts), serial ())) notes), - (map (fn (name, morph) => - make_dep (name, (Morphism.reset_context morph, Morphism.identity))) dependencies, + (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies, Inttab.empty)))) #> snd); (* FIXME Morphism.identity *) @@ -236,15 +242,17 @@ fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy; fun instance_of thy name morph = params_of thy name |> - map (Morphism.term morph o Free o #1); + map (Morphism.term (Morphism.set_context thy morph) o Free o #1); fun specification_of thy = #spec o the_locale thy; -fun hyp_spec_of thy = #hyp_spec o the_locale thy; +fun hyp_spec_of thy = map (Element.transfer_ctxt thy) o #hyp_spec o the_locale thy; + +fun dependencies_of thy = map (transfer_dep thy) o #dependencies o the_locale thy; -fun dependencies_of thy = #dependencies o the_locale thy; - -fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial; +fun mixins_of thy name serial = + lookup_mixins (#mixins (the_locale thy name)) serial + |> (map o apfst o apfst) (Morphism.set_context thy); (* Print instance and qualifiers *) @@ -398,7 +406,10 @@ fun add_reg thy export (name, morph) = let - val reg = {morphisms = (morph, export), pos = Position.thread_data (), serial = serial ()}; + val reg = + {morphisms = (Morphism.reset_context morph, Morphism.reset_context export), + pos = Position.thread_data (), + serial = serial ()}; val id = (name, instance_of thy name (morph $> export)); in (map_registrations o apfst) (Idtab.insert (K false) (id, reg)) end; @@ -494,28 +505,28 @@ handle ERROR msg => activate_err msg "syntax" (name, morph) context end; -fun activate_notes activ_elem transfer context export' (name, morph) input = +fun activate_notes activ_elem context export' (name, morph) input = let val thy = Context.theory_of context; val mixin = (case export' of NONE => Morphism.identity | SOME export => collect_mixins context (name, morph $> export) $> export); - val morph' = transfer input $> morph $> mixin; + val morph' = Morphism.set_context thy (morph $> mixin); val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name); in (notes', input) |-> fold (fn elem => fn res => - activ_elem (Element.transform_ctxt (transfer res) elem) res) + activ_elem (Element.transfer_ctxt thy elem) res) end handle ERROR msg => activate_err msg "facts" (name, morph) context; -fun activate_notes_trace activ_elem transfer context export' (name, morph) context' = +fun activate_notes_trace activ_elem context export' (name, morph) context' = let val _ = trace "facts" (name, morph) context'; in - activate_notes activ_elem transfer context export' (name, morph) context' + activate_notes activ_elem context export' (name, morph) context' end; -fun activate_all name thy activ_elem transfer (marked, input) = +fun activate_all name thy activ_elem (marked, input) = let val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name; val input' = input |> @@ -525,7 +536,7 @@ (case asm of SOME A => activ_elem (Assumes [(Binding.empty_atts, [(A, [])])]) | _ => I) |> (not (null defs) ? activ_elem (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs))); - val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE; + val activate = activate_notes activ_elem (Context.Theory thy) NONE; in roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input') end; @@ -538,7 +549,7 @@ |> Context_Position.set_visible_generic false |> pair (Idents.get context) |> roundup (Context.theory_of context) - (activate_notes_trace init_element Morphism.transfer_morphism'' context export) + (activate_notes_trace init_element context export) (Morphism.default export) dep |-> Idents.put |> Context_Position.restore_visible_generic context; @@ -559,7 +570,7 @@ context |> Context_Position.set_visible_generic false |> pair empty_idents - |> activate_all name thy init_element Morphism.transfer_morphism'' + |> activate_all name thy init_element |-> (fn marked' => Idents.put (merge_idents (marked, marked'))) |> Context_Position.restore_visible_generic context |> Context.proof_of @@ -735,7 +746,7 @@ | cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem | cons_elem elem = cons elem; val elems = - activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, []) + activate_all name thy cons_elem (empty_idents, []) |> snd |> rev |> tap consolidate_notes |> map force_notes;