author | haftmann |
Wed, 11 Aug 2010 12:24:24 +0200 | |
changeset 38341 | 72dba5bd5f63 |
parent 38339 | fb8fd73827d4 |
child 38342 | 09d4a04d5c2e |
permissions | -rw-r--r-- |
20894 | 1 |
(* Title: Pure/Isar/theory_target.ML |
2 |
Author: Makarius |
|
30437 | 3 |
Author: Florian Haftmann, TU Muenchen |
20894 | 4 |
|
25542 | 5 |
Common theory/locale/class/instantiation/overloading targets. |
20894 | 6 |
*) |
7 |
||
8 |
signature THEORY_TARGET = |
|
9 |
sig |
|
38339 | 10 |
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} |
25269 | 11 |
val init: string option -> theory -> local_theory |
35205 | 12 |
val context_cmd: xstring -> theory -> local_theory |
25864 | 13 |
val instantiation: string list * (string * sort) list * sort -> theory -> local_theory |
29971 | 14 |
val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory |
25864 | 15 |
val overloading: (string * (string * typ) * bool) list -> theory -> local_theory |
26049
8186c03194ed
overloading: reduced code redundancy, no xstrings here;
wenzelm
parents:
25984
diff
changeset
|
16 |
val overloading_cmd: (string * string * bool) list -> theory -> local_theory |
20894 | 17 |
end; |
18 |
||
33553 | 19 |
structure Theory_Target: THEORY_TARGET = |
20894 | 20 |
struct |
21 |
||
21006 | 22 |
(* context data *) |
23 |
||
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
24 |
datatype target = Target of {target: string, is_locale: bool, is_class: bool}; |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
25 |
|
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
26 |
fun make_target target is_locale is_class = |
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
27 |
Target {target = target, is_locale = is_locale, is_class = is_class}; |
25291 | 28 |
|
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
29 |
val global_target = make_target "" false false; |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
30 |
|
33519 | 31 |
structure Data = Proof_Data |
21006 | 32 |
( |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
33 |
type T = target; |
25291 | 34 |
fun init _ = global_target; |
21006 | 35 |
); |
36 |
||
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
37 |
val peek = (fn Target args => args) o Data.get; |
21006 | 38 |
|
39 |
||
33456
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33282
diff
changeset
|
40 |
(* generic declarations *) |
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33282
diff
changeset
|
41 |
|
38305 | 42 |
fun locale_declaration locale { syntax, pervasive } decl lthy = |
24838 | 43 |
let |
38305 | 44 |
val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration; |
45 |
val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl; |
|
24838 | 46 |
in |
38305 | 47 |
lthy |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
48 |
|> pervasive ? Generic_Target.theory_declaration decl |
38305 | 49 |
|> Local_Theory.target (add locale locale_decl) |
24838 | 50 |
end; |
51 |
||
38305 | 52 |
fun target_declaration (Target {target, ...}) { syntax, pervasive } = |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
53 |
if target = "" then Generic_Target.theory_declaration |
38305 | 54 |
else locale_declaration target { syntax = syntax, pervasive = pervasive }; |
24838 | 55 |
|
21611
fc95ff1fe738
notes: proper import/export of proofs (still inactive);
wenzelm
parents:
21594
diff
changeset
|
56 |
|
38297 | 57 |
(* consts in locales *) |
58 |
||
59 |
fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi = |
|
60 |
let |
|
61 |
val b' = Morphism.binding phi b; |
|
62 |
val rhs' = Morphism.term phi rhs; |
|
63 |
val arg = (b', Term.close_schematic_term rhs'); |
|
64 |
val same_shape = Term.aconv_untyped (rhs, rhs'); |
|
65 |
(* FIXME workaround based on educated guess *) |
|
66 |
val prefix' = Binding.prefix_of b'; |
|
67 |
val is_canonical_class = is_class andalso |
|
68 |
(Binding.eq_name (b, b') |
|
69 |
andalso not (null prefix') |
|
70 |
andalso List.last prefix' = (Class_Target.class_prefix target, false) |
|
71 |
orelse same_shape); |
|
72 |
in |
|
73 |
not is_canonical_class ? |
|
74 |
(Context.mapping_result |
|
75 |
(Sign.add_abbrev Print_Mode.internal arg) |
|
76 |
(ProofContext.add_abbrev Print_Mode.internal arg) |
|
77 |
#-> (fn (lhs' as Const (d, _), _) => |
|
78 |
same_shape ? |
|
38310 | 79 |
(Context.mapping |
80 |
(Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #> |
|
38297 | 81 |
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))) |
82 |
end; |
|
83 |
||
38305 | 84 |
fun locale_const_declaration (ta as Target {target, ...}) prmode arg = |
85 |
locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg); |
|
86 |
||
87 |
fun class_target (Target {target, ...}) f = |
|
88 |
Local_Theory.raw_theory f #> |
|
89 |
Local_Theory.target (Class_Target.refresh_syntax target); |
|
90 |
||
38297 | 91 |
|
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
92 |
(* define *) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
93 |
|
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
94 |
fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
95 |
|
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
96 |
fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
97 |
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
98 |
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
99 |
#> pair (lhs, def)) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
100 |
|
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
101 |
fun class_foundation (ta as Target {target, ...}) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
102 |
(((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
103 |
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
104 |
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
105 |
#> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs))) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
106 |
#> pair (lhs, def)) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
107 |
|
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
108 |
fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
109 |
case Class_Target.instantiation_param lthy b |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
110 |
of SOME c => if mx <> NoSyn then syntax_error c |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
111 |
else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
112 |
##>> AxClass.define_overloaded b_def (c, rhs)) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
113 |
||> Class_Target.confirm_declaration b |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
114 |
| NONE => lthy |> |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
115 |
Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
116 |
|
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
117 |
fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
118 |
case Overloading.operation lthy b |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
119 |
of SOME (c, checked) => if mx <> NoSyn then syntax_error c |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
120 |
else lthy |> Local_Theory.theory_result (Overloading.declare (c, U) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
121 |
##>> Overloading.define checked b_def (c, rhs)) |
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
122 |
||> Overloading.confirm b |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
123 |
| NONE => lthy |> |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
124 |
Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); |
37314
f5abedb7aed5
more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);
wenzelm
parents:
37205
diff
changeset
|
125 |
|
25105
c9f67836c4d8
internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
wenzelm
parents:
25096
diff
changeset
|
126 |
fun fork_mixfix (Target {is_locale, is_class, ...}) mx = |
c9f67836c4d8
internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
wenzelm
parents:
25096
diff
changeset
|
127 |
if not is_locale then (NoSyn, NoSyn, mx) |
c9f67836c4d8
internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
wenzelm
parents:
25096
diff
changeset
|
128 |
else if not is_class then (NoSyn, mx, NoSyn) |
c9f67836c4d8
internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
wenzelm
parents:
25096
diff
changeset
|
129 |
else (mx, NoSyn, NoSyn); |
25068 | 130 |
|
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
131 |
fun foundation (ta as Target {target, is_locale, is_class, ...}) |
38314 | 132 |
(((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
133 |
let |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
134 |
val (mx1, mx2, mx3) = fork_mixfix ta mx; |
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
135 |
val (const, lthy2) = lthy |> |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
136 |
(case Class_Target.instantiation_param lthy b of |
38314 | 137 |
SOME c => |
138 |
if mx3 <> NoSyn then syntax_error c |
|
139 |
else Local_Theory.theory_result (AxClass.declare_overloaded (c, U)) |
|
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
140 |
##> Class_Target.confirm_declaration b |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
141 |
| NONE => |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
142 |
(case Overloading.operation lthy b of |
38314 | 143 |
SOME (c, _) => |
144 |
if mx3 <> NoSyn then syntax_error c |
|
145 |
else Local_Theory.theory_result (Overloading.declare (c, U)) |
|
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
146 |
##> Overloading.confirm b |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
147 |
| NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3)))); |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
148 |
val Const (head, _) = const; |
38314 | 149 |
val lhs = list_comb (const, type_params @ term_params); |
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
150 |
in |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
151 |
lthy2 |
38314 | 152 |
|> pair lhs |
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
153 |
||>> Local_Theory.theory_result |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
154 |
(case Overloading.operation lthy b of |
38314 | 155 |
SOME (_, checked) => Overloading.define checked b_def (head, rhs) |
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
156 |
| NONE => |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
157 |
if is_some (Class_Target.instantiation_param lthy b) |
38314 | 158 |
then AxClass.define_overloaded b_def (head, rhs) |
159 |
else Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)) #>> snd) |
|
160 |
||> is_locale ? locale_const_declaration ta Syntax.mode_default ((b, mx2), lhs) |
|
38310 | 161 |
||> is_class ? class_target ta |
38314 | 162 |
(Class_Target.declare target ((b, mx1), (type_params, lhs))) |
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
163 |
end; |
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
164 |
|
24939 | 165 |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
166 |
(* notes *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
167 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
168 |
fun locale_notes locale kind global_facts local_facts lthy = |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
169 |
let |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
170 |
val global_facts' = Attrib.map_facts (K I) global_facts; |
38310 | 171 |
val local_facts' = Element.facts_map |
172 |
(Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts; |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
173 |
in |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
174 |
lthy |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
175 |
|> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
176 |
|> Local_Theory.target (Locale.add_thmss locale kind local_facts') |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
177 |
end |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
178 |
|
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
179 |
fun target_notes (ta as Target {target, is_locale, ...}) = |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
180 |
if is_locale then locale_notes target |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
181 |
else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
182 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
183 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
184 |
(* abbrev *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
185 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
186 |
fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result |
38310 | 187 |
(Sign.add_abbrev Print_Mode.internal (b, t)) #-> |
188 |
(fn (lhs, _) => locale_const_declaration ta prmode |
|
189 |
((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
|
190 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
191 |
fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
192 |
prmode (b, mx) (global_rhs, t') xs lthy = |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
193 |
if is_locale |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
194 |
then lthy |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
195 |
|> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
196 |
|> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t')) |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
197 |
else lthy |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
198 |
|> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
199 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
200 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
201 |
(* pretty *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
202 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
203 |
fun pretty_thy ctxt target is_class = |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
204 |
let |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
205 |
val thy = ProofContext.theory_of ctxt; |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
206 |
val target_name = |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
207 |
[Pretty.command (if is_class then "class" else "locale"), |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
208 |
Pretty.str (" " ^ Locale.extern thy target)]; |
38310 | 209 |
val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) |
210 |
(#1 (ProofContext.inferred_fixes ctxt)); |
|
211 |
val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) |
|
212 |
(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
|
213 |
val elems = |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
214 |
(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
|
215 |
(if null assumes then [] else [Element.Assumes assumes]); |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
216 |
in |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
217 |
if target = "" then [] |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
218 |
else if null elems then [Pretty.block target_name] |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
219 |
else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
220 |
map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))] |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
221 |
end; |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
222 |
|
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
223 |
fun pretty (Target {target, is_class, ...}) ctxt = |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
224 |
Pretty.block [Pretty.command "theory", Pretty.brk 1, |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
225 |
Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: |
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
226 |
pretty_thy ctxt target is_class; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
227 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
228 |
|
35205 | 229 |
(* init various targets *) |
25291 | 230 |
|
231 |
local |
|
20894 | 232 |
|
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
233 |
fun init_data (Target {target, is_locale, is_class}) = |
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
234 |
if not is_locale then ProofContext.init_global |
29576 | 235 |
else if not is_class then Locale.init target |
29358 | 236 |
else Class_Target.init target; |
25269 | 237 |
|
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
238 |
fun init_target (ta as Target {target, ...}) thy = |
38247 | 239 |
thy |
240 |
|> init_data ta |
|
241 |
|> Data.put ta |
|
242 |
|> Local_Theory.init NONE (Long_Name.base_name target) |
|
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
243 |
{define = Generic_Target.define (foundation ta), |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
244 |
notes = Generic_Target.notes (target_notes ta), |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
245 |
abbrev = Generic_Target.abbrev (target_abbrev ta), |
38310 | 246 |
declaration = fn pervasive => target_declaration ta |
247 |
{ syntax = false, pervasive = pervasive }, |
|
248 |
syntax_declaration = fn pervasive => target_declaration ta |
|
249 |
{ syntax = true, pervasive = pervasive }, |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
250 |
pretty = pretty ta, |
38247 | 251 |
reinit = init_target ta o ProofContext.theory_of, |
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
252 |
exit = Local_Theory.target_of}; |
38247 | 253 |
|
254 |
fun named_target _ NONE = global_target |
|
255 |
| named_target thy (SOME target) = |
|
256 |
if Locale.defined thy target |
|
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
257 |
then make_target target true (Class_Target.is_class thy target) |
38247 | 258 |
else error ("No such locale: " ^ quote target); |
20894 | 259 |
|
26049
8186c03194ed
overloading: reduced code redundancy, no xstrings here;
wenzelm
parents:
25984
diff
changeset
|
260 |
fun gen_overloading prep_const raw_ops thy = |
8186c03194ed
overloading: reduced code redundancy, no xstrings here;
wenzelm
parents:
25984
diff
changeset
|
261 |
let |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36106
diff
changeset
|
262 |
val ctxt = ProofContext.init_global thy; |
26049
8186c03194ed
overloading: reduced code redundancy, no xstrings here;
wenzelm
parents:
25984
diff
changeset
|
263 |
val ops = raw_ops |> map (fn (name, const, checked) => |
8186c03194ed
overloading: reduced code redundancy, no xstrings here;
wenzelm
parents:
25984
diff
changeset
|
264 |
(name, Term.dest_Const (prep_const ctxt const), checked)); |
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
265 |
in |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
266 |
thy |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
267 |
|> Overloading.init ops |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
268 |
|> Local_Theory.init NONE "" |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
269 |
{define = Generic_Target.define overloading_foundation, |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
270 |
notes = Generic_Target.notes |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
271 |
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), |
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
272 |
abbrev = Generic_Target.abbrev |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
273 |
(fn prmode => fn (b, mx) => fn (t, _) => fn _ => |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
274 |
Generic_Target.theory_abbrev prmode ((b, mx), t)), |
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
275 |
declaration = K Generic_Target.theory_declaration, |
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
276 |
syntax_declaration = K Generic_Target.theory_declaration, |
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
277 |
pretty = single o Overloading.pretty, |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
278 |
reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of, |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
279 |
exit = Local_Theory.target_of o Overloading.conclude} |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
280 |
end; |
26049
8186c03194ed
overloading: reduced code redundancy, no xstrings here;
wenzelm
parents:
25984
diff
changeset
|
281 |
|
25291 | 282 |
in |
20894 | 283 |
|
38247 | 284 |
fun init target thy = init_target (named_target thy target) thy; |
25269 | 285 |
|
35205 | 286 |
fun context_cmd "-" thy = init NONE thy |
287 |
| context_cmd target thy = init (SOME (Locale.intern thy target)) thy; |
|
33282 | 288 |
|
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
289 |
fun instantiation arities thy = |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
290 |
thy |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
291 |
|> Class_Target.init_instantiation arities |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
292 |
|> Local_Theory.init NONE "" |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
293 |
{define = Generic_Target.define instantiation_foundation, |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
294 |
notes = Generic_Target.notes |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
295 |
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), |
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
296 |
abbrev = Generic_Target.abbrev |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
297 |
(fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)), |
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
298 |
declaration = K Generic_Target.theory_declaration, |
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
299 |
syntax_declaration = K Generic_Target.theory_declaration, |
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
300 |
pretty = single o Class_Target.pretty_instantiation, |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
301 |
reinit = instantiation arities o ProofContext.theory_of, |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
302 |
exit = Local_Theory.target_of o Class_Target.conclude_instantiation}; |
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
303 |
|
38310 | 304 |
fun instantiation_cmd arities thy = |
305 |
instantiation (Class_Target.read_multi_arity thy arities) thy; |
|
25519 | 306 |
|
26049
8186c03194ed
overloading: reduced code redundancy, no xstrings here;
wenzelm
parents:
25984
diff
changeset
|
307 |
val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); |
8186c03194ed
overloading: reduced code redundancy, no xstrings here;
wenzelm
parents:
25984
diff
changeset
|
308 |
val overloading_cmd = gen_overloading Syntax.read_term; |
25462 | 309 |
|
20894 | 310 |
end; |
25291 | 311 |
|
312 |
end; |