From 3a7e06297454dec4df45ebf247a447e42ce201da Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Sat, 10 Aug 2024 12:19:04 -0500 Subject: [PATCH] Factor out loader functions and core loads as hol_loader.ml and hol_lib.ml This patch is a second one of splitted patches to support module compilation of HOL Light. This (1) Factors out core library loads as hol_lib.ml, which will be compiled into one giant module in the future (2) Moves `#install_printer` commands from local files to `hol.ml` because the directive cannot be compiled (3) Also factors out `use_file`, `loads`, `needs`, `loadt` and the functions they use to `hol_loader.ml` because these will be independently used by the inliner script which will be included in the later patch. Passed holtest on OCaml 4.14 and 4.05, and also checked that hol.sh can be successfully loaded outside hol-light dir. --- .gitignore | 1 + Makefile | 5 +- help.ml | 2 - hol.ml | 150 +++++--------------------------------------------- hol_lib.ml | 101 +++++++++++++++++++++++++++++++++ hol_loader.ml | 71 ++++++++++++++++++++++++ lib.ml | 4 +- printer.ml | 8 --- system.ml | 2 - tactics.ml | 7 --- thecops.ml | 2 +- 11 files changed, 192 insertions(+), 161 deletions(-) create mode 100644 hol_lib.ml create mode 100644 hol_loader.ml diff --git a/.gitignore b/.gitignore index c6c9e4ff..8d13c150 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ .DS_Store +.vscode _opam *.cmi *.cmo diff --git a/Makefile b/Makefile index 70e2f9aa..adcfa0f9 100644 --- a/Makefile +++ b/Makefile @@ -19,11 +19,12 @@ BINDIR=${HOME}/bin HOLSRC=system.ml lib.ml fusion.ml basics.ml nets.ml preterm.ml \ parser.ml printer.ml equal.ml bool.ml drule.ml tactics.ml \ itab.ml simp.ml theorems.ml ind_defs.ml class.ml trivia.ml \ - canon.ml meson.ml metis.ml quot.ml recursion.ml pair.ml \ + canon.ml meson.ml firstorder.ml metis.ml thecops.ml quot.ml \ + impconv.ml recursion.ml pair.ml \ nums.ml arith.ml wf.ml calc_num.ml normalizer.ml grobner.ml \ ind_types.ml lists.ml realax.ml calc_int.ml realarith.ml \ real.ml calc_rat.ml int.ml sets.ml iterate.ml cart.ml define.ml \ - help.ml database.ml update_database.ml + help.ml database.ml update_database.ml hol_lib.ml hol_loader.ml # Some parameters to help decide how to build things diff --git a/help.ml b/help.ml index 01910c61..7ad350bc 100755 --- a/help.ml +++ b/help.ml @@ -7,8 +7,6 @@ (* (c) Copyright, John Harrison 1998-2007 *) (* ========================================================================= *) -needs "define.ml";; - (* ------------------------------------------------------------------------- *) (* Help system. *) (* ------------------------------------------------------------------------- *) diff --git a/hol.ml b/hol.ml index dededb1a..df1c9e2d 100644 --- a/hol.ml +++ b/hol.ml @@ -13,9 +13,6 @@ let hol_version = "2.20++";; #directory "+compiler-libs";; -let hol_dir = ref - (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());; - (* ------------------------------------------------------------------------- *) (* Should eventually change to "ref(Filename.temp_dir_name)". *) (* However that's not available in 3.08, which is still the default *) @@ -24,60 +21,11 @@ let hol_dir = ref let temp_path = ref "/tmp";; -(* ------------------------------------------------------------------------- *) -(* Load files from system and/or user-settable directories. *) -(* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual *) -(* $ character at the start of a directory. *) -(* ------------------------------------------------------------------------- *) +#use "hol_loader.ml";; -(* A flag that sets whether use_file must raise Failure if loading the file *) -(* did not succeed. If set to true, this helps (nested) loading of files fail*) -(* early. However, propagation of the failure will cause Toplevel to forget *) -(* bindings ('let .. = ..;;') that have been made before the erroneous *) -(* statement in the file. This leads to an inconsistent state between *) -(* variable and defined constants in HOL Light. *) -let use_file_raise_failure = ref false;; - -let use_file s = - if Toploop.use_file Format.std_formatter s then () - else if !use_file_raise_failure - then failwith("Error in included file "^s) - else (Format.print_string("Error in included file "^s); - Format.print_newline());; - -let hol_expand_directory s = - if s = "$" || s = "$/" then !hol_dir - else if s = "$$" then "$" - else if String.length s <= 2 then s - else if String.sub s 0 2 = "$$" then (String.sub s 1 (String.length s - 1)) - else if String.sub s 0 2 = "$/" - then Filename.concat (!hol_dir) (String.sub s 2 (String.length s - 2)) - else s;; - -let load_path = ref ["."; "$"];; - -let loaded_files = ref [];; - -let file_on_path p s = - if not (Filename.is_relative s) then s else - let p' = List.map hol_expand_directory p in - let d = List.find (fun d -> Sys.file_exists(Filename.concat d s)) p' in - Filename.concat (if d = "." then Sys.getcwd() else d) s;; - -let load_on_path p s = - let s' = file_on_path p s in - let fileid = (Filename.basename s',Digest.file s') in - (use_file s'; loaded_files := fileid::(!loaded_files));; - -let loads s = load_on_path ["$"] s;; - -let loadt s = load_on_path (!load_path) s;; - -let needs s = - let s' = file_on_path (!load_path) s in - let fileid = (Filename.basename s',Digest.file s') in - if List.mem fileid (!loaded_files) - then Format.print_string("File \""^s^"\" already loaded\n") else loadt s;; +file_loader := fun s -> Toploop.use_file Format.std_formatter s;; +(* Hide the definition of file_loader of hol_loader.ml. *) +let file_loader = ();; (* ------------------------------------------------------------------------- *) (* Load in parsing extensions. *) @@ -98,96 +46,26 @@ else loads "load_camlp4.ml";; Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");; -include Bignum;; - - -(* ------------------------------------------------------------------------- *) -(* Bind these to names that are independent of OCaml versions before they *) -(* are potentially overwritten by an identifier of the same name. In older *) -(* and newer Ocaml versions these are respectively: *) -(* *) -(* Pervasives.sqrt -> Float.sqrt *) -(* Pervasives.abs_float -> Stdlib.abs_float / Float.abs *) -(* ------------------------------------------------------------------------- *) - -let float_sqrt = sqrt;; -let float_fabs = abs_float;; - (* ------------------------------------------------------------------------- *) -(* Various tweaks to OCaml and general library functions. *) +(* Load the core files. *) (* ------------------------------------------------------------------------- *) -loads "system.ml";; (* Set up proper parsing and load bignums *) -loads "lib.ml";; (* Various useful general library functions *) +loads "hol_lib.ml";; (* ------------------------------------------------------------------------- *) -(* The logical core. *) +(* Install printers. *) (* ------------------------------------------------------------------------- *) -loads "fusion.ml";; +#install_printer pp_print_num;; -(* ------------------------------------------------------------------------- *) -(* Some extra support stuff needed outside the core. *) -(* ------------------------------------------------------------------------- *) +#install_printer pp_print_fpf;; -loads "basics.ml";; (* Additional syntax operations and other utilities *) -loads "nets.ml";; (* Term nets for fast matchability-based lookup *) - -(* ------------------------------------------------------------------------- *) -(* The interface. *) -(* ------------------------------------------------------------------------- *) - -loads "printer.ml";; (* Crude prettyprinter *) -loads "preterm.ml";; (* Preterms and their interconversion with terms *) -loads "parser.ml";; (* Lexer and parser *) - -(* ------------------------------------------------------------------------- *) -(* Higher level deductive system. *) -(* ------------------------------------------------------------------------- *) - -loads "equal.ml";; (* Basic equality reasoning and conversionals *) -loads "bool.ml";; (* Boolean theory and basic derived rules *) -loads "drule.ml";; (* Additional derived rules *) -loads "tactics.ml";; (* Tactics, tacticals and goal stack *) -loads "itab.ml";; (* Toy prover for intuitionistic logic *) -loads "simp.ml";; (* Basic rewriting and simplification tools *) -loads "theorems.ml";; (* Additional theorems (mainly for quantifiers) etc. *) -loads "ind_defs.ml";; (* Derived rules for inductive definitions *) -loads "class.ml";; (* Classical reasoning: Choice and Extensionality *) -loads "trivia.ml";; (* Some very basic theories, e.g. type ":1" *) -loads "canon.ml";; (* Tools for putting terms in canonical forms *) -loads "meson.ml";; (* First order automation: MESON (model elimination) *) -loads "firstorder.ml";; (* More utilities for first-order shadow terms *) -loads "metis.ml";; (* More advanced first-order automation: Metis *) -loads "thecops.ml";; (* Connection-based automation: leanCoP and nanoCoP *) -loads "quot.ml";; (* Derived rules for defining quotient types *) -loads "impconv.ml";; (* More powerful implicational rewriting etc. *) - -(* ------------------------------------------------------------------------- *) -(* Mathematical theories and additional proof tools. *) -(* ------------------------------------------------------------------------- *) +#install_printer pp_print_qtype;; +#install_printer pp_print_qterm;; +#install_printer pp_print_thm;; -loads "pair.ml";; (* Theory of pairs *) -loads "compute.ml";; (* General call-by-value reduction tool for terms *) -loads "nums.ml";; (* Axiom of Infinity, definition of natural numbers *) -loads "recursion.ml";; (* Tools for primitive recursion on inductive types *) -loads "arith.ml";; (* Natural number arithmetic *) -loads "wf.ml";; (* Theory of wellfounded relations *) -loads "calc_num.ml";; (* Calculation with natural numbers *) -loads "normalizer.ml";; (* Polynomial normalizer for rings and semirings *) -loads "grobner.ml";; (* Groebner basis procedure for most semirings *) -loads "ind_types.ml";; (* Tools for defining inductive types *) -loads "lists.ml";; (* Theory of lists *) -loads "realax.ml";; (* Definition of real numbers *) -loads "calc_int.ml";; (* Calculation with integer-valued reals *) -loads "realarith.ml";; (* Universal linear real decision procedure *) -loads "real.ml";; (* Derived properties of reals *) -loads "calc_rat.ml";; (* Calculation with rational-valued reals *) -loads "int.ml";; (* Definition of integers *) -loads "sets.ml";; (* Basic set theory *) -loads "iterate.ml";; (* Iterated operations *) -loads "cart.ml";; (* Finite Cartesian products *) -loads "define.ml";; (* Support for general recursive definitions *) +#install_printer pp_print_goal;; +#install_printer pp_print_goalstack;; (* ------------------------------------------------------------------------- *) (* The help system. *) diff --git a/hol_lib.ml b/hol_lib.ml new file mode 100644 index 00000000..6a056963 --- /dev/null +++ b/hol_lib.ml @@ -0,0 +1,101 @@ +(* ========================================================================= *) +(* HOL LIGHT *) +(* *) +(* Modern OCaml version of the HOL theorem prover *) +(* *) +(* John Harrison *) +(* *) +(* (c) Copyright, University of Cambridge 1998 *) +(* (c) Copyright, John Harrison 1998-2024 *) +(* (c) Copyright, Juneyoung Lee 2024 *) +(* ========================================================================= *) + +include Bignum;; + +(* ------------------------------------------------------------------------- *) +(* Bind these to names that are independent of OCaml versions before they *) +(* are potentially overwritten by an identifier of the same name. In older *) +(* and newer Ocaml versions these are respectively: *) +(* *) +(* Pervasives.sqrt -> Float.sqrt *) +(* Pervasives.abs_float -> Stdlib.abs_float / Float.abs *) +(* ------------------------------------------------------------------------- *) + +let float_sqrt = sqrt;; +let float_fabs = abs_float;; + +(* ------------------------------------------------------------------------- *) +(* Various tweaks to OCaml and general library functions. *) +(* ------------------------------------------------------------------------- *) + +loads "system.ml";; (* Set up proper parsing and load bignums *) +loads "lib.ml";; (* Various useful general library functions *) + +(* ------------------------------------------------------------------------- *) +(* The logical core. *) +(* ------------------------------------------------------------------------- *) + +loads "fusion.ml";; + +(* ------------------------------------------------------------------------- *) +(* Some extra support stuff needed outside the core. *) +(* ------------------------------------------------------------------------- *) + +loads "basics.ml";; (* Additional syntax operations and other utilities *) +loads "nets.ml";; (* Term nets for fast matchability-based lookup *) + +(* ------------------------------------------------------------------------- *) +(* The interface. *) +(* ------------------------------------------------------------------------- *) + +loads "printer.ml";; (* Crude prettyprinter *) +loads "preterm.ml";; (* Preterms and their interconversion with terms *) +loads "parser.ml";; (* Lexer and parser *) + +(* ------------------------------------------------------------------------- *) +(* Higher level deductive system. *) +(* ------------------------------------------------------------------------- *) + +loads "equal.ml";; (* Basic equality reasoning and conversionals *) +loads "bool.ml";; (* Boolean theory and basic derived rules *) +loads "drule.ml";; (* Additional derived rules *) +loads "tactics.ml";; (* Tactics, tacticals and goal stack *) +loads "itab.ml";; (* Toy prover for intuitionistic logic *) +loads "simp.ml";; (* Basic rewriting and simplification tools *) +loads "theorems.ml";; (* Additional theorems (mainly for quantifiers) etc. *) +loads "ind_defs.ml";; (* Derived rules for inductive definitions *) +loads "class.ml";; (* Classical reasoning: Choice and Extensionality *) +loads "trivia.ml";; (* Some very basic theories, e.g. type ":1" *) +loads "canon.ml";; (* Tools for putting terms in canonical forms *) +loads "meson.ml";; (* First order automation: MESON (model elimination) *) +loads "firstorder.ml";; (* More utilities for first-order shadow terms *) +loads "metis.ml";; (* More advanced first-order automation: Metis *) +loads "thecops.ml";; (* Connection-based automation: leanCoP and nanoCoP *) +loads "quot.ml";; (* Derived rules for defining quotient types *) +loads "impconv.ml";; (* More powerful implicational rewriting etc. *) + +(* ------------------------------------------------------------------------- *) +(* Mathematical theories and additional proof tools. *) +(* ------------------------------------------------------------------------- *) + +loads "pair.ml";; (* Theory of pairs *) +loads "compute.ml";; (* General call-by-value reduction tool for terms *) +loads "nums.ml";; (* Axiom of Infinity, definition of natural numbers *) +loads "recursion.ml";; (* Tools for primitive recursion on inductive types *) +loads "arith.ml";; (* Natural number arithmetic *) +loads "wf.ml";; (* Theory of wellfounded relations *) +loads "calc_num.ml";; (* Calculation with natural numbers *) +loads "normalizer.ml";; (* Polynomial normalizer for rings and semirings *) +loads "grobner.ml";; (* Groebner basis procedure for most semirings *) +loads "ind_types.ml";; (* Tools for defining inductive types *) +loads "lists.ml";; (* Theory of lists *) +loads "realax.ml";; (* Definition of real numbers *) +loads "calc_int.ml";; (* Calculation with integer-valued reals *) +loads "realarith.ml";; (* Universal linear real decision procedure *) +loads "real.ml";; (* Derived properties of reals *) +loads "calc_rat.ml";; (* Calculation with rational-valued reals *) +loads "int.ml";; (* Definition of integers *) +loads "sets.ml";; (* Basic set theory *) +loads "iterate.ml";; (* Iterated operations *) +loads "cart.ml";; (* Finite Cartesian products *) +loads "define.ml";; (* Support for general recursive definitions *) diff --git a/hol_loader.ml b/hol_loader.ml new file mode 100644 index 00000000..a87d06cf --- /dev/null +++ b/hol_loader.ml @@ -0,0 +1,71 @@ +(* ========================================================================= *) +(* HOL LIGHT *) +(* *) +(* Modern OCaml version of the HOL theorem prover *) +(* *) +(* John Harrison *) +(* *) +(* (c) Copyright, University of Cambridge 1998 *) +(* (c) Copyright, John Harrison 1998-2024 *) +(* (c) Copyright, Juneyoung Lee 2024 *) +(* ========================================================================= *) + +let hol_dir = ref + (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());; + +(* ------------------------------------------------------------------------- *) +(* Load files from system and/or user-settable directories. *) +(* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual *) +(* $ character at the start of a directory. *) +(* ------------------------------------------------------------------------- *) + +(* A flag that sets whether use_file must raise Failure if loading the file *) +(* did not succeed. If set to true, this helps (nested) loading of files fail*) +(* early. However, propagation of the failure will cause Toplevel to forget *) +(* bindings ('let .. = ..;;') that have been made before the erroneous *) +(* statement in the file. This leads to an inconsistent state between *) +(* variable and defined constants in HOL Light. *) +let use_file_raise_failure = ref false;; + +let file_loader = ref (fun (s:string) -> failwith "uninitialized"; false);; + +let use_file s = + if !file_loader s then () + else if !use_file_raise_failure + then failwith("Error in included file "^s) + else (Format.print_string("Error in included file "^s); + Format.print_newline());; + +let hol_expand_directory s = + if s = "$" || s = "$/" then !hol_dir + else if s = "$$" then "$" + else if String.length s <= 2 then s + else if String.sub s 0 2 = "$$" then (String.sub s 1 (String.length s - 1)) + else if String.sub s 0 2 = "$/" + then Filename.concat (!hol_dir) (String.sub s 2 (String.length s - 2)) + else s;; + +let load_path = ref ["."; "$"];; + +let loaded_files = ref [];; + +let file_on_path p s = + if not (Filename.is_relative s) then s else + let p' = List.map hol_expand_directory p in + let d = List.find (fun d -> Sys.file_exists(Filename.concat d s)) p' in + Filename.concat (if d = "." then Sys.getcwd() else d) s;; + +let load_on_path p s = + let s' = file_on_path p s in + let fileid = (Filename.basename s',Digest.file s') in + (use_file s'; loaded_files := fileid::(!loaded_files));; + +let loads s = load_on_path ["$"] s;; + +let loadt s = load_on_path (!load_path) s;; + +let needs s = + let s' = file_on_path (!load_path) s in + let fileid = (Filename.basename s',Digest.file s') in + if List.mem fileid (!loaded_files) + then Format.print_string("File \""^s^"\" already loaded\n") else loadt s;; diff --git a/lib.ml b/lib.ml index 42670e76..72ce1ba5 100755 --- a/lib.ml +++ b/lib.ml @@ -777,9 +777,7 @@ let rec choose t = let pp_print_fpf fmt (f:('a,'b)func) = Format.pp_print_string fmt "";; -let print_fpf = pp_print_fpf Format.std_formatter;; - -#install_printer pp_print_fpf;; +let print_fpf f = pp_print_fpf Format.std_formatter f;; (* ------------------------------------------------------------------------- *) (* Set operations parametrized by equality (from Steven Obua). *) diff --git a/printer.ml b/printer.ml index 4c280bd1..a2d3ba9f 100755 --- a/printer.ml +++ b/printer.ml @@ -568,14 +568,6 @@ let print_term = pp_print_term std_formatter;; let print_qterm = pp_print_qterm std_formatter;; let print_thm = pp_print_thm std_formatter;; -(* ------------------------------------------------------------------------- *) -(* Install all the printers. *) -(* ------------------------------------------------------------------------- *) - -#install_printer pp_print_qtype;; -#install_printer pp_print_qterm;; -#install_printer pp_print_thm;; - (* ------------------------------------------------------------------------- *) (* Conversions to string. *) (* ------------------------------------------------------------------------- *) diff --git a/system.ml b/system.ml index 7be5b6f8..c51a2fbc 100644 --- a/system.ml +++ b/system.ml @@ -22,5 +22,3 @@ let pp_print_num fmt n = Format.pp_close_box fmt ();; let print_num = pp_print_num Format.std_formatter;; - -#install_printer pp_print_num;; diff --git a/tactics.ml b/tactics.ml index 5a80389d..ec6a0466 100644 --- a/tactics.ml +++ b/tactics.ml @@ -944,10 +944,3 @@ let top_goal() = let top_thm() = let (_,[],f)::_ = !current_goalstack in f null_inst [];; - -(* ------------------------------------------------------------------------- *) -(* Install the goal-related printers. *) -(* ------------------------------------------------------------------------- *) - -#install_printer pp_print_goal;; -#install_printer pp_print_goalstack;; diff --git a/thecops.ml b/thecops.ml index 42125ae5..33d4d7e7 100644 --- a/thecops.ml +++ b/thecops.ml @@ -930,7 +930,7 @@ let string_of_iclause_i = print_to_string (pp_print_iclause pp_print_index) let string_of_nclause c = print_to_string (pp_print_nclause pp_print_null) c let string_of_matrix m = print_to_string (pp_print_matrix pp_print_null) m -let pp_print_matrix_ni = pp_print_matrix pp_print_null +let pp_print_matrix_ni fmt x = pp_print_matrix pp_print_null fmt x let print_iclause c = pp_nl (pp_print_iclause pp_print_null) std_formatter c let print_iclause_i = pp_nl (pp_print_iclause pp_print_index) std_formatter