update_database.ml

   1 (* ========================================================================= *)
   2 (* Create search database from OCaml / modify search database dynamically.   *)
   3 (*                                                                           *)
   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.        *)
   7 (*                                                                           *)
   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 (* ========================================================================= *)
  12
  13 (* Execute any OCaml expression given as a string. *)
  14
  15 let exec = ignore o Toploop.execute_phrase false Format.std_formatter
  16   o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
  17
  18 type dummy;;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* Basic data structures copied from OCaml. May be version-dependent.        *)
  22 (* ------------------------------------------------------------------------- *)
  23
  24 type label = int;;
  25
  26 (*** from ./typing/ident.ml: ***)
  27
  28 type ident_t = { stamp: int; name: string; mutable flags: int };;
  29
  30 type 'a tbl =
  31     Empty
  32   | Node of 'a tbl * 'a data * 'a tbl * int
  33
  34 and 'a data =
  35   { ident: ident_t;
  36     data: 'a;
  37     previous: 'a data option };;
  38
  39 (*** from ./typing/path.ml: ***)
  40
  41 type path_t =
  42     Pident of ident_t
  43   | Pdot of path_t * string * int
  44   | Papply of path_t * path_t;;
  45
  46 (*** from typing/types.ml: ***)
  47
  48 exec (
  49 "type type_expr =
  50   { mutable desc: type_desc;
  51     mutable level: int;
  52     mutable id: int }
  53
  54 and type_desc =
  55 " ^
  56 (if String.sub Sys.ocaml_version 0 1 = "4"
  57  then "Tvar of string option\n"
  58  else "Tvar\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
  64   | Tnil
  65   | Tlink of type_expr
  66   | Tsubst of type_expr
  67   | Tvariant of row_desc
  68   | Tunivar
  69   | Tpoly of type_expr * type_expr list
  70
  71 and row_desc =
  72     { row_fields: (label * row_field) list;
  73       row_more: type_expr;
  74       row_bound: type_expr list;
  75       row_closed: bool;
  76       row_fixed: bool;
  77       row_name: (path_t * type_expr list) option }
  78
  79 and row_field =
  80     Rpresent of type_expr option
  81   | Reither of bool * type_expr list * bool * row_field option ref
  82   | Rabsent
  83
  84 and abbrev_memo =
  85     Mnil
  86   | Mcons of path_t * type_expr * type_expr * abbrev_memo
  87   | Mlink of abbrev_memo ref
  88
  89 and field_kind =
  90     Fvar of field_kind option ref
  91   | Fpresent
  92   | Fabsent
  93
  94 and commutable =
  95     Cok
  96   | Cunknown
  97   | Clink of commutable ref;;
  98 ");;
  99
 100 type value_description =
 101   { val_type: type_expr;
 102     val_kind: dummy };;
 103
 104 type module_type =
 105     Tmty_ident of path_t
 106   | Tmty_signature of signature
 107   | Tmty_functor of ident_t * module_type * module_type
 108
 109 and signature = signature_item list
 110
 111 and signature_item =
 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;;
 119
 120 (*** from ./typing/env.ml: ***)
 121
 122 exec (
 123 "type env_t = {\n" ^
 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")
 128   then ""
 129   else "annotations: dummy;\n") ^
 130 " constrs: dummy;
 131   labels: dummy;\n" ^
 132 (if String.sub Sys.ocaml_version 0 1 = "4"
 133  then "constrs_by_path: dummy;\n"
 134  else "") ^
 135 " types: 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") ^
 139 " modtypes: dummy;
 140   components: dummy;
 141   classes: dummy;
 142   cltypes: dummy;
 143   summary: dummy;\n" ^
 144 (if String.sub Sys.ocaml_version 0 1 = "4"
 145  then "local_constraints: dummy;
 146        gadt_instances: dummy;
 147        in_signature: dummy;
 148        };;\n"
 149  else "};;\n"));;
 150
 151 (* ------------------------------------------------------------------------- *)
 152 (* End of basic data structures copied from OCaml.                           *)
 153 (* ------------------------------------------------------------------------- *)
 154
 155 (* Iterate over the entries of a table. *)
 156
 157 let rec iterTbl (f : ident_t -> 'a -> unit) = function
 158   | Empty -> ()
 159   | Node (t1,d,t2,_) ->
 160       f d.ident d.data;
 161       iterTbl f t1;
 162       iterTbl f t2;;
 163
 164 (* If the given type is simple return its name, otherwise None. *)
 165
 166 let rec get_simple_type = function
 167   | Tlink { desc = Tconstr (Pident p,[],_) } -> Some p.name
 168   | Tlink { desc = d } -> get_simple_type d
 169   | _ -> None;;
 170
 171 (* Evaluate any OCaml expression given as a string. *)
 172
 173 let eval n =
 174   exec ("let buf__ = ( " ^ n ^ " );;");
 175   Obj.magic (Toploop.getvalue "buf__");;
 176
 177 (* Register all theorems added since the last update. *)
 178
 179 exec (
 180 "let update_database =
 181   let lastStamp = ref 0
 182   and currentStamp = ref 0
 183   and thms = Hashtbl.create 5000 in
 184
 185   let ifNew f i x =
 186     if i.stamp > !lastStamp then
 187       ((if i.stamp > !currentStamp then currentStamp := i.stamp);
 188        f i x) in
 189
 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))
 196
 197   and regMod pfx = ifNew (fun i mt ->
 198        match mt with
 199          | Tmty_signature sg ->
 200              let pfx' = pfx ^ i.name ^ \".\" in
 201              List.iter (function
 202                | Tsig_value (i',vd) -> regVal pfx' i' vd
 203                | Tsig_module (i',mt',_) -> regMod pfx' i' mt'
 204                | _ -> ()) sg
 205          | _ -> ())
 206
 207   in fun () ->
 208     let env = Obj.magic !Toploop.toplevel_env in
 209 " ^
 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;
 213       "
 214  else
 215       "iterTbl (fun i (_,vd) -> regVal \"\" i vd) env.values;
 216        iterTbl (fun i (_,mt) -> regMod \"\" i mt) env.modules;
 217       ") ^
 218 "   lastStamp := !currentStamp;
 219     theorems := Hashtbl.fold (fun s t l -> (s,t)::l) thms [];;
 220 ");;
 221
 222 (* ------------------------------------------------------------------------- *)
 223 (* Put an assignment of a theorem database in the named file.                *)
 224 (* ------------------------------------------------------------------------- *)
 225
 226 let make_database_assignment filename =
 227   update_database();
 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"^
 232               "theorems :=\n[\n"^
 233               end_itlist (fun a b -> a^";\n"^b) entries^"\n];;\n" in
 234    file_of_string filename text);;
 235
 236 (* ------------------------------------------------------------------------- *)
 237 (* Search (automatically updates)                                            *)
 238 (* ------------------------------------------------------------------------- *)
 239
 240 let search =
 241   let rec immediatesublist l1 l2 =
 242     match (l1,l2) with
 243       [],_ -> true
 244     | _,[] -> false
 245     | (h1::t1,h2::t2) -> h1 = h2 & immediatesublist t1 t2 in
 246   let rec sublist l1 l2 =
 247     match (l1,l2) with
 248       [],_ -> true
 249     | _,[] -> false
 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 =
 254     match tm with
 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
 259   fun pats ->
 260     update_database();
 261     let triv,nontriv = partition is_var pats in
 262     (if triv <> [] then
 263       warn true
 264          ("Ignoring plain variables in search: "^
 265           end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv))
 266      else ());
 267     (if nontriv = [] & triv <> [] then []
 268      else sort (increasing fst)
 269                (itlist (filter o filterpred) pats (!theorems)));;
 270
 271 (* ------------------------------------------------------------------------- *)
 272 (* Update to bring things back to current state.                             *)
 273 (* ------------------------------------------------------------------------- *)
 274
 275 update_database();;