11 val make_ctyp: Proof.context -> typ -> ctyp |
11 val make_ctyp: Proof.context -> typ -> ctyp |
12 val make_cterm: Proof.context -> term -> cterm |
12 val make_cterm: Proof.context -> term -> cterm |
13 type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list |
13 type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list |
14 type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
14 type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
15 val instantiate_typ: insts -> typ -> typ |
15 val instantiate_typ: insts -> typ -> typ |
16 val instantiate_ctyp: cinsts -> ctyp -> ctyp |
16 val instantiate_ctyp: Position.T -> cinsts -> ctyp -> ctyp |
17 val instantiate_term: insts -> term -> term |
17 val instantiate_term: insts -> term -> term |
18 val instantiate_cterm: cinsts -> cterm -> cterm |
18 val instantiate_cterm: Position.T -> cinsts -> cterm -> cterm |
19 end; |
19 end; |
20 |
20 |
21 structure ML_Antiquotations: ML_ANTIQUOTATIONS = |
21 structure ML_Antiquotations: ML_ANTIQUOTATIONS = |
22 struct |
22 struct |
23 |
23 |
233 fun make_cterm ctxt t = Thm.cterm_of ctxt t |> Thm.trim_context_cterm; |
233 fun make_cterm ctxt t = Thm.cterm_of ctxt t |> Thm.trim_context_cterm; |
234 |
234 |
235 type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list |
235 type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list |
236 type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
236 type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
237 |
237 |
238 fun instantiate_typ (insts: insts) = Term_Subst.instantiateT (TVars.make (#1 insts)); |
238 fun instantiate_typ (insts: insts) = |
239 fun instantiate_ctyp (cinsts: cinsts) = Thm.instantiate_ctyp (TVars.make (#1 cinsts)); |
239 Term_Subst.instantiateT (TVars.make (#1 insts)); |
|
240 |
|
241 fun instantiate_ctyp pos (cinsts: cinsts) cT = |
|
242 Thm.instantiate_ctyp (TVars.make (#1 cinsts)) cT |
|
243 handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args)); |
240 |
244 |
241 fun instantiate_term (insts: insts) = |
245 fun instantiate_term (insts: insts) = |
242 let |
246 let |
243 val instT = TVars.make (#1 insts); |
247 val instT = TVars.make (#1 insts); |
244 val instantiateT = Term_Subst.instantiateT instT; |
248 val instantiateT = Term_Subst.instantiateT instT; |
245 val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts)); |
249 val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts)); |
246 in Term_Subst.instantiate_beta (instT, inst) end; |
250 in Term_Subst.instantiate_beta (instT, inst) end; |
247 |
251 |
248 fun instantiate_cterm (cinsts: cinsts) = |
252 fun instantiate_cterm pos (cinsts: cinsts) ct = |
249 let |
253 let |
250 val cinstT = TVars.make (#1 cinsts); |
254 val cinstT = TVars.make (#1 cinsts); |
251 val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT); |
255 val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT); |
252 val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts)); |
256 val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts)); |
253 in Thm.instantiate_beta_cterm (cinstT, cinst) end; |
257 in Thm.instantiate_beta_cterm (cinstT, cinst) ct end |
|
258 handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args)); |
254 |
259 |
255 |
260 |
256 local |
261 local |
257 |
262 |
258 fun make_keywords ctxt = |
263 fun make_keywords ctxt = |
336 val t = read ctxt' s; |
341 val t = read ctxt' s; |
337 val ctxt1 = Proof_Context.augment t ctxt'; |
342 val ctxt1 = Proof_Context.augment t ctxt'; |
338 val (ml_insts, t') = prepare_insts ctxt1 ctxt insts t; |
343 val (ml_insts, t') = prepare_insts ctxt1 ctxt insts t; |
339 in prepare_ml range arg (ML_Syntax.print_term t') ml_insts ctxt end; |
344 in prepare_ml range arg (ML_Syntax.print_term t') ml_insts ctxt end; |
340 |
345 |
341 fun typ_ml kind = (kind, "", "ML_Antiquotations.instantiate_typ"); |
346 val ml_here = ML_Syntax.atomic o ML_Syntax.print_position; |
342 fun term_ml kind = (kind, "", "ML_Antiquotations.instantiate_term"); |
347 |
343 fun ctyp_ml kind = |
348 fun typ_ml (kind, _: Position.T) = (kind, "", "ML_Antiquotations.instantiate_typ "); |
344 (kind, "ML_Antiquotations.make_ctyp ML_context", "ML_Antiquotations.instantiate_ctyp"); |
349 fun term_ml (kind, _: Position.T) = (kind, "", "ML_Antiquotations.instantiate_term "); |
345 fun cterm_ml kind = |
350 fun ctyp_ml (kind, pos) = |
346 (kind, "ML_Antiquotations.make_cterm ML_context", "ML_Antiquotations.instantiate_cterm"); |
351 (kind, "ML_Antiquotations.make_ctyp ML_context", |
|
352 "ML_Antiquotations.instantiate_ctyp " ^ ml_here pos); |
|
353 fun cterm_ml (kind, pos) = |
|
354 (kind, "ML_Antiquotations.make_cterm ML_context", |
|
355 "ML_Antiquotations.instantiate_cterm " ^ ml_here pos); |
|
356 |
|
357 val command_name = Parse.position o Parse.command_name; |
347 |
358 |
348 fun parse_body range = |
359 fun parse_body range = |
349 (Parse.command_name "typ" >> typ_ml || Parse.command_name "ctyp" >> ctyp_ml) -- |
360 (command_name "typ" >> typ_ml || command_name "ctyp" >> ctyp_ml) -- |
350 Parse.!!! Parse.typ >> prepare_type range || |
361 Parse.!!! Parse.typ >> prepare_type range || |
351 (Parse.command_name "term" >> term_ml || Parse.command_name "cterm" >> cterm_ml) |
362 (command_name "term" >> term_ml || command_name "cterm" >> cterm_ml) |
352 -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range || |
363 -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range || |
353 (Parse.command_name "prop" >> term_ml || Parse.command_name "cprop" >> cterm_ml) |
364 (command_name "prop" >> term_ml || command_name "cprop" >> cterm_ml) |
354 -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_prop range; |
365 -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_prop range; |
355 |
366 |
356 val _ = Theory.setup |
367 val _ = Theory.setup |
357 (ML_Context.add_antiquotation \<^binding>\<open>instantiate\<close> true |
368 (ML_Context.add_antiquotation \<^binding>\<open>instantiate\<close> true |
358 (fn range => fn src => fn ctxt => |
369 (fn range => fn src => fn ctxt => |