--- a/src/Doc/Isar_Ref/Spec.thy Thu May 18 15:34:01 2023 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu May 18 17:21:29 2023 +0200
@@ -417,7 +417,7 @@
@@{command declare} (@{syntax thms} + @'and')
\<close>
- \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>declaration\<close>, to the current local theory under construction. In later
+ \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>Morphism.declaration_fn\<close>, to the current local theory under construction. In later
application contexts, the function is transformed according to the morphisms
being involved in the interpretation hierarchy.
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu May 18 17:21:29 2023 +0200
@@ -15,7 +15,7 @@
val funs: thm ->
{isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
whatis: morphism -> cterm -> cterm -> ord,
- simpset: morphism -> Proof.context -> simpset} -> declaration
+ simpset: morphism -> Proof.context -> simpset} -> Morphism.declaration_fn
val match: Proof.context -> cterm -> entry option
end;
--- a/src/HOL/Tools/Function/partial_function.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Thu May 18 17:21:29 2023 +0200
@@ -6,7 +6,7 @@
signature PARTIAL_FUNCTION =
sig
- val init: string -> term -> term -> thm -> thm -> thm option -> declaration
+ val init: string -> term -> term -> thm -> thm -> thm option -> Morphism.declaration_fn
val mono_tac: Proof.context -> int -> tactic
val add_partial_function: string -> (binding * typ option * mixfix) list ->
Attrib.binding * term -> local_theory -> (term * thm) * local_theory
--- a/src/HOL/Tools/groebner.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/HOL/Tools/groebner.ML Thu May 18 17:21:29 2023 +0200
@@ -781,7 +781,7 @@
in
Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
{lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
- proc = fn _ => fn _ => proc}
+ proc = Morphism.entity (fn _ => fn _ => proc)}
end;
val poly_eq_ss =
--- a/src/Pure/Isar/args.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/Isar/args.ML Thu May 18 17:21:29 2023 +0200
@@ -36,15 +36,15 @@
val internal_typ: typ parser
val internal_term: term parser
val internal_fact: thm list parser
- val internal_attribute: (morphism -> attribute) parser
- val internal_declaration: declaration parser
+ val internal_attribute: attribute Morphism.entity parser
+ val internal_declaration: Morphism.declaration parser
val named_source: (Token.T -> Token.src) -> Token.src parser
val named_typ: (string -> typ) -> typ parser
val named_term: (string -> term) -> term parser
val named_fact: (string -> string option * thm list) -> thm list parser
- val named_attribute: (string * Position.T -> morphism -> attribute) ->
- (morphism -> attribute) parser
- val embedded_declaration: (Input.source -> declaration) -> declaration parser
+ val named_attribute: (string * Position.T -> attribute Morphism.entity) ->
+ attribute Morphism.entity parser
+ val embedded_declaration: (Input.source -> Morphism.declaration) -> Morphism.declaration parser
val typ_abbrev: typ context_parser
val typ: typ context_parser
val term: term context_parser
--- a/src/Pure/Isar/attrib.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/Isar/attrib.ML Thu May 18 17:21:29 2023 +0200
@@ -49,7 +49,7 @@
val attribute_setup: bstring * Position.T -> Input.source -> string ->
local_theory -> local_theory
val internal: (morphism -> attribute) -> Token.src
- val internal_declaration: declaration -> thms
+ val internal_declaration: Morphism.declaration -> thms
val add_del: attribute -> attribute -> attribute context_parser
val thm: thm context_parser
val thms: thm list context_parser
@@ -257,10 +257,8 @@
in
-fun internal att = internal_source (Token.Attribute att);
-
-fun internal_declaration decl =
- [([Drule.dummy_thm], [internal_source (Token.Declaration decl)])];
+fun internal arg = internal_source (Token.Attribute (Morphism.entity arg));
+fun internal_declaration arg = [([Drule.dummy_thm], [internal_source (Token.Declaration arg)])];
end;
@@ -442,7 +440,8 @@
fun register binding config thy =
let val name = Sign.full_name thy binding in
thy
- |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option"
+ |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form_entity)
+ "configuration option"
|> Configs.map (Symtab.update (name, config))
end;
--- a/src/Pure/Isar/generic_target.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/Isar/generic_target.ML Thu May 18 17:21:29 2023 +0200
@@ -16,7 +16,7 @@
(*background primitives*)
val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
- val background_declaration: declaration -> local_theory -> local_theory
+ val background_declaration: Morphism.declaration -> local_theory -> local_theory
val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
val add_foundation_interpretation: (binding * (term * term list) -> Context.generic -> Context.generic) ->
theory -> theory
@@ -25,8 +25,8 @@
val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list
val standard_notes: (int * int -> bool) -> string -> Attrib.fact list ->
local_theory -> local_theory
- val standard_declaration: (int * int -> bool) ->
- (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
+ val standard_declaration: (int * int -> bool) -> Morphism.declaration ->
+ local_theory -> local_theory
val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
val local_interpretation: Locale.registration ->
@@ -55,7 +55,7 @@
(*theory target operations*)
val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
local_theory -> (term * term) * local_theory
- val theory_declaration: declaration -> local_theory -> local_theory
+ val theory_declaration: Morphism.declaration -> local_theory -> local_theory
val theory_registration: Locale.registration -> local_theory -> local_theory
(*locale target primitives*)
@@ -63,14 +63,15 @@
local_theory -> local_theory
val locale_target_abbrev: string -> Syntax.mode ->
(binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory
- val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
+ val locale_target_declaration: string -> bool -> Morphism.declaration ->
+ local_theory -> local_theory
val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
(binding * mixfix) * term -> local_theory -> local_theory
(*locale operations*)
val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> (term * term) * local_theory
- val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
+ val locale_declaration: string -> {syntax: bool, pervasive: bool} -> Morphism.declaration ->
local_theory -> local_theory
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
@@ -123,7 +124,7 @@
| same_const (t $ _, t' $ _) = same_const (t, t')
| same_const (_, _) = false;
-fun const_decl phi_pred prmode ((b, mx), rhs) phi context =
+fun const_decl phi_pred prmode ((b, mx), rhs) = Morphism.entity (fn phi => fn context =>
if phi_pred phi then
let
val b' = Morphism.binding phi b;
@@ -149,7 +150,7 @@
SOME c =>
context
|> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c)
- |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)])
+ |> Morphism.form_entity (Proof_Context.generic_notation true prmode [(rhs', mx)])
| NONE =>
context
|> Proof_Context.generic_add_abbrev Print_Mode.internal
@@ -157,9 +158,9 @@
|-> (fn (const as Const (c, _), _) => same_stem ?
(Proof_Context.generic_revert_abbrev (#1 prmode) c #>
same_shape ?
- Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
+ Morphism.form_entity (Proof_Context.generic_notation true prmode [(const, mx)]))))
end
- else context;
+ else context);
--- a/src/Pure/Isar/local_theory.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/Isar/local_theory.ML Thu May 18 17:21:29 2023 +0200
@@ -34,7 +34,7 @@
val reset_group: local_theory -> local_theory
val standard_morphism: local_theory -> Proof.context -> morphism
val standard_morphism_theory: local_theory -> morphism
- val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
+ val standard_form: local_theory -> Proof.context -> 'a Morphism.entity -> 'a
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
@@ -55,7 +55,8 @@
(string * thm list) list * local_theory
val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
+ val declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration_fn ->
+ local_theory -> local_theory
val theory_registration: Locale.registration -> local_theory -> local_theory
val locale_dependency: Locale.registration -> local_theory -> local_theory
val pretty: local_theory -> Pretty.T list
@@ -102,7 +103,8 @@
notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory,
abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory,
- declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
+ declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration ->
+ local_theory -> local_theory,
theory_registration: Locale.registration -> local_theory -> local_theory,
locale_dependency: Locale.registration -> local_theory -> local_theory,
pretty: local_theory -> Pretty.T list};
@@ -280,7 +282,7 @@
val define = operation2 #define false;
val define_internal = operation2 #define true;
val notes_kind = operation2 #notes;
-val declaration = operation2 #declaration;
+fun declaration args = operation2 #declaration args o Morphism.entity;
val theory_registration = operation1 #theory_registration;
fun locale_dependency registration =
assert_bottom #> operation1 #locale_dependency registration;
--- a/src/Pure/Isar/locale.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/Isar/locale.ML Thu May 18 17:21:29 2023 +0200
@@ -39,7 +39,7 @@
term option * term list ->
thm option * thm option -> thm list ->
Element.context_i list ->
- declaration list ->
+ Morphism.declaration list ->
(string * Attrib.fact list) list ->
(string * morphism) list -> theory -> theory
val locale_space: theory -> Name_Space.T
@@ -59,7 +59,7 @@
(* Storing results *)
val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
- val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
+ val add_declaration: string -> bool -> Morphism.declaration -> Proof.context -> Proof.context
(* Activation *)
val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
@@ -152,7 +152,7 @@
(* dynamic part *)
(*syntax declarations*)
- syntax_decls: (declaration * serial) list,
+ syntax_decls: (Morphism.declaration * serial) list,
(*theorem declarations*)
notes: ((string * Attrib.fact list) * serial) list,
(*locale dependencies (sublocale relation) in reverse order*)
@@ -501,7 +501,7 @@
val {syntax_decls, ...} = the_locale thy name;
in
context
- |> fold_rev (fn (decl, _) => decl morph) syntax_decls
+ |> fold_rev (Morphism.form o Morphism.transform morph o #1) syntax_decls
handle ERROR msg => activate_err msg "syntax" (name, morph) context
end;
--- a/src/Pure/Isar/method.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/Isar/method.ML Thu May 18 17:21:29 2023 +0200
@@ -335,8 +335,9 @@
ML_Lex.read_source source @ ML_Lex.read ")))")
|> the_tactic;
in
- fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi))
- end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
+ Morphism.entity (fn phi =>
+ set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi)))
+ end)) >> (fn decl => Morphism.form_entity (the_tactic (Morphism.form decl context))));
(* method facts *)
@@ -608,9 +609,10 @@
Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
|> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
- fun decl phi =
- Context.mapping I init #>
- Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
+ val decl =
+ Morphism.entity (fn phi =>
+ Context.mapping I init #>
+ Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd);
val modifier_report =
(#1 (Token.range_of modifier_toks),
--- a/src/Pure/Isar/token.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/Isar/token.ML Thu May 18 17:21:29 2023 +0200
@@ -29,8 +29,8 @@
Typ of typ |
Term of term |
Fact of string option * thm list |
- Attribute of morphism -> attribute |
- Declaration of declaration |
+ Attribute of attribute Morphism.entity |
+ Declaration of Morphism.declaration |
Files of file Exn.result list |
Output of XML.body option
val pos_of: T -> Position.T
@@ -197,8 +197,8 @@
Typ of typ |
Term of term |
Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*)
- Attribute of morphism -> attribute |
- Declaration of declaration |
+ Attribute of attribute Morphism.entity |
+ Declaration of Morphism.declaration |
Files of file Exn.result list |
Output of XML.body option;
--- a/src/Pure/morphism.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/morphism.ML Thu May 18 17:21:29 2023 +0200
@@ -9,7 +9,6 @@
signature BASIC_MORPHISM =
sig
type morphism
- type declaration = morphism -> Context.generic -> Context.generic
val $> : morphism * morphism -> morphism
end
@@ -40,8 +39,13 @@
val identity: morphism
val default: morphism option -> morphism
val compose: morphism -> morphism -> morphism
- val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
- val form: (morphism -> 'a) -> 'a
+ type 'a entity
+ val entity: (morphism -> 'a) -> 'a entity
+ val transform: morphism -> 'a entity -> 'a entity
+ val form: 'a entity -> 'a
+ val form_entity: (morphism -> 'a) -> 'a
+ type declaration = (Context.generic -> Context.generic) entity
+ type declaration_fn = morphism -> Context.generic -> Context.generic
val binding_morphism: string -> (binding -> binding) -> morphism
val typ_morphism': string -> (theory -> typ -> typ) -> morphism
val typ_morphism: string -> (typ -> typ) -> morphism
@@ -95,8 +99,6 @@
term: term funs,
fact: thm list funs};
-type declaration = morphism -> Context.generic -> Context.generic;
-
fun rep (Morphism args) = args;
fun apply which phi =
@@ -166,8 +168,18 @@
fun phi1 $> phi2 = compose phi2 phi1;
-fun transform phi f = fn psi => f (phi $> psi);
-fun form f = f identity;
+
+(* abstract entities *)
+
+datatype 'a entity = Entity of morphism -> 'a
+fun entity f = Entity f;
+
+fun transform phi (Entity f) = Entity (fn psi => f (phi $> psi));
+fun form (Entity f) = f identity;
+fun form_entity f = f identity;
+
+type declaration = (Context.generic -> Context.generic) entity;
+type declaration_fn = morphism -> Context.generic -> Context.generic;
(* concrete morphisms *)
--- a/src/Pure/raw_simplifier.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/raw_simplifier.ML Thu May 18 17:21:29 2023 +0200
@@ -36,7 +36,7 @@
type simproc
val eq_simproc: simproc * simproc -> bool
val cert_simproc: theory -> string ->
- {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
+ {lhss: term list, proc: (Proof.context -> cterm -> thm option) Morphism.entity} -> simproc
val transform_simproc: morphism -> simproc -> simproc
val simpset_of: Proof.context -> simpset
val put_simpset: simpset -> Proof.context -> Proof.context
@@ -710,7 +710,7 @@
Simproc of
{name: string,
lhss: term list,
- proc: morphism -> Proof.context -> cterm -> thm option,
+ proc: (Proof.context -> cterm -> thm option) Morphism.entity,
stamp: stamp};
fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
--- a/src/Pure/simplifier.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/simplifier.ML Thu May 18 17:21:29 2023 +0200
@@ -128,7 +128,8 @@
val ctxt' = fold Proof_Context.augment lhss ctxt;
val lhss' = Variable.export_terms ctxt' ctxt lhss;
in
- cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
+ cert_simproc (Proof_Context.theory_of ctxt) name
+ {lhss = lhss', proc = Morphism.entity proc}
end;
local
@@ -311,8 +312,8 @@
val add_del =
(Args.del -- Args.colon >> K (op delsimprocs) ||
Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
- >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
- (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc])))));
+ >> (fn f => fn simproc => Morphism.entity (fn phi => Thm.declaration_attribute
+ (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc]))))));
in