author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 52230 | 1105b3b5aa77 |
child 54742 | 7a86358a3c0b |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: Pure/Isar/generic_target.ML |
38309 | 2 |
Author: Makarius |
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
5 |
Common target infrastructure. |
|
6 |
*) |
|
7 |
||
8 |
signature GENERIC_TARGET = |
|
9 |
sig |
|
40782 | 10 |
val define: (((binding * typ) * mixfix) * (binding * term) -> |
11 |
term list * term list -> local_theory -> (term * thm) * local_theory) -> |
|
46992
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46916
diff
changeset
|
12 |
bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
40782 | 13 |
(term * (string * thm)) * local_theory |
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
14 |
val notes: |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
15 |
(string -> (Attrib.binding * (thm list * Args.src list) list) list -> |
40782 | 16 |
(Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) -> |
17 |
string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> |
|
18 |
(string * thm list) list * local_theory |
|
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
19 |
val locale_notes: string -> string -> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
20 |
(Attrib.binding * (thm list * Args.src list) list) list -> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
21 |
(Attrib.binding * (thm list * Args.src list) list) list -> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
22 |
local_theory -> local_theory |
40782 | 23 |
val abbrev: (string * bool -> binding * mixfix -> term * term -> |
24 |
term list -> local_theory -> local_theory) -> |
|
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
25 |
string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory |
47081
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
26 |
val background_declaration: declaration -> local_theory -> local_theory |
47280 | 27 |
val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory |
47282 | 28 |
val standard_declaration: (int -> bool) -> declaration -> local_theory -> local_theory |
29 |
val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term -> |
|
30 |
Context.generic -> Context.generic |
|
31 |
val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> |
|
32 |
local_theory -> local_theory |
|
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
33 |
val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> |
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
34 |
term list * term list -> local_theory -> (term * thm) * local_theory |
40782 | 35 |
val theory_foundation: ((binding * typ) * mixfix) * (binding * term) -> |
36 |
term list * term list -> local_theory -> (term * thm) * local_theory |
|
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
37 |
val theory_notes: string -> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
38 |
(Attrib.binding * (thm list * Args.src list) list) list -> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
39 |
(Attrib.binding * (thm list * Args.src list) list) list -> |
40782 | 40 |
local_theory -> local_theory |
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
41 |
val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list -> |
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
42 |
local_theory -> local_theory |
47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47276
diff
changeset
|
43 |
val theory_declaration: declaration -> local_theory -> local_theory |
52153
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
44 |
val theory_registration: string * morphism -> (morphism * bool) option -> morphism -> |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
45 |
local_theory -> local_theory |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
46 |
val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism -> |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
47 |
local_theory -> local_theory |
45353 | 48 |
end |
38309 | 49 |
|
50 |
structure Generic_Target: GENERIC_TARGET = |
|
51 |
struct |
|
52 |
||
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
53 |
(** lifting primitive to target operations **) |
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
54 |
|
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
55 |
(* mixfix syntax *) |
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
56 |
|
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
57 |
fun check_mixfix ctxt (b, extra_tfrees) mx = |
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
58 |
if null extra_tfrees then mx |
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
59 |
else |
38831
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38757
diff
changeset
|
60 |
(Context_Position.if_visible ctxt warning |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42375
diff
changeset
|
61 |
("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
62 |
commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^ |
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
63 |
(if mx = NoSyn then "" |
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
41959
diff
changeset
|
64 |
else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))); |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
65 |
NoSyn); |
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
66 |
|
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
67 |
fun check_mixfix_global (b, no_params) mx = |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
68 |
if no_params orelse mx = NoSyn then mx |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
69 |
else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
70 |
Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
71 |
|
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
72 |
|
38309 | 73 |
(* define *) |
74 |
||
46992
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46916
diff
changeset
|
75 |
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy = |
38309 | 76 |
let |
42360 | 77 |
val thy = Proof_Context.theory_of lthy; |
78 |
val thy_ctxt = Proof_Context.init_global thy; |
|
38309 | 79 |
|
80 |
(*term and type parameters*) |
|
47276 | 81 |
val ((defs, _), rhs') = Thm.cterm_of thy rhs |
82 |
|> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; |
|
38309 | 83 |
|
47272
ca31cfa509b1
refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
wenzelm
parents:
47250
diff
changeset
|
84 |
val xs = Variable.add_fixed lthy rhs' []; |
38309 | 85 |
val T = Term.fastype_of rhs; |
86 |
val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []); |
|
87 |
val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs [])); |
|
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
88 |
val mx' = check_mixfix lthy (b, extra_tfrees) mx; |
38309 | 89 |
|
90 |
val type_params = map (Logic.mk_type o TFree) extra_tfrees; |
|
47272
ca31cfa509b1
refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
wenzelm
parents:
47250
diff
changeset
|
91 |
val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs); |
38309 | 92 |
val params = type_params @ term_params; |
93 |
||
94 |
val U = map Term.fastype_of params ---> T; |
|
95 |
||
96 |
(*foundation*) |
|
45353 | 97 |
val ((lhs', global_def), lthy2) = lthy |
98 |
|> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params); |
|
38309 | 99 |
|
100 |
(*local definition*) |
|
38315 | 101 |
val ((lhs, local_def), lthy3) = lthy2 |
38309 | 102 |
|> Local_Defs.add_def ((b, NoSyn), lhs'); |
47240 | 103 |
|
104 |
(*result*) |
|
47238 | 105 |
val def = |
47240 | 106 |
Thm.transitive local_def global_def |
107 |
|> Local_Defs.contract defs |
|
108 |
(Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs))); |
|
38315 | 109 |
val ([(res_name, [res])], lthy4) = lthy3 |
47080 | 110 |
|> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; |
38315 | 111 |
in ((lhs, (res_name, res)), lthy4) end; |
38309 | 112 |
|
113 |
||
114 |
(* notes *) |
|
115 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
116 |
local |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
117 |
|
38309 | 118 |
fun import_export_proof ctxt (name, raw_th) = |
119 |
let |
|
42360 | 120 |
val thy = Proof_Context.theory_of ctxt; |
121 |
val thy_ctxt = Proof_Context.init_global thy; |
|
38309 | 122 |
val certT = Thm.ctyp_of thy; |
123 |
val cert = Thm.cterm_of thy; |
|
124 |
||
125 |
(*export assumes/defines*) |
|
126 |
val th = Goal.norm_result raw_th; |
|
45407
a83574606719
more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents:
45390
diff
changeset
|
127 |
val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th; |
52230 | 128 |
val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms; |
38309 | 129 |
|
130 |
(*export fixes*) |
|
131 |
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); |
|
132 |
val frees = map Free (Thm.fold_terms Term.add_frees th' []); |
|
45352 | 133 |
val (th'' :: vs) = |
134 |
(th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees)) |
|
38309 | 135 |
|> Variable.export ctxt thy_ctxt |
136 |
|> Drule.zero_var_indexes_list; |
|
137 |
||
138 |
(*thm definition*) |
|
45413
117ff038f8f7
disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
wenzelm
parents:
45407
diff
changeset
|
139 |
val result = Global_Theory.name_thm true true name th''; |
38309 | 140 |
|
141 |
(*import fixes*) |
|
142 |
val (tvars, vars) = |
|
143 |
chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |
|
144 |
|>> map Logic.dest_type; |
|
145 |
||
146 |
val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); |
|
147 |
val inst = filter (is_Var o fst) (vars ~~ frees); |
|
148 |
val cinstT = map (pairself certT o apfst TVar) instT; |
|
149 |
val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst; |
|
150 |
val result' = Thm.instantiate (cinstT, cinst) result; |
|
151 |
||
152 |
(*import assumes/defines*) |
|
153 |
val result'' = |
|
45407
a83574606719
more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents:
45390
diff
changeset
|
154 |
(fold (curry op COMP) asms' result' |
a83574606719
more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents:
45390
diff
changeset
|
155 |
handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms')) |
47238 | 156 |
|> Local_Defs.contract defs (Thm.cprop_of th) |
38309 | 157 |
|> Goal.norm_result |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38831
diff
changeset
|
158 |
|> Global_Theory.name_thm false false name; |
38309 | 159 |
|
160 |
in (result'', result) end; |
|
161 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
162 |
fun standard_facts lthy ctxt = |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
163 |
Element.transform_facts (Local_Theory.standard_morphism lthy ctxt); |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
164 |
|
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
165 |
in |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
166 |
|
38309 | 167 |
fun notes target_notes kind facts lthy = |
168 |
let |
|
169 |
val facts' = facts |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38831
diff
changeset
|
170 |
|> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi |
38309 | 171 |
(Local_Theory.full_name lthy (fst a))) bs)) |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38831
diff
changeset
|
172 |
|> Global_Theory.map_facts (import_export_proof lthy); |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38831
diff
changeset
|
173 |
val local_facts = Global_Theory.map_facts #1 facts'; |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38831
diff
changeset
|
174 |
val global_facts = Global_Theory.map_facts #2 facts'; |
38309 | 175 |
in |
176 |
lthy |
|
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
177 |
|> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts) |
47249
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47246
diff
changeset
|
178 |
|> Attrib.local_notes kind local_facts |
38309 | 179 |
end; |
180 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
181 |
fun locale_notes locale kind global_facts local_facts = |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
182 |
Local_Theory.background_theory |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
183 |
(Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
184 |
(fn lthy => lthy |> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
185 |
Local_Theory.target (fn ctxt => ctxt |> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
186 |
Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
187 |
(fn lthy => lthy |> |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
188 |
Local_Theory.map_contexts (fn level => fn ctxt => |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
189 |
if level = 0 orelse level = Local_Theory.level lthy then ctxt |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
190 |
else ctxt |> Attrib.local_notes kind (standard_facts lthy ctxt local_facts) |> snd)); |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
191 |
|
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
192 |
end; |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
193 |
|
38309 | 194 |
|
195 |
(* abbrev *) |
|
196 |
||
197 |
fun abbrev target_abbrev prmode ((b, mx), t) lthy = |
|
198 |
let |
|
42360 | 199 |
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); |
38309 | 200 |
|
47292
1884d34e9aab
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
wenzelm
parents:
47291
diff
changeset
|
201 |
val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t; |
47290 | 202 |
val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' [])); |
38309 | 203 |
val u = fold_rev lambda xs t'; |
47290 | 204 |
val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; |
38309 | 205 |
|
206 |
val extra_tfrees = |
|
207 |
subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []); |
|
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
208 |
val mx' = check_mixfix lthy (b, extra_tfrees) mx; |
38309 | 209 |
in |
210 |
lthy |
|
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
211 |
|> target_abbrev prmode (b, mx') (global_rhs, t') xs |
42360 | 212 |
|> Proof_Context.add_abbrev Print_Mode.internal (b, t) |> snd |
38309 | 213 |
|> Local_Defs.fixed_abbrev ((b, NoSyn), t) |
214 |
end; |
|
215 |
||
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
216 |
|
47081
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
217 |
(* declaration *) |
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
218 |
|
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
219 |
fun background_declaration decl lthy = |
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
220 |
let |
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
221 |
val theory_decl = |
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
222 |
Local_Theory.standard_form lthy |
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
223 |
(Proof_Context.init_global (Proof_Context.theory_of lthy)) decl; |
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
224 |
in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end; |
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
225 |
|
47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset
|
226 |
fun locale_declaration locale syntax decl lthy = lthy |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset
|
227 |
|> Local_Theory.target (fn ctxt => ctxt |> |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset
|
228 |
Locale.add_declaration locale syntax |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset
|
229 |
(Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); |
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset
|
230 |
|
47282 | 231 |
fun standard_declaration pred decl lthy = |
232 |
Local_Theory.map_contexts (fn level => fn ctxt => |
|
233 |
if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt |
|
234 |
else ctxt) lthy; |
|
235 |
||
236 |
||
237 |
(* const declaration *) |
|
238 |
||
239 |
fun generic_const same_shape prmode ((b, mx), t) context = |
|
240 |
let |
|
241 |
val const_alias = |
|
242 |
if same_shape then |
|
243 |
(case t of |
|
244 |
Const (c, T) => |
|
245 |
let |
|
246 |
val thy = Context.theory_of context; |
|
247 |
val ctxt = Context.proof_of context; |
|
248 |
in |
|
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
249 |
(case Type_Infer_Context.const_type ctxt c of |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
250 |
SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
251 |
| NONE => NONE) |
47282 | 252 |
end |
253 |
| _ => NONE) |
|
254 |
else NONE; |
|
255 |
in |
|
256 |
(case const_alias of |
|
257 |
SOME c => |
|
258 |
context |
|
259 |
|> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c) |
|
260 |
|> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)]) |
|
261 |
| NONE => |
|
262 |
context |
|
47288
b79bf8288b29
clarified generic_const vs. close_schematic_term;
wenzelm
parents:
47286
diff
changeset
|
263 |
|> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t) |
47282 | 264 |
|-> (fn (const as Const (c, _), _) => same_shape ? |
265 |
(Proof_Context.generic_revert_abbrev (#1 prmode) c #> |
|
266 |
Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) |
|
267 |
end; |
|
268 |
||
269 |
fun const_declaration pred prmode ((b, mx), rhs) = |
|
270 |
standard_declaration pred (fn phi => |
|
271 |
let |
|
272 |
val b' = Morphism.binding phi b; |
|
273 |
val rhs' = Morphism.term phi rhs; |
|
274 |
val same_shape = Term.aconv_untyped (rhs, rhs'); |
|
47288
b79bf8288b29
clarified generic_const vs. close_schematic_term;
wenzelm
parents:
47286
diff
changeset
|
275 |
in generic_const same_shape prmode ((b', mx), rhs') end); |
47280 | 276 |
|
47081
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset
|
277 |
|
52153
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
278 |
(* registrations and dependencies *) |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
279 |
|
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
280 |
val theory_registration = |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
281 |
Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration; |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
282 |
|
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
283 |
fun locale_dependency locale dep_morph mixin export = |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
284 |
(Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
285 |
#> Local_Theory.activate_nonbrittle dep_morph mixin export; |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
286 |
|
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
287 |
|
45352 | 288 |
|
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
289 |
(** primitive theory operations **) |
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
290 |
|
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
291 |
fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
292 |
let |
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
293 |
val params = type_params @ term_params; |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
294 |
val mx' = check_mixfix_global (b, null params) mx; |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
295 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset
|
296 |
val (const, lthy2) = lthy |
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
297 |
|> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
298 |
val lhs = Term.list_comb (const, params); |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
299 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset
|
300 |
val ((_, def), lthy3) = lthy2 |
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset
|
301 |
|> Local_Theory.background_theory_result |
46916
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
45413
diff
changeset
|
302 |
(Thm.add_def lthy2 false false |
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
45413
diff
changeset
|
303 |
(Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
304 |
in ((lhs, def), lthy3) end; |
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
305 |
|
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
306 |
fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
307 |
background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) |
47285
ca4cf5de366c
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents:
47284
diff
changeset
|
308 |
#-> (fn (lhs, def) => fn lthy' => lthy' |> |
ca4cf5de366c
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents:
47284
diff
changeset
|
309 |
const_declaration (fn level => level <> Local_Theory.level lthy') |
ca4cf5de366c
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents:
47284
diff
changeset
|
310 |
Syntax.mode_default ((b, mx), lhs) |
ca4cf5de366c
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents:
47284
diff
changeset
|
311 |
|> pair (lhs, def)); |
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
312 |
|
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
313 |
fun theory_notes kind global_facts local_facts = |
47249
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47246
diff
changeset
|
314 |
Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #> |
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
315 |
(fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt => |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
316 |
if level = Local_Theory.level lthy then ctxt |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
317 |
else |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
318 |
ctxt |> Attrib.local_notes kind |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
319 |
(Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd)); |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
320 |
|
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
321 |
fun theory_abbrev prmode (b, mx) (t, _) xs = |
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
322 |
Local_Theory.background_theory_result |
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:
38341
diff
changeset
|
323 |
(Sign.add_abbrev (#1 prmode) (b, t) #-> |
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
324 |
(fn (lhs, _) => (* FIXME type_params!? *) |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
325 |
Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs)) |
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
326 |
#-> (fn lhs => fn lthy' => lthy' |> |
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
327 |
const_declaration (fn level => level <> Local_Theory.level lthy') prmode |
47293
052cd5f1a591
another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
wenzelm
parents:
47292
diff
changeset
|
328 |
((b, if null xs then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
329 |
|
47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47276
diff
changeset
|
330 |
fun theory_declaration decl = |
47282 | 331 |
background_declaration decl #> standard_declaration (K true) decl; |
47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47276
diff
changeset
|
332 |
|
38309 | 333 |
end; |