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