support for context within morphism (for background theory);

--- a/src/Pure/General/basics.ML	Mon May 15 22:46:04 2023 +0200
+++ b/src/Pure/General/basics.ML	Tue May 16 14:30:32 2023 +0200
@@ -32,6 +32,7 @@
   val the_default: 'a -> 'a option -> 'a
   val perhaps: ('a -> 'a option) -> 'a -> 'a
   val merge_options: 'a option * 'a option -> 'a option
+  val join_options: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option
   val eq_option: ('a * 'b -> bool) -> 'a option * 'b option -> bool
 
   (*partiality*)
@@ -94,6 +95,9 @@
 
 fun merge_options (x, y) = if is_some x then x else y;
 
+fun join_options f (SOME x, SOME y) = SOME (f (x, y))
+  | join_options _ args = merge_options args;
+
 fun eq_option eq (SOME x, SOME y) = eq (x, y)
   | eq_option _ (NONE, NONE) = true
   | eq_option _ _ = false;

--- a/src/Pure/Isar/element.ML	Mon May 15 22:46:04 2023 +0200
+++ b/src/Pure/Isar/element.ML	Tue May 16 14:30:32 2023 +0200
@@ -390,6 +390,7 @@
 fun eq_term_morphism _ [] = NONE
   | eq_term_morphism thy props =
       let
+        (* FIXME proper morphism context *)
         fun decomp_simp prop =
           let
             val ctxt = Proof_Context.init_global thy;
@@ -402,21 +403,21 @@
           Morphism.morphism "Element.eq_term_morphism"
            {binding = [],
             typ = [],
-            term = [Pattern.rewrite_term thy (map decomp_simp props) []],
-            fact = [fn _ => error "Illegal application of Element.eq_term_morphism"]};
+            term = [K (Pattern.rewrite_term thy (map decomp_simp props) [])],
+            fact = [fn _ => fn _ => error "Illegal application of Element.eq_term_morphism"]};
       in SOME phi end;
 
 fun eq_morphism _ [] = NONE
   | eq_morphism thy thms =
       let
-        (* FIXME proper context!? *)
+        (* FIXME proper morphism context *)
         fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th;
         val phi =
           Morphism.morphism "Element.eq_morphism"
            {binding = [],
             typ = [],
-            term = [Raw_Simplifier.rewrite_term thy thms []],
-            fact = [map rewrite]};
+            term = [K (Raw_Simplifier.rewrite_term thy thms [])],
+            fact = [K (map rewrite)]};
       in SOME phi end;
 
 

--- a/src/Pure/Isar/expression.ML	Mon May 15 22:46:04 2023 +0200
+++ b/src/Pure/Isar/expression.ML	Tue May 16 14:30:32 2023 +0200
@@ -556,7 +556,7 @@
     val exp_typ = Logic.type_map exp_term;
     val export' =
       Morphism.morphism "Expression.prep_goal"
