author | wenzelm |
Sat, 08 Mar 2014 21:08:10 +0100 | |
changeset 55997 | 9dc5ce83202c |
parent 55914 | c5b752d549e3 |
child 56069 | 451d5b73f8cf |
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 |
55516 | 38 |
(ML_Context.add_antiq @{binding attributes} |
53171 | 39 |
(Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs => |
40 |
let |
|
41 |
val ctxt = Context.the_proof context; |
|
45592 | 42 |
|
53171 | 43 |
val i = serial (); |
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55914
diff
changeset
|
44 |
val srcs = map (Attrib.check_src ctxt) raw_srcs; |
53171 | 45 |
val _ = map (Attrib.attribute ctxt) srcs; |
46 |
val (a, ctxt') = ctxt |
|
47 |
|> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs); |
|
48 |
val ml = |
|
49 |
("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ |
|
50 |
string_of_int i ^ ";\n", "Isabelle." ^ a); |
|
51 |
in (Context.Proof ctxt', K ml) end)))); |
|
45592 | 52 |
|
53 |
||
54 |
(* fact references *) |
|
27389 | 55 |
|
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
56 |
fun thm_binding kind is_single context thms = |
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 ctxt = Context.the_proof context; |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
59 |
|
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
60 |
val initial = null (get_thmss ctxt); |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
61 |
val (name, ctxt') = ML_Antiquote.variant kind ctxt; |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
62 |
val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
27389 | 63 |
|
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 |
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
|
65 |
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
|
66 |
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
|
67 |
let |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
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
|
71 |
else ("", ml_body); |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
72 |
in (Context.Proof ctxt'', decl) end; |
27389 | 73 |
|
53171 | 74 |
val _ = Theory.setup |
55516 | 75 |
(ML_Context.add_antiq @{binding thm} |
53171 | 76 |
(Scan.depend (fn context => |
77 |
Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #> |
|
55516 | 78 |
ML_Context.add_antiq @{binding thms} |
53171 | 79 |
(Scan.depend (fn context => |
80 |
Scan.pass context Attrib.thms >> thm_binding "thms" false context))); |
|
27389 | 81 |
|
82 |
||
83 |
(* ad-hoc goals *) |
|
84 |
||
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents:
29606
diff
changeset
|
85 |
val and_ = Args.$$$ "and"; |
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27521
diff
changeset
|
86 |
val by = Args.$$$ "by"; |
55111 | 87 |
val goal = Scan.unless (by || and_) Args.name_inner_syntax; |
27389 | 88 |
|
53171 | 89 |
val _ = Theory.setup |
55516 | 90 |
(ML_Context.add_antiq @{binding lemma} |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
91 |
(Scan.depend (fn context => |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55795
diff
changeset
|
92 |
Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) -- |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55795
diff
changeset
|
93 |
(by |-- Method.parse -- Scan.option Method.parse) |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55795
diff
changeset
|
94 |
>> (fn ((is_open, raw_propss), (m1, m2)) => |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
95 |
let |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
96 |
val ctxt = Context.proof_of context; |
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
|
97 |
|
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55795
diff
changeset
|
98 |
val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2)); |
55515 | 99 |
|
55764 | 100 |
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
53171
diff
changeset
|
101 |
val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation; |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
102 |
fun after_qed res goal_ctxt = |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
103 |
Proof_Context.put_thms false (Auto_Bind.thisN, |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
104 |
SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt; |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
105 |
|
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
106 |
val ctxt' = ctxt |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
107 |
|> Proof.theorem NONE after_qed propss |
55795 | 108 |
|> Proof.global_terminal_proof (m1, m2); |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
109 |
val thms = |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
110 |
Proof_Context.get_fact ctxt' |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
111 |
(Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); |
53171 | 112 |
in thm_binding "lemma" (length (flat propss) = 1) context thms end)))); |
27389 | 113 |
|
114 |
end; |
|
115 |