From c8f948a5f6cf37e807f011f6770d388c849d1c42 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Mon, 1 Apr 2024 01:53:10 -0500 Subject: [PATCH] Use Zarith in OCaml 4.14, introduce a custom Num wrapper for compatibility This commit updates HOL Light to use Zarith when OCaml 4.14 is used. --- .github/workflows/main.yml | 2 +- Makefile | 5 +- README | 15 ++-- bignum_num.ml | 19 +++++ bignum_zarith.ml | 141 +++++++++++++++++++++++++++++++++++++ hol.ml | 4 ++ lib.ml | 8 +-- load_camlp5_topfind.ml | 1 - system.ml | 30 ++++---- 9 files changed, 192 insertions(+), 33 deletions(-) create mode 100644 bignum_num.ml create mode 100644 bignum_zarith.ml diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 565b358c..681f124b 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -50,7 +50,7 @@ jobs: sudo apt update && sudo apt install -y opam xdot opam init --disable-sandboxing --compiler=4.14.0 opam pin -y add camlp5 8.02.01 - opam install -y num + opam install -y zarith - name: Checkout this repo uses: actions/checkout@v2 diff --git a/Makefile b/Makefile index 177912af..5e2bf6e3 100644 --- a/Makefile +++ b/Makefile @@ -89,10 +89,9 @@ pa_j.ml: pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml pa_j_3.1x_5.xx.ml pa_j_3.1x_6.xx hol.sh: pa_j.cmo ${HOLSRC} update_database.ml if [ `uname` = "Linux" ] || [ `uname` = "Darwin" ] ; then \ - ocamlmktop -o ocaml-hol nums.cma ; \ if test ${OCAML_VERSION} = "4.14" ; \ - then sed "s^__DIR__^`pwd`^g" hol_4.14.sh > hol.sh ; \ - else sed "s^__DIR__^`pwd`^g" hol_4.sh > hol.sh ; \ + then ocamlmktop -o ocaml-hol ; sed "s^__DIR__^`pwd`^g" hol_4.14.sh > hol.sh ; \ + else ocamlmktop -o ocaml-hol nums.cma ; sed "s^__DIR__^`pwd`^g" hol_4.sh > hol.sh ; \ fi ; \ chmod +x hol.sh ; \ else \ diff --git a/README b/README index 9639b7bb..b97ca05e 100644 --- a/README +++ b/README @@ -54,10 +54,17 @@ too difficult, depending on the platform. http://caml.inria.fr/ocaml/index.en.html - 2. num: The HOL Light system uses the OCaml "Num" library for rational - arithmetic. As of OCaml 4.06, this is no longer included in - the core system and will need to be added separately. You can - do this using the OCaml package manager "opam" if you use it by + 2. zarith or num: The HOL Light system uses the OCaml "Num" library + or "Zarith" library for rational arithmetic. If OCaml 4.14 is used, + HOL Light will use Zarith. You can install it using the OCaml package + manager "opam" by + + opam install zarith + + If OCaml 4.05 is used, HOL Light will use Num which is included in + the core system. If you are using an OCaml version between 4.06 and 4.13, + Num must be installed separately because it is no longer included in + the core system. You can use "opam" by opam install num diff --git a/bignum_num.ml b/bignum_num.ml new file mode 100644 index 00000000..7d2b78ff --- /dev/null +++ b/bignum_num.ml @@ -0,0 +1,19 @@ +(* ------------------------------------------------------------------------- *) +(* Load in the bignum library. *) +(* ------------------------------------------------------------------------- *) + +#load "nums.cma";; + +include Num;; + +module NumExt = struct + let numdom (r:num):num * num = + let r' = Ratio.normalize_ratio (ratio_of_num r) in + num_of_big_int(Ratio.numerator_ratio r'), + num_of_big_int(Ratio.denominator_ratio r');; + + let gcd_num (n1:num) (n2:num): num = + num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));; +end;; + +open NumExt;; diff --git a/bignum_zarith.ml b/bignum_zarith.ml new file mode 100644 index 00000000..a05b6475 --- /dev/null +++ b/bignum_zarith.ml @@ -0,0 +1,141 @@ +(* ------------------------------------------------------------------------- *) +(* Load in the bignum library. *) +(* ------------------------------------------------------------------------- *) + +Topfind.load_deeply ["zarith"];; + +(* A wrapper of Zarith that has an interface of Num. + However, this is different from the real Num library because it supports + infinity and undef. If exception happens, Failure with the name of the + exception is raised. *) +module Num = struct + type num = Q.t + + let num_of_int (n:int):num = Q.of_int n + + let int_of_num (n:num):int = + try Q.to_int n + with Z.Overflow -> failwith "Z.Overflow" + + (* base must be Z.t and exponent + must fit in the range of OCaml int type *) + let power_num (base:num) (exponent:num):num = + let exp_i = int_of_num exponent in + Q.of_bigint (Z.pow (Q.to_bigint base) exp_i) + + let pow (base:num) (exponent:int):num = + Q.of_bigint (Z.pow (Q.to_bigint base) exponent) + + let add_num = Q.add + + let abs_num = Q.abs + + let ceiling_num (c:num) = + try Q.of_bigint (Z.cdiv c.num c.den) + with Division_by_zero -> failwith "Division_by_zero" + + let compare_num = Q.compare + + let div_num = Q.div + + let eq_num = Q.equal + + let floor_num (c:num) = + try Q.of_bigint (Z.fdiv c.num c.den) + with Division_by_zero -> failwith "Division_by_zero" + + let ge_num = Q.geq + + let gt_num = Q.gt + + let le_num = Q.leq + + let lt_num = Q.lt + + let max_num = Q.max + + let minus_num = Q.neg + + let min_num = Q.min + + let mod_num = fun x y -> + Q.of_bigint (Z.erem (Q.to_bigint x) (Q.to_bigint y)) + + let mult_num = Q.mul + + (* 1/2 -> 1, -1/2 -> -1 *) + let round_num = + let half = Q.make (Z.of_int 1) (Z.of_int 2) in + let one = Q.make (Z.of_int 1) (Z.of_int 1) in + fun x -> + let s = Q.sign x in + if s = 0 then x + else + let v = Q.abs x in + let vint = floor_num v in + let vfrac = Q.sub v vint in + let absres = + if Q.leq half vfrac + then Q.add vint one + else vint in + Q.mul (Q.of_int s) absres + + let sign_num = Q.sign + + let sub_num = Q.sub + + let quo_num = fun x y -> + Q.of_bigint (Z.ediv (Q.to_bigint x) (Q.to_bigint y)) + + let is_integer_num (n:num) = + try let _ = Q.to_int n in true + with _ -> false + + let succ_num = fun n -> + Q.of_bigint (Z.succ (Q.to_bigint n)) + + let string_of_num (n:num) = Q.to_string n +end;; + +let (=/) x y = Num.eq_num x y;; + +let (<>/) x y = not (x =/ y);; + +let (+/) x y = Num.add_num x y;; + +let (-/) x y = Num.sub_num x y;; + +let (//) x y = Num.div_num x y;; + +let ( */) x y = Num.mult_num x y;; + +let (/) x y = Num.gt_num x y;; + +let (<=/) x y = Num.le_num x y;; + +let (>=/) x y = Num.ge_num x y;; + + +let pp_print_num fmt (n:Num.num) = + Format.pp_open_hbox fmt (); + Format.pp_print_string fmt (Num.string_of_num n); + Format.pp_close_box fmt ();; + +let print_num = pp_print_num Format.std_formatter;; + +#install_printer pp_print_num;; + +include Num;; + +module NumExt = struct + let numdom (r:num):num * num = + Q.of_bigint r.num, Q.of_bigint r.den + + let gcd_num = + fun x y -> Q.of_bigint (Z.gcd (Q.to_bigint x) (Q.to_bigint y)) + +end;; + +open NumExt;; diff --git a/hol.ml b/hol.ml index 91aada61..fdb477cd 100644 --- a/hol.ml +++ b/hol.ml @@ -98,6 +98,10 @@ else loads "load_camlp4.ml";; Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");; +if version_ge_4_14 +then loads "bignum_zarith.ml" +else loads "bignum_num.ml";; + (* ------------------------------------------------------------------------- *) (* Various tweaks to OCaml and general library functions. *) (* ------------------------------------------------------------------------- *) diff --git a/lib.ml b/lib.ml index f9703ac1..aa0a5411 100755 --- a/lib.ml +++ b/lib.ml @@ -389,16 +389,10 @@ and num_10 = Num.num_of_int 10;; let pow2 n = power_num num_2 (Num.num_of_int n);; let pow10 n = power_num num_10 (Num.num_of_int n);; -let numdom r = - let r' = Ratio.normalize_ratio (ratio_of_num r) in - num_of_big_int(Ratio.numerator_ratio r'), - num_of_big_int(Ratio.denominator_ratio r');; - let numerator = fst o numdom and denominator = snd o numdom;; -let gcd_num n1 n2 = - num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));; +(* gcd_num x y is defined in the NumExt module. *) let lcm_num x y = if x =/ num_0 && y =/ num_0 then num_0 diff --git a/load_camlp5_topfind.ml b/load_camlp5_topfind.ml index 113690a3..e4c05309 100644 --- a/load_camlp5_topfind.ml +++ b/load_camlp5_topfind.ml @@ -5,5 +5,4 @@ Topdirs.dir_use Format.std_formatter "topfind";; Topfind.don't_load ["compiler-libs.common"];; Topfind.load_deeply ["camlp5"];; -Topfind.load_deeply ["num"];; Topdirs.dir_load Format.std_formatter "camlp5o.cma";; diff --git a/system.ml b/system.ml index 4c3573ae..402cec3a 100644 --- a/system.ml +++ b/system.ml @@ -12,6 +12,19 @@ Gc.set { (Gc.get()) with Gc.stack_limit = 16777216 };; Sys.catch_break true;; +(* ------------------------------------------------------------------------- *) +(* Set up a printer for num. *) +(* ------------------------------------------------------------------------- *) + +let pp_print_num fmt n = + Format.pp_open_hbox fmt (); + Format.pp_print_string fmt (string_of_num n); + Format.pp_close_box fmt ();; + +let print_num = pp_print_num Format.std_formatter;; + +#install_printer pp_print_num;; + (* ------------------------------------------------------------------------- *) (* Set up a quotation expander for the `...` quotes. *) (* This includes the case `;...` to support miz3, even if that isn't loaded. *) @@ -38,20 +51,3 @@ Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander));; (* ------------------------------------------------------------------------- *) set_jrh_lexer;; - -(* ------------------------------------------------------------------------- *) -(* Load in the bignum library and set up printing in the toplevel. *) -(* ------------------------------------------------------------------------- *) - -#load "nums.cma";; - -include Num;; - -let pp_print_num fmt n = - Format.pp_open_hbox fmt (); - Format.pp_print_string fmt (string_of_num n); - Format.pp_close_box fmt ();; - -let print_num = pp_print_num Format.std_formatter;; - -#install_printer pp_print_num;;