author | wenzelm |
Wed, 09 Dec 2015 16:36:26 +0100 | |
changeset 61814 | 1ca1142e1711 |
parent 59127 | 723b11f8ffbf |
child 62876 | 507c90523113 |
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 |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56304
diff
changeset
|
9 |
val the_attributes: Proof.context -> int -> Token.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 |
56199 | 11 |
val get_stored_thms: unit -> thm list |
12 |
val get_stored_thm: unit -> thm |
|
13 |
val store_thms: string * thm list -> unit |
|
14 |
val store_thm: string * thm -> unit |
|
15 |
val bind_thm: string * thm -> unit |
|
16 |
val bind_thms: string * thm list -> unit |
|
27389 | 17 |
end; |
18 |
||
19 |
structure ML_Thms: ML_THMS = |
|
20 |
struct |
|
21 |
||
45592 | 22 |
(* auxiliary data *) |
27389 | 23 |
|
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
|
24 |
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
|
25 |
|
45592 | 26 |
structure Data = Proof_Data |
27389 | 27 |
( |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56304
diff
changeset
|
28 |
type T = Token.src list Inttab.table * thms 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
|
29 |
fun init _ = (Inttab.empty, []); |
27389 | 30 |
); |
31 |
||
45592 | 32 |
val put_attributes = Data.map o apfst o Inttab.update; |
33 |
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name); |
|
34 |
||
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
|
35 |
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
|
36 |
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
|
37 |
val cons_thms = Data.map o apsnd o cons; |
45592 | 38 |
|
39 |
||
40 |
(* attribute source *) |
|
27389 | 41 |
|
53171 | 42 |
val _ = Theory.setup |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
59127
diff
changeset
|
43 |
(ML_Antiquotation.declaration @{binding attributes} Attrib.attribs |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
59127
diff
changeset
|
44 |
(fn _ => fn srcs => fn ctxt => |
59112 | 45 |
let val i = serial () in |
46 |
ctxt |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
59127
diff
changeset
|
47 |
|> put_attributes (i, srcs) |
59112 | 48 |
|> ML_Context.value_decl "attributes" |
49 |
("ML_Thms.the_attributes ML_context " ^ string_of_int i) |
|
50 |
end)); |
|
45592 | 51 |
|
52 |
||
53 |
(* fact references *) |
|
27389 | 54 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
55 |
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
|
56 |
let |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
57 |
val initial = null (get_thmss ctxt); |
59112 | 58 |
val (name, ctxt') = ML_Context.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
|
59 |
val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
27389 | 60 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
61 |
val ml_body = ML_Context.struct_name ctxt ^ "." ^ name; |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
let |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
65 |
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
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
in (decl, ctxt'') end; |
27389 | 70 |
|
53171 | 71 |
val _ = Theory.setup |
56205 | 72 |
(ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #> |
73 |
ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false))); |
|
27389 | 74 |
|
75 |
||
76 |
(* ad-hoc goals *) |
|
77 |
||
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents:
29606
diff
changeset
|
78 |
val and_ = Args.$$$ "and"; |
58866
f81e11391562
clarified syntax -- avoid overlap with command category;
wenzelm
parents:
58045
diff
changeset
|
79 |
val by = Parse.reserved "by"; |
55111 | 80 |
val goal = Scan.unless (by || and_) Args.name_inner_syntax; |
27389 | 81 |
|
53171 | 82 |
val _ = Theory.setup |
56205 | 83 |
(ML_Antiquotation.declaration @{binding lemma} |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
84 |
(Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) -- |
58866
f81e11391562
clarified syntax -- avoid overlap with command category;
wenzelm
parents:
58045
diff
changeset
|
85 |
(Parse.position by -- Method.parse -- Scan.option Method.parse))) |
f81e11391562
clarified syntax -- avoid overlap with command category;
wenzelm
parents:
58045
diff
changeset
|
86 |
(fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt => |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
87 |
let |
58866
f81e11391562
clarified syntax -- avoid overlap with command category;
wenzelm
parents:
58045
diff
changeset
|
88 |
val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2); |
f81e11391562
clarified syntax -- avoid overlap with command category;
wenzelm
parents:
58045
diff
changeset
|
89 |
val _ = Context_Position.reports ctxt reports; |
55515 | 90 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
91 |
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
|
92 |
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
|
93 |
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
|
94 |
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
|
95 |
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
|
96 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
97 |
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
|
98 |
|> 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
|
99 |
|> 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
|
100 |
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
|
101 |
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
|
102 |
(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
|
103 |
in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end)); |
27389 | 104 |
|
56199 | 105 |
|
106 |
(* old-style theorem bindings *) |
|
107 |
||
108 |
structure Stored_Thms = Theory_Data |
|
109 |
( |
|
110 |
type T = thm list; |
|
111 |
val empty = []; |
|
112 |
fun extend _ = []; |
|
113 |
fun merge _ = []; |
|
114 |
); |
|
115 |
||
116 |
fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ()); |
|
117 |
val get_stored_thm = hd o get_stored_thms; |
|
118 |
||
119 |
fun ml_store get (name, ths) = |
|
120 |
let |
|
121 |
val ths' = Context.>>> (Context.map_theory_result |
|
122 |
(Global_Theory.store_thms (Binding.name name, ths))); |
|
123 |
val _ = Theory.setup (Stored_Thms.put ths'); |
|
124 |
val _ = |
|
125 |
if name = "" then () |
|
126 |
else if not (ML_Syntax.is_identifier name) then |
|
127 |
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") |
|
128 |
else |
|
56304
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents:
56275
diff
changeset
|
129 |
ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none |
56199 | 130 |
(ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); |
131 |
val _ = Theory.setup (Stored_Thms.put []); |
|
132 |
in () end; |
|
133 |
||
134 |
val store_thms = ml_store "ML_Thms.get_stored_thms"; |
|
135 |
fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]); |
|
136 |
||
137 |
fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm); |
|
138 |
fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms); |
|
139 |
||
27389 | 140 |
end; |
141 |