1 (* Title: HOL/Eisbach/eisbach_antiquotations.ML |
|
2 Author: Daniel Matichuk, NICTA/UNSW |
|
3 |
|
4 ML antiquotations for Eisbach. |
|
5 *) |
|
6 |
|
7 structure Eisbach_Antiquotations: sig end = |
|
8 struct |
|
9 |
|
10 (** evaluate Eisbach method from ML **) |
|
11 |
|
12 val _ = |
|
13 Theory.setup |
|
14 (ML_Antiquotation.inline @{binding method} (* FIXME ML_Antiquotation.value (!?) *) |
|
15 (Args.context -- Scan.lift (Args.mode "drop_cases") -- Scan.lift (Parse.position Parse.name) |
|
16 >> (fn ((ctxt, drop_cases), nameref) => |
|
17 let |
|
18 val ((targs, (factargs, margs)), _) = Method_Closure.get_method ctxt nameref; |
|
19 |
|
20 val has_factargs = not (null factargs); |
|
21 |
|
22 val (targnms, ctxt') = |
|
23 fold_map (fn (Var ((x, _), _)) => ML_Context.variant x) targs ctxt; |
|
24 val (margnms, ctxt'') = fold_map ML_Context.variant margs ctxt'; |
|
25 val (factsnm, _) = ML_Context.variant "facts" ctxt''; |
|
26 |
|
27 val fn_header = |
|
28 margnms |
|
29 |> has_factargs ? append [factsnm] |
|
30 |> append targnms |
|
31 |> map (fn nm => "fn " ^ nm ^ " => ") |
|
32 |> implode; |
|
33 |
|
34 val ML_context = ML_Context.struct_name ctxt ^ ".ML_context"; |
|
35 val ml_inner = |
|
36 ML_Syntax.atomic |
|
37 ("Method_Closure.get_method " ^ ML_context ^ |
|
38 ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position nameref ^ |
|
39 "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_method " ^ |
|
40 ML_context ^ " ((targs, margs), text))"); |
|
41 |
|
42 val drop_cases_suffix = |
|
43 if drop_cases then "#> (fn f => (fn ctxt => fn thms => f ctxt thms |> Seq.map snd))" |
|
44 else ""; |
|
45 |
|
46 val factsnm = if has_factargs then factsnm else "[]"; |
|
47 in |
|
48 ML_Syntax.atomic |
|
49 (fn_header ^ ml_inner ^ " " ^ ML_Syntax.print_list I targnms ^ " " ^ |
|
50 factsnm ^ " " ^ |
|
51 ML_Syntax.print_list I margnms ^ drop_cases_suffix) |
|
52 end))); |
|
53 |
|
54 end; |
|