author | wenzelm |
Fri, 15 Dec 2006 00:08:06 +0100 | |
changeset 21858 | 05f57309170c |
parent 21482 | 7bb5de80917f |
child 22086 | cf6019fece63 |
permissions | -rw-r--r-- |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
1 |
(* Title: Pure/Thy/thm_database.ML |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
11895 | 3 |
Author: Markus Wenzel, TU Muenchen |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
4 |
|
17170 | 5 |
ML toplevel interface to the theorem database. |
4023 | 6 |
*) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
7 |
|
6204 | 8 |
signature BASIC_THM_DATABASE = |
4023 | 9 |
sig |
10 |
val store_thm: string * thm -> thm |
|
7410 | 11 |
val store_thms: string * thm list -> thm list |
17170 | 12 |
val legacy_bindings: theory -> string |
13 |
val use_legacy_bindings: theory -> unit |
|
4023 | 14 |
end; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
15 |
|
6204 | 16 |
signature THM_DATABASE = |
17 |
sig |
|
18 |
include BASIC_THM_DATABASE |
|
7410 | 19 |
val qed_thms: thm list ref |
6204 | 20 |
val ml_store_thm: string * thm -> unit |
7410 | 21 |
val ml_store_thms: string * thm list -> unit |
6204 | 22 |
end; |
23 |
||
3627 | 24 |
structure ThmDatabase: THM_DATABASE = |
1221 | 25 |
struct |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
26 |
|
4023 | 27 |
(** store theorems **) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
28 |
|
13279
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
29 |
(* store in theory and perform presentation *) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
30 |
|
4023 | 31 |
fun store_thm (name, thm) = |
7410 | 32 |
let val thm' = hd (PureThy.smart_store_thms (name, [thm])) |
6327 | 33 |
in Present.theorem name thm'; thm' end; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
34 |
|
7410 | 35 |
fun store_thms (name, thms) = |
36 |
let val thms' = PureThy.smart_store_thms (name, thms) |
|
37 |
in Present.theorems name thms'; thms' end; |
|
38 |
||
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
39 |
|
4023 | 40 |
(* store on ML toplevel *) |
41 |
||
7410 | 42 |
val qed_thms: thm list ref = ref []; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
43 |
|
7410 | 44 |
fun warn_ml name = |
21482 | 45 |
if ML_Syntax.is_identifier name then false |
7573 | 46 |
else if name = "" then true |
7410 | 47 |
else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true); |
48 |
||
20926 | 49 |
val use_text_verbose = use_text Output.ml_output true; |
7854 | 50 |
|
4023 | 51 |
fun ml_store_thm (name, thm) = |
52 |
let val thm' = store_thm (name, thm) in |
|
7410 | 53 |
if warn_ml name then () |
13279
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
54 |
else (qed_thms := [thm']; |
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
55 |
use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")) |
7410 | 56 |
end; |
57 |
||
58 |
fun ml_store_thms (name, thms) = |
|
59 |
let val thms' = store_thms (name, thms) in |
|
60 |
if warn_ml name then () |
|
7854 | 61 |
else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
62 |
end; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
63 |
|
4023 | 64 |
|
17170 | 65 |
(* legacy bindings *) |
66 |
||
67 |
fun legacy_bindings thy = |
|
68 |
let |
|
69 |
val thy_name = Context.theory_name thy; |
|
70 |
val (space, thms) = PureThy.theorems_of thy; |
|
71 |
||
72 |
fun prune name = |
|
73 |
let |
|
74 |
val xname = NameSpace.extern space name; |
|
75 |
fun result prfx bname = |
|
21482 | 76 |
if (prfx = "" orelse ML_Syntax.is_identifier prfx) andalso |
77 |
ML_Syntax.is_identifier bname andalso |
|
17170 | 78 |
NameSpace.intern space xname = name then |
17412 | 79 |
SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1)) |
17170 | 80 |
else NONE; |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21482
diff
changeset
|
81 |
val names = NameSpace.explode name; |
17170 | 82 |
in |
19012 | 83 |
(case #2 (chop (length names - 2) names) of |
17170 | 84 |
[bname] => result "" bname |
85 |
| [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname |
|
86 |
| _ => NONE) |
|
87 |
end; |
|
88 |
||
89 |
fun mk_struct "" = I |
|
90 |
| mk_struct prfx = enclose ("structure " ^ prfx ^ " =\nstruct\n") "\nend\n"; |
|
91 |
||
92 |
fun mk_thm (bname, xname, singleton) = |
|
93 |
"val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname; |
|
94 |
in |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19012
diff
changeset
|
95 |
Symtab.keys thms |> map_filter prune |
18931 | 96 |
|> Symtab.make_list |> Symtab.dest |> sort_wrt #1 |
17170 | 97 |
|> map (fn (prfx, entries) => |
98 |
entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx) |
|
99 |
|> cat_lines |
|
100 |
end; |
|
101 |
||
102 |
fun use_legacy_bindings thy = Context.use_mltext (legacy_bindings thy) true (SOME thy); |
|
103 |
||
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
104 |
end; |
6204 | 105 |
|
106 |
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase; |
|
107 |
open BasicThmDatabase; |