author | haftmann |
Mon, 06 Feb 2017 20:56:34 +0100 | |
changeset 64990 | c6a7de505796 |
parent 63402 | f199837304d7 |
child 66259 | b5279a21e658 |
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 |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47061
diff
changeset
|
5 |
Targets for theory, locale, class -- at the bottom 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 |
63402 | 14 |
val init: (local_theory -> local_theory) option -> string -> theory -> local_theory |
38388 | 15 |
val theory_init: theory -> local_theory |
58665 | 16 |
val theory_map: (local_theory -> local_theory) -> theory -> theory |
57483
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
17 |
val begin: xstring * Position.T -> theory -> local_theory |
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
18 |
val exit: local_theory -> theory |
63402 | 19 |
val switch: (xstring * Position.T) option -> Context.generic -> |
20 |
(local_theory -> Context.generic) * local_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 |
||
33519 | 28 |
structure Data = Proof_Data |
21006 | 29 |
( |
57196 | 30 |
type T = (string * bool) option; |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
31 |
fun init _ = NONE; |
21006 | 32 |
); |
33 |
||
57196 | 34 |
val get_bottom_data = Data.get; |
57195
ec0e10f11276
recovered level-free fishing for locale, accidentally lost in dce365931721
haftmann
parents:
57193
diff
changeset
|
35 |
|
ec0e10f11276
recovered level-free fishing for locale, accidentally lost in dce365931721
haftmann
parents:
57193
diff
changeset
|
36 |
fun get_data lthy = |
57177
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
37 |
if Local_Theory.level lthy = 1 |
57195
ec0e10f11276
recovered level-free fishing for locale, accidentally lost in dce365931721
haftmann
parents:
57193
diff
changeset
|
38 |
then get_bottom_data lthy |
57177
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
39 |
else NONE; |
21006 | 40 |
|
57185 | 41 |
fun is_theory lthy = |
63268 | 42 |
(case get_data lthy of |
57196 | 43 |
SOME ("", _) => true |
63268 | 44 |
| _ => false); |
52140 | 45 |
|
57484
cc309f3c0490
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
haftmann
parents:
57483
diff
changeset
|
46 |
fun target_of lthy = |
63268 | 47 |
(case get_data 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
|
48 |
NONE => error "Not in a named target" |
63268 | 49 |
| SOME (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
|
50 |
|
57196 | 51 |
fun locale_name_of NONE = NONE |
52 |
| locale_name_of (SOME ("", _)) = NONE |
|
53 |
| locale_name_of (SOME (locale, _)) = SOME locale; |
|
57195
ec0e10f11276
recovered level-free fishing for locale, accidentally lost in dce365931721
haftmann
parents:
57193
diff
changeset
|
54 |
|
57196 | 55 |
val locale_of = locale_name_of o get_data; |
56 |
||
57 |
val bottom_locale_of = locale_name_of o get_bottom_data; |
|
57182 | 58 |
|
59 |
fun class_of lthy = |
|
63268 | 60 |
(case get_data lthy of |
57196 | 61 |
SOME (class, true) => SOME class |
63268 | 62 |
| _ => NONE); |
57182 | 63 |
|
21006 | 64 |
|
61777 | 65 |
(* operations *) |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
66 |
|
57074 | 67 |
fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = |
47289 | 68 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
57074 | 69 |
#-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) |
47282 | 70 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
71 |
|
57074 | 72 |
fun class_foundation class (((b, U), mx), (b_def, rhs)) params = |
47289 | 73 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
57074 | 74 |
#-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params |
47282 | 75 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
76 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60244
diff
changeset
|
77 |
fun foundation ("", _) = Generic_Target.theory_target_foundation |
57196 | 78 |
| foundation (locale, false) = locale_foundation locale |
79 |
| foundation (class, true) = class_foundation class; |
|
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
80 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60244
diff
changeset
|
81 |
fun notes ("", _) = Generic_Target.theory_target_notes |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60244
diff
changeset
|
82 |
| notes (locale, _) = Generic_Target.locale_target_notes locale; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
83 |
|
60344
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60341
diff
changeset
|
84 |
fun abbrev ("", _) = Generic_Target.theory_abbrev |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60341
diff
changeset
|
85 |
| abbrev (locale, false) = Generic_Target.locale_abbrev locale |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60341
diff
changeset
|
86 |
| abbrev (class, true) = Class.abbrev class; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
87 |
|
62239 | 88 |
fun declaration ("", _) _ decl = Generic_Target.theory_declaration decl |
57196 | 89 |
| declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl; |
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
90 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
91 |
fun theory_registration ("", _) = Generic_Target.theory_registration |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
92 |
| theory_registration _ = (fn _ => error "Not possible in theory target"); |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
93 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
94 |
fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target") |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
95 |
| locale_dependency ("", true) = (fn _ => error "Not possible in class target") |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
96 |
| locale_dependency (locale, _) = Generic_Target.locale_dependency locale; |
56723
a8f71445c265
subscription as target-specific implementation device
haftmann
parents:
56056
diff
changeset
|
97 |
|
57196 | 98 |
fun pretty (target, is_class) ctxt = |
60244 | 99 |
if target = "" then |
100 |
[Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, |
|
101 |
Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]] |
|
102 |
else if is_class then Class.pretty_specification (Proof_Context.theory_of ctxt) target |
|
103 |
else |
|
104 |
(* FIXME pretty locale content *) |
|
105 |
let |
|
106 |
val target_name = [Pretty.keyword1 "locale", Pretty.brk 1, Locale.pretty_name ctxt target]; |
|
107 |
val fixes = |
|
108 |
map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) |
|
109 |
(#1 (Proof_Context.inferred_fixes ctxt)); |
|
110 |
val assumes = |
|
63352 | 111 |
map (fn A => (Binding.empty_atts, [(Thm.term_of A, [])])) |
60244 | 112 |
(Assumption.all_assms_of ctxt); |
113 |
val elems = |
|
114 |
(if null fixes then [] else [Element.Fixes fixes]) @ |
|
115 |
(if null assumes then [] else [Element.Assumes assumes]); |
|
116 |
in |
|
117 |
if null elems then [Pretty.block target_name] |
|
39639 | 118 |
else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: |
60244 | 119 |
map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))] |
120 |
end; |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
121 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
122 |
|
38378 | 123 |
(* init *) |
25291 | 124 |
|
57196 | 125 |
fun make_name_data _ "" = ("", false) |
126 |
| make_name_data thy target = |
|
127 |
if Locale.defined thy target |
|
128 |
then (target, Class.is_class thy target) |
|
129 |
else error ("No such locale: " ^ quote target); |
|
130 |
||
131 |
fun init_context ("", _) = Proof_Context.init_global |
|
132 |
| init_context (locale, false) = Locale.init locale |
|
133 |
| init_context (class, true) = Class.init class; |
|
25269 | 134 |
|
63402 | 135 |
fun init before_exit target thy = |
39639 | 136 |
let |
57196 | 137 |
val name_data = make_name_data thy target; |
59880
30687c3f2b10
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
wenzelm
parents:
59876
diff
changeset
|
138 |
val background_naming = |
59876 | 139 |
Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target); |
39639 | 140 |
in |
141 |
thy |
|
56056
4d46d53566e6
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents:
55763
diff
changeset
|
142 |
|> Sign.change_begin |
57196 | 143 |
|> init_context name_data |
57485 | 144 |
|> is_none before_exit ? Data.put (SOME name_data) |
59880
30687c3f2b10
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
wenzelm
parents:
59876
diff
changeset
|
145 |
|> Local_Theory.init background_naming |
57196 | 146 |
{define = Generic_Target.define (foundation name_data), |
147 |
notes = Generic_Target.notes (notes name_data), |
|
60344
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60341
diff
changeset
|
148 |
abbrev = abbrev name_data, |
57196 | 149 |
declaration = declaration name_data, |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
150 |
theory_registration = theory_registration name_data, |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61777
diff
changeset
|
151 |
locale_dependency = locale_dependency name_data, |
57196 | 152 |
pretty = pretty name_data, |
57485 | 153 |
exit = the_default I before_exit |
154 |
#> Local_Theory.target_of #> Sign.change_end_local} |
|
39639 | 155 |
end; |
38247 | 156 |
|
63402 | 157 |
val theory_init = init NONE ""; |
58665 | 158 |
fun theory_map f = theory_init #> f #> Local_Theory.exit_global; |
159 |
||
57483
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
160 |
|
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
161 |
(* toplevel interaction *) |
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
162 |
|
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
163 |
fun begin ("-", _) thy = theory_init thy |
63402 | 164 |
| begin target thy = init NONE (Locale.check thy target) thy; |
57483
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
165 |
|
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
166 |
val exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; |
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
167 |
|
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
168 |
fun switch NONE (Context.Theory thy) = |
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
169 |
(Context.Theory o exit, theory_init thy) |
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
170 |
| switch (SOME name) (Context.Theory thy) = |
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
171 |
(Context.Theory o exit, begin name thy) |
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
172 |
| switch NONE (Context.Proof lthy) = |
62514 | 173 |
(Context.Proof o Local_Theory.reset, lthy) |
57483
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
174 |
| switch (SOME name) (Context.Proof lthy) = |
63402 | 175 |
(Context.Proof o init NONE (target_of lthy) o exit, |
57483
950dc7446454
centralized (ad-hoc) switching of targets in named_target.ML
haftmann
parents:
57196
diff
changeset
|
176 |
(begin name o exit o Local_Theory.assert_nonbrittle) lthy); |
33282 | 177 |
|
20894 | 178 |
end; |