text_formalization/general/update_database_400.ml

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Update theorem search                                                      *)\r
   5 (* Date: 2010-07-16                                                           *)\r
   6 (*                                                                            *)\r
   7 (* 2012-09-06: JRH fixed up for OCaml 4.0 and added alphabetic sorting.       *)\r
   8 (* ========================================================================== *)\r
   9 \r
  10 (* ========================================================================= *)\r
  11 (* Create search database from OCaml / modify search database dynamically.   *)\r
  12 (*                                                                           *)\r
  13 (* This file assigns to "theorems", which is a list of name-theorem pairs.   *)\r
  14 (* The core system already has such a database set up. Use this file if you  *)\r
  15 (* want to update the database beyond the core, so you can search it.        *)\r
  16 (*                                                                           *)\r
  17 (* The trickery to get at the OCaml environment is due to Roland Zumkeller.  *)\r
  18 (* It works by copying some internal data structures and casting into the    *)\r
  19 (* copy using Obj.magic.                                                     *)\r
  20 (* ========================================================================= *)\r
  21 \r
  22 \r
  23 (* module Update_database_310 = struct *)\r
  24 \r
  25 (* Execute any OCaml expression given as a string. *)\r
  26 \r
  27 let exec = ignore o Toploop.execute_phrase false Format.std_formatter\r
  28   o !Toploop.parse_toplevel_phrase o Lexing.from_string;;\r
  29 \r
  30 type dummy;;\r
  31 \r
  32 (* ------------------------------------------------------------------------- *)\r
  33 (* Basic data structures copied from OCaml. May be version-dependent.        *)\r
  34 (* ------------------------------------------------------------------------- *)\r
  35 \r
  36 type label = int;;\r
  37 \r
  38 (*** from ./typing/ident.ml: ***)\r
  39 \r
  40 type ident_t = { stamp: int; name: string; mutable flags: int };;\r
  41 \r
  42 type 'a tbl =\r
  43     Empty\r
  44   | Node of 'a tbl * 'a data * 'a tbl * int\r
  45 \r
  46 and 'a data =\r
  47   { ident: ident_t;\r
  48     data: 'a;\r
  49     previous: 'a data option };;\r
  50 \r
  51 (*** from ./typing/path.ml: ***)\r
  52 \r
  53 type path_t =\r
  54     Pident of ident_t\r
  55   | Pdot of path_t * string * int\r
  56   | Papply of path_t * path_t;;\r
  57 \r
  58 (*** from typing/types.ml: ***)\r
  59 \r
  60 exec (\r
  61 "type type_expr =\r
  62   { mutable desc: type_desc;\r
  63     mutable level: int;\r
  64     mutable id: int }\r
  65 \r
  66 and type_desc =\r
  67 " ^\r
  68 (if String.sub Sys.ocaml_version 0 1 = "4"\r
  69  then "Tvar of string option\n"\r
  70  else "Tvar\n") ^\r
  71 " | Tarrow of label * type_expr * type_expr * commutable\r
  72   | Ttuple of type_expr list\r
  73   | Tconstr of path_t * type_expr list * abbrev_memo ref\r
  74   | Tobject of type_expr * (path_t * type_expr list) option ref\r
  75   | Tfield of string * field_kind * type_expr * type_expr\r
  76   | Tnil\r
  77   | Tlink of type_expr\r
  78   | Tsubst of type_expr\r
  79   | Tvariant of row_desc\r
  80   | Tunivar\r
  81   | Tpoly of type_expr * type_expr list\r
  82 \r
  83 and row_desc =\r
  84     { row_fields: (label * row_field) list;\r
  85       row_more: type_expr;\r
  86       row_bound: type_expr list;\r
  87       row_closed: bool;\r
  88       row_fixed: bool;\r
  89       row_name: (path_t * type_expr list) option }\r
  90 \r
  91 and row_field =\r
  92     Rpresent of type_expr option\r
  93   | Reither of bool * type_expr list * bool * row_field option ref\r
  94   | Rabsent\r
  95 \r
  96 and abbrev_memo =\r
  97     Mnil\r
  98   | Mcons of path_t * type_expr * type_expr * abbrev_memo\r
  99   | Mlink of abbrev_memo ref\r
 100 \r
 101 and field_kind =\r
 102     Fvar of field_kind option ref\r
 103   | Fpresent\r
 104   | Fabsent\r
 105 \r
 106 and commutable =\r
 107     Cok\r
 108   | Cunknown\r
 109   | Clink of commutable ref;;\r
 110 ");;\r
 111 \r
 112 type value_description =\r
 113   { val_type: type_expr;\r
 114     val_kind: dummy };;\r
 115 \r
 116 type module_type =\r
 117     Tmty_ident of path_t\r
 118   | Tmty_signature of signature\r
 119   | Tmty_functor of ident_t * module_type * module_type\r
 120 \r
 121 and signature = signature_item list\r
 122 \r
 123 and signature_item =\r
 124     Tsig_value of ident_t * value_description\r
 125   | Tsig_type of ident_t * dummy * dummy\r
 126   | Tsig_exception of ident_t * dummy\r
 127   | Tsig_module of ident_t * module_type * dummy\r
 128   | Tsig_modtype of ident_t * dummy\r
 129   | Tsig_class of ident_t * dummy * dummy\r
 130   | Tsig_cltype of ident_t * dummy * dummy;;\r
 131 \r
 132 (*** from ./typing/env.ml: ***)\r
 133 \r
 134 exec (\r
 135 "type env_t = {\n" ^\r
 136  (if String.sub Sys.ocaml_version 0 1 = "4"\r
 137   then "values: ((path_t * value_description) * bool ref) tbl;\n"\r
 138   else "values: (path_t * value_description) tbl;\n") ^\r
 139  (if (let v = String.sub Sys.ocaml_version 0 4 in v = "3.09" or v = "3.10")\r
 140   then ""\r
 141   else "annotations: dummy;\n") ^\r
 142 " constrs: dummy;\r
 143   labels: dummy;\n" ^\r
 144 (if String.sub Sys.ocaml_version 0 1 = "4"\r
 145  then "constrs_by_path: dummy;\n"\r
 146  else "") ^\r
 147 " types: dummy;\n" ^\r
 148 (if String.sub Sys.ocaml_version 0 1 = "4"\r
 149   then "modules: ((path_t * module_type) * bool ref) tbl;\n"\r
 150   else "modules: (path_t * module_type) tbl;\n") ^\r
 151 " modtypes: dummy;\r
 152   components: dummy;\r
 153   classes: dummy;\r
 154   cltypes: dummy;\r
 155   summary: dummy;\n" ^\r
 156 (if String.sub Sys.ocaml_version 0 1 = "4"\r
 157  then "local_constraints: dummy;\r
 158        gadt_instances: dummy;\r
 159        in_signature: dummy;\r
 160        };;\n"\r
 161  else "};;\n"));;\r
 162 \r
 163 (* ------------------------------------------------------------------------- *)\r
 164 (* End of basic data structures copied from OCaml.                           *)\r
 165 (* ------------------------------------------------------------------------- *)\r
 166 \r
 167 (* Iterate over the entries of a table. *)\r
 168 \r
 169 let rec iterTbl (f : ident_t -> 'a -> unit) = function\r
 170   | Empty -> ()\r
 171   | Node (t1,d,t2,_) ->\r
 172       f d.ident d.data;\r
 173       iterTbl f t1;\r
 174       iterTbl f t2;;\r
 175 \r
 176 (* If the given type is simple return its name, otherwise None. *)\r
 177 \r
 178 let rec get_simple_type = function\r
 179   | Tlink { desc = Tconstr (Pident p,[],_) } -> Some p.name\r
 180   | Tlink { desc = d } -> get_simple_type d\r
 181   | _ -> None;;\r
 182 \r
 183 (* Evaluate any OCaml expression given as a string. *)\r
 184 \r
 185 let eval n =\r
 186   exec ("let buf__ = ( " ^ n ^ " );;");\r
 187   Obj.magic (Toploop.getvalue "buf__");;\r
 188 \r
 189 (* Register all theorems added since the last update. *)\r
 190 \r
 191 let thm_hashtable = Hashtbl.create 5000;;\r
 192 \r
 193 exec (                                          \r
 194 "let update_database =             \r
 195   let lastStamp = ref 0                  \r
 196   and currentStamp = ref 0\r
 197   and thms = thm_hashtable in\r
 198 \r
 199   let ifNew f i x =\r
 200     if i.stamp > !lastStamp then\r
 201       ((if i.stamp > !currentStamp then currentStamp := i.stamp);\r
 202        f i x) in\r
 203 \r
 204   let rec regVal pfx = ifNew (fun i vd ->\r
 205     let n = pfx ^ i.name in\r
 206       if n <> \"buf__\" then\r
 207         (if get_simple_type vd.val_type.desc = Some \"thm\"\r
 208          then Hashtbl.replace thms n (eval n)\r
 209          else Hashtbl.remove thms n))\r
 210 \r
 211   and regMod pfx = ifNew (fun i mt ->\r
 212        match mt with\r
 213          | Tmty_signature sg ->\r
 214              let pfx' = pfx ^ i.name ^ \".\" in\r
 215              List.iter (function\r
 216                | Tsig_value (i',vd) -> regVal pfx' i' vd\r
 217                | Tsig_module (i',mt',_) -> regMod pfx' i' mt'\r
 218                | _ -> ()) sg\r
 219          | _ -> ())\r
 220 \r
 221   in fun () ->\r
 222     let env = Obj.magic !Toploop.toplevel_env in\r
 223 " ^\r
 224 (if String.sub Sys.ocaml_version 0 1 = "4"\r
 225  then "iterTbl (fun i ((_,vd),_) -> regVal \"\" i vd) env.values;\r
 226        iterTbl (fun i ((_,mt),_) -> regMod \"\" i mt) env.modules;\r
 227       "\r
 228  else\r
 229       "iterTbl (fun i (_,vd) -> regVal \"\" i vd) env.values;\r
 230        iterTbl (fun i (_,mt) -> regMod \"\" i mt) env.modules;\r
 231       ") ^\r
 232 "   lastStamp := !currentStamp;\r
 233     theorems := Hashtbl.fold (fun s t l -> (s,t)::l) thms [];;\r
 234 ");;\r
 235 \r
 236 (* ------------------------------------------------------------------------- *)\r
 237 (* Search (automatically updates)                                            *)\r
 238 (* ------------------------------------------------------------------------- *)\r
 239 \r
 240 let omit t = mk_comb(mk_var("<omit this pattern>",W mk_fun_ty (type_of t)),t);;\r
 241 \r
 242 let exactly t = mk_comb(mk_var("<match aconv>",W mk_fun_ty (type_of t)),t);;\r
 243 \r
 244 let name s = mk_comb(mk_var("<match theorem name>",W mk_fun_ty aty),\r
 245                      mk_var(s,aty));;\r
 246 \r
 247 let full t = mk_comb(mk_var("<full term>",W mk_fun_ty (type_of t)),t);;\r
 248 \r
 249 let rewrite t = mk_comb(mk_var("<rewrite>",W mk_fun_ty (type_of t)),t);;\r
 250 \r
 251 let regexp s = mk_comb(mk_var("<regexp>",W mk_fun_ty aty),\r
 252                      mk_var(s,aty));;\r
 253 \r
 254 let disjunct pr =\r
 255   let u = mk_pair pr in\r
 256   let ty = type_of u in\r
 257   let h = mk_var ("<search_or>",(mk_type("fun",[ty;aty]))) in\r
 258     mk_comb (h,u);;\r
 259 \r
 260 \r
 261 (* very rough measure of the size of a printed term *)\r
 262 let rec term_length =\r
 263   let n = `NUMERAL` in\r
 264   let d = `DECIMAL` in\r
 265   function\r
 266   | Abs(s,x) -> 1 + term_length x\r
 267   | Comb(s,x) -> if ((s = n) or (s = d)) then 2\r
 268     else ( term_length s + term_length x)\r
 269   | _ -> 1;;\r
 270 \r
 271 let sortlength_thml thml =\r
 272   let ltml = map\r
 273    (function (s,t) as r -> (term_length (concl t),r)) thml in\r
 274   let stml = sort (fun (a,_) (b,_) -> (a < b)) ltml in\r
 275     map snd stml;;\r
 276 \r
 277 \r
 278 (* main search function *)\r
 279 \r
 280 let search_thml term_matcher =\r
 281   let rec immediatesublist l1 l2 =\r
 282     match (l1,l2) with\r
 283       [],_ -> true\r
 284     | _,[] -> false\r
 285     | (h1::t1,h2::t2) -> h1 = h2 & immediatesublist t1 t2 in\r
 286   let rec sublist l1 l2 =\r
 287     match (l1,l2) with\r
 288       [],_ -> true\r
 289     | _,[] -> false\r
 290     | (h1::t1,h2::t2) -> immediatesublist l1 l2 or sublist l1 t2 in\r
 291 \r
 292   let rec conjuncts t =\r
 293     let t' = snd (strip_forall t) in\r
 294       if (is_conj t') then (let (a,b) = dest_conj t' in conjuncts a @ conjuncts b) else [t'] in\r
 295 \r
 296   let heads t =\r
 297     let c = map (fst o dest_eq) (filter (is_eq) (conjuncts t)) in\r
 298     let h = map (fst o strip_comb) c in\r
 299     let hc = filter (is_const) h in\r
 300       map (fst o dest_const) hc in\r
 301 \r
 302   let is_rewrite t (n,th) =\r
 303     mem (fst(dest_const t)) (heads(snd( dest_thm th))) in\r
 304 \r
 305   let name_matches_regexp s (n,th) =\r
 306     let pat = Str.regexp (".*"^s) in\r
 307       Str.string_match pat n 0 in\r
 308 \r
 309   let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th) in\r
 310   let exists_fullterm_satisfying p (n,th) =  p (concl th) in\r
 311   let name_contains s (n,th) = sublist (explode s) (explode n) in\r
 312   let rec filterpred tm =\r
 313     match tm with\r
 314       Comb(Var("<omit this pattern>",_),t) -> not o filterpred t\r
 315     | Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat\r
 316     | Comb(Var("<regexp>",_),Var(pat,_)) -> name_matches_regexp pat\r
 317     | Comb(Var("<search_or>",_),t) ->\r
 318         let (pat1,pat2) = dest_pair t in\r
 319         (fun (n,th) -> exists_subterm_satisfying (can (term_matcher pat1)) (n,th) or\r
 320            exists_subterm_satisfying (can (term_matcher pat2)) (n,th))\r
 321     | Comb(Var("<rewrite>",_),t) -> is_rewrite t\r
 322     | Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)\r
 323     | Comb(Var("<full term>",_),pat) -> exists_fullterm_satisfying (can (term_matcher pat))\r
 324     | pat -> exists_subterm_satisfying (can (term_matcher pat)) in\r
 325   fun pats thml -> update_database ();\r
 326     if (pats = []) then failwith ("keywords: omit (term), name (string),"^\r
 327                                     " disjunct (term,term), "^\r
 328       " regexp (string), exactly (term), full (term), rewrite (term constant)") else\r
 329         (itlist (filter o filterpred) pats thml);;\r
 330 \r
 331 \r
 332 let search pat = sort (increasing fst) (search_thml (term_match [])  pat (!theorems));;\r
 333 \r
 334 (* ------------------------------------------------------------------------- *)\r
 335 (* Update to bring to current state.                                         *)\r
 336 (* ------------------------------------------------------------------------- *)\r
 337 \r
 338 update_database ();;\r
 339 \r
 340 (* end;; *)\r