-        {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
+        {binding = [], typ = [K exp_typ], term = [K exp_term], fact = [K exp_fact]};
   in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end;
 
 in

--- a/src/Pure/assumption.ML	Mon May 15 22:46:04 2023 +0200
+++ b/src/Pure/assumption.ML	Tue May 16 14:30:32 2023 +0200
@@ -143,7 +143,7 @@
     val typ = Logic.type_map term;
   in
     Morphism.morphism "Assumption.export"
-      {binding = [], typ = [typ], term = [term], fact = [map thm]}
+      {binding = [], typ = [K typ], term = [K term], fact = [K (map thm)]}
   end;
 
 end;

--- a/src/Pure/context.ML	Mon May 15 22:46:04 2023 +0200
+++ b/src/Pure/context.ML	Tue May 16 14:30:32 2023 +0200
@@ -65,6 +65,7 @@
   val certificate_theory_id: certificate -> theory_id
   val eq_certificate: certificate * certificate -> bool
   val join_certificate: certificate * certificate -> certificate
+  val join_certificate_theory: theory * theory -> theory
   (*generic context*)
   datatype generic = Theory of theory | Proof of Proof.context
   val theory_tracing: bool Unsynchronized.ref
@@ -627,16 +628,24 @@
   | eq_certificate (Certificate_Id thy_id1, Certificate_Id thy_id2) = eq_thy_id (thy_id1, thy_id2)
   | eq_certificate _ = false;
 
+fun err_join (thy_id1, thy_id2) =
+  error ("Cannot join unrelated theory certificates " ^
+    display_name thy_id1 ^ " and " ^ display_name thy_id2);
+
 fun join_certificate (cert1, cert2) =
   let val (thy_id1, thy_id2) = apply2 certificate_theory_id (cert1, cert2) in
     if eq_thy_id (thy_id1, thy_id2) then (case cert1 of Certificate _ => cert1 | _ => cert2)
     else if proper_subthy_id (thy_id2, thy_id1) then cert1
     else if proper_subthy_id (thy_id1, thy_id2) then cert2
-    else
-      error ("Cannot join unrelated theory certificates " ^
-        display_name thy_id1 ^ " and " ^ display_name thy_id2)
+    else err_join (thy_id1, thy_id2)
   end;
 
+fun join_certificate_theory (thy1, thy2) =
+  let val (thy_id1, thy_id2) = apply2 theory_id (thy1, thy2) in
+    if subthy_id (thy_id2, thy_id1) then thy1
+    else if proper_subthy_id (thy_id1, thy_id2) then thy2
+    else err_join (thy_id1, thy_id2)
+  end;
 
 
 (*** generic context ***)

--- a/src/Pure/morphism.ML	Mon May 15 22:46:04 2023 +0200
+++ b/src/Pure/morphism.ML	Tue May 16 14:30:32 2023 +0200
@@ -17,12 +17,16 @@
 sig
   include BASIC_MORPHISM
   exception MORPHISM of string * exn
+  val the_theory: theory option -> theory
+  val set_context: theory -> morphism -> morphism
+  val reset_context: morphism -> morphism
   val morphism: string ->
-   {binding: (binding -> binding) list,
-    typ: (typ -> typ) list,
-    term: (term -> term) list,
-    fact: (thm list -> thm list) list} -> morphism
+   {binding: (theory option -> binding -> binding) list,
+    typ: (theory option -> typ -> typ) list,
+    term: (theory option -> term -> term) list,
+    fact: (theory option -> thm list -> thm list) list} -> morphism
   val is_identity: morphism -> bool
+  val is_empty: morphism -> bool
   val pretty: morphism -> Pretty.T
   val binding: morphism -> binding -> binding
   val binding_prefix: morphism -> (string * bool) list
@@ -37,7 +41,9 @@
   val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
   val form: (morphism -> 'a) -> 'a
   val binding_morphism: string -> (binding -> binding) -> morphism
+  val typ_morphism': string -> (theory -> typ -> typ) -> morphism
   val typ_morphism: string -> (typ -> typ) -> morphism
+  val term_morphism': string -> (theory -> term -> term) -> morphism
   val term_morphism: string -> (term -> term) -> morphism
   val fact_morphism: string -> (thm list -> thm list) -> morphism
   val thm_morphism: string -> (thm -> thm) -> morphism
@@ -54,32 +60,53 @@
 
 (* named functions *)
 
-type 'a funs = (string * ('a -> 'a)) list;
+type 'a funs = (string * (theory option -> 'a -> 'a)) list;
 
 exception MORPHISM of string * exn;
 
-fun app (name, f) x = f x
+fun app context (name, f) x = f context x
   handle exn =>
     if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
 
-fun apply fs = fold_rev app fs;
+
+(* optional context *)
+
+fun the_theory (SOME thy) = thy
+  | the_theory NONE = raise Fail "Morphism lacks theory context";
+
+fun join_transfer (SOME thy) = Thm.join_transfer thy
+  | join_transfer NONE = I;
+
+val join_context = join_options Context.join_certificate_theory;
 
 
 (* type morphism *)
 
 datatype morphism = Morphism of
- {names: string list,
+ {context: theory option,
+  names: string list,
   binding: binding funs,
   typ: typ funs,
   term: term funs,
   fact: thm list funs};
 
+type declaration = morphism -> Context.generic -> Context.generic;
+
 fun rep (Morphism args) = args;
 
-type declaration = morphism -> Context.generic -> Context.generic;
+fun apply which phi =
+  let val args = rep phi
+  in fold_rev (app (#context args)) (which args) end;
+
+fun put_context context (Morphism {context = _, names, binding, typ, term, fact}) =
+  Morphism {context = context, names = names, binding = binding, typ = typ, term = term, fact = fact};
+
+val set_context = put_context o SOME;
+val reset_context = put_context NONE;
 
 fun morphism a {binding, typ, term, fact} =
   Morphism {
+    context = NONE,
     names = if a = "" then [] else [a],
     binding = map (pair a) binding,
     typ = map (pair a) typ,
@@ -87,18 +114,20 @@
     fact = map (pair a) fact};
 
 (*syntactic test only!*)
-fun is_identity (Morphism {names, binding, typ, term, fact}) =
+fun is_identity (Morphism {context = _, names, binding, typ, term, fact}) =
   null names andalso null binding andalso null typ andalso null term andalso null fact;
 
+fun is_empty phi = is_none (#context (rep phi)) andalso is_identity phi;
+
 fun pretty phi = Pretty.enum ";" "{" "}" (map Pretty.str (rev (#names (rep phi))));
 
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
-val binding = apply o #binding o rep;
+val binding = apply #binding;
 fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of;
-val typ = apply o #typ o rep;
-val term = apply o #term o rep;
-val fact = apply o #fact o rep;
+val typ = apply #typ;
+val term = apply #term;
+fun fact phi = map (join_transfer (#context (rep phi))) #> apply #fact phi;
 val thm = singleton o fact;
 val cterm = Drule.cterm_rule o thm;
 
@@ -110,14 +139,17 @@
 val default = the_default identity;
 
 fun compose phi1 phi2 =
-  if is_identity phi1 then phi2
-  else if is_identity phi2 then phi1
+  if is_empty phi1 then phi2
+  else if is_empty phi2 then phi1
   else
     let
-      val {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1} = rep phi1;
-      val {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2} = rep phi2;
+      val {context = context1, names = names1, binding = binding1,
+        typ = typ1, term = term1, fact = fact1} = rep phi1;
+      val {context = context2, names = names2, binding = binding2,
+        typ = typ2, term = term2, fact = fact2} = rep phi2;
     in
       Morphism {
+        context = join_context (context1, context2),
         names = names1 @ names2,
         binding = binding1 @ binding2,
         typ = typ1 @ typ2,
@@ -133,11 +165,13 @@
 
 (* concrete morphisms *)
 
-fun binding_morphism a binding = morphism a {binding = [binding], typ = [], term = [], fact = []};
-fun typ_morphism a typ = morphism a {binding = [], typ = [typ], term = [], fact = []};
-fun term_morphism a term = morphism a {binding = [], typ = [], term = [term], fact = []};
-fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]};
-fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
+fun binding_morphism a binding = morphism a {binding = [K binding], typ = [], term = [], fact = []};
+fun typ_morphism' a typ = morphism a {binding = [], typ = [typ o the_theory], term = [], fact = []};
+fun typ_morphism a typ = morphism a {binding = [], typ = [K typ], term = [], fact = []};
+fun term_morphism' a term = morphism a {binding = [], typ = [], term = [term o the_theory], fact = []};
+fun term_morphism a term = morphism a {binding = [], typ = [], term = [K term], fact = []};
+fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [K fact]};
+fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [K (map thm)]};
 
 val transfer_morphism = thm_morphism "transfer" o Thm.join_transfer;
 val transfer_morphism' = transfer_morphism o Proof_Context.theory_of;
@@ -159,9 +193,9 @@
         {binding = [],
          typ =
           if TFrees.is_empty instT then []
-          else [Term_Subst.instantiateT_frees instT],
-         term = [Term_Subst.instantiate_frees (instT, inst)],
-         fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
+          else [K (Term_Subst.instantiateT_frees instT)],
+         term = [K (Term_Subst.instantiate_frees (instT, inst))],
+         fact = [K (map (Thm.instantiate_frees (cinstT, cinst)))]}
     end;
 
 fun instantiate_morphism (cinstT, cinst) =
@@ -175,9 +209,9 @@
         {binding = [],
          typ =
           if TVars.is_empty instT then []
-          else [Term_Subst.instantiateT instT],
-         term = [Term_Subst.instantiate (instT, inst)],
-         fact = [map (Thm.instantiate (cinstT, cinst))]}
+          else [K (Term_Subst.instantiateT instT)],
+         term = [K (Term_Subst.instantiate (instT, inst))],
+         fact = [K (map (Thm.instantiate (cinstT, cinst)))]}
     end;
 
 end;

--- a/src/Pure/variable.ML	Mon May 15 22:46:04 2023 +0200
+++ b/src/Pure/variable.ML	Tue May 16 14:30:32 2023 +0200
@@ -583,7 +583,8 @@
     val term = singleton (export_terms inner outer);
     val typ = Logic.type_map term;
   in
-    Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]}
+    Morphism.morphism "Variable.export"
+      {binding = [], typ = [K typ], term = [K term], fact = [K fact]}
   end;