--- a/src/HOL/BNF/Tools/bnf_def.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_def.ML Fri Dec 13 23:53:02 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 *)
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Dec 13 23:53:02 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;
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML Fri Dec 13 23:53:02 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;
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Fri Dec 13 23:53:02 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;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 13 23:53:02 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
(
--- a/src/HOL/Tools/Function/function_common.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/HOL/Tools/Function/function_common.ML Fri Dec 13 23:53:02 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 =
--- a/src/HOL/Tools/Function/function_elims.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/HOL/Tools/Function/function_elims.ML Fri Dec 13 23:53:02 2013 +0100
@@ -33,118 +33,121 @@
local
-fun propagate_tac i thm =
- let fun inspect eq = case eq of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
- if Logic.occs (Free x, t) then raise Match else true
- | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
- if Logic.occs (Free x, t) then raise Match else false
- | _ => raise Match;
- fun mk_eq thm = (if inspect (prop_of thm) then
- [thm RS eq_reflection]
- else
- [Thm.symmetric (thm RS eq_reflection)])
- handle Match => [];
- val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss
- |> Simplifier.set_mksimps (K mk_eq)
+fun propagate_tac ctxt i =
+ let
+ fun inspect eq =
+ (case eq of
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
+ if Logic.occs (Free x, t) then raise Match else true
+ | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
+ if Logic.occs (Free x, t) then raise Match else false
+ | _ => raise Match);
+ fun mk_eq thm =
+ (if inspect (prop_of thm) then [thm RS eq_reflection]
+ else [Thm.symmetric (thm RS eq_reflection)])
+ handle Match => [];
+ val simpset =
+ empty_simpset ctxt
+ |> Simplifier.set_mksimps (K mk_eq);
in
- asm_lr_simp_tac ss i thm
+ asm_lr_simp_tac simpset i
end;
-val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}
-val boolE = @{thms HOL.TrueE HOL.FalseE}
-val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}
-val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}
+val eq_boolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+};
+val boolE = @{thms HOL.TrueE HOL.FalseE};
+val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+};
+val eq_bool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False};
fun bool_subst_tac ctxt i =
- REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i)
- THEN REPEAT (dresolve_tac boolD i)
- THEN REPEAT (eresolve_tac boolE i)
+ REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool i)
+ THEN REPEAT (dresolve_tac boolD i)
+ THEN REPEAT (eresolve_tac boolE i)
fun mk_bool_elims ctxt elim =
- let val tac = ALLGOALS (bool_subst_tac ctxt)
- fun mk_bool_elim b =
- elim
- |> Thm.forall_elim b
- |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1))
- |> Tactic.rule_by_tactic ctxt tac
+ let
+ val tac = ALLGOALS (bool_subst_tac ctxt);
+ fun mk_bool_elim b =
+ elim
+ |> Thm.forall_elim b
+ |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eq_boolI 1))
+ |> Tactic.rule_by_tactic ctxt tac;
in
- map mk_bool_elim [@{cterm True}, @{cterm False}]
+ map mk_bool_elim [@{cterm True}, @{cterm False}]
end;
in
fun mk_partial_elim_rules ctxt result =
let
- val thy = Proof_Context.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
+ val cert = cterm_of thy;
- val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
- termination, domintros, ...} = result;
- val n_fs = length fs;
+ val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
+ val n_fs = length fs;
- fun mk_partial_elim_rule (idx,f) =
- let fun mk_funeq 0 T (acc_vars, acc_lhs) =
- let val y = Free("y",T) in
- (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T)
- end
- | mk_funeq n (Type(@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
- let val xn = Free ("x" ^ Int.toString n,S) in
- mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn)
- end
- | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f]))
+ fun mk_partial_elim_rule (idx, f) =
+ let
+ fun mk_funeq 0 T (acc_vars, acc_lhs) =
+ let val y = Free("y", T)
+ in (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T) end
+ | mk_funeq n (Type (@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
+ let val xn = Free ("x" ^ Int.toString n, S)
+ in mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) end
+ | mk_funeq _ _ _ = raise TERM ("Not a function.", [f]);
- val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl
- |> HOLogic.dest_Trueprop
- |> dest_funprop |> fst |> fst) = f)
- psimps
+ val f_simps =
+ filter (fn r =>
+ (prop_of r |> Logic.strip_assums_concl
+ |> HOLogic.dest_Trueprop
+ |> dest_funprop |> fst |> fst) = f)
+ psimps;
- val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl
- |> HOLogic.dest_Trueprop
- |> snd o fst o dest_funprop |> length;
- val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f)
- val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs)
- val args = HOLogic.mk_tuple arg_vars;
- val domT = R |> dest_Free |> snd |> hd o snd o dest_Type
-
- val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
-
- val cprop = cterm_of thy prop
+ val arity =
+ hd f_simps
+ |> prop_of
+ |> Logic.strip_assums_concl
+ |> HOLogic.dest_Trueprop
+ |> snd o fst o dest_funprop
+ |> length;
+ val (free_vars, prop, ranT) = mk_funeq arity (fastype_of f) ([], f);
+ val (rhs_var, arg_vars) = (case free_vars of x :: xs => (x, rev xs));
+ val args = HOLogic.mk_tuple arg_vars;
+ val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
- val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
- val asms_thms = map Thm.assume asms;
+ val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
+
+ val cprop = cert prop;
+
+ val asms = [cprop, cert (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
+ val asms_thms = map Thm.assume asms;
- fun prep_subgoal i =
- REPEAT (eresolve_tac @{thms Pair_inject} i)
- THEN Method.insert_tac (case asms_thms of
- thm::thms => (thm RS sym) :: thms) i
- THEN propagate_tac i
- THEN TRY
- ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
- THEN bool_subst_tac ctxt i;
-
- val tac = ALLGOALS prep_subgoal;
+ fun prep_subgoal_tac i =
+ REPEAT (eresolve_tac @{thms Pair_inject} i)
+ THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
+ THEN propagate_tac ctxt i
+ THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
+ THEN bool_subst_tac ctxt i;
- val elim_stripped =
- nth cases idx
- |> Thm.forall_elim @{cterm "P::bool"}
- |> Thm.forall_elim (cterm_of thy args)
- |> Tactic.rule_by_tactic ctxt tac
- |> fold_rev Thm.implies_intr asms
- |> Thm.forall_intr (cterm_of thy rhs_var)
+ val elim_stripped =
+ nth cases idx
+ |> Thm.forall_elim @{cterm "P::bool"}
+ |> Thm.forall_elim (cert args)
+ |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
+ |> fold_rev Thm.implies_intr asms
+ |> Thm.forall_intr (cert rhs_var);
- val bool_elims = (case ranT of
- Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
- | _ => []);
+ val bool_elims =
+ (case ranT of
+ Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
+ | _ => []);
- fun unstrip rl =
- rl |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm
- (map (cterm_of thy) arg_vars))
- |> Thm.forall_intr @{cterm "P::bool"}
-
- in
- map unstrip (elim_stripped :: bool_elims)
- end;
-
+ fun unstrip rl =
+ rl
+ |> fold_rev (Thm.forall_intr o cert) arg_vars
+ |> Thm.forall_intr @{cterm "P::bool"};
+ in
+ map unstrip (elim_stripped :: bool_elims)
+ end;
in
map_index mk_partial_elim_rule fs
end;
--- a/src/Pure/Isar/class_declaration.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/Isar/class_declaration.ML Fri Dec 13 23:53:02 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);
--- a/src/Pure/Isar/element.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/Isar/element.ML Fri Dec 13 23:53:02 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 []],
--- a/src/Pure/Isar/expression.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/Isar/expression.ML Fri Dec 13 23:53:02 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
--- a/src/Pure/Isar/local_theory.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/Isar/local_theory.ML Fri Dec 13 23:53:02 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);
--- a/src/Pure/Isar/proof_context.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/Isar/proof_context.ML Fri Dec 13 23:53:02 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;
--- a/src/Pure/ROOT.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/ROOT.ML Fri Dec 13 23:53:02 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 ();
--- a/src/Pure/assumption.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/assumption.ML Fri Dec 13 23:53:02 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;
--- a/src/Pure/morphism.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/morphism.ML Fri Dec 13 23:53:02 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;
--- a/src/Pure/variable.ML Fri Dec 13 22:54:39 2013 +0800
+++ b/src/Pure/variable.ML Fri Dec 13 23:53:02 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;