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