Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 1 commit into from
Aug 23, 2024
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
.DS_Store
.vscode
_opam
*.cmi
*.cmo
Expand Down
5 changes: 3 additions & 2 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 0 additions & 2 deletions help.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,6 @@
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)

needs "define.ml";;

(* ------------------------------------------------------------------------- *)
(* Help system. *)
(* ------------------------------------------------------------------------- *)
Expand Down
150 changes: 14 additions & 136 deletions hol.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand All @@ -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. *)
Expand All @@ -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. *)
Expand Down
101 changes: 101 additions & 0 deletions hol_lib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 *)
Loading
Loading