author | haftmann |
Sat, 19 Dec 2020 09:33:11 +0000 | |
changeset 72953 | 90ada01470cb |
parent 72952 | 09479be1fe2a |
child 73845 | bfce186331be |
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 |
72953 | 19 |
val revoke_reinitializability: local_theory -> local_theory |
20 |
val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory |
|
20894 | 21 |
end; |
22 |
||
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38349
diff
changeset
|
23 |
structure Named_Target: NAMED_TARGET = |
20894 | 24 |
struct |
25 |
||
21006 | 26 |
(* context data *) |
27 |
||
66333 | 28 |
datatype target = Theory | Locale of string | Class of string; |
29 |
||
66338 | 30 |
fun target_of_ident _ "" = Theory |
31 |
| target_of_ident thy ident = |
|
32 |
if Locale.defined thy ident |
|
33 |
then (if Class.is_class thy ident then Class else Locale) ident |
|
34 |
else error ("No such locale: " ^ quote ident); |
|
35 |
||
66333 | 36 |
fun ident_of_target Theory = "" |
37 |
| ident_of_target (Locale locale) = locale |
|
38 |
| ident_of_target (Class class) = class; |
|
39 |
||
40 |
fun target_is_theory (SOME Theory) = true |
|
41 |
| target_is_theory _ = false; |
|
42 |
||
43 |
fun locale_of_target (SOME (Locale locale)) = SOME locale |
|
44 |
| locale_of_target (SOME (Class locale)) = SOME locale |
|
45 |
| locale_of_target _ = NONE; |
|
46 |
||
47 |
fun class_of_target (SOME (Class class)) = SOME class |
|
48 |
| class_of_target _ = NONE; |
|
49 |
||
33519 | 50 |
structure Data = Proof_Data |
21006 | 51 |
( |
72953 | 52 |
type T = (target * bool) option; |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
53 |
fun init _ = NONE; |
21006 | 54 |
); |
55 |
||
72953 | 56 |
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
|
57 |
|
66333 | 58 |
fun get_target lthy = |
57177
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
59 |
if Local_Theory.level lthy = 1 |
66333 | 60 |
then get_bottom_target lthy |
57177
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
61 |
else NONE; |
21006 | 62 |
|
66333 | 63 |
fun ident_of lthy = |
64 |
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
|
65 |
NONE => error "Not in a named target" |
66333 | 66 |
| 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
|
67 |
|
66333 | 68 |
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
|
69 |
|
66333 | 70 |
val locale_of = locale_of_target o get_target; |
57196 | 71 |
|
66333 | 72 |
val bottom_locale_of = locale_of_target o get_bottom_target; |
57182 | 73 |
|
66333 | 74 |
val class_of = class_of_target o get_target; |
57182 | 75 |
|
72953 | 76 |
fun is_reinitializable lthy = |
77 |
Local_Theory.level lthy = 1 andalso (the_default false o Option.map snd o Data.get) lthy; |
|
78 |
||
21006 | 79 |
|
61777 | 80 |
(* operations *) |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
81 |
|
57074 | 82 |
fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = |
47289 | 83 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
57074 | 84 |
#-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) |
47282 | 85 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
86 |
|
57074 | 87 |
fun class_foundation class (((b, U), mx), (b_def, rhs)) params = |
47289 | 88 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
57074 | 89 |
#-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params |
47282 | 90 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
91 |
|
66338 | 92 |
fun operations Theory = |
93 |
{define = Generic_Target.define Generic_Target.theory_target_foundation, |
|
94 |
notes = Generic_Target.notes Generic_Target.theory_target_notes, |
|
95 |
abbrev = Generic_Target.theory_abbrev, |
|
96 |
declaration = fn _ => Generic_Target.theory_declaration, |
|
72505 | 97 |
theory_registration = Locale.add_registration_theory, |
66338 | 98 |
locale_dependency = fn _ => error "Not possible in theory target", |
99 |
pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, |
|
100 |
Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]} |
|
101 |
| operations (Locale locale) = |
|
102 |
{define = Generic_Target.define (locale_foundation locale), |
|
103 |
notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), |
|
104 |
abbrev = Generic_Target.locale_abbrev locale, |
|
105 |
declaration = Generic_Target.locale_declaration locale, |
|
106 |
theory_registration = fn _ => error "Not possible in locale target", |
|
72505 | 107 |
locale_dependency = Locale.add_dependency locale, |
69057
56c6378ebaea
tuned signature: prefer value-oriented pretty-printing;
wenzelm
parents:
67615
diff
changeset
|
108 |
pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]} |
66338 | 109 |
| operations (Class class) = |
110 |
{define = Generic_Target.define (class_foundation class), |
|
111 |
notes = Generic_Target.notes (Generic_Target.locale_target_notes class), |
|
112 |
abbrev = Class.abbrev class, |
|
113 |
declaration = Generic_Target.locale_declaration class, |
|
114 |
theory_registration = fn _ => error "Not possible in class target", |
|
72505 | 115 |
locale_dependency = Locale.add_dependency class, |
66338 | 116 |
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
|
117 |
|
66338 | 118 |
fun setup_context Theory = Proof_Context.init_global |
119 |
| setup_context (Locale locale) = Locale.init locale |
|
120 |
| setup_context (Class class) = Class.init class; |
|
25269 | 121 |
|
72953 | 122 |
fun setup target includes = |
123 |
setup_context target |
|
124 |
#> Data.put (SOME (target, null includes)) |
|
125 |
#> Bundle.includes includes; |
|
126 |
||
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72516
diff
changeset
|
127 |
fun init includes ident thy = |
39639 | 128 |
let |
66338 | 129 |
val target = target_of_ident thy ident; |
39639 | 130 |
in |
131 |
thy |
|
72516
17dc99589a91
unified Local_Theory.init with Generic_Target.init
haftmann
parents:
72505
diff
changeset
|
132 |
|> Local_Theory.init |
66335
a849ce33923d
treat exit separate from regular local theory operations
haftmann
parents:
66334
diff
changeset
|
133 |
{background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident), |
72953 | 134 |
setup = setup target includes, |
72516
17dc99589a91
unified Local_Theory.init with Generic_Target.init
haftmann
parents:
72505
diff
changeset
|
135 |
conclude = I} |
66338 | 136 |
(operations target) |
39639 | 137 |
end; |
38247 | 138 |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72516
diff
changeset
|
139 |
val theory_init = init [] ""; |
66333 | 140 |
|
69732
49d25343d3d4
combinator to lift local theory update to theory update
haftmann
parents:
69057
diff
changeset
|
141 |
fun theory_map g = theory_init #> g #> Local_Theory.exit_global; |
49d25343d3d4
combinator to lift local theory update to theory update
haftmann
parents:
69057
diff
changeset
|
142 |
|
49d25343d3d4
combinator to lift local theory update to theory update
haftmann
parents:
69057
diff
changeset
|
143 |
fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; |
58665 | 144 |
|
72953 | 145 |
val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false); |
146 |
||
147 |
fun exit_global_reinitialize lthy = |
|
148 |
if is_reinitializable lthy |
|
149 |
then (init [] (ident_of lthy), Local_Theory.exit_global lthy) |
|
150 |
else error "Non-reinitializable local theory context"; |
|
33282 | 151 |
|
20894 | 152 |
end; |