# HG changeset patch # User wenzelm # Date 1684423289 -7200 # Node ID 001739cb8d087d9a2ad6a76ff05062a54a482e22 # Parent 61a1bf9eb0ce4bcc4d19e60c45077319cabcc51f clarified signature: more explicit types; diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Doc/Isar_Ref/Spec.thy --- 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') \ - \<^descr> \<^theory_text>\declaration d\ adds the declaration function \d\ of ML type \<^ML_type>\declaration\, to the current local theory under construction. In later + \<^descr> \<^theory_text>\declaration d\ adds the declaration function \d\ of ML type \<^ML_type>\Morphism.declaration_fn\, 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. diff -r 61a1bf9eb0ce -r 001739cb8d08 src/HOL/Decision_Procs/ferrante_rackoff_data.ML --- 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; diff -r 61a1bf9eb0ce -r 001739cb8d08 src/HOL/Tools/Function/partial_function.ML --- 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 diff -r 61a1bf9eb0ce -r 001739cb8d08 src/HOL/Tools/groebner.ML --- 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 = diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/Isar/args.ML --- 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 diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/Isar/attrib.ML --- 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; diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/Isar/generic_target.ML --- 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); diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/Isar/local_theory.ML --- 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; diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/Isar/locale.ML --- 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; diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/Isar/method.ML --- 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), diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/Isar/token.ML --- 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; diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/morphism.ML --- 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 *) diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/raw_simplifier.ML --- 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; diff -r 61a1bf9eb0ce -r 001739cb8d08 src/Pure/simplifier.ML --- 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