author | huffman |
Wed, 13 Sep 2006 00:38:38 +0200 | |
changeset 20522 | 05072ae0d435 |
parent 19482 | 9f11af8f7ef9 |
child 20676 | 21e096f30c5d |
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 |
14680 | 22 |
val ml_reserved: string list |
6204 | 23 |
val is_ml_identifier: string -> bool |
24 |
end; |
|
25 |
||
3627 | 26 |
structure ThmDatabase: THM_DATABASE = |
1221 | 27 |
struct |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
28 |
|
4023 | 29 |
(** store theorems **) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
30 |
|
13279
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
31 |
(* store in theory and perform presentation *) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
32 |
|
4023 | 33 |
fun store_thm (name, thm) = |
7410 | 34 |
let val thm' = hd (PureThy.smart_store_thms (name, [thm])) |
6327 | 35 |
in Present.theorem name thm'; thm' end; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
36 |
|
7410 | 37 |
fun store_thms (name, thms) = |
38 |
let val thms' = PureThy.smart_store_thms (name, thms) |
|
39 |
in Present.theorems name thms'; thms' end; |
|
40 |
||
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
41 |
|
4023 | 42 |
(* store on ML toplevel *) |
43 |
||
7410 | 44 |
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
|
45 |
|
4023 | 46 |
val ml_reserved = |
47 |
["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", |
|
48 |
"end", "exception", "fn", "fun", "handle", "if", "in", "infix", |
|
49 |
"infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", |
|
50 |
"raise", "rec", "then", "type", "val", "with", "withtype", "while", |
|
51 |
"eqtype", "functor", "include", "sharing", "sig", "signature", |
|
52 |
"struct", "structure", "where"]; |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
53 |
|
4023 | 54 |
fun is_ml_identifier name = |
14680 | 55 |
not (name mem_string ml_reserved) andalso Syntax.is_ascii_identifier name; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
56 |
|
7410 | 57 |
fun warn_ml name = |
58 |
if is_ml_identifier name then false |
|
7573 | 59 |
else if name = "" then true |
7410 | 60 |
else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true); |
61 |
||
10914 | 62 |
val use_text_verbose = use_text Context.ml_output true; |
7854 | 63 |
|
4023 | 64 |
fun ml_store_thm (name, thm) = |
65 |
let val thm' = store_thm (name, thm) in |
|
7410 | 66 |
if warn_ml name then () |
13279
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
67 |
else (qed_thms := [thm']; |
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
68 |
use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")) |
7410 | 69 |
end; |
70 |
||
71 |
fun ml_store_thms (name, thms) = |
|
72 |
let val thms' = store_thms (name, thms) in |
|
73 |
if warn_ml name then () |
|
7854 | 74 |
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
|
75 |
end; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
76 |
|
4023 | 77 |
|
17170 | 78 |
(* legacy bindings *) |
79 |
||
80 |
fun legacy_bindings thy = |
|
81 |
let |
|
82 |
val thy_name = Context.theory_name thy; |
|
83 |
val (space, thms) = PureThy.theorems_of thy; |
|
84 |
||
85 |
fun prune name = |
|
86 |
let |
|
87 |
val xname = NameSpace.extern space name; |
|
88 |
fun result prfx bname = |
|
89 |
if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso |
|
90 |
NameSpace.intern space xname = name then |
|
17412 | 91 |
SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1)) |
17170 | 92 |
else NONE; |
93 |
val names = NameSpace.unpack name; |
|
94 |
in |
|
19012 | 95 |
(case #2 (chop (length names - 2) names) of |
17170 | 96 |
[bname] => result "" bname |
97 |
| [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname |
|
98 |
| _ => NONE) |
|
99 |
end; |
|
100 |
||
101 |
fun mk_struct "" = I |
|
102 |
| mk_struct prfx = enclose ("structure " ^ prfx ^ " =\nstruct\n") "\nend\n"; |
|
103 |
||
104 |
fun mk_thm (bname, xname, singleton) = |
|
105 |
"val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname; |
|
106 |
in |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19012
diff
changeset
|
107 |
Symtab.keys thms |> map_filter prune |
18931 | 108 |
|> Symtab.make_list |> Symtab.dest |> sort_wrt #1 |
17170 | 109 |
|> map (fn (prfx, entries) => |
110 |
entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx) |
|
111 |
|> cat_lines |
|
112 |
end; |
|
113 |
||
114 |
fun use_legacy_bindings thy = Context.use_mltext (legacy_bindings thy) true (SOME thy); |
|
115 |
||
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
116 |
end; |
6204 | 117 |
|
118 |
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase; |
|
119 |
open BasicThmDatabase; |