author | wenzelm |
Thu, 06 Jun 2024 22:26:40 +0200 | |
changeset 80274 | cff00b3dddf5 |
parent 78798 | 200daaab2578 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: Pure/Isar/named_target.ML |
20894 | 2 |
Author: Makarius |
30437 | 3 |
Author: Florian Haftmann, TU Muenchen |
20894 | 4 |
|
66338 | 5 |
Targets for theory, locale, class -- at the bottom of the nested structure. |
20894 | 6 |
*) |
7 |
||
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38349
diff
changeset
|
8 |
signature NAMED_TARGET = |
20894 | 9 |
sig |
52140 | 10 |
val is_theory: local_theory -> bool |
57182 | 11 |
val locale_of: local_theory -> string option |
57195
ec0e10f11276
recovered level-free fishing for locale, accidentally lost in dce365931721
haftmann
parents:
57193
diff
changeset
|
12 |
val bottom_locale_of: local_theory -> string option |
57182 | 13 |
val class_of: local_theory -> string option |
72605 | 14 |
val init: Bundle.name list -> string -> theory -> local_theory |
38388 | 15 |
val theory_init: theory -> local_theory |
58665 | 16 |
val theory_map: (local_theory -> local_theory) -> theory -> theory |
69732
49d25343d3d4
combinator to lift local theory update to theory update
haftmann
parents:
69057
diff
changeset
|
17 |
val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> |
49d25343d3d4
combinator to lift local theory update to theory update
haftmann
parents:
69057
diff
changeset
|
18 |
theory -> 'b * theory |
78798
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78795
diff
changeset
|
19 |
val setup: (local_theory -> local_theory) -> unit |
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78795
diff
changeset
|
20 |
val setup_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> 'b |
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78795
diff
changeset
|
21 |
val setup_result0: (local_theory -> 'a * local_theory) -> 'a |
72953 | 22 |
val revoke_reinitializability: local_theory -> local_theory |
23 |
val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory |
|
20894 | 24 |
end; |
25 |
||
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38349
diff
changeset
|
26 |
structure Named_Target: NAMED_TARGET = |
20894 | 27 |
struct |
28 |
||
21006 | 29 |
(* context data *) |
30 |
||
66333 | 31 |
datatype target = Theory | Locale of string | Class of string; |
32 |
||
66338 | 33 |
fun target_of_ident _ "" = Theory |
34 |
| target_of_ident thy ident = |
|
35 |
if Locale.defined thy ident |
|
36 |
then (if Class.is_class thy ident then Class else Locale) ident |
|
37 |
else error ("No such locale: " ^ quote ident); |
|
38 |
||
66333 | 39 |
fun ident_of_target Theory = "" |
40 |
| ident_of_target (Locale locale) = locale |
|
41 |
| ident_of_target (Class class) = class; |
|
42 |
||
43 |
fun target_is_theory (SOME Theory) = true |
|
44 |
| target_is_theory _ = false; |
|
45 |
||
46 |
fun locale_of_target (SOME (Locale locale)) = SOME locale |
|
47 |
| locale_of_target (SOME (Class locale)) = SOME locale |
|
48 |
| locale_of_target _ = NONE; |
|
49 |
||
50 |
fun class_of_target (SOME (Class class)) = SOME class |
|
51 |
| class_of_target _ = NONE; |
|
52 |
||
33519 | 53 |
structure Data = Proof_Data |
21006 | 54 |
( |
72953 | 55 |
type T = (target * bool) option; |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
56 |
fun init _ = NONE; |
21006 | 57 |
); |
58 |
||
72953 | 59 |
val get_bottom_target = Option.map fst o Data.get; |
57195
ec0e10f11276
recovered level-free fishing for locale, accidentally lost in dce365931721
haftmann
parents:
57193
diff
changeset
|
60 |
|
66333 | 61 |
fun get_target lthy = |
57177
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
62 |
if Local_Theory.level lthy = 1 |
66333 | 63 |
then get_bottom_target lthy |
57177
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
64 |
else NONE; |
21006 | 65 |
|
66333 | 66 |
fun ident_of lthy = |
67 |
case get_target lthy of |
|
57484
cc309f3c0490
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
haftmann
parents:
57483
diff
changeset
|
68 |
NONE => error "Not in a named target" |
66333 | 69 |
| SOME target => ident_of_target target; |
57484
cc309f3c0490
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
haftmann
parents:
57483
diff
changeset
|
70 |
|
66333 | 71 |
val is_theory = target_is_theory o get_target; |
57195
ec0e10f11276
recovered level-free fishing for locale, accidentally lost in dce365931721
haftmann
parents:
57193
diff
changeset
|
72 |
|
66333 | 73 |
val locale_of = locale_of_target o get_target; |
57196 | 74 |
|
66333 | 75 |
val bottom_locale_of = locale_of_target o get_bottom_target; |
57182 | 76 |
|
66333 | 77 |
val class_of = class_of_target o get_target; |
57182 | 78 |
|
72953 | 79 |
fun is_reinitializable lthy = |
80 |
Local_Theory.level lthy = 1 andalso (the_default false o Option.map snd o Data.get) lthy; |
|
81 |
||
21006 | 82 |
|
61777 | 83 |
(* operations *) |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
84 |
|
57074 | 85 |
fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = |
47289 | 86 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
57074 | 87 |
#-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) |
47282 | 88 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
89 |
|
57074 | 90 |
fun class_foundation class (((b, U), mx), (b_def, rhs)) params = |
47289 | 91 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
57074 | 92 |
#-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params |
47282 | 93 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
94 |
|
66338 | 95 |
fun operations Theory = |
96 |
{define = Generic_Target.define Generic_Target.theory_target_foundation, |
|
97 |
notes = Generic_Target.notes Generic_Target.theory_target_notes, |
|
98 |
abbrev = Generic_Target.theory_abbrev, |
|
99 |
declaration = fn _ => Generic_Target.theory_declaration, |
|
73845 | 100 |
theory_registration = Generic_Target.theory_registration, |
66338 | 101 |
locale_dependency = fn _ => error "Not possible in theory target", |
102 |
pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, |
|
77889
5db014c36f42
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
wenzelm
parents:
73845
diff
changeset
|
103 |
Pretty.str (Context.theory_base_name (Proof_Context.theory_of ctxt))]]} |
66338 | 104 |
| operations (Locale locale) = |
105 |
{define = Generic_Target.define (locale_foundation locale), |
|
106 |
notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), |
|
107 |
abbrev = Generic_Target.locale_abbrev locale, |
|
108 |
declaration = Generic_Target.locale_declaration locale, |
|
109 |
theory_registration = fn _ => error "Not possible in locale target", |
|
73845 | 110 |
locale_dependency = Generic_Target.locale_dependency locale, |
69057
56c6378ebaea
tuned signature: prefer value-oriented pretty-printing;
wenzelm
parents:
67615
diff
changeset
|
111 |
pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]} |
66338 | 112 |
| operations (Class class) = |
113 |
{define = Generic_Target.define (class_foundation class), |
|
114 |
notes = Generic_Target.notes (Generic_Target.locale_target_notes class), |
|
115 |
abbrev = Class.abbrev class, |
|
116 |
declaration = Generic_Target.locale_declaration class, |
|
117 |
theory_registration = fn _ => error "Not possible in class target", |
|
73845 | 118 |
locale_dependency = Generic_Target.locale_dependency class, |
66338 | 119 |
pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class}; |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
120 |
|
66338 | 121 |
fun setup_context Theory = Proof_Context.init_global |
122 |
| setup_context (Locale locale) = Locale.init locale |
|
123 |
| setup_context (Class class) = Class.init class; |
|
25269 | 124 |
|
72953 | 125 |
fun setup target includes = |
126 |
setup_context target |
|
127 |
#> Data.put (SOME (target, null includes)) |
|
128 |
#> Bundle.includes includes; |
|
129 |
||
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72516
diff
changeset
|
130 |
fun init includes ident thy = |
39639 | 131 |
let |
66338 | 132 |
val target = target_of_ident thy ident; |
39639 | 133 |
in |
134 |
thy |
|
72516
17dc99589a91
unified Local_Theory.init with Generic_Target.init
haftmann
parents:
72505
diff
changeset
|
135 |
|> Local_Theory.init |
66335
a849ce33923d
treat exit separate from regular local theory operations
haftmann
parents:
66334
diff
changeset
|
136 |
{background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident), |
72953 | 137 |
setup = setup target includes, |
72516
17dc99589a91
unified Local_Theory.init with Generic_Target.init
haftmann
parents:
72505
diff
changeset
|
138 |
conclude = I} |
66338 | 139 |
(operations target) |
39639 | 140 |
end; |
38247 | 141 |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72516
diff
changeset
|
142 |
val theory_init = init [] ""; |
66333 | 143 |
|
69732
49d25343d3d4
combinator to lift local theory update to theory update
haftmann
parents:
69057
diff
changeset
|
144 |
fun theory_map g = theory_init #> g #> Local_Theory.exit_global; |
78795
f7e972d567f3
clarified signature: more concise variations on implicit theory setup;
wenzelm
parents:
77889
diff
changeset
|
145 |
fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; |
69732
49d25343d3d4
combinator to lift local theory update to theory update
haftmann
parents:
69057
diff
changeset
|
146 |
|
78798
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78795
diff
changeset
|
147 |
fun setup g = Context.>> (Context.mapping (theory_map g) g); |
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78795
diff
changeset
|
148 |
fun setup_result f g = |
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78795
diff
changeset
|
149 |
Context.>>> (Context.mapping_result (theory_map_result f g) (g #>> f Morphism.identity)); |
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78795
diff
changeset
|
150 |
fun setup_result0 g = setup_result (K I) g; |
58665 | 151 |
|
72953 | 152 |
val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false); |
153 |
||
154 |
fun exit_global_reinitialize lthy = |
|
155 |
if is_reinitializable lthy |
|
156 |
then (init [] (ident_of lthy), Local_Theory.exit_global lthy) |
|
157 |
else error "Non-reinitializable local theory context"; |
|
33282 | 158 |
|
20894 | 159 |
end; |