--- a/src/Pure/Isar/class.ML Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/class.ML Wed Jun 09 18:04:21 2021 +0000
@@ -493,7 +493,7 @@
val add_dependency =
(case some_dep_morph of
SOME dep_morph =>
- Locale.add_dependency sub
+ Generic_Target.locale_dependency sub
{inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
mixin = NONE, export = export}
| NONE => I);
@@ -667,7 +667,7 @@
fun registration thy_ctxt {inst, mixin, export} lthy =
lthy
- |> Locale.add_registration_theory
+ |> Generic_Target.theory_registration
{inst = inst,
mixin = mixin,
export = export $> Proof_Context.export_morphism lthy thy_ctxt}
--- a/src/Pure/Isar/class_declaration.ML Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/class_declaration.ML Wed Jun 09 18:04:21 2021 +0000
@@ -331,10 +331,10 @@
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
#-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
- Locale.add_registration_theory'
+ Context.theory_map (Locale.add_registration
{inst = (class, base_morph),
mixin = Option.map (rpair true) eq_morph,
- export = export_morph}
+ export = export_morph})
#> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
#> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
|> snd
--- a/src/Pure/Isar/generic_target.ML Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML Wed Jun 09 18:04:21 2021 +0000
@@ -29,6 +29,8 @@
(morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
+ val local_interpretation: Locale.registration ->
+ local_theory -> local_theory
(*lifting target primitives to local theory operations*)
val define: (((binding * typ) * mixfix) * (binding * term) ->
@@ -54,6 +56,7 @@
val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
local_theory -> (term * term) * local_theory
val theory_declaration: declaration -> local_theory -> local_theory
+ val theory_registration: Locale.registration -> local_theory -> local_theory
(*locale target primitives*)
val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list ->
@@ -71,6 +74,8 @@
local_theory -> local_theory
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
+ val locale_dependency: string -> Locale.registration ->
+ local_theory -> local_theory
end
structure Generic_Target: GENERIC_TARGET =
@@ -230,6 +235,14 @@
fun standard_const pred prmode ((b, mx), rhs) =
standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
+fun local_interpretation registration lthy =
+ let val n = Local_Theory.level lthy in
+ lthy
+ |> Local_Theory.map_contexts (fn level =>
+ level = n - 1 ? Context.proof_map (Locale.add_registration registration))
+ end;
+
+
(** lifting target primitives to local theory operations **)
@@ -393,6 +406,8 @@
fun theory_declaration decl =
background_declaration decl #> standard_declaration (K true) decl;
+val theory_registration = Local_Theory.raw_theory o Context.theory_map o Locale.add_registration;
+
(** locale target primitives **)
@@ -424,6 +439,10 @@
locale_target_const locale (K true) prmode ((b, mx), rhs)
#> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
+fun locale_dependency loc registration =
+ Local_Theory.raw_theory (Locale.add_dependency loc registration)
+ #> local_interpretation registration;
+
(** locale abbreviations **)
--- a/src/Pure/Isar/interpretation.ML Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/interpretation.ML Wed Jun 09 18:04:21 2021 +0000
@@ -140,11 +140,16 @@
(fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
"interpret" propss eqns goal_ctxt state;
+fun add_registration_proof registration ctxt = ctxt
+ |> Proof_Context.set_stmt false
+ |> Context.proof_map (Locale.add_registration registration)
+ |> Proof_Context.restore_stmt ctxt;
+
fun gen_interpret prep_interpretation expression state =
Proof.assert_forward_or_chain state
|> Proof.context_of
|> generic_interpretation prep_interpretation (setup_proof state)
- Attrib.local_notes Locale.add_registration_proof expression [];
+ Attrib.local_notes add_registration_proof expression [];
in
@@ -157,7 +162,7 @@
(* interpretation in local theories *)
val add_registration_local_theory =
- Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory;
+ Named_Target.revoke_reinitializability oo Generic_Target.local_interpretation;
fun interpretation expression =
generic_interpretation cert_interpretation Element.witness_proof_eqs
--- a/src/Pure/Isar/locale.ML Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/locale.ML Wed Jun 09 18:04:21 2021 +0000
@@ -79,13 +79,8 @@
type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism}
val amend_registration: registration -> Context.generic -> Context.generic
val add_registration: registration -> Context.generic -> Context.generic
- val add_registration_theory': registration -> theory -> theory
- val add_registration_theory: registration -> local_theory -> local_theory
- val add_registration_local_theory: registration -> local_theory -> local_theory
- val add_registration_proof: registration -> Proof.context -> Proof.context
val registrations_of: Context.generic -> string -> (string * morphism) list
- val add_dependency': string -> registration -> theory -> theory
- val add_dependency: string -> registration -> local_theory -> local_theory
+ val add_dependency: string -> registration -> theory -> theory
(* Diagnostic *)
val get_locales: theory -> string list
@@ -611,21 +606,6 @@
|> activate_facts (SOME export) (name, mix_morph $> pos_morph)
end;
-val add_registration_theory' = Context.theory_map o add_registration;
-
-val add_registration_theory = Local_Theory.raw_theory o add_registration_theory';
-
-fun add_registration_local_theory registration lthy =
- let val n = Local_Theory.level lthy in
- lthy
- |> Local_Theory.map_contexts (fn level =>
- level = n - 1 ? Context.proof_map (add_registration registration))
- end;
-
-fun add_registration_proof registration ctxt = ctxt
- |> Proof_Context.set_stmt false
- |> Context.proof_map (add_registration registration)
- |> Proof_Context.restore_stmt ctxt;
(*** Dependencies ***)
@@ -637,7 +617,7 @@
|> map (fn (name, (base, export)) =>
(name, base $> (collect_mixins context (name, base $> export)) $> export));
-fun add_dependency' loc {inst = (name, morph), mixin, export} thy =
+fun add_dependency loc {inst = (name, morph), mixin, export} thy =
let
val dep = make_dep (name, (morph, export));
val add_dep =
@@ -649,13 +629,10 @@
fold_rev (roundup thy' cons export)
(registrations_of context' loc) (Idents.get context', []);
in
- fold_rev (fn inst => add_registration_theory' {inst = inst, mixin = NONE, export = export})
+ fold_rev (fn inst => Context.theory_map (add_registration {inst = inst, mixin = NONE, export = export}))
regs thy'
end;
-fun add_dependency loc registration =
- Local_Theory.raw_theory (add_dependency' loc registration)
- #> add_registration_local_theory registration;
(*** Storing results ***)
--- a/src/Pure/Isar/named_target.ML Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/named_target.ML Wed Jun 09 18:04:21 2021 +0000
@@ -94,7 +94,7 @@
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.theory_abbrev,
declaration = fn _ => Generic_Target.theory_declaration,
- theory_registration = Locale.add_registration_theory,
+ theory_registration = Generic_Target.theory_registration,
locale_dependency = fn _ => error "Not possible in theory target",
pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
@@ -104,7 +104,7 @@
abbrev = Generic_Target.locale_abbrev locale,
declaration = Generic_Target.locale_declaration locale,
theory_registration = fn _ => error "Not possible in locale target",
- locale_dependency = Locale.add_dependency locale,
+ locale_dependency = Generic_Target.locale_dependency locale,
pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]}
| operations (Class class) =
{define = Generic_Target.define (class_foundation class),
@@ -112,7 +112,7 @@
abbrev = Class.abbrev class,
declaration = Generic_Target.locale_declaration class,
theory_registration = fn _ => error "Not possible in class target",
- locale_dependency = Locale.add_dependency class,
+ locale_dependency = Generic_Target.locale_dependency class,
pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class};
fun setup_context Theory = Proof_Context.init_global
--- a/src/Pure/Isar/overloading.ML Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/overloading.ML Wed Jun 09 18:04:21 2021 +0000
@@ -210,7 +210,7 @@
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
declaration = K Generic_Target.theory_declaration,
- theory_registration = Locale.add_registration_theory,
+ theory_registration = Generic_Target.theory_registration,
locale_dependency = fn _ => error "Not possible in overloading target",
pretty = pretty}
end;