author | haftmann |
Sat, 07 Jun 2014 08:16:03 +0200 | |
changeset 57185 | 188da8aaae24 |
parent 57184 | 56f3351cc492 |
child 57192 | 180e955711cf |
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 |
12 |
val class_of: local_theory -> string option |
|
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
13 |
val init: string -> theory -> local_theory |
38388 | 14 |
val theory_init: theory -> local_theory |
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
45390
diff
changeset
|
15 |
val context_cmd: xstring * Position.T -> theory -> local_theory |
20894 | 16 |
end; |
17 |
||
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38349
diff
changeset
|
18 |
structure Named_Target: NAMED_TARGET = |
20894 | 19 |
struct |
20 |
||
21006 | 21 |
(* context data *) |
22 |
||
41585
45d7da4e4ccf
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents:
40782
diff
changeset
|
23 |
datatype target = |
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
24 |
Target of {target: string, is_locale: bool, is_class: bool}; |
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
25 |
|
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
26 |
fun make_target target is_locale is_class = |
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
27 |
Target {target = target, is_locale = is_locale, is_class = is_class}; |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
28 |
|
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
29 |
fun named_target _ "" = make_target "" false false |
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
30 |
| named_target thy target = |
57176 | 31 |
if Locale.defined thy target |
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
32 |
then make_target target true (Class.is_class thy target) |
57176 | 33 |
else error ("No such locale: " ^ quote target); |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
34 |
|
33519 | 35 |
structure Data = Proof_Data |
21006 | 36 |
( |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
37 |
type T = target option; |
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
38 |
fun init _ = NONE; |
21006 | 39 |
); |
40 |
||
57177
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
41 |
fun peek lthy = |
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
42 |
if Local_Theory.level lthy = 1 |
57182 | 43 |
then Option.map (fn Target ta => ta) (Data.get lthy) |
57177
dce365931721
sharpened criterion: bare named target is only at the bottom level
haftmann
parents:
57176
diff
changeset
|
44 |
else NONE; |
21006 | 45 |
|
57185 | 46 |
fun is_theory lthy = |
47 |
case peek lthy of |
|
48 |
SOME {target = "", ...} => true |
|
49 |
| _ => false; |
|
52140 | 50 |
|
57182 | 51 |
fun locale_of lthy = |
52 |
case peek lthy of |
|
53 |
SOME {target = locale, is_locale = true, ...} => SOME locale |
|
54 |
| _ => NONE; |
|
55 |
||
56 |
fun class_of lthy = |
|
57 |
case peek lthy of |
|
58 |
SOME {target = class, is_class = true, ...} => SOME class |
|
59 |
| _ => NONE; |
|
60 |
||
21006 | 61 |
|
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
62 |
(* define *) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
63 |
|
57074 | 64 |
fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = |
47289 | 65 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
57074 | 66 |
#-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) |
47282 | 67 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
68 |
|
57074 | 69 |
fun class_foundation class (((b, U), mx), (b_def, rhs)) params = |
47289 | 70 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
57074 | 71 |
#-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params |
47282 | 72 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
73 |
|
57176 | 74 |
fun foundation (ta as Target {target, is_locale, is_class, ...}) = |
57066
78651e94746f
tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents:
57065
diff
changeset
|
75 |
if is_class then class_foundation target |
78651e94746f
tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents:
57065
diff
changeset
|
76 |
else if is_locale then locale_foundation target |
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
77 |
else Generic_Target.theory_foundation; |
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
78 |
|
24939 | 79 |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
80 |
(* notes *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
81 |
|
57176 | 82 |
fun notes (Target {target, is_locale, ...}) = |
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47247
diff
changeset
|
83 |
if is_locale then Generic_Target.locale_notes target |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47247
diff
changeset
|
84 |
else Generic_Target.theory_notes; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
85 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
86 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
87 |
(* abbrev *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
88 |
|
57118 | 89 |
fun locale_abbrev locale prmode (b, mx) global_rhs params = |
57160 | 90 |
Generic_Target.background_abbrev (b, global_rhs) (snd params) |
57074 | 91 |
#-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs)); |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
92 |
|
57118 | 93 |
fun class_abbrev class prmode (b, mx) global_rhs params = |
57160 | 94 |
Generic_Target.background_abbrev (b, global_rhs) (snd params) |
57161
6254c51cd210
formal treatment of dangling parameters for class abbrevs analogously to class consts
haftmann
parents:
57160
diff
changeset
|
95 |
#-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs params); |
57066
78651e94746f
tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents:
57065
diff
changeset
|
96 |
|
57176 | 97 |
fun abbrev (ta as Target {target, is_locale, is_class, ...}) = |
57066
78651e94746f
tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents:
57065
diff
changeset
|
98 |
if is_class then class_abbrev target |
78651e94746f
tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents:
57065
diff
changeset
|
99 |
else if is_locale then locale_abbrev target |
78651e94746f
tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents:
57065
diff
changeset
|
100 |
else Generic_Target.theory_abbrev; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
101 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
102 |
|
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
103 |
(* declaration *) |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
104 |
|
57176 | 105 |
fun declaration (Target {target, is_locale, ...}) {syntax, pervasive} decl = |
106 |
if is_locale then |
|
107 |
pervasive ? Generic_Target.background_declaration decl |
|
108 |
#> Generic_Target.locale_declaration target syntax decl |
|
109 |
#> Generic_Target.standard_declaration (fn (_, other) => other <> 0) decl |
|
110 |
else Generic_Target.theory_declaration decl; |
|
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
111 |
|
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
112 |
|
56723
a8f71445c265
subscription as target-specific implementation device
haftmann
parents:
56056
diff
changeset
|
113 |
(* subscription *) |
a8f71445c265
subscription as target-specific implementation device
haftmann
parents:
56056
diff
changeset
|
114 |
|
57176 | 115 |
fun subscription (Target {target, is_locale, ...}) = |
116 |
if is_locale then Generic_Target.locale_dependency target |
|
117 |
else Generic_Target.theory_registration; |
|
56723
a8f71445c265
subscription as target-specific implementation device
haftmann
parents:
56056
diff
changeset
|
118 |
|
a8f71445c265
subscription as target-specific implementation device
haftmann
parents:
56056
diff
changeset
|
119 |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
120 |
(* pretty *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
121 |
|
39639 | 122 |
fun pretty (Target {target, is_locale, is_class, ...}) ctxt = |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
123 |
let |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
124 |
val target_name = |
55763 | 125 |
[Pretty.keyword1 (if is_class then "class" else "locale"), Pretty.brk 1, |
52103 | 126 |
Locale.pretty_name ctxt target]; |
45353 | 127 |
val fixes = |
128 |
map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) |
|
129 |
(#1 (Proof_Context.inferred_fixes ctxt)); |
|
130 |
val assumes = |
|
131 |
map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) |
|
132 |
(Assumption.all_assms_of ctxt); |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
133 |
val elems = |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
134 |
(if null fixes then [] else [Element.Fixes fixes]) @ |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
135 |
(if null assumes then [] else [Element.Assumes assumes]); |
40782 | 136 |
val body_elems = |
137 |
if not is_locale then [] |
|
39639 | 138 |
else if null elems then [Pretty.block target_name] |
139 |
else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: |
|
40782 | 140 |
map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
141 |
in |
55763 | 142 |
Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, |
42360 | 143 |
Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
144 |
end; |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
145 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
146 |
|
38378 | 147 |
(* init *) |
25291 | 148 |
|
41585
45d7da4e4ccf
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents:
40782
diff
changeset
|
149 |
fun init_context (Target {target, is_locale, is_class, ...}) = |
42360 | 150 |
if not is_locale then Proof_Context.init_global |
29576 | 151 |
else if not is_class then Locale.init target |
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38378
diff
changeset
|
152 |
else Class.init target; |
25269 | 153 |
|
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
154 |
fun init target thy = |
39639 | 155 |
let |
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
156 |
val ta = named_target thy target; |
47061
355317493f34
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
wenzelm
parents:
47000
diff
changeset
|
157 |
val naming = Sign.naming_of thy |
355317493f34
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
wenzelm
parents:
47000
diff
changeset
|
158 |
|> Name_Space.mandatory_path (Long_Name.base_name target); |
39639 | 159 |
in |
160 |
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
|
161 |
|> Sign.change_begin |
39639 | 162 |
|> init_context ta |
163 |
|> Data.put (SOME ta) |
|
47061
355317493f34
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
wenzelm
parents:
47000
diff
changeset
|
164 |
|> Local_Theory.init naming |
57176 | 165 |
{define = Generic_Target.define (foundation ta), |
166 |
notes = Generic_Target.notes (notes ta), |
|
167 |
abbrev = Generic_Target.abbrev (abbrev ta), |
|
168 |
declaration = declaration ta, |
|
169 |
subscription = subscription ta, |
|
39639 | 170 |
pretty = pretty ta, |
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
171 |
exit = Local_Theory.target_of #> Sign.change_end_local} |
39639 | 172 |
end; |
38247 | 173 |
|
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
174 |
val theory_init = init ""; |
25269 | 175 |
|
47274 | 176 |
fun context_cmd ("-", _) thy = theory_init thy |
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
57177
diff
changeset
|
177 |
| context_cmd target thy = init (Locale.check thy target) thy; |
33282 | 178 |
|
20894 | 179 |
end; |