author | wenzelm |
Wed, 26 Feb 2014 11:14:38 +0100 | |
changeset 55764 | 484cd3a304a8 |
parent 55761 | 213b9811f59f |
child 55795 | 2d4cf0005a02 |
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; |
|
42 |
val thy = Proof_Context.theory_of ctxt; |
|
45592 | 43 |
|
53171 | 44 |
val i = serial (); |
45 |
val srcs = map (Attrib.intern_src thy) raw_srcs; |
|
46 |
val _ = map (Attrib.attribute ctxt) srcs; |
|
47 |
val (a, ctxt') = ctxt |
|
48 |
|> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs); |
|
49 |
val ml = |
|
50 |
("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ |
|
51 |
string_of_int i ^ ";\n", "Isabelle." ^ a); |
|
52 |
in (Context.Proof ctxt', K ml) end)))); |
|
45592 | 53 |
|
54 |
||
55 |
(* fact references *) |
|
27389 | 56 |
|
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
57 |
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
|
58 |
let |
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 = 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
|
60 |
|
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
61 |
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
|
62 |
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
|
63 |
val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
27389 | 64 |
|
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_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
|
66 |
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
|
67 |
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
|
68 |
let |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
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
|
72 |
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
|
73 |
in (Context.Proof ctxt'', decl) end; |
27389 | 74 |
|
53171 | 75 |
val _ = Theory.setup |
55516 | 76 |
(ML_Context.add_antiq @{binding thm} |
53171 | 77 |
(Scan.depend (fn context => |
78 |
Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #> |
|
55516 | 79 |
ML_Context.add_antiq @{binding thms} |
53171 | 80 |
(Scan.depend (fn context => |
81 |
Scan.pass context Attrib.thms >> thm_binding "thms" false context))); |
|
27389 | 82 |
|
83 |
||
84 |
(* ad-hoc goals *) |
|
85 |
||
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents:
29606
diff
changeset
|
86 |
val and_ = Args.$$$ "and"; |
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27521
diff
changeset
|
87 |
val by = Args.$$$ "by"; |
55111 | 88 |
val goal = Scan.unless (by || and_) Args.name_inner_syntax; |
27389 | 89 |
|
53171 | 90 |
val _ = Theory.setup |
55516 | 91 |
(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
|
92 |
(Scan.depend (fn context => |
55764 | 93 |
Args.mode "open" -- Parse.enum1_positions "and" (Scan.repeat1 goal) -- |
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55516
diff
changeset
|
94 |
(Parse.position by -- |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55516
diff
changeset
|
95 |
Scan.pass context (Method.parse_context_report -- Scan.option Method.parse_context_report)) |
55764 | 96 |
>> (fn ((is_open, (raw_propss, and_positions)), ((_, by_pos), methods)) => |
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
97 |
let |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
98 |
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
|
99 |
|
55764 | 100 |
val reports = (by_pos, Markup.keyword1) :: map (rpair Markup.keyword2) and_positions; |
55515 | 101 |
val _ = Context_Position.reports ctxt reports; |
102 |
||
55764 | 103 |
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
|
104 |
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
|
105 |
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
|
106 |
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
|
107 |
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
|
108 |
|
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
109 |
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
|
110 |
|> Proof.theorem NONE after_qed propss |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
111 |
|> Proof.global_terminal_proof methods; |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
112 |
val thms = |
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
53168
diff
changeset
|
113 |
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
|
114 |
(Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); |
53171 | 115 |
in thm_binding "lemma" (length (flat propss) = 1) context thms end)))); |
27389 | 116 |
|
117 |
end; |
|
118 |