Use Zarith in OCaml 4.14, introduce a custom Num wrapper for compatib…

…ility

This commit updates HOL Light to use Zarith when OCaml 4.14 is used.

.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

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 \

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
 

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;;

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.lt_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;;

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

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

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";;

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;;