Add update_database for OCaml 5, fix a bug in search, add make switch-5

This patch
- Adds update_database for OCaml5, which is almost a copy of the file for OCaml 4.14
- Fixes a failure when there are theorems inside a module (OCaml 4.14). My test code:
```
loads "update_database.ml";;
unset_jrh_lexer;;
module A_SIMPLE_MODULE = struct let mythm = new_axiom `1 + 1 = 2` end;;
set_jrh_lexer;;
search [name "A_SIMPLE_MODULE"];;
search [name "ADD_SUB"];;
```
- Moves update_database_*.ml files into a separate directory
- Fixes usage of a deprecated function in Mizarlight.
- Add switch-5 which is a command for setting OPAM switch with OCaml 5.2 (the latest version).

After this patch, I think HOL Light is ready to support OCaml 5, resolving github issue #95 and partially resolving #101.
I tested holtest on OCaml 5.2 and it worked fine.
About the new command 'switch-5': I would like to suggest having switch-X for each major version X.

Makefile

@@ -59,12 +59,20 @@ switch:; \
   opam install -y zarith ledit ; \
   opam pin -y add camlp5 8.03.00
 
+switch-5:; \
+  opam update ; \
+  opam switch create . ocaml-base-compiler.5.2.0 ; \
+  eval $(opam env) ; \
+  opam install -y zarith ledit ; \
+  opam pin -y add camlp5 8.03.00
+
 # Choose an appropriate "update_database.ml" file
 
-update_database.ml:; if [ ${OCAML_VERSION} = "4.14" ] ; \
-                     then cp update_database_4.14.ml update_database.ml ; \
-                     else cp update_database_${OCAML_UNARY_VERSION}.ml update_database.ml ; \
-                     fi
+update_database.ml:; \
+  if [ ${OCAML_VERSION} = "4.14" ] ; \
+  then cp update_database/update_database_4.14.ml update_database.ml ; \
+  else cp update_database/update_database_${OCAML_UNARY_VERSION}.ml update_database.ml ; \
+  fi
 
 # Build the camlp4 syntax extension file (camlp5 for OCaml >= 3.10)
 
@@ -174,7 +182,7 @@ unit_tests.native: unit_tests_inlined.ml hol_lib.cmx inline_load.ml hol.sh ; \
         ocamlfind ocamlopt -package zarith -linkpkg -pp "`./hol.sh -pp`" \
         -I . bignum.cmx hol_loader.cmx hol_lib.cmx unit_tests_inlined.ml -o unit_tests.native
 
-default: hol_lib.cma unit_tests.byte unit_tests.native
+default: hol_lib.cma hol_lib.cmxa unit_tests.byte unit_tests.native
 endif
 
 # TODO: update this and hol.* commands to use one of checkpointing  tools

Mizarlight/make.ml

@@ -21,7 +21,7 @@ let e tac =
 
 Topdirs.dir_directory (!hol_dir);;
 
-Topdirs.load_file Format.std_formatter
+Toploop.load_file Format.std_formatter
  (Filename.concat (!hol_dir) "Mizarlight/pa_f.cmo");;
 
 List.iter (fun s -> Hashtbl.add (Pa_j.ht) s true)

update_database_4.14.ml → update_database/update_database_4.14.ml

@@ -26,14 +26,16 @@ let rec get_simple_type = function
 
 (* Execute any OCaml expression given as a string. *)
 
-let exec = ignore o Toploop.execute_phrase false Format.std_formatter
-  o !Toploop.parse_toplevel_phrase o Lexing.from_string
+let exec s = (ignore o Toploop.execute_phrase false Format.std_formatter
+  o !Toploop.parse_toplevel_phrase o Lexing.from_string) s
 
 (* Evaluate any OCaml expression given as a string. *)
 
 let eval n =
-  exec ("let buf__ = ( " ^ n ^ " );;");
-  Obj.magic (Toploop.getvalue "buf__")
+  if String.contains n '.' then begin
+    exec ("let buf__ = ( " ^ n ^ " );;");
+    Obj.magic (Toploop.getvalue "buf__")
+  end else Obj.magic (Toploop.getvalue n)
 
 (* Register all theorems added since the last update. *)
 end
@@ -75,10 +77,13 @@ let string_of_longident lid =
   String.concat "." (Longident.flatten lid)
 
 let all_theorems () =
-  enum1 None []
-  |> List.map (fun lid ->
-      let s = string_of_longident lid in
-      (s, (Ocaml_typing.eval s : thm)))
+  let _ = Ocaml_typing.exec ("unset_jrh_lexer;;") in
+  let res = enum1 None []
+    |> List.map (fun lid ->
+        let s = string_of_longident lid in
+        (s, (Ocaml_typing.eval s : thm))) in
+  let _ = Ocaml_typing.exec ("set_jrh_lexer;;") in
+  res
 end
 
 

update_database/update_database_5.ml

