# HG changeset patch
# User wenzelm
# Date 1386962415 -3600
# Node ID 91f54d386680a5a715d7b30f7785a7e1f8018eea
# Parent  d41099c829bf9626635d436d08c57312de3e2e73
maintain morphism names for diagnostic purposes;

diff -r d41099c829bf -r 91f54d386680 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -459,7 +459,7 @@
 
 fun bnf_of ctxt =
   Symtab.lookup (Data.get (Context.Proof ctxt))
-  #> Option.map (morph_bnf (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
+  #> Option.map (morph_bnf (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
 
 
 (* Utilities *)
diff -r d41099c829bf -r 91f54d386680 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -156,7 +156,7 @@
    sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
 
 val transfer_fp_sugar =
-  morph_fp_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 structure Data = Generic_Data
 (
@@ -344,7 +344,7 @@
    (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs));
 
 val transfer_lfp_sugar_thms =
-  morph_lfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 type gfp_sugar_thms =
   ((thm list * thm) list * Args.src list)
@@ -368,7 +368,7 @@
     map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs));
 
 val transfer_gfp_sugar_thms =
-  morph_gfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
diff -r d41099c829bf -r 91f54d386680 src/HOL/BNF/Tools/bnf_fp_n2m.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -370,7 +370,7 @@
         xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
         xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
         rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
-       |> morph_fp_result (Morphism.term_morphism (singleton (Variable.polymorphic lthy))));
+       |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   in
     (fp_res, lthy)
   end;
diff -r d41099c829bf -r 91f54d386680 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -52,7 +52,7 @@
     Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
 
 val transfer_n2m_sugar =
-  morph_n2m_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_n2m_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 fun n2m_sugar_of ctxt =
   Typtab.lookup (Data.get (Context.Proof ctxt))
@@ -127,7 +127,7 @@
     fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
       let
         val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
-        val phi = Morphism.term_morphism (Term.subst_TVars rho);
+        val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
       in
         morph_ctr_sugar phi (nth ctr_sugars index)
       end;
diff -r d41099c829bf -r 91f54d386680 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -125,7 +125,7 @@
    case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
 
 val transfer_ctr_sugar =
-  morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_ctr_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 structure Data = Generic_Data
 (
diff -r d41099c829bf -r 91f54d386680 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -189,8 +189,11 @@
   let
     fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
   in
-    Morphism.thm_morphism f $> Morphism.term_morphism term
-    $> Morphism.typ_morphism (Logic.type_map term)
+    Morphism.morphism "lift_morphism"
+      {binding = [],
+       typ = [Logic.type_map term],
+       term = [term],
+       fact = [map f]}
   end
 
 fun import_function_data t ctxt =
diff -r d41099c829bf -r 91f54d386680 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -64,7 +64,7 @@
 
     (* canonical interpretation *)
     val base_morph = inst_morph
-      $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class))
+      $> 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);
 
diff -r d41099c829bf -r 91f54d386680 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/Isar/element.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -391,7 +391,7 @@
     in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
 
 fun instT_morphism thy env =
