author | wenzelm |
Mon, 20 Mar 2023 10:59:27 +0100 | |
changeset 77692 | 3e746e684f4b |
parent 74606 | 40f5c6b2e8aa |
child 78795 | f7e972d567f3 |
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 |
74606 | 11 |
val embedded_lemma: (Proof.context -> thm list * (term list * Proof.context)) parser |
56199 | 12 |
val get_stored_thms: unit -> thm list |
13 |
val get_stored_thm: unit -> thm |
|
14 |
val store_thms: string * thm list -> unit |
|
15 |
val store_thm: string * thm -> unit |
|
16 |
val bind_thm: string * thm -> unit |
|
17 |
val bind_thms: string * thm list -> unit |
|
27389 | 18 |
end; |
19 |
||
20 |
structure ML_Thms: ML_THMS = |
|
21 |
struct |
|
22 |
||
45592 | 23 |
(* auxiliary data *) |
27389 | 24 |
|
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
|
25 |
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
|
26 |
|
45592 | 27 |
structure Data = Proof_Data |
27389 | 28 |
( |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56304
diff
changeset
|
29 |
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
|
30 |
fun init _ = (Inttab.empty, []); |
27389 | 31 |
); |
32 |
||
45592 | 33 |
val put_attributes = Data.map o apfst o Inttab.update; |
34 |
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name); |
|
35 |
||
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
|
36 |
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
|
37 |
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
|
38 |
val cons_thms = Data.map o apsnd o cons; |
45592 | 39 |
|
40 |
||
41 |
(* attribute source *) |
|
27389 | 42 |
|
53171 | 43 |
val _ = Theory.setup |
67147 | 44 |
(ML_Antiquotation.declaration \<^binding>\<open>attributes\<close> Attrib.attribs |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
59127
diff
changeset
|
45 |
(fn _ => fn srcs => fn ctxt => |
59112 | 46 |
let val i = serial () in |
47 |
ctxt |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
59127
diff
changeset
|
48 |
|> put_attributes (i, srcs) |
73549
a2c589d5e1e4
clarified signature: more detailed token positions for antiquotations;
wenzelm
parents:
72054
diff
changeset
|
49 |
|> ML_Antiquotation.value_decl "attributes" |
59112 | 50 |
("ML_Thms.the_attributes ML_context " ^ string_of_int i) |
51 |
end)); |
|
45592 | 52 |
|
53 |
||
54 |
(* fact references *) |
|
27389 | 55 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55997
diff
changeset
|
56 |
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
|
57 |
let |
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 initial = null (get_thmss ctxt); |
59112 | 59 |
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
|
60 |
val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
27389 | 61 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
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
|
65 |
let |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
in (decl, ctxt'') end; |
27389 | 71 |
|
53171 | 72 |
val _ = Theory.setup |
67147 | 73 |
(ML_Antiquotation.declaration \<^binding>\<open>thm\<close> (Attrib.thm >> single) (K (thm_binding "thm" true)) #> |
74 |
ML_Antiquotation.declaration \<^binding>\<open>thms\<close> Attrib.thms (K (thm_binding "thms" false))); |
|
27389 | 75 |
|
76 |
||
74603 | 77 |
(* embedded lemma *) |
78 |
||
79 |
val embedded_lemma = |
|
74604 | 80 |
Args.mode "open" -- Parse.and_list1 (Scan.repeat1 Parse.embedded_inner_syntax) |
81 |
-- Parse.for_fixes -- Method.parse_by |
|
82 |
>> (fn (((is_open, raw_stmt), fixes), (methods, reports)) => fn ctxt => |
|
74603 | 83 |
let |
84 |
val _ = Context_Position.reports ctxt reports; |
|
85 |
||
74606 | 86 |
val fixes_ctxt = #2 (Proof_Context.add_fixes_cmd fixes ctxt); |
87 |
val stmt = burrow (map (rpair []) o Syntax.read_props fixes_ctxt) raw_stmt; |
|
88 |
val stmt_ctxt = (fold o fold) (Proof_Context.augment o #1) stmt fixes_ctxt; |
|
74604 | 89 |
|
74603 | 90 |
val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>; |
91 |
fun after_qed res goal_ctxt = |
|
92 |
Proof_Context.put_thms false (Auto_Bind.thisN, |
|
93 |
SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt; |
|
94 |
||
74604 | 95 |
val thms_ctxt = stmt_ctxt |
74603 | 96 |
|> Proof.theorem NONE after_qed stmt |
97 |
|> Proof.global_terminal_proof methods; |
|
98 |
val thms = |
|
74604 | 99 |
Proof_Context.get_fact thms_ctxt |
100 |
(Facts.named (Proof_Context.full_name thms_ctxt (Binding.name Auto_Bind.thisN))) |
|
74606 | 101 |
in (thms, (map #1 (flat stmt), stmt_ctxt)) end); |
27389 | 102 |
|
53171 | 103 |
val _ = Theory.setup |
74603 | 104 |
(ML_Antiquotation.declaration \<^binding>\<open>lemma\<close> (Scan.lift embedded_lemma) |
105 |
(fn _ => fn make_lemma => fn ctxt => |
|
74606 | 106 |
let val thms = #1 (make_lemma ctxt) |
74596 | 107 |
in thm_binding "lemma" (length thms = 1) thms ctxt end)); |
27389 | 108 |
|
56199 | 109 |
|
110 |
(* old-style theorem bindings *) |
|
111 |
||
72054 | 112 |
structure Data = Theory_Data |
56199 | 113 |
( |
114 |
type T = thm list; |
|
115 |
val empty = []; |
|
72054 | 116 |
val merge = #1; |
56199 | 117 |
); |
118 |
||
72054 | 119 |
fun get_stored_thms () = Data.get (Context.the_global_context ()); |
56199 | 120 |
val get_stored_thm = hd o get_stored_thms; |
121 |
||
122 |
fun ml_store get (name, ths) = |
|
123 |
let |
|
67715 | 124 |
val (_, ths') = |
125 |
Context.>>> (Context.map_theory_result |
|
126 |
(Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]))); |
|
72054 | 127 |
val _ = Theory.setup (Data.put ths'); |
56199 | 128 |
val _ = |
129 |
if name = "" then () |
|
130 |
else if not (ML_Syntax.is_identifier name) then |
|
131 |
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") |
|
132 |
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
|
133 |
ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none |
56199 | 134 |
(ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); |
72054 | 135 |
val _ = Theory.setup (Data.put []); |
56199 | 136 |
in () end; |
137 |
||
138 |
val store_thms = ml_store "ML_Thms.get_stored_thms"; |
|
139 |
fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]); |
|
140 |
||
141 |
fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm); |
|
142 |
fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms); |
|
143 |
||
27389 | 144 |
end; |