author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 52140 | 88a69da5d3fa |
child 53088 | 6cd0feb85e35 |
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 |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47061
diff
changeset
|
10 |
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option |
52140 | 11 |
val is_theory: local_theory -> bool |
12 |
val the_name: local_theory -> string |
|
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
|
13 |
val init: (local_theory -> local_theory) -> string -> theory -> local_theory |
38388 | 14 |
val theory_init: theory -> local_theory |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
15 |
val reinit: local_theory -> local_theory -> local_theory |
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
45390
diff
changeset
|
16 |
val context_cmd: xstring * Position.T -> theory -> local_theory |
20894 | 17 |
end; |
18 |
||
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38349
diff
changeset
|
19 |
structure Named_Target: NAMED_TARGET = |
20894 | 20 |
struct |
21 |
||
21006 | 22 |
(* context data *) |
23 |
||
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
|
24 |
datatype target = |
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
|
25 |
Target of {target: string, is_locale: bool, is_class: bool, |
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
|
26 |
before_exit: local_theory -> local_theory}; |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
27 |
|
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
|
28 |
fun make_target target is_locale is_class before_exit = |
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
|
29 |
Target {target = target, is_locale = is_locale, is_class = is_class, |
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
|
30 |
before_exit = before_exit}; |
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
|
31 |
|
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
|
32 |
fun named_target _ "" before_exit = make_target "" false false before_exit |
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
|
33 |
| named_target thy locale before_exit = |
38378 | 34 |
if Locale.defined thy locale |
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
|
35 |
then make_target locale true (Class.is_class thy locale) before_exit |
38378 | 36 |
else error ("No such locale: " ^ quote locale); |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
37 |
|
33519 | 38 |
structure Data = Proof_Data |
21006 | 39 |
( |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
40 |
type T = target option; |
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
41 |
fun init _ = NONE; |
21006 | 42 |
); |
43 |
||
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
|
44 |
val peek = |
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
|
45 |
Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} => |
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
|
46 |
{target = target, is_locale = is_locale, is_class = is_class}); |
21006 | 47 |
|
52140 | 48 |
fun is_theory lthy = Option.map #target (peek lthy) = SOME "" |
49 |
andalso Local_Theory.level lthy = 1; |
|
50 |
||
51 |
fun the_name lthy = |
|
52 |
let |
|
53 |
val _ = Local_Theory.assert_bottom true lthy; |
|
54 |
in case Option.map #target (peek lthy) of |
|
55 |
SOME target => target |
|
56 |
| _ => error "Not in a named target" |
|
57 |
end; |
|
58 |
||
21006 | 59 |
|
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
60 |
(* consts in locale *) |
24838 | 61 |
|
47282 | 62 |
fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) = |
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
63 |
Generic_Target.locale_declaration target true (fn phi => |
45352 | 64 |
let |
65 |
val b' = Morphism.binding phi b; |
|
66 |
val rhs' = Morphism.term phi rhs; |
|
67 |
val same_shape = Term.aconv_untyped (rhs, rhs'); |
|
38297 | 68 |
|
45352 | 69 |
(* FIXME workaround based on educated guess *) |
70 |
val prefix' = Binding.prefix_of b'; |
|
71 |
val is_canonical_class = is_class andalso |
|
72 |
(Binding.eq_name (b, b') |
|
73 |
andalso not (null prefix') |
|
74 |
andalso List.last prefix' = (Class.class_prefix target, false) |
|
75 |
orelse same_shape); |
|
47282 | 76 |
in |
47288
b79bf8288b29
clarified generic_const vs. close_schematic_term;
wenzelm
parents:
47286
diff
changeset
|
77 |
not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs') |
47282 | 78 |
end) #> |
79 |
(fn lthy => lthy |> Generic_Target.const_declaration |
|
80 |
(fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs)); |
|
38305 | 81 |
|
38297 | 82 |
|
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
83 |
(* define *) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
84 |
|
47289 | 85 |
fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params = |
86 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
|
45352 | 87 |
#-> (fn (lhs, def) => locale_const ta 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 |
|
47289 | 90 |
fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params = |
91 |
Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
|
45352 | 92 |
#-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) |
48102
9ed089bcad93
class target handles additional non-class term parameters appropriately
haftmann
parents:
47289
diff
changeset
|
93 |
#> Class.const target ((b, mx), (#1 params, #2 params, lhs)) |
47282 | 94 |
#> pair (lhs, def)); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
95 |
|
39639 | 96 |
fun target_foundation (ta as Target {is_locale, is_class, ...}) = |
38349 | 97 |
if is_class then class_foundation ta |
98 |
else if is_locale then locale_foundation ta |
|
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
99 |
else Generic_Target.theory_foundation; |
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
100 |
|
24939 | 101 |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
102 |
(* notes *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
103 |
|
39639 | 104 |
fun target_notes (Target {target, is_locale, ...}) = |
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47247
diff
changeset
|
105 |
if is_locale then Generic_Target.locale_notes target |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47247
diff
changeset
|
106 |
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
|
107 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
108 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
109 |
(* abbrev *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
110 |
|
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
111 |
fun locale_abbrev ta prmode ((b, mx), t) xs = |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
112 |
Local_Theory.background_theory_result |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
113 |
(Sign.add_abbrev Print_Mode.internal (b, t)) #-> |
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47284
diff
changeset
|
114 |
(fn (lhs, _) => |
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47284
diff
changeset
|
115 |
locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
116 |
|
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47284
diff
changeset
|
117 |
fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy = |
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
118 |
if is_locale then |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
119 |
lthy |
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47284
diff
changeset
|
120 |
|> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs |
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
121 |
|> is_class ? Class.abbrev target prmode ((b, mx), t') |
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47284
diff
changeset
|
122 |
else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
123 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
124 |
|
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
125 |
(* declaration *) |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
126 |
|
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
127 |
fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy = |
47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47278
diff
changeset
|
128 |
if target = "" then Generic_Target.theory_declaration decl lthy |
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
129 |
else |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
130 |
lthy |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
131 |
|> pervasive ? Generic_Target.background_declaration decl |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
132 |
|> Generic_Target.locale_declaration target syntax decl |
47282 | 133 |
|> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl); |
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
134 |
|
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47081
diff
changeset
|
135 |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
136 |
(* pretty *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
137 |
|
39639 | 138 |
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
|
139 |
let |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
140 |
val target_name = |
52103 | 141 |
[Pretty.command (if is_class then "class" else "locale"), Pretty.brk 1, |
142 |
Locale.pretty_name ctxt target]; |
|
45353 | 143 |
val fixes = |
144 |
map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) |
|
145 |
(#1 (Proof_Context.inferred_fixes ctxt)); |
|
146 |
val assumes = |
|
147 |
map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) |
|
148 |
(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
|
149 |
val elems = |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
150 |
(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
|
151 |
(if null assumes then [] else [Element.Assumes assumes]); |
40782 | 152 |
val body_elems = |
153 |
if not is_locale then [] |
|
39639 | 154 |
else if null elems then [Pretty.block target_name] |
155 |
else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: |
|
40782 | 156 |
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
|
157 |
in |
39639 | 158 |
Pretty.block [Pretty.command "theory", Pretty.brk 1, |
42360 | 159 |
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
|
160 |
end; |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
161 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
162 |
|
38378 | 163 |
(* init *) |
25291 | 164 |
|
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
|
165 |
fun init_context (Target {target, is_locale, is_class, ...}) = |
42360 | 166 |
if not is_locale then Proof_Context.init_global |
29576 | 167 |
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
|
168 |
else Class.init target; |
25269 | 169 |
|
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
|
170 |
fun init before_exit target thy = |
39639 | 171 |
let |
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
|
172 |
val ta = named_target thy target before_exit; |
47061
355317493f34
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
wenzelm
parents:
47000
diff
changeset
|
173 |
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
|
174 |
|> Name_Space.mandatory_path (Long_Name.base_name target); |
39639 | 175 |
in |
176 |
thy |
|
177 |
|> init_context ta |
|
178 |
|> 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
|
179 |
|> Local_Theory.init naming |
39639 | 180 |
{define = Generic_Target.define (target_foundation ta), |
181 |
notes = Generic_Target.notes (target_notes ta), |
|
182 |
abbrev = Generic_Target.abbrev (target_abbrev ta), |
|
45291
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
45290
diff
changeset
|
183 |
declaration = target_declaration ta, |
39639 | 184 |
pretty = pretty ta, |
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
|
185 |
exit = Local_Theory.target_of o before_exit} |
39639 | 186 |
end; |
38247 | 187 |
|
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
|
188 |
val theory_init = init I ""; |
25269 | 189 |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47061
diff
changeset
|
190 |
val reinit = |
47069 | 191 |
Local_Theory.assert_bottom true #> Data.get #> the #> |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47061
diff
changeset
|
192 |
(fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target); |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
193 |
|
47274 | 194 |
fun context_cmd ("-", _) thy = theory_init thy |
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
45390
diff
changeset
|
195 |
| context_cmd target thy = init I (Locale.check thy target) thy; |
33282 | 196 |
|
20894 | 197 |
end; |