-  Morphism.morphism
+  Morphism.morphism "Element.instT"
    {binding = [],
     typ = [instT_type env],
     term = [instT_term env],
@@ -434,7 +434,7 @@
     end;
 
 fun inst_morphism thy (envT, env) =
-  Morphism.morphism
+  Morphism.morphism "Element.inst"
    {binding = [],
     typ = [instT_type envT],
     term = [inst_term (envT, env)],
@@ -449,14 +449,14 @@
       NONE => I
     | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
 
-val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
+val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm;
 
 
 (* rewriting with equalities *)
 
 fun eq_morphism _ [] = NONE
   | eq_morphism thy thms =
-      SOME (Morphism.morphism
+      SOME (Morphism.morphism "Element.eq_morphism"
        {binding = [],
         typ = [],
         term = [Raw_Simplifier.rewrite_term thy thms []],
diff -r d41099c829bf -r 91f54d386680 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -171,7 +171,7 @@
 
 (* Instantiation morphism *)
 
-fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
+fun inst_morphism (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
   let
     (* parameters *)
     val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
@@ -192,7 +192,7 @@
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
-      Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
+      Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
   end;
 
 
@@ -299,7 +299,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
-    val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
+    val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst) ctxt;
   in (loc, morph) end;
 
 fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
@@ -368,7 +368,7 @@
         val insts' = insts @ [(loc, (prfx, inst''))];
         val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
-        val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
+        val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
         val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
       in (i + 1, insts', ctxt'') end;
 
@@ -513,7 +513,8 @@
     val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
     val export' =
-      Morphism.morphism {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
+      Morphism.morphism "Expression.prep_goal"
+        {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
   in ((propss, deps, export'), goal_ctxt) end;
 
 in
diff -r d41099c829bf -r 91f54d386680 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -189,7 +189,8 @@
 
 fun standard_morphism lthy ctxt =
   Proof_Context.norm_export_morphism lthy ctxt $>
-  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
+  Morphism.binding_morphism "Local_Theory.standard_binding"
+    (Name_Space.transform_binding (naming_of lthy));
 
 fun standard_form lthy ctxt x =
   Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
diff -r d41099c829bf -r 91f54d386680 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -762,7 +762,7 @@
 
 fun norm_export_morphism inner outer =
   export_morphism inner outer $>
-  Morphism.thm_morphism Goal.norm_result;
+  Morphism.thm_morphism "Proof_Context.norm_export" Goal.norm_result;
 
 
 
diff -r d41099c829bf -r 91f54d386680 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/ROOT.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -328,6 +328,7 @@
 toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
+toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
 
 if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
 
diff -r d41099c829bf -r 91f54d386680 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/assumption.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -121,6 +121,9 @@
     val thm = export false inner outer;
     val term = export_term inner outer;
     val typ = Logic.type_map term;
-  in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [map thm]} end;
+  in
+    Morphism.morphism "Assumption.export"
+      {binding = [], typ = [typ], term = [term], fact = [map thm]}
+  end;
 
 end;
diff -r d41099c829bf -r 91f54d386680 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/morphism.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -16,23 +16,24 @@
 signature MORPHISM =
 sig
   include BASIC_MORPHISM
-  type 'a funs = ('a -> 'a) list
+  exception MORPHISM of string * exn
+  val pretty: morphism -> Pretty.T
   val binding: morphism -> binding -> binding
   val typ: morphism -> typ -> typ
   val term: morphism -> term -> term
   val fact: morphism -> thm list -> thm list
   val thm: morphism -> thm -> thm
   val cterm: morphism -> cterm -> cterm
-  val morphism:
-   {binding: binding funs,
-    typ: typ funs,
-    term: term funs,
-    fact: thm list funs} -> morphism
-  val binding_morphism: (binding -> binding) -> morphism
-  val typ_morphism: (typ -> typ) -> morphism
-  val term_morphism: (term -> term) -> morphism
-  val fact_morphism: (thm list -> thm list) -> morphism
-  val thm_morphism: (thm -> thm) -> morphism
+  val morphism: string ->
+   {binding: (binding -> binding) list,
+    typ: (typ -> typ) list,
+    term: (term -> term) list,
+    fact: (thm list -> thm list) list} -> morphism
+  val binding_morphism: string -> (binding -> binding) -> morphism
+  val typ_morphism: string -> (typ -> typ) -> morphism
+  val term_morphism: string -> (term -> term) -> morphism
+  val fact_morphism: string -> (thm list -> thm list) -> morphism
+  val thm_morphism: string -> (thm -> thm) -> morphism
   val transfer_morphism: theory -> morphism
   val identity: morphism
   val compose: morphism -> morphism -> morphism
@@ -43,17 +44,31 @@
 structure Morphism: MORPHISM =
 struct
 
-type 'a funs = ('a -> 'a) list;
-fun apply fs = fold_rev (fn f => fn x => f x) fs;
+(* named functions *)
+
+type 'a funs = (string * ('a -> 'a)) list;
+
+exception MORPHISM of string * exn;
+
+fun app (name, f) x = f x
+  handle exn => if Exn.is_interrupt exn then reraise exn else raise MORPHISM (name, exn);
+
+fun apply fs = fold_rev app fs;
+
+
+(* type morphism *)
 
 datatype morphism = Morphism of
- {binding: binding funs,
+ {names: string list,
+  binding: binding funs,
   typ: typ funs,
   term: term funs,
   fact: thm list funs};
 
 type declaration = morphism -> Context.generic -> Context.generic;
 
+fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
+
 fun binding (Morphism {binding, ...}) = apply binding;
 fun typ (Morphism {typ, ...}) = apply typ;
 fun term (Morphism {term, ...}) = apply term;
@@ -61,22 +76,36 @@
 val thm = singleton o fact;
 val cterm = Drule.cterm_rule o thm;
 
-val morphism = Morphism;
+
+fun morphism a {binding, typ, term, fact} =
+  Morphism {
+    names = if a = "" then [] else [a],
+    binding = map (pair a) binding,
+    typ = map (pair a) typ,
+    term = map (pair a) term,
+    fact = map (pair a) fact};
 
-fun binding_morphism binding = morphism {binding = [binding], typ = [], term = [], fact = []};
-fun typ_morphism typ = morphism {binding = [], typ = [typ], term = [], fact = []};
-fun term_morphism term = morphism {binding = [], typ = [], term = [term], fact = []};
-fun fact_morphism fact = morphism {binding = [], typ = [], term = [], fact = [fact]};
-fun thm_morphism thm = morphism {binding = [], typ = [], term = [], fact = [map thm]};
-val transfer_morphism = thm_morphism o Thm.transfer;
+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]};
+val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
 
-val identity = morphism {binding = [], typ = [], term = [], fact = []};
+val identity = morphism "" {binding = [], typ = [], term = [], fact = []};
+
+
+(* morphism combinators *)
 
 fun compose
-    (Morphism {binding = binding1, typ = typ1, term = term1, fact = fact1})
-    (Morphism {binding = binding2, typ = typ2, term = term2, fact = fact2}) =
-  morphism {binding = binding1 @ binding2, typ = typ1 @ typ2,
-    term = term1 @ term2, fact = fact1 @ fact2};
+    (Morphism {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1})
+    (Morphism {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2}) =
+  Morphism {
+    names = names1 @ names2,
+    binding = binding1 @ binding2,
+    typ = typ1 @ typ2,
+    term = term1 @ term2,
+    fact = fact1 @ fact2};
 
 fun phi1 $> phi2 = compose phi2 phi1;
 
diff -r d41099c829bf -r 91f54d386680 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/variable.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -461,7 +461,9 @@
     val fact = export inner outer;
     val term = singleton (export_terms inner outer);
     val typ = Logic.type_map term;
-  in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [fact]} end;
+  in
+    Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]}
+  end;