wenzelm@42830
|
1 |
(* Title: Pure/Isar/named_target.ML
|
wenzelm@20894
|
2 |
Author: Makarius
|
wenzelm@30451
|
3 |
Author: Florian Haftmann, TU Muenchen
|
wenzelm@20894
|
4 |
|
haftmann@38586
|
5 |
Targets for theory, locale and class.
|
wenzelm@20894
|
6 |
*)
|
wenzelm@20894
|
7 |
|
haftmann@38586
|
8 |
signature NAMED_TARGET =
|
haftmann@38530
|
9 |
sig
|
wenzelm@41833
|
10 |
val init: (local_theory -> local_theory) -> string -> theory -> local_theory
|
haftmann@38614
|
11 |
val theory_init: theory -> local_theory
|
haftmann@38617
|
12 |
val reinit: local_theory -> local_theory -> local_theory
|
haftmann@38530
|
13 |
val context_cmd: xstring -> theory -> local_theory
|
haftmann@38617
|
14 |
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
|
haftmann@38530
|
15 |
end;
|
haftmann@38530
|
16 |
|
haftmann@38586
|
17 |
structure Named_Target: NAMED_TARGET =
|
haftmann@38530
|
18 |
struct
|
haftmann@38530
|
19 |
|
haftmann@38530
|
20 |
(* context data *)
|
haftmann@38530
|
21 |
|
wenzelm@41833
|
22 |
datatype target =
|
wenzelm@41833
|
23 |
Target of {target: string, is_locale: bool, is_class: bool,
|
wenzelm@41833
|
24 |
before_exit: local_theory -> local_theory};
|
haftmann@38530
|
25 |
|
wenzelm@41833
|
26 |
fun make_target target is_locale is_class before_exit =
|
wenzelm@41833
|
27 |
Target {target = target, is_locale = is_locale, is_class = is_class,
|
wenzelm@41833
|
28 |
before_exit = before_exit};
|
wenzelm@41833
|
29 |
|
wenzelm@41833
|
30 |
fun named_target _ "" before_exit = make_target "" false false before_exit
|
wenzelm@41833
|
31 |
| named_target thy locale before_exit =
|
haftmann@38604
|
32 |
if Locale.defined thy locale
|
wenzelm@41833
|
33 |
then make_target locale true (Class.is_class thy locale) before_exit
|
haftmann@38604
|
34 |
else error ("No such locale: " ^ quote locale);
|
haftmann@38530
|
35 |
|
haftmann@38530
|
36 |
structure Data = Proof_Data
|
haftmann@38530
|
37 |
(
|
haftmann@38617
|
38 |
type T = target option;
|
haftmann@38617
|
39 |
fun init _ = NONE;
|
haftmann@38530
|
40 |
);
|
haftmann@38530
|
41 |
|
wenzelm@41833
|
42 |
val peek =
|
wenzelm@41833
|
43 |
Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
|
wenzelm@41833
|
44 |
{target = target, is_locale = is_locale, is_class = is_class});
|
haftmann@38530
|
45 |
|
haftmann@38530
|
46 |
|
haftmann@38530
|
47 |
(* generic declarations *)
|
haftmann@38530
|
48 |
|
wenzelm@41032
|
49 |
fun locale_declaration locale {syntax, pervasive} decl lthy =
|
haftmann@38530
|
50 |
let
|
haftmann@38530
|
51 |
val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
|
haftmann@38530
|
52 |
val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
|
haftmann@38530
|
53 |
in
|
haftmann@38530
|
54 |
lthy
|
haftmann@38577
|
55 |
|> pervasive ? Generic_Target.theory_declaration decl
|
haftmann@38530
|
56 |
|> Local_Theory.target (add locale locale_decl)
|
haftmann@38530
|
57 |
end;
|
haftmann@38530
|
58 |
|
wenzelm@41032
|
59 |
fun target_declaration (Target {target, ...}) {syntax, pervasive} =
|
haftmann@38577
|
60 |
if target = "" then Generic_Target.theory_declaration
|
wenzelm@41032
|
61 |
else locale_declaration target {syntax = syntax, pervasive = pervasive};
|
haftmann@38530
|
62 |
|
haftmann@38530
|
63 |
|
haftmann@38521
|
64 |
(* consts in locales *)
|
haftmann@38521
|
65 |
|
haftmann@38521
|
66 |
fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
|
haftmann@38521
|
67 |
let
|
haftmann@38521
|
68 |
val b' = Morphism.binding phi b;
|
haftmann@38521
|
69 |
val rhs' = Morphism.term phi rhs;
|
haftmann@38521
|
70 |
val arg = (b', Term.close_schematic_term rhs');
|
haftmann@38521
|
71 |
val same_shape = Term.aconv_untyped (rhs, rhs');
|
haftmann@38521
|
72 |
(* FIXME workaround based on educated guess *)
|
haftmann@38521
|
73 |
val prefix' = Binding.prefix_of b';
|
haftmann@38521
|
74 |
val is_canonical_class = is_class andalso
|
haftmann@38521
|
75 |
(Binding.eq_name (b, b')
|
haftmann@38521
|
76 |
andalso not (null prefix')
|
haftmann@38605
|
77 |
andalso List.last prefix' = (Class.class_prefix target, false)
|
haftmann@38521
|
78 |
orelse same_shape);
|
haftmann@38521
|
79 |
in
|
haftmann@38521
|
80 |
not is_canonical_class ?
|
haftmann@38521
|
81 |
(Context.mapping_result
|
haftmann@38521
|
82 |
(Sign.add_abbrev Print_Mode.internal arg)
|
haftmann@38521
|
83 |
(ProofContext.add_abbrev Print_Mode.internal arg)
|
haftmann@38521
|
84 |
#-> (fn (lhs' as Const (d, _), _) =>
|
haftmann@38521
|
85 |
same_shape ?
|
haftmann@38534
|
86 |
(Context.mapping
|
haftmann@38534
|
87 |
(Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
|
haftmann@38521
|
88 |
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
|
haftmann@38521
|
89 |
end;
|
haftmann@38521
|
90 |
|
haftmann@38529
|
91 |
fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
|
wenzelm@41032
|
92 |
locale_declaration target {syntax = true, pervasive = false} (locale_const ta prmode arg);
|
haftmann@38529
|
93 |
|
haftmann@38521
|
94 |
|
haftmann@38542
|
95 |
(* define *)
|
haftmann@38542
|
96 |
|
haftmann@38542
|
97 |
fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
|
haftmann@38577
|
98 |
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
|
haftmann@38542
|
99 |
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
|
haftmann@38542
|
100 |
#> pair (lhs, def))
|
haftmann@38542
|
101 |
|
haftmann@38542
|
102 |
fun class_foundation (ta as Target {target, ...})
|
haftmann@38542
|
103 |
(((b, U), mx), (b_def, rhs)) (type_params, term_params) =
|
haftmann@38577
|
104 |
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
|
haftmann@38542
|
105 |
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
|
haftmann@38842
|
106 |
#> Class.const target ((b, mx), (type_params, lhs))
|
haftmann@38542
|
107 |
#> pair (lhs, def))
|
haftmann@38542
|
108 |
|
haftmann@39863
|
109 |
fun target_foundation (ta as Target {is_locale, is_class, ...}) =
|
haftmann@38585
|
110 |
if is_class then class_foundation ta
|
haftmann@38585
|
111 |
else if is_locale then locale_foundation ta
|
haftmann@38585
|
112 |
else Generic_Target.theory_foundation;
|
haftmann@38527
|
113 |
|
wenzelm@24939
|
114 |
|
haftmann@38532
|
115 |
(* notes *)
|
haftmann@38532
|
116 |
|
wenzelm@41032
|
117 |
fun locale_notes locale kind global_facts local_facts lthy =
|
haftmann@38532
|
118 |
let
|
haftmann@38532
|
119 |
val global_facts' = Attrib.map_facts (K I) global_facts;
|
haftmann@38534
|
120 |
val local_facts' = Element.facts_map
|
haftmann@38534
|
121 |
(Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
|
haftmann@38532
|
122 |
in
|
haftmann@38532
|
123 |
lthy
|
wenzelm@39814
|
124 |
|> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
|
haftmann@38532
|
125 |
|> Local_Theory.target (Locale.add_thmss locale kind local_facts')
|
haftmann@38532
|
126 |
end
|
haftmann@38532
|
127 |
|
haftmann@39863
|
128 |
fun target_notes (Target {target, is_locale, ...}) =
|
haftmann@38543
|
129 |
if is_locale then locale_notes target
|
wenzelm@41032
|
130 |
else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
|
haftmann@38532
|
131 |
|
haftmann@38532
|
132 |
|
haftmann@38532
|
133 |
(* abbrev *)
|
haftmann@38532
|
134 |
|
wenzelm@39032
|
135 |
fun locale_abbrev ta prmode ((b, mx), t) xs =
|
wenzelm@39032
|
136 |
Local_Theory.background_theory_result
|
wenzelm@39032
|
137 |
(Sign.add_abbrev Print_Mode.internal (b, t)) #->
|
wenzelm@39032
|
138 |
(fn (lhs, _) => locale_const_declaration ta prmode
|
wenzelm@39032
|
139 |
((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
|
haftmann@38532
|
140 |
|
haftmann@38532
|
141 |
fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
|
haftmann@38536
|
142 |
prmode (b, mx) (global_rhs, t') xs lthy =
|
wenzelm@39032
|
143 |
if is_locale then
|
wenzelm@39032
|
144 |
lthy
|
wenzelm@39032
|
145 |
|> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
|
wenzelm@39032
|
146 |
|> is_class ? Class.abbrev target prmode ((b, mx), t')
|
wenzelm@39032
|
147 |
else
|
wenzelm@39032
|
148 |
lthy
|
wenzelm@39032
|
149 |
|> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
|
haftmann@38532
|
150 |
|
haftmann@38532
|
151 |
|
haftmann@38532
|
152 |
(* pretty *)
|
haftmann@38532
|
153 |
|
haftmann@39863
|
154 |
fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
|
haftmann@38532
|
155 |
let
|
haftmann@38532
|
156 |
val thy = ProofContext.theory_of ctxt;
|
haftmann@38532
|
157 |
val target_name =
|
haftmann@38532
|
158 |
[Pretty.command (if is_class then "class" else "locale"),
|
haftmann@38532
|
159 |
Pretty.str (" " ^ Locale.extern thy target)];
|
haftmann@38534
|
160 |
val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
|
haftmann@38534
|
161 |
(#1 (ProofContext.inferred_fixes ctxt));
|
haftmann@38534
|
162 |
val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
|
haftmann@38534
|
163 |
(Assumption.all_assms_of ctxt);
|
haftmann@38532
|
164 |
val elems =
|
haftmann@38532
|
165 |
(if null fixes then [] else [Element.Fixes fixes]) @
|
haftmann@38532
|
166 |
(if null assumes then [] else [Element.Assumes assumes]);
|
wenzelm@41032
|
167 |
val body_elems =
|
wenzelm@41032
|
168 |
if not is_locale then []
|
haftmann@39863
|
169 |
else if null elems then [Pretty.block target_name]
|
haftmann@39863
|
170 |
else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
|
wenzelm@41032
|
171 |
map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
|
haftmann@38532
|
172 |
in
|
haftmann@39863
|
173 |
Pretty.block [Pretty.command "theory", Pretty.brk 1,
|
haftmann@39863
|
174 |
Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
|
haftmann@38532
|
175 |
end;
|
haftmann@38532
|
176 |
|
haftmann@38532
|
177 |
|
haftmann@38604
|
178 |
(* init *)
|
wenzelm@20894
|
179 |
|
wenzelm@41833
|
180 |
fun init_context (Target {target, is_locale, is_class, ...}) =
|
haftmann@38574
|
181 |
if not is_locale then ProofContext.init_global
|
haftmann@29576
|
182 |
else if not is_class then Locale.init target
|
haftmann@38605
|
183 |
else Class.init target;
|
haftmann@25462
|
184 |
|
wenzelm@41833
|
185 |
fun init before_exit target thy =
|
haftmann@39863
|
186 |
let
|
wenzelm@41833
|
187 |
val ta = named_target thy target before_exit;
|
haftmann@39863
|
188 |
in
|
haftmann@39863
|
189 |
thy
|
haftmann@39863
|
190 |
|> init_context ta
|
haftmann@39863
|
191 |
|> Data.put (SOME ta)
|
haftmann@39863
|
192 |
|> Local_Theory.init NONE (Long_Name.base_name target)
|
haftmann@39863
|
193 |
{define = Generic_Target.define (target_foundation ta),
|
haftmann@39863
|
194 |
notes = Generic_Target.notes (target_notes ta),
|
haftmann@39863
|
195 |
abbrev = Generic_Target.abbrev (target_abbrev ta),
|
haftmann@39863
|
196 |
declaration = fn pervasive => target_declaration ta
|
wenzelm@41032
|
197 |
{syntax = false, pervasive = pervasive},
|
haftmann@39863
|
198 |
syntax_declaration = fn pervasive => target_declaration ta
|
wenzelm@41032
|
199 |
{syntax = true, pervasive = pervasive},
|
haftmann@39863
|
200 |
pretty = pretty ta,
|
wenzelm@41833
|
201 |
exit = Local_Theory.target_of o before_exit}
|
haftmann@39863
|
202 |
end;
|
haftmann@38471
|
203 |
|
wenzelm@41833
|
204 |
val theory_init = init I "";
|
wenzelm@25291
|
205 |
|
wenzelm@39032
|
206 |
fun reinit lthy =
|
wenzelm@41833
|
207 |
(case Data.get lthy of
|
wenzelm@41833
|
208 |
SOME (Target {target, before_exit, ...}) => init before_exit target o Local_Theory.exit_global
|
wenzelm@39032
|
209 |
| NONE => error "Not in a named target");
|
haftmann@38617
|
210 |
|
wenzelm@41833
|
211 |
fun context_cmd "-" thy = init I "" thy
|
wenzelm@41833
|
212 |
| context_cmd target thy = init I (Locale.intern thy target) thy;
|
wenzelm@33282
|
213 |
|
wenzelm@20894
|
214 |
end;
|