author | wenzelm |
Wed, 12 Mar 2014 22:57:50 +0100 | |
changeset 56072 | 31e427387ab5 |
parent 56069 | 451d5b73f8cf |
child 56199 | 8e8d28ed7529 |
permissions | -rw-r--r-- |
27389 | 1 |
(* Title: Pure/ML/ml_thms.ML |
2 |
Author: Makarius |
|
3 |
||
45592 | 4 |
Attribute source and theorem values within ML. |
27389 | 5 |
*) |
6 |
||
7 |
signature ML_THMS = |
|
8 |
sig |
|
45592 | 9 |
val the_attributes: Proof.context -> int -> Args.src list |
48782
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
10 |
val the_thmss: Proof.context -> thm list list |
27389 | 11 |
end; |
12 |
||
13 |
structure ML_Thms: ML_THMS = |
|
14 |
struct |
|
15 |
||
45592 | 16 |
(* auxiliary data *) |
27389 | 17 |
|
48782
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
18 |
type thms = (string * bool) * thm list; (*name, single, value*) |
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
19 |
|
45592 | 20 |
structure Data = Proof_Data |
27389 | 21 |
( |
48782
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
22 |
type T = Args.src list Inttab.table * thms list; |
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
23 |
fun init _ = (Inttab.empty, []); |
27389 | 24 |
); |
25 |
||
45592 | 26 |
val put_attributes = Data.map o apfst o Inttab.update; |
27 |
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name); |
|
28 |
||
48782
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
29 |
val get_thmss = snd o Data.get; |
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
30 |
val the_thmss = map snd o get_thmss; |
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
31 |
val cons_thms = Data.map o apsnd o cons; |
45592 | 32 |
|
33 |
||
34 |
||
35 |
(* attribute source *) |
|
27389 | 36 |
|
53171 | 37 |
val _ = Theory.setup |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
38 |
(ML_Context.antiquotation @{binding attributes} (Scan.lift Parse_Spec.attribs) |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
39 |
(fn _ => fn raw_srcs => fn ctxt => |
53171 | 40 |
let |
41 |
val i = serial (); |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55914
diff
changeset
|
42 |
val srcs = map (Attrib.check_src ctxt) raw_srcs; |
53171 | 43 |
val _ = map (Attrib.attribute ctxt) srcs; |
44 |
val (a, ctxt') = ctxt |
|
56072 | 45 |
|> ML_Antiquotation.variant "attributes" ||> put_attributes (i, srcs); |
53171 | 46 |
val ml = |
47 |
("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ |
|
48 |
string_of_int i ^ ";\n", "Isabelle." ^ a); |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
49 |
in (K ml, ctxt') end)); |
45592 | 50 |
|
51 |
||
52 |
(* fact references *) |
|
27389 | 53 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
54 |
fun thm_binding kind is_single thms ctxt = |
48782
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
55 |
let |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
56 |
val initial = null (get_thmss ctxt); |
56072 | 57 |
val (name, ctxt') = ML_Antiquotation.variant kind ctxt; |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
58 |
val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
27389 | 59 |
|
48782
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
60 |
val ml_body = "Isabelle." ^ name; |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
61 |
fun decl final_ctxt = |
48782
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
62 |
if initial then |
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
63 |
let |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
64 |
val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a); |
48782
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
65 |
val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n"; |
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
66 |
in (ml_env, ml_body) end |
e955964d89cb
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents:
48776
diff
changeset
|
67 |
else ("", ml_body); |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
68 |
in (decl, ctxt'') end; |
27389 | 69 |
|
53171 | 70 |
val _ = Theory.setup |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
71 |
(ML_Context.antiquotation @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #> |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
72 |
ML_Context.antiquotation @{binding thms} Attrib.thms (K (thm_binding "thms" false))); |
27389 | 73 |
|
74 |
||
75 |
(* ad-hoc goals *) |
|
76 |
||
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents:
29606
diff
changeset
|
77 |
val and_ = Args.$$$ "and"; |
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27521
diff
changeset
|
78 |
val by = Args.$$$ "by"; |
55111 | 79 |
val goal = Scan.unless (by || and_) Args.name_inner_syntax; |
27389 | 80 |
|
53171 | 81 |
val _ = Theory.setup |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
82 |
(ML_Context.antiquotation @{binding lemma} |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
83 |
(Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) -- |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
84 |
(by |-- Method.parse -- Scan.option Method.parse))) |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
85 |
(fn _ => fn ((is_open, raw_propss), (m1, m2)) => fn ctxt => |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
86 |
let |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
87 |
val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2)); |
55515 | 88 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
89 |
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
90 |
val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
91 |
fun after_qed res goal_ctxt = |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
92 |
Proof_Context.put_thms false (Auto_Bind.thisN, |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
93 |
SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt; |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
94 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
95 |
val ctxt' = ctxt |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
96 |
|> Proof.theorem NONE after_qed propss |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
97 |
|> Proof.global_terminal_proof (m1, m2); |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
98 |
val thms = |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
99 |
Proof_Context.get_fact ctxt' |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
100 |
(Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
101 |
in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end)); |
27389 | 102 |
|
103 |
end; |
|
104 |