6 Common theory/locale/class/instantiation/overloading targets. |
6 Common theory/locale/class/instantiation/overloading targets. |
7 *) |
7 *) |
8 |
8 |
9 signature THEORY_TARGET = |
9 signature THEORY_TARGET = |
10 sig |
10 sig |
11 val peek: local_theory -> {target: string, is_locale: bool, |
11 val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool, |
12 is_class: bool, instantiation: string list * (string * sort) list * sort, |
12 is_class: bool, instantiation: string list * (string * sort) list * sort, |
13 overloading: (string * (string * typ) * bool) list} |
13 overloading: (string * (string * typ) * bool) list} |
14 val init: string option -> theory -> local_theory |
14 val init: string option -> theory -> local_theory |
15 val begin: string -> Proof.context -> local_theory |
15 val begin: string -> Proof.context -> local_theory |
16 val context: xstring -> theory -> local_theory |
16 val context: xstring -> theory -> local_theory |
22 structure TheoryTarget: THEORY_TARGET = |
22 structure TheoryTarget: THEORY_TARGET = |
23 struct |
23 struct |
24 |
24 |
25 (* new locales *) |
25 (* new locales *) |
26 |
26 |
27 fun locale_extern is_class x = |
27 fun locale_extern new_locale x = |
28 if !new_locales andalso not is_class then NewLocale.extern x else Locale.extern x; |
28 if !new_locales andalso new_locale then NewLocale.extern x else Locale.extern x; |
29 fun locale_add_type_syntax is_class x = |
29 fun locale_add_type_syntax new_locale x = |
30 if !new_locales andalso not is_class then NewLocale.add_type_syntax x else Locale.add_type_syntax x; |
30 if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x; |
31 fun locale_add_term_syntax is_class x = |
31 fun locale_add_term_syntax new_locale x = |
32 if !new_locales andalso not is_class then NewLocale.add_term_syntax x else Locale.add_term_syntax x; |
32 if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x; |
33 fun locale_add_declaration is_class x = |
33 fun locale_add_declaration new_locale x = |
34 if !new_locales andalso not is_class then NewLocale.add_declaration x else Locale.add_declaration x; |
34 if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x; |
35 fun locale_add_thmss is_class x = |
35 fun locale_add_thmss new_locale x = |
36 if !new_locales andalso not is_class then NewLocale.add_thmss x else Locale.add_thmss x; |
36 if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x; |
37 fun locale_init x = |
37 fun locale_init new_locale x = |
38 if !new_locales then NewLocale.init x else Locale.init x; |
38 if !new_locales andalso new_locale then NewLocale.init x else Locale.init x; |
39 fun locale_intern is_class x = |
39 fun locale_intern new_locale x = |
40 if !new_locales andalso not is_class then NewLocale.intern x else Locale.intern x; |
40 if !new_locales andalso new_locale then NewLocale.intern x else Locale.intern x; |
41 |
41 |
42 (* context data *) |
42 (* context data *) |
43 |
43 |
44 datatype target = Target of {target: string, is_locale: bool, |
44 datatype target = Target of {target: string, new_locale: bool, is_locale: bool, |
45 is_class: bool, instantiation: string list * (string * sort) list * sort, |
45 is_class: bool, instantiation: string list * (string * sort) list * sort, |
46 overloading: (string * (string * typ) * bool) list}; |
46 overloading: (string * (string * typ) * bool) list}; |
47 |
47 |
48 fun make_target target is_locale is_class instantiation overloading = |
48 fun make_target target new_locale is_locale is_class instantiation overloading = |
49 Target {target = target, is_locale = is_locale, |
49 Target {target = target, new_locale = new_locale, is_locale = is_locale, |
50 is_class = is_class, instantiation = instantiation, overloading = overloading}; |
50 is_class = is_class, instantiation = instantiation, overloading = overloading}; |
51 |
51 |
52 val global_target = make_target "" false false ([], [], []) []; |
52 val global_target = make_target "" false false false ([], [], []) []; |
53 |
53 |
54 structure Data = ProofDataFun |
54 structure Data = ProofDataFun |
55 ( |
55 ( |
56 type T = target; |
56 type T = target; |
57 fun init _ = global_target; |
57 fun init _ = global_target; |
78 else if null elems then [Pretty.str target_name] |
78 else if null elems then [Pretty.str target_name] |
79 else [Pretty.big_list (target_name ^ " =") |
79 else [Pretty.big_list (target_name ^ " =") |
80 (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] |
80 (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] |
81 end; |
81 end; |
82 |
82 |
83 fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt = |
83 fun pretty (Target {target, is_locale, is_class, instantiation, overloading, ...}) ctxt = |
84 Pretty.block [Pretty.str "theory", Pretty.brk 1, |
84 Pretty.block [Pretty.str "theory", Pretty.brk 1, |
85 Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: |
85 Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: |
86 (if not (null overloading) then [Overloading.pretty ctxt] |
86 (if not (null overloading) then [Overloading.pretty ctxt] |
87 else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt] |
87 else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt] |
88 else pretty_thy ctxt target is_locale is_class); |
88 else pretty_thy ctxt target is_locale is_class); |
89 |
89 |
90 |
90 |
91 (* target declarations *) |
91 (* target declarations *) |
92 |
92 |
93 fun target_decl add (Target {target, is_class, ...}) d lthy = |
93 fun target_decl add (Target {target, new_locale, ...}) d lthy = |
94 let |
94 let |
95 val d' = Morphism.transform (LocalTheory.target_morphism lthy) d; |
95 val d' = Morphism.transform (LocalTheory.target_morphism lthy) d; |
96 val d0 = Morphism.form d'; |
96 val d0 = Morphism.form d'; |
97 in |
97 in |
98 if target = "" then |
98 if target = "" then |
99 lthy |
99 lthy |
100 |> LocalTheory.theory (Context.theory_map d0) |
100 |> LocalTheory.theory (Context.theory_map d0) |
101 |> LocalTheory.target (Context.proof_map d0) |
101 |> LocalTheory.target (Context.proof_map d0) |
102 else |
102 else |
103 lthy |
103 lthy |
104 |> LocalTheory.target (add is_class target d') |
104 |> LocalTheory.target (add new_locale target d') |
105 end; |
105 end; |
106 |
106 |
107 val type_syntax = target_decl locale_add_type_syntax; |
107 val type_syntax = target_decl locale_add_type_syntax; |
108 val term_syntax = target_decl locale_add_term_syntax; |
108 val term_syntax = target_decl locale_add_term_syntax; |
109 val declaration = target_decl locale_add_declaration; |
109 val declaration = target_decl locale_add_declaration; |
165 ctxt |
165 ctxt |
166 |> ProofContext.qualified_names |
166 |> ProofContext.qualified_names |
167 |> ProofContext.note_thmss_i kind facts |
167 |> ProofContext.note_thmss_i kind facts |
168 ||> ProofContext.restore_naming ctxt; |
168 ||> ProofContext.restore_naming ctxt; |
169 |
169 |
170 fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy = |
170 fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy = |
171 let |
171 let |
172 val thy = ProofContext.theory_of lthy; |
172 val thy = ProofContext.theory_of lthy; |
173 val facts' = facts |
173 val facts' = facts |
174 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi |
174 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi |
175 (LocalTheory.full_name lthy (fst a))) bs)) |
175 (LocalTheory.full_name lthy (fst a))) bs)) |
184 lthy |> LocalTheory.theory |
184 lthy |> LocalTheory.theory |
185 (Sign.qualified_names |
185 (Sign.qualified_names |
186 #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd |
186 #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd |
187 #> Sign.restore_naming thy) |
187 #> Sign.restore_naming thy) |
188 |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd) |
188 |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd) |
189 |> is_locale ? LocalTheory.target (locale_add_thmss is_class target kind target_facts) |
189 |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts) |
190 |> note_local kind local_facts |
190 |> note_local kind local_facts |
191 end; |
191 end; |
192 |
192 |
193 |
193 |
194 (* declare_const *) |
194 (* declare_const *) |
333 |
333 |
334 local |
334 local |
335 |
335 |
336 fun init_target _ NONE = global_target |
336 fun init_target _ NONE = global_target |
337 | init_target thy (SOME target) = |
337 | init_target thy (SOME target) = |
338 make_target target true (Class.is_class thy target) ([], [], []) []; |
338 make_target target (NewLocale.test_locale thy (NewLocale.intern thy target)) |
339 |
339 true (Class.is_class thy target) ([], [], []) []; |
340 fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) = |
340 |
|
341 fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) = |
341 if not (null (#1 instantiation)) then Class.init_instantiation instantiation |
342 if not (null (#1 instantiation)) then Class.init_instantiation instantiation |
342 else if not (null overloading) then Overloading.init overloading |
343 else if not (null overloading) then Overloading.init overloading |
343 else if not is_locale then ProofContext.init |
344 else if not is_locale then ProofContext.init |
344 else if not is_class then locale_init target |
345 else if not is_class then locale_init new_locale target |
345 else Class.init target; |
346 else Class.init target; |
346 |
347 |
347 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = |
348 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = |
348 Data.put ta #> |
349 Data.put ta #> |
349 LocalTheory.init (NameSpace.base target) |
350 LocalTheory.init (NameSpace.base target) |
364 fun gen_overloading prep_const raw_ops thy = |
365 fun gen_overloading prep_const raw_ops thy = |
365 let |
366 let |
366 val ctxt = ProofContext.init thy; |
367 val ctxt = ProofContext.init thy; |
367 val ops = raw_ops |> map (fn (name, const, checked) => |
368 val ops = raw_ops |> map (fn (name, const, checked) => |
368 (name, Term.dest_Const (prep_const ctxt const), checked)); |
369 (name, Term.dest_Const (prep_const ctxt const), checked)); |
369 in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end; |
370 in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end; |
370 |
371 |
371 in |
372 in |
372 |
373 |
373 fun init target thy = init_lthy_ctxt (init_target thy target) thy; |
374 fun init target thy = init_lthy_ctxt (init_target thy target) thy; |
374 fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt; |
375 fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt; |
375 |
376 |
376 fun context "-" thy = init NONE thy |
377 fun context "-" thy = init NONE thy |
377 | context target thy = init (SOME (locale_intern |
378 | context target thy = init (SOME (locale_intern |
378 (not (NewLocale.test_locale thy (NewLocale.intern thy target))) thy target)) thy; |
379 (NewLocale.test_locale thy (NewLocale.intern thy target)) thy target)) thy; |
379 |
380 |
380 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []); |
381 fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []); |
381 |
382 |
382 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); |
383 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); |
383 val overloading_cmd = gen_overloading Syntax.read_term; |
384 val overloading_cmd = gen_overloading Syntax.read_term; |
384 |
385 |
385 end; |
386 end; |