1 (* ========================================================================= *)
2 (* Create search database from OCaml / modify search database dynamically. *)
4 (* This file assigns to "theorems", which is a list of name-theorem pairs. *)
5 (* The core system already has such a database set up. Use this file if you *)
6 (* want to update the database beyond the core, so you can search it. *)
8 (* The trickery to get at the OCaml environment is due to Roland Zumkeller. *)
9 (* It works by copying some internal data structures and casting into the *)
10 (* copy using Obj.magic. *)
11 (* ========================================================================= *)
13 (* Execute any OCaml expression given as a string. *)
15 let exec = ignore o Toploop.execute_phrase false Format.std_formatter
16 o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
20 (* ------------------------------------------------------------------------- *)
21 (* Basic data structures copied from OCaml. May be version-dependent. *)
22 (* ------------------------------------------------------------------------- *)
26 (*** from ./typing/ident.ml: ***)
28 type ident_t = { stamp: int; name: string; mutable flags: int };;
32 | Node of 'a tbl * 'a data * 'a tbl * int
37 previous: 'a data option };;
39 (*** from ./typing/path.ml: ***)
43 | Pdot of path_t * string * int
44 | Papply of path_t * path_t;;
46 (*** from typing/types.ml: ***)
50 { mutable desc: type_desc;
56 (if String.sub Sys.ocaml_version 0 1 = "4"
57 then "Tvar of string option\n"
59 " | Tarrow of label * type_expr * type_expr * commutable
60 | Ttuple of type_expr list
61 | Tconstr of path_t * type_expr list * abbrev_memo ref
62 | Tobject of type_expr * (path_t * type_expr list) option ref
63 | Tfield of string * field_kind * type_expr * type_expr
67 | Tvariant of row_desc
69 | Tpoly of type_expr * type_expr list
72 { row_fields: (label * row_field) list;
74 row_bound: type_expr list;
77 row_name: (path_t * type_expr list) option }
80 Rpresent of type_expr option
81 | Reither of bool * type_expr list * bool * row_field option ref
86 | Mcons of path_t * type_expr * type_expr * abbrev_memo
87 | Mlink of abbrev_memo ref
90 Fvar of field_kind option ref
97 | Clink of commutable ref;;
100 type value_description =
101 { val_type: type_expr;
106 | Tmty_signature of signature
107 | Tmty_functor of ident_t * module_type * module_type
109 and signature = signature_item list
112 Tsig_value of ident_t * value_description
113 | Tsig_type of ident_t * dummy * dummy
114 | Tsig_exception of ident_t * dummy
115 | Tsig_module of ident_t * module_type * dummy
116 | Tsig_modtype of ident_t * dummy
117 | Tsig_class of ident_t * dummy * dummy
118 | Tsig_cltype of ident_t * dummy * dummy;;
120 (*** from ./typing/env.ml: ***)
124 (if String.sub Sys.ocaml_version 0 1 = "4"
125 then "values: ((path_t * value_description) * bool ref) tbl;\n"
126 else "values: (path_t * value_description) tbl;\n") ^
127 (if (let v = String.sub Sys.ocaml_version 0 4 in v = "3.09" or v = "3.10")
129 else "annotations: dummy;\n") ^
132 (if String.sub Sys.ocaml_version 0 1 = "4"
133 then "constrs_by_path: dummy;\n"
136 (if String.sub Sys.ocaml_version 0 1 = "4"
137 then "modules: ((path_t * module_type) * bool ref) tbl;\n"
138 else "modules: (path_t * module_type) tbl;\n") ^
144 (if String.sub Sys.ocaml_version 0 1 = "4"
145 then "local_constraints: dummy;
146 gadt_instances: dummy;
151 (* ------------------------------------------------------------------------- *)
152 (* End of basic data structures copied from OCaml. *)
153 (* ------------------------------------------------------------------------- *)
155 (* Iterate over the entries of a table. *)
157 let rec iterTbl (f : ident_t -> 'a -> unit) = function
159 | Node (t1,d,t2,_) ->
164 (* If the given type is simple return its name, otherwise None. *)
166 let rec get_simple_type = function
167 | Tlink { desc = Tconstr (Pident p,[],_) } -> Some p.name
168 | Tlink { desc = d } -> get_simple_type d
171 (* Evaluate any OCaml expression given as a string. *)
174 exec ("let buf__ = ( " ^ n ^ " );;");
175 Obj.magic (Toploop.getvalue "buf__");;
177 (* Register all theorems added since the last update. *)
180 "let update_database =
181 let lastStamp = ref 0
182 and currentStamp = ref 0
183 and thms = Hashtbl.create 5000 in
186 if i.stamp > !lastStamp then
187 ((if i.stamp > !currentStamp then currentStamp := i.stamp);
190 let rec regVal pfx = ifNew (fun i vd ->
191 let n = pfx ^ i.name in
192 if n <> \"buf__\" then
193 (if get_simple_type vd.val_type.desc = Some \"thm\"
194 then Hashtbl.replace thms n (eval n)
195 else Hashtbl.remove thms n))
197 and regMod pfx = ifNew (fun i mt ->
199 | Tmty_signature sg ->
200 let pfx' = pfx ^ i.name ^ \".\" in
202 | Tsig_value (i',vd) -> regVal pfx' i' vd
203 | Tsig_module (i',mt',_) -> regMod pfx' i' mt'
208 let env = Obj.magic !Toploop.toplevel_env in
210 (if String.sub Sys.ocaml_version 0 1 = "4"
211 then "iterTbl (fun i ((_,vd),_) -> regVal \"\" i vd) env.values;
212 iterTbl (fun i ((_,mt),_) -> regMod \"\" i mt) env.modules;
215 "iterTbl (fun i (_,vd) -> regVal \"\" i vd) env.values;
216 iterTbl (fun i (_,mt) -> regMod \"\" i mt) env.modules;
218 " lastStamp := !currentStamp;
219 theorems := Hashtbl.fold (fun s t l -> (s,t)::l) thms [];;
222 (* ------------------------------------------------------------------------- *)
223 (* Put an assignment of a theorem database in the named file. *)
224 (* ------------------------------------------------------------------------- *)
226 let make_database_assignment filename =
228 (let allnames = uniq(sort (<) (map fst (!theorems))) in
229 let names = subtract allnames ["it"] in
230 let entries = map (fun n -> "\""^n^"\","^n) names in
231 let text = "needs \"help.ml\";;\n\n"^
233 end_itlist (fun a b -> a^";\n"^b) entries^"\n];;\n" in
234 file_of_string filename text);;
236 (* ------------------------------------------------------------------------- *)
237 (* Search (automatically updates) *)
238 (* ------------------------------------------------------------------------- *)
241 let rec immediatesublist l1 l2 =
245 | (h1::t1,h2::t2) -> h1 = h2 & immediatesublist t1 t2 in
246 let rec sublist l1 l2 =
250 | (h1::t1,h2::t2) -> immediatesublist l1 l2 or sublist l1 t2 in
251 let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th)
252 and name_contains s (n,th) = sublist (explode s) (explode n) in
253 let rec filterpred tm =
255 Comb(Var("<omit this pattern>",_),t) -> not o filterpred t
256 | Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
257 | Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)
258 | pat -> exists_subterm_satisfying (can (term_match [] pat)) in
261 let triv,nontriv = partition is_var pats in
264 ("Ignoring plain variables in search: "^
265 end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv))
267 (if nontriv = [] & triv <> [] then []
268 else sort (increasing fst)
269 (itlist (filter o filterpred) pats (!theorems)));;
271 (* ------------------------------------------------------------------------- *)
272 (* Update to bring things back to current state. *)
273 (* ------------------------------------------------------------------------- *)