text_formalization/general/update_database_310.ml

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