1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
(* ========================================================================= *)
(* Create search database from OCaml / modify search database dynamically. *)
(* *)
(* This file assigns to "theorems", which is a list of name-theorem pairs. *)
(* The core system already has such a database set up. Use this file if you *)
(* want to update the database beyond the core, so you can search it. *)
(* *)
(* The trickery to get at the OCaml environment is due to oleg@pobox.com *)
(* (see his message to the caml-list on Tuesday 26th September 2006). *)
(* ========================================================================= *)
(* !!!!!!! You must set this to point at the source directory in
!!!!!!! which OCaml was built. (And don't do "make clean" beforehand.)
*)
let ocaml_source_dir =
Filename.concat (Sys.getenv "HOME")
("software/ocaml-"^Sys.ocaml_version);;
do_list (fun s -> Topdirs.dir_directory(Filename.concat ocaml_source_dir s))
["parsing"; "typing"; "toplevel"; "utils"];;
(* This must be loaded first! It is stateful, and affects Predef *)
#load "ident.cmo";;
#load "misc.cmo";;
#load "path.cmo";;
#load "types.cmo";;
#load "btype.cmo";;
#load "tbl.cmo";;
#load "subst.cmo";;
#load "predef.cmo";;
#load "datarepr.cmo";;
#load "config.cmo";;
#load "consistbl.cmo";;
#load "clflags.cmo";;
#load "env.cmo";;
#load "ctype.cmo";;
#load "printast.cmo";;
#load "oprint.cmo";;
#load "primitive.cmo";;
#load "printtyp.cmo";;
(* ------------------------------------------------------------------------- *)
(* Get the toplevel environment as raw data. *)
(* ------------------------------------------------------------------------- *)
let get_value_bindings env =
let rec get_val acc = function
| Env.Env_empty -> acc
| Env.Env_value (next, ident, val_descr) ->
get_val ((ident,val_descr)::acc) next
| Env.Env_type (next,_,_) -> get_val acc next
| Env.Env_exception (next,_,_) -> get_val acc next
| Env.Env_module (next,_,_) -> get_val acc next
| Env.Env_modtype (next,_,_) -> get_val acc next
| Env.Env_class (next,_,_) -> get_val acc next
| Env.Env_cltype (next,_,_) -> get_val acc next
| Env.Env_open (next,_) -> get_val acc next
in get_val [] (Env.summary env);;
(* ------------------------------------------------------------------------- *)
(* Convert a type to a string, for ease of comparison. *)
(* ------------------------------------------------------------------------- *)
let type_to_str (x : Types.type_expr) =
Printtyp.type_expr Format.str_formatter x;
Format.flush_str_formatter ();;
(* ------------------------------------------------------------------------- *)
(* Put an assignment of a theorem database in the named file. *)
(* ------------------------------------------------------------------------- *)
let make_database_assignment filename =
let all_bnds = get_value_bindings (!Toploop.toplevel_env) in
let thm_bnds = filter (fun (ident,val_descr) ->
type_to_str val_descr.Types.val_type = "thm")
all_bnds in
let names =
subtract (map (fun (ident,val_descr) -> Ident.name ident) thm_bnds)
["it"] in
let entries = map (fun n -> "\""^n^"\","^n) (uniq(sort (<) names)) in
let text = "theorems :=\n[\n"^
end_itlist (fun a b -> a^";\n"^b) entries^"\n];;\n" in
file_of_string filename text;;
(* ------------------------------------------------------------------------- *)
(* Remove bindings in first list from second assoc list (all ordered). *)
(* ------------------------------------------------------------------------- *)
let rec demerge s l =
match (s,l) with
u::t,(x,y as p)::m ->
if u = x then demerge t m
else if u < x then demerge t l
else p::(demerge s m)
| _ -> l;;
(* ------------------------------------------------------------------------- *)
(* Incrementally update database. *)
(* ------------------------------------------------------------------------- *)
let update_database =
let value_bindings_checked = ref 0
and theorem_bindings_existing = ref undefined in
let listify l = if l = [] then "[]"
else "[\n"^end_itlist (fun a b -> a^";\n"^b) l^"\n]\n" in
let purenames = map (fun n -> "\""^n^"\"")
and pairnames = map (fun n -> "\""^n^"\","^n) in
fun () ->
let old_count = !value_bindings_checked
and old_ths = !theorem_bindings_existing in
let all_bnds = get_value_bindings (!Toploop.toplevel_env) in
let new_bnds = funpow old_count tl all_bnds in
let new_count = old_count + length new_bnds
and new_ths =
rev_itlist (fun (ident,val_descr) ->
let n = Ident.name ident in
if type_to_str val_descr.Types.val_type = "thm" && n <> "it"
then (n |-> ()) else undefine n) new_bnds old_ths in
value_bindings_checked := new_count;
if new_ths = old_ths then () else
(print_string "Updating search database\n";
theorem_bindings_existing := new_ths;
let all_ths = combine (fun _ _ -> ()) (fun _ -> false) old_ths new_ths in
let del_ths = combine (fun _ _ -> ()) (fun _ -> true) all_ths new_ths
and add_ths = combine (fun _ _ -> ()) (fun _ -> true) all_ths old_ths in
let del_names = mergesort (<) (foldr (fun a _ l -> a::l) del_ths [])
and add_names = mergesort (<) (foldr (fun a _ l -> a::l) add_ths []) in
let exptext =
"theorems :=\n merge (increasing fst) (demerge "^
(listify(purenames del_names))^
" (!theorems)) "^
(listify(pairnames add_names))^
";;\n" in
(let filename = Filename.temp_file "database" ".ml" in
file_of_string filename exptext;
loadt filename;
Sys.remove filename));;
(* ------------------------------------------------------------------------- *)
(* Include a call to this on each search. *)
(* ------------------------------------------------------------------------- *)
let search =
let rec immediatesublist l1 l2 =
match (l1,l2) with
[],_ -> true
| _,[] -> false
| (h1::t1,h2::t2) -> h1 = h2 && immediatesublist t1 t2 in
let rec sublist l1 l2 =
match (l1,l2) with
[],_ -> true
| _,[] -> false
| (h1::t1,h2::t2) -> immediatesublist l1 l2 || sublist l1 t2 in
let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th)
and name_contains s (n,th) = sublist (explode s) (explode n) in
let rec filterpred tm =
match tm with
Comb(Var("<omit this pattern>",_),t) -> not o filterpred t
| Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
| Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)
| pat -> exists_subterm_satisfying (can (term_match [] pat)) in
fun pats ->
update_database();
let triv,nontriv = partition is_var pats in
(if triv <> [] then
warn true
("Ignoring plain variables in search: "^
end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv))
else ());
(if nontriv = [] && triv <> [] then []
else itlist (filter o filterpred) pats (!theorems));;
(* ------------------------------------------------------------------------- *)
(* Update to bring things back to current state. *)
(* ------------------------------------------------------------------------- *)
theorems := [];;
update_database();;
|
