Merge pull request #107 from aqjune-aws/module2

Factor out loader functions and core loads as hol_loader.ml and hol_lib.ml

.gitignore

@@ -1,4 +1,5 @@
 .DS_Store
+.vscode
 _opam
 *.cmi
 *.cmo

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
 

help.ml

@@ -7,8 +7,6 @@
 (* (c) Copyright, John Harrison 1998-2007 *)
 (* ========================================================================= *)
 
-needs "define.ml";;
-
 (* ------------------------------------------------------------------------- *)
 (* Help system. *)
 (* ------------------------------------------------------------------------- *)

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. *)

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 *)