author | wenzelm |
Sat, 11 Aug 2012 22:17:46 +0200 | |
changeset 48776 | 37cd53e69840 |
parent 47815 | 43f677b3ae91 |
child 48782 | e955964d89cb |
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 |
27389 | 10 |
val the_thms: Proof.context -> int -> thm list |
11 |
val the_thm: Proof.context -> int -> thm |
|
12 |
end; |
|
13 |
||
14 |
structure ML_Thms: ML_THMS = |
|
15 |
struct |
|
16 |
||
45592 | 17 |
(* auxiliary data *) |
27389 | 18 |
|
45592 | 19 |
structure Data = Proof_Data |
27389 | 20 |
( |
45592 | 21 |
type T = Args.src list Inttab.table * thm list Inttab.table; |
22 |
fun init _ = (Inttab.empty, Inttab.empty); |
|
27389 | 23 |
); |
24 |
||
45592 | 25 |
val put_attributes = Data.map o apfst o Inttab.update; |
26 |
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name); |
|
27 |
||
28 |
val put_thms = Data.map o apsnd o Inttab.update; |
|
29 |
||
30 |
fun the_thms ctxt name = the (Inttab.lookup (snd (Data.get ctxt)) name); |
|
31 |
fun the_thm ctxt name = the_single (the_thms ctxt name); |
|
32 |
||
33 |
||
34 |
(* attribute source *) |
|
27389 | 35 |
|
45592 | 36 |
val _ = |
37 |
Context.>> (Context.map_theory |
|
38 |
(ML_Context.add_antiq (Binding.name "attributes") |
|
39 |
(fn _ => Scan.lift Parse_Spec.attribs >> (fn raw_srcs => fn background => |
|
40 |
let |
|
41 |
val thy = Proof_Context.theory_of background; |
|
42 |
||
43 |
val i = serial (); |
|
44 |
val srcs = map (Attrib.intern_src thy) raw_srcs; |
|
47815 | 45 |
val _ = map (Attrib.attribute background) srcs; |
45592 | 46 |
val (a, background') = background |
47 |
|> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs); |
|
48 |
val ml = |
|
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset
|
49 |
("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ |
45592 | 50 |
string_of_int i ^ ";\n", "Isabelle." ^ a); |
51 |
in (K ml, background') end)))); |
|
52 |
||
53 |
||
54 |
(* fact references *) |
|
27389 | 55 |
|
56 |
fun thm_bind kind a i = |
|
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset
|
57 |
"val " ^ a ^ " = ML_Thms.the_" ^ kind ^ " ML_context " ^ string_of_int i ^ ";\n"; |
27389 | 58 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
59 |
fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind) |
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33700
diff
changeset
|
60 |
(fn _ => scan >> (fn ths => fn background => |
27389 | 61 |
let |
62 |
val i = serial (); |
|
63 |
val (a, background') = background |
|
64 |
|> ML_Antiquote.variant kind ||> put_thms (i, ths); |
|
41486
82c1e348bc18
reverted 08240feb69c7 -- breaks positions of reports;
wenzelm
parents:
41376
diff
changeset
|
65 |
val ml = (thm_bind kind a i, "Isabelle." ^ a); |
27389 | 66 |
in (K ml, background') end)); |
67 |
||
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
68 |
val _ = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
69 |
Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
70 |
(thm_antiq "thm" (Attrib.thm >> single) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
71 |
thm_antiq "thms" Attrib.thms)); |
27389 | 72 |
|
73 |
||
74 |
(* ad-hoc goals *) |
|
75 |
||
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents:
29606
diff
changeset
|
76 |
val and_ = Args.$$$ "and"; |
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27521
diff
changeset
|
77 |
val by = Args.$$$ "by"; |
45198 | 78 |
val goal = Scan.unless (by || and_) Args.name_source; |
27389 | 79 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
80 |
val _ = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
81 |
Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
82 |
(ML_Context.add_antiq (Binding.name "lemma") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
83 |
(fn _ => Args.context -- Args.mode "open" -- |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
84 |
Scan.lift (Parse.and_list1 (Scan.repeat1 goal) -- |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
85 |
(by |-- Method.parse -- Scan.option Method.parse)) >> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
86 |
(fn ((ctxt, is_open), (raw_propss, methods)) => fn background => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
87 |
let |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
88 |
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
89 |
val i = serial (); |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
90 |
val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
91 |
fun after_qed res goal_ctxt = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
92 |
put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
93 |
val ctxt' = ctxt |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
94 |
|> Proof.theorem NONE after_qed propss |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
95 |
|> Proof.global_terminal_proof methods; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
96 |
val (a, background') = background |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
97 |
|> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i); |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
98 |
val ml = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
99 |
(thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a); |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
100 |
in (K ml, background') end)))); |
27389 | 101 |
|
102 |
end; |
|
103 |