|
| 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 | +(* and Michael Farber. It works by copying some internal data structures and *) |
| 10 | +(* casting into the copy using Obj.magic. *) |
| 11 | +(* ========================================================================= *) |
| 12 | + |
| 13 | +module Ocaml_typing = struct |
| 14 | + |
| 15 | +open Types |
| 16 | + |
| 17 | +(* If the given type is simple return its name, otherwise None. *) |
| 18 | + |
| 19 | +let rec get_simple_type = function |
| 20 | + | Tlink texpr -> |
| 21 | + (match get_desc texpr with |
| 22 | + | Tconstr (Pident p,[],_) -> Some (Ident.name p) |
| 23 | + | d -> get_simple_type d) |
| 24 | + | Tconstr (Path.Pident p, [], _) -> Some (Ident.name p) |
| 25 | + | _ -> None;; |
| 26 | + |
| 27 | +(* Execute any OCaml expression given as a string. *) |
| 28 | + |
| 29 | +let exec = ignore o Toploop.execute_phrase false Format.std_formatter |
| 30 | + o !Toploop.parse_toplevel_phrase o Lexing.from_string |
| 31 | + |
| 32 | +(* Evaluate any OCaml expression given as a string. *) |
| 33 | + |
| 34 | +let eval n = |
| 35 | + exec ("let buf__ = ( " ^ n ^ " );;"); |
| 36 | + Obj.magic (Toploop.getvalue "buf__") |
| 37 | + |
| 38 | +(* Register all theorems added since the last update. *) |
| 39 | +end |
| 40 | + |
| 41 | +module Lookuptheorems = struct |
| 42 | +open Types |
| 43 | + |
| 44 | +let lid_cons lidopt id = |
| 45 | + match lidopt with |
| 46 | + None -> Longident.Lident id |
| 47 | + | Some li -> Longident.Ldot(li, id) |
| 48 | + |
| 49 | +let it_val_1 lidopt s p vd acc = |
| 50 | + if (Some "thm") = Ocaml_typing.get_simple_type (get_desc vd.Types.val_type) then |
| 51 | + (lid_cons lidopt s)::acc else acc |
| 52 | + |
| 53 | +let it_mod_1 lidopt s p md acc = (lid_cons lidopt s)::acc |
| 54 | + |
| 55 | +let enum0 lidopt = |
| 56 | + try |
| 57 | + let vl = Env.fold_values (it_val_1 lidopt) lidopt !Toploop.toplevel_env [] in |
| 58 | + let ml = Env.fold_modules (it_mod_1 lidopt) lidopt !Toploop.toplevel_env [] in |
| 59 | + (vl, ml) |
| 60 | + with Not_found -> |
| 61 | + (* Looking for (Longident.Lident "Stream") raises Not_found. |
| 62 | + Stream is a deprecated alias module of "Stdlib.Stream", and the camlp-streams |
| 63 | + package that is used by pa_hol_syntax redefines Stream, which seems to |
| 64 | + confuse Env.fold_values and Env.fold_modules. *) |
| 65 | + ([], []) |
| 66 | + |
| 67 | +let rec enum1 lidopt acc = |
| 68 | + match enum0 lidopt with |
| 69 | + (vl, []) -> vl@acc |
| 70 | + | (vl, ml) -> |
| 71 | + List.fold_left (fun acc mlid -> |
| 72 | + enum1 (Some mlid) acc) (vl@acc) ml |
| 73 | + |
| 74 | +let string_of_longident lid = |
| 75 | + String.concat "." (Longident.flatten lid) |
| 76 | + |
| 77 | +let all_theorems () = |
| 78 | + enum1 None [] |
| 79 | + |> List.map (fun lid -> |
| 80 | + let s = string_of_longident lid in |
| 81 | + (s, (Ocaml_typing.eval s : thm))) |
| 82 | +end |
| 83 | + |
| 84 | + |
| 85 | +let update_database () = |
| 86 | + theorems := Lookuptheorems.all_theorems() |
| 87 | + |
| 88 | +(* ------------------------------------------------------------------------- *) |
| 89 | +(* Put an assignment of a theorem database in the named file. *) |
| 90 | +(* ------------------------------------------------------------------------- *) |
| 91 | + |
| 92 | +let make_database_assignment filename = |
| 93 | + update_database(); |
| 94 | + (let allnames = uniq(sort (<) (map fst (!theorems))) in |
| 95 | + let names = subtract allnames ["it"] in |
| 96 | + let entries = map (fun n -> "\""^n^"\","^n) names in |
| 97 | + let text = "needs \"help.ml\";;\n\n"^ |
| 98 | + "theorems :=\n[\n"^ |
| 99 | + end_itlist (fun a b -> a^";\n"^b) entries^"\n];;\n" in |
| 100 | + file_of_string filename text);; |
| 101 | + |
| 102 | +(* ------------------------------------------------------------------------- *) |
| 103 | +(* Search (automatically updates) *) |
| 104 | +(* ------------------------------------------------------------------------- *) |
| 105 | + |
| 106 | +let search = |
| 107 | + let rec immediatesublist l1 l2 = |
| 108 | + match (l1,l2) with |
| 109 | + [],_ -> true |
| 110 | + | _,[] -> false |
| 111 | + | (h1::t1,h2::t2) -> h1 = h2 && immediatesublist t1 t2 in |
| 112 | + let rec sublist l1 l2 = |
| 113 | + match (l1,l2) with |
| 114 | + [],_ -> true |
| 115 | + | _,[] -> false |
| 116 | + | (h1::t1,h2::t2) -> immediatesublist l1 l2 || sublist l1 t2 in |
| 117 | + let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th) |
| 118 | + and name_contains s (n,th) = sublist (explode s) (explode n) in |
| 119 | + let rec filterpred tm = |
| 120 | + match tm with |
| 121 | + Comb(Var("<omit this pattern>",_),t) -> not o filterpred t |
| 122 | + | Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat |
| 123 | + | Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat) |
| 124 | + | pat -> exists_subterm_satisfying (can (term_match [] pat)) in |
| 125 | + fun pats -> |
| 126 | + update_database(); |
| 127 | + let triv,nontriv = partition is_var pats in |
| 128 | + (if triv <> [] then |
| 129 | + warn true |
| 130 | + ("Ignoring plain variables in search: "^ |
| 131 | + end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv)) |
| 132 | + else ()); |
| 133 | + (if nontriv = [] && triv <> [] then [] |
| 134 | + else sort (increasing fst) |
| 135 | + (itlist (filter o filterpred) pats (!theorems)));; |
| 136 | + |
| 137 | +(* ------------------------------------------------------------------------- *) |
| 138 | +(* Update to bring things back to current state. *) |
| 139 | +(* ------------------------------------------------------------------------- *) |
| 140 | + |
| 141 | +update_database();; |
0 commit comments