@@ -0,0 +1,152 @@
+(* ========================================================================= *)
+(* Create search database from OCaml / modify search database dynamically.   *)
+(*                                                                           *)
+(* This file assigns to "theorems", which is a list of name-theorem pairs.   *)
+(* The core system already has such a database set up. Use this file if you  *)
+(* want to update the database beyond the core, so you can search it.        *)
+(*                                                                           *)
+(* The trickery to get at the OCaml environment is due to Roland Zumkeller   *)
+(* and Michael Farber. It works by copying some internal data structures and *)
+(* casting into the copy using Obj.magic.                                    *)
+(* ========================================================================= *)
+
+module Ocaml_typing = struct
+
+open Types
+
+(* If the given type is simple return its name, otherwise None. *)
+
+let rec get_simple_type = function
+  | Tlink texpr ->
+    (match get_desc texpr with
+    | Tconstr (Pident p,[],_) -> Some (Ident.name p)
+    | d -> get_simple_type d)
+  | Tconstr (Path.Pident p,  [], _) -> Some (Ident.name p)
+  | _ -> None;;
+
+(* Execute any OCaml expression given as a string. *)
+
+let exec s = (ignore o Toploop.execute_phrase false Format.std_formatter
+  o !Toploop.parse_toplevel_phrase o Lexing.from_string) s
+
+(* Evaluate any OCaml expression given as a string. *)
+
+let eval n =
+  if String.contains n '.' then begin
+    exec ("let buf__ = ( " ^ n ^ " );;");
+    Obj.magic (Toploop.getvalue "buf__")
+  end else Obj.magic (Toploop.getvalue n)
+
+(* Register all theorems added since the last update. *)
+end
+
+module Lookuptheorems = struct
+open Types
+
+let lid_cons lidopt id =
+  match lidopt with
+    None -> Longident.Lident id
+  | Some li -> Longident.Ldot(li, id)
+
+let it_val_1 lidopt s p vd acc =
+  if (Some "thm") = Ocaml_typing.get_simple_type (get_desc vd.Types.val_type) then
+    (lid_cons lidopt s)::acc else acc
+
+let it_mod_1 lidopt s p md acc = (lid_cons lidopt s)::acc
+
+let enum0 lidopt =
+  try
+    let vl = Env.fold_values (it_val_1 lidopt) lidopt !Toploop.toplevel_env [] in
+    let ml = Env.fold_modules (it_mod_1 lidopt) lidopt !Toploop.toplevel_env [] in
+    (vl, ml)
+  with Not_found ->
+    (* Looking for (Longident.Lident "Stream") raises Not_found.
+       Stream is a deprecated alias module of "Stdlib.Stream", and the camlp-streams
+       package that is used by pa_hol_syntax redefines Stream, which seems to
+       confuse Env.fold_values and Env.fold_modules. *)
+    ([], [])
+
+let rec enum1 lidopt acc =
+  match enum0 lidopt with
+    (vl, []) -> vl@acc
+  | (vl, ml) ->
+     List.fold_left (fun acc mlid ->
+         enum1 (Some mlid) acc) (vl@acc) ml
+
+let string_of_longident lid =
+  String.concat "." (Longident.flatten lid)
+
+let all_theorems () =
+  let _ = Ocaml_typing.exec ("unset_jrh_lexer;;") in
+  let res = enum1 None []
+    |> List.map (fun lid ->
+        let s = string_of_longident lid in
+        (s, (Ocaml_typing.eval s : thm))) in
+  let _ = Ocaml_typing.exec ("set_jrh_lexer;;") in
+  res
+end
+
+
+let update_database () =
+    theorems := Lookuptheorems.all_theorems()
+
+(* ------------------------------------------------------------------------- *)
+(* Put an assignment of a theorem database in the named file.                *)
+(* ------------------------------------------------------------------------- *)
+
+let make_database_assignment filename =
+  update_database();
+  (let allnames = uniq(sort (<) (map fst (!theorems))) in
+   let names = subtract allnames ["it"] in
+   let entries = map (fun n -> "\""^n^"\","^n) names in
+   let text = "needs \"help.ml\";;\n\n"^
+              "theorems :=\n[\n"^
+              end_itlist (fun a b -> a^";\n"^b) entries^"\n];;\n" in
+   file_of_string filename text);;
+
+(* ------------------------------------------------------------------------- *)
+(* Search (automatically updates)                                            *)
+(* ------------------------------------------------------------------------- *)
+
+let search =
+  let rec immediatesublist l1 l2 =
+    match (l1,l2) with
+      [],_ -> true
+    | _,[] -> false
+    | (h1::t1,h2::t2) -> h1 = h2 && immediatesublist t1 t2 in
+  let rec sublist l1 l2 =
+    match (l1,l2) with
+      [],_ -> true
+    | _,[] -> false
+    | (h1::t1,h2::t2) -> immediatesublist l1 l2 || sublist l1 t2 in
+  let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th)
+  and name_contains s (n,th) = sublist (explode s) (explode n) in
+  let rec filterpred tm =
+    match tm with
+      Comb(Var("<omit this pattern>",_),t) -> not o filterpred t
+    | Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
+    | Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)
+    | pat -> exists_subterm_satisfying (can (term_match [] pat)) in
+  fun pats ->
+    update_database();
+    let triv,nontriv = partition is_var pats in
+    (if triv <> [] then
+      warn true
+         ("Ignoring plain variables in search: "^
+          end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv))
+     else ());
+    (if nontriv = [] && triv <> [] then []
+     else sort (increasing fst)
+               (itlist (filter o filterpred) pats (!theorems)));;
+
+(* ------------------------------------------------------------------------- *)
+(* Update to bring things back to current state.                             *)
+(* ------------------------------------------------------------------------- *)
+
+update_database();;
+
+(* This printf checks whether standard modules like Printf are still alive
+   after update_database.
+   See also: https://github.com/ocaml/ocaml/issues/12271 *)
+Printf.printf "update_database.ml loaded! # theorems: %d\n"
+   (List.length !theorems);;