| changeset 47876 | 421760a1efe7 |
| parent 47872 | a0e370d3d149 |
| child 48123 | 23654b331d5c |
| 47875:6f00d8a83eb7 | 47876:421760a1efe7 |
|---|---|
19 val set_mode: mode -> Proof.context -> Proof.context |
19 val set_mode: mode -> Proof.context -> Proof.context |
20 val get_mode: Proof.context -> mode |
20 val get_mode: Proof.context -> mode |
21 val restore_mode: Proof.context -> Proof.context -> Proof.context |
21 val restore_mode: Proof.context -> Proof.context -> Proof.context |
22 val abbrev_mode: Proof.context -> bool |
22 val abbrev_mode: Proof.context -> bool |
23 val set_stmt: bool -> Proof.context -> Proof.context |
23 val set_stmt: bool -> Proof.context -> Proof.context |
24 val local_naming: Name_Space.naming |
|
25 val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context |
|
26 val naming_of: Proof.context -> Name_Space.naming |
|
27 val restore_naming: Proof.context -> Proof.context -> Proof.context |
|
28 val full_name: Proof.context -> binding -> string |
|
29 val syntax_of: Proof.context -> Local_Syntax.T |
24 val syntax_of: Proof.context -> Local_Syntax.T |
30 val syn_of: Proof.context -> Syntax.syntax |
25 val syn_of: Proof.context -> Syntax.syntax |
31 val tsig_of: Proof.context -> Type.tsig |
26 val tsig_of: Proof.context -> Type.tsig |
32 val set_defsort: sort -> Proof.context -> Proof.context |
27 val set_defsort: sort -> Proof.context -> Proof.context |
33 val default_sort: Proof.context -> indexname -> sort |
28 val default_sort: Proof.context -> indexname -> sort |
35 val the_const_constraint: Proof.context -> string -> typ |
30 val the_const_constraint: Proof.context -> string -> typ |
36 val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context |
31 val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context |
37 val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context |
32 val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context |
38 val facts_of: Proof.context -> Facts.T |
33 val facts_of: Proof.context -> Facts.T |
39 val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list |
34 val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list |
35 val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context |
|
36 val naming_of: Proof.context -> Name_Space.naming |
|
37 val restore_naming: Proof.context -> Proof.context -> Proof.context |
|
38 val full_name: Proof.context -> binding -> string |
|
40 val class_space: Proof.context -> Name_Space.T |
39 val class_space: Proof.context -> Name_Space.T |
41 val type_space: Proof.context -> Name_Space.T |
40 val type_space: Proof.context -> Name_Space.T |
42 val const_space: Proof.context -> Name_Space.T |
41 val const_space: Proof.context -> Name_Space.T |
43 val intern_class: Proof.context -> xstring -> string |
42 val intern_class: Proof.context -> xstring -> string |
44 val intern_type: Proof.context -> xstring -> string |
43 val intern_type: Proof.context -> xstring -> string |
139 val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context |
138 val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context |
140 val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> |
139 val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> |
141 Context.generic -> Context.generic |
140 Context.generic -> Context.generic |
142 val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism -> |
141 val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism -> |
143 Context.generic -> Context.generic |
142 Context.generic -> Context.generic |
144 val target_naming_of: Context.generic -> Name_Space.naming |
|
145 val class_alias: binding -> class -> Proof.context -> Proof.context |
143 val class_alias: binding -> class -> Proof.context -> Proof.context |
146 val type_alias: binding -> string -> Proof.context -> Proof.context |
144 val type_alias: binding -> string -> Proof.context -> Proof.context |
147 val const_alias: binding -> string -> Proof.context -> Proof.context |
145 val const_alias: binding -> string -> Proof.context -> Proof.context |
148 val add_const_constraint: string * typ option -> Proof.context -> Proof.context |
146 val add_const_constraint: string * typ option -> Proof.context -> Proof.context |
149 val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context |
147 val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context |
190 (** Isar proof context information **) |
188 (** Isar proof context information **) |
191 |
189 |
192 datatype data = |
190 datatype data = |
193 Data of |
191 Data of |
194 {mode: mode, (*inner syntax mode*) |
192 {mode: mode, (*inner syntax mode*) |
195 naming: Name_Space.naming, (*local naming conventions*) |
|
196 syntax: Local_Syntax.T, (*local syntax*) |
193 syntax: Local_Syntax.T, (*local syntax*) |
197 tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*) |
194 tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*) |
198 consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*) |
195 consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*) |
199 facts: Facts.T, (*local facts*) |
196 facts: Facts.T, (*local facts*) |
200 cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*) |
197 cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*) |
201 |
198 |
202 fun make_data (mode, naming, syntax, tsig, consts, facts, cases) = |
199 fun make_data (mode, syntax, tsig, consts, facts, cases) = |
203 Data {mode = mode, naming = naming, syntax = syntax, |
200 Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases}; |
204 tsig = tsig, consts = consts, facts = facts, cases = cases}; |
|
205 |
|
206 val local_naming = Name_Space.default_naming |> Name_Space.add_path "local"; |
|
207 |
201 |
208 structure Data = Proof_Data |
202 structure Data = Proof_Data |
209 ( |
203 ( |
210 type T = data; |
204 type T = data; |
211 fun init thy = |
205 fun init thy = |
212 make_data (mode_default, local_naming, Local_Syntax.init thy, |
206 make_data (mode_default, Local_Syntax.init thy, |
213 (Sign.tsig_of thy, Sign.tsig_of thy), |
207 (Sign.tsig_of thy, Sign.tsig_of thy), |
214 (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []); |
208 (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []); |
215 ); |
209 ); |
216 |
210 |
217 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); |
211 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); |
218 |
212 |
219 fun map_data f = |
213 fun map_data f = |
220 Data.map (fn Data {mode, naming, syntax, tsig, consts, facts, cases} => |
214 Data.map (fn Data {mode, syntax, tsig, consts, facts, cases} => |
221 make_data (f (mode, naming, syntax, tsig, consts, facts, cases))); |
215 make_data (f (mode, syntax, tsig, consts, facts, cases))); |
222 |
216 |
223 fun set_mode mode = map_data (fn (_, naming, syntax, tsig, consts, facts, cases) => |
217 fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) => |
224 (mode, naming, syntax, tsig, consts, facts, cases)); |
218 (mode, syntax, tsig, consts, facts, cases)); |
225 |
219 |
226 fun map_mode f = |
220 fun map_mode f = |
227 map_data (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) => |
221 map_data (fn (Mode {stmt, pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) => |
228 (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases)); |
222 (make_mode (f (stmt, pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases)); |
229 |
|
230 fun map_naming f = |
|
231 map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => |
|
232 (mode, f naming, syntax, tsig, consts, facts, cases)); |
|
233 |
223 |
234 fun map_syntax f = |
224 fun map_syntax f = |
235 map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => |
225 map_data (fn (mode, syntax, tsig, consts, facts, cases) => |
236 (mode, naming, f syntax, tsig, consts, facts, cases)); |
226 (mode, f syntax, tsig, consts, facts, cases)); |
237 |
227 |
238 fun map_tsig f = |
228 fun map_tsig f = |
239 map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => |
229 map_data (fn (mode, syntax, tsig, consts, facts, cases) => |
240 (mode, naming, syntax, f tsig, consts, facts, cases)); |
230 (mode, syntax, f tsig, consts, facts, cases)); |
241 |
231 |
242 fun map_consts f = |
232 fun map_consts f = |
243 map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => |
233 map_data (fn (mode, syntax, tsig, consts, facts, cases) => |
244 (mode, naming, syntax, tsig, f consts, facts, cases)); |
234 (mode, syntax, tsig, f consts, facts, cases)); |
245 |
235 |
246 fun map_facts f = |
236 fun map_facts f = |
247 map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => |
237 map_data (fn (mode, syntax, tsig, consts, facts, cases) => |
248 (mode, naming, syntax, tsig, consts, f facts, cases)); |
238 (mode, syntax, tsig, consts, f facts, cases)); |
249 |
239 |
250 fun map_cases f = |
240 fun map_cases f = |
251 map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) => |
241 map_data (fn (mode, syntax, tsig, consts, facts, cases) => |
252 (mode, naming, syntax, tsig, consts, facts, f cases)); |
242 (mode, syntax, tsig, consts, facts, f cases)); |
253 |
243 |
254 val get_mode = #mode o rep_data; |
244 val get_mode = #mode o rep_data; |
255 val restore_mode = set_mode o get_mode; |
245 val restore_mode = set_mode o get_mode; |
256 val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev); |
246 val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev); |
257 |
247 |
258 fun set_stmt stmt = |
248 fun set_stmt stmt = |
259 map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev)); |
249 map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev)); |
260 |
|
261 val naming_of = #naming o rep_data; |
|
262 val restore_naming = map_naming o K o naming_of |
|
263 val full_name = Name_Space.full_name o naming_of; |
|
264 |
250 |
265 val syntax_of = #syntax o rep_data; |
251 val syntax_of = #syntax o rep_data; |
266 val syn_of = Local_Syntax.syn_of o syntax_of; |
252 val syn_of = Local_Syntax.syn_of o syntax_of; |
267 val set_syntax_mode = map_syntax o Local_Syntax.set_mode; |
253 val set_syntax_mode = map_syntax o Local_Syntax.set_mode; |
268 val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; |
254 val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; |
274 val consts_of = #1 o #consts o rep_data; |
260 val consts_of = #1 o #consts o rep_data; |
275 val the_const_constraint = Consts.the_constraint o consts_of; |
261 val the_const_constraint = Consts.the_constraint o consts_of; |
276 |
262 |
277 val facts_of = #facts o rep_data; |
263 val facts_of = #facts o rep_data; |
278 val cases_of = #cases o rep_data; |
264 val cases_of = #cases o rep_data; |
265 |
|
266 |
|
267 (* naming *) |
|
268 |
|
269 val naming_of = Name_Space.naming_of o Context.Proof; |
|
270 val map_naming = Context.proof_map o Name_Space.map_naming; |
|
271 val restore_naming = map_naming o K o naming_of; |
|
272 |
|
273 val full_name = Name_Space.full_name o naming_of; |
|
279 |
274 |
280 |
275 |
281 (* name spaces *) |
276 (* name spaces *) |
282 |
277 |
283 val class_space = Type.class_space o tsig_of; |
278 val class_space = Type.class_space o tsig_of; |
298 fun transfer_syntax thy ctxt = ctxt |> |
293 fun transfer_syntax thy ctxt = ctxt |> |
299 map_syntax (Local_Syntax.rebuild thy) |> |
294 map_syntax (Local_Syntax.rebuild thy) |> |
300 map_tsig (fn tsig as (local_tsig, global_tsig) => |
295 map_tsig (fn tsig as (local_tsig, global_tsig) => |
301 let val thy_tsig = Sign.tsig_of thy in |
296 let val thy_tsig = Sign.tsig_of thy in |
302 if Type.eq_tsig (thy_tsig, global_tsig) then tsig |
297 if Type.eq_tsig (thy_tsig, global_tsig) then tsig |
303 else (Type.merge_tsig ctxt (local_tsig, thy_tsig), thy_tsig) |
298 else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) |
304 end) |> |
299 end) |> |
305 map_consts (fn consts as (local_consts, global_consts) => |
300 map_consts (fn consts as (local_consts, global_consts) => |
306 let val thy_consts = Sign.consts_of thy in |
301 let val thy_consts = Sign.consts_of thy in |
307 if Consts.eq_consts (thy_consts, global_consts) then consts |
302 if Consts.eq_consts (thy_consts, global_consts) then consts |
308 else (Consts.merge (local_consts, thy_consts), thy_consts) |
303 else (Consts.merge (local_consts, thy_consts), thy_consts) |
493 |
488 |
494 local |
489 local |
495 |
490 |
496 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) = |
491 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) = |
497 let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S) |
492 let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S) |
498 in Type.add_arity ctxt arity (tsig_of ctxt); arity end; |
493 in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end; |
499 |
494 |
500 in |
495 in |
501 |
496 |
502 val read_arity = |
497 val read_arity = |
503 prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort; |
498 prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort; |
499 |
|
504 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of); |
500 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of); |
505 |
501 |
506 end; |
502 end; |
507 |
503 |
508 |
504 |
890 |
886 |
891 local |
887 local |
892 |
888 |
893 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b)) |
889 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b)) |
894 | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts |
890 | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts |
895 (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd); |
891 (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd); |
896 |
892 |
897 in |
893 in |
898 |
894 |
899 fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt => |
895 fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt => |
900 let |
896 let |
906 val thms = Global_Theory.name_thms false false name (flat res); |
902 val thms = Global_Theory.name_thms false false name (flat res); |
907 val Mode {stmt, ...} = get_mode ctxt; |
903 val Mode {stmt, ...} = get_mode ctxt; |
908 in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); |
904 in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); |
909 |
905 |
910 fun put_thms do_props thms ctxt = ctxt |
906 fun put_thms do_props thms ctxt = ctxt |
911 |> map_naming (K local_naming) |
907 |> map_naming (K Name_Space.local_naming) |
912 |> Context_Position.set_visible false |
908 |> Context_Position.set_visible false |
913 |> update_thms do_props (apfst Binding.name thms) |
909 |> update_thms do_props (apfst Binding.name thms) |
914 |> Context_Position.restore_visible ctxt |
910 |> Context_Position.restore_visible ctxt |
915 |> restore_naming ctxt; |
911 |> restore_naming ctxt; |
916 |
912 |
991 in Context.mapping (Sign.notation add mode args') (notation add mode args') end; |
987 in Context.mapping (Sign.notation add mode args') (notation add mode args') end; |
992 |
988 |
993 end; |
989 end; |
994 |
990 |
995 |
991 |
996 (* naming *) |
|
997 |
|
998 val target_naming_of = Context.cases Sign.naming_of naming_of; |
|
999 |
|
1000 |
|
1001 (* aliases *) |
992 (* aliases *) |
1002 |
993 |
1003 fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt; |
994 fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt; |
1004 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; |
995 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; |
1005 fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; |
996 fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; |
1018 let |
1009 let |
1019 val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t |
1010 val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t |
1020 handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); |
1011 handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); |
1021 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; |
1012 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; |
1022 val ((lhs, rhs), consts') = consts_of ctxt |
1013 val ((lhs, rhs), consts') = consts_of ctxt |
1023 |> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t); |
1014 |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t); |
1024 in |
1015 in |
1025 ctxt |
1016 ctxt |
1026 |> (map_consts o apfst) (K consts') |
1017 |> (map_consts o apfst) (K consts') |
1027 |> Variable.declare_term rhs |
1018 |> Variable.declare_term rhs |
1028 |> pair (lhs, rhs) |
1019 |> pair (lhs, rhs) |