From 094e4649c29e2426daca0476c140439de901dafe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 16 Oct 2018 14:55:30 +0200 Subject: [numeral] [plugins] Switch from `Big_int` to ZArith. We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte --- interp/notation.ml | 44 +++++++++++++++++++++----------------------- 1 file changed, 21 insertions(+), 23 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 0bd5da5729..c0ebffcdb9 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -388,7 +388,7 @@ module InnerPrimToken = struct type interpreter = | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr) - | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr) + | BigNumInterp of (?loc:Loc.t -> Z.t -> glob_constr) | StringInterp of (?loc:Loc.t -> string -> glob_constr) let interp_eq f f' = match f,f' with @@ -410,7 +410,7 @@ module InnerPrimToken = struct type uninterpreter = | RawNumUninterp of (any_glob_constr -> rawnum option) - | BigNumUninterp of (any_glob_constr -> Bigint.bigint option) + | BigNumUninterp of (any_glob_constr -> Z.t option) | StringUninterp of (any_glob_constr -> string option) let uninterp_eq f f' = match f,f' with @@ -614,11 +614,10 @@ end (** Conversion from bigint to int63 *) let rec int63_of_pos_bigint i = - let open Bigint in - if equal i zero then Uint63.of_int 0 + if Z.(equal i zero) then Uint63.of_int 0 else - let (quo,rem) = div2_with_rest i in - if rem then Uint63.add (Uint63.of_int 1) + let quo, remi = Z.div_rem i (Z.of_int 2) in + if Z.(equal remi one) then Uint63.add (Uint63.of_int 1) (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)) else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo) @@ -800,24 +799,24 @@ let rawnum_of_coqint c = (** First, [positive] from/to bigint *) let rec pos_of_bigint posty n = - match Bigint.div2_with_rest n with - | (q, false) -> + match Z.div_rem n (Z.of_int 2) with + | (q, rem) when rem = Z.zero -> let c = mkConstruct (posty, 2) in (* xO *) mkApp (c, [| pos_of_bigint posty q |]) - | (q, true) when not (Bigint.equal q Bigint.zero) -> + | (q, _) when not (Z.equal q Z.zero) -> let c = mkConstruct (posty, 1) in (* xI *) mkApp (c, [| pos_of_bigint posty q |]) - | (q, true) -> + | (q, _) -> mkConstruct (posty, 3) (* xH *) let rec bigint_of_pos c = match Constr.kind c with - | Construct ((_, 3), _) -> (* xH *) Bigint.one + | Construct ((_, 3), _) -> (* xH *) Z.one | App (c, [| d |]) -> begin match Constr.kind c with | Construct ((_, n), _) -> begin match n with - | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d)) - | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d) + | 1 -> (* xI *) Z.add Z.one (Z.mul Z.(of_int 2) (bigint_of_pos d)) + | 2 -> (* xO *) Z.mul Z.(of_int 2) (bigint_of_pos d) | n -> assert false (* no other constructor of type positive *) end | x -> raise NotAValidPrimToken @@ -827,24 +826,24 @@ let rec bigint_of_pos c = match Constr.kind c with (** Now, [Z] from/to bigint *) let z_of_bigint { z_ty; pos_ty } n = - if Bigint.equal n Bigint.zero then + if Z.(equal n zero) then mkConstruct (z_ty, 1) (* Z0 *) else let (s, n) = - if Bigint.is_pos_or_zero n then (2, n) (* Zpos *) - else (3, Bigint.neg n) (* Zneg *) + if Z.(leq zero n) then (2, n) (* Zpos *) + else (3, Z.neg n) (* Zneg *) in let c = mkConstruct (z_ty, s) in mkApp (c, [| pos_of_bigint pos_ty n |]) let bigint_of_z z = match Constr.kind z with - | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero + | Construct ((_, 1), _) -> (* Z0 *) Z.zero | App (c, [| d |]) -> begin match Constr.kind c with | Construct ((_, n), _) -> begin match n with | 2 -> (* Zpos *) bigint_of_pos d - | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d) + | 3 -> (* Zneg *) Z.neg (bigint_of_pos d) | n -> assert false (* no other constructor of type Z *) end | _ -> raise NotAValidPrimToken @@ -861,20 +860,19 @@ let error_negative ?loc = CErrors.user_err ?loc ~hdr:"interp_int63" (Pp.str "int63 are only non-negative numbers.") let error_overflow ?loc n = - CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Bigint.to_string n)) + CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n)) let interp_int63 ?loc n = - let open Bigint in - if is_pos_or_zero n + if Z.(leq zero n) then - if less_than n (pow two 63) + if Z.(lt n (pow (of_int 2) 63)) then int63_of_pos_bigint ?loc n else error_overflow ?loc n else error_negative ?loc let bigint_of_int63 c = match Constr.kind c with - | Int i -> Bigint.of_string (Uint63.to_string i) + | Int i -> Z.of_string (Uint63.to_string i) | _ -> raise NotAValidPrimToken let interp o ?loc n = -- cgit v1.2.3 From 3fcd90f590bf0b40e24e20d18f96776232cb014e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 4 Mar 2020 16:37:49 -0500 Subject: [zarith] [notation] Build less intermediate values We could still optimize the functions in that file a bit more if there is need. --- interp/notation.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index c0ebffcdb9..17ae045187 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -612,11 +612,13 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) = end +let z_two = Z.of_int 2 + (** Conversion from bigint to int63 *) let rec int63_of_pos_bigint i = if Z.(equal i zero) then Uint63.of_int 0 else - let quo, remi = Z.div_rem i (Z.of_int 2) in + let quo, remi = Z.div_rem i z_two in if Z.(equal remi one) then Uint63.add (Uint63.of_int 1) (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)) else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo) @@ -799,7 +801,7 @@ let rawnum_of_coqint c = (** First, [positive] from/to bigint *) let rec pos_of_bigint posty n = - match Z.div_rem n (Z.of_int 2) with + match Z.div_rem n z_two with | (q, rem) when rem = Z.zero -> let c = mkConstruct (posty, 2) in (* xO *) mkApp (c, [| pos_of_bigint posty q |]) @@ -815,8 +817,8 @@ let rec bigint_of_pos c = match Constr.kind c with begin match Constr.kind c with | Construct ((_, n), _) -> begin match n with - | 1 -> (* xI *) Z.add Z.one (Z.mul Z.(of_int 2) (bigint_of_pos d)) - | 2 -> (* xO *) Z.mul Z.(of_int 2) (bigint_of_pos d) + | 1 -> (* xI *) Z.add Z.one (Z.mul z_two (bigint_of_pos d)) + | 2 -> (* xO *) Z.mul z_two (bigint_of_pos d) | n -> assert false (* no other constructor of type positive *) end | x -> raise NotAValidPrimToken @@ -865,7 +867,7 @@ let error_overflow ?loc n = let interp_int63 ?loc n = if Z.(leq zero n) then - if Z.(lt n (pow (of_int 2) 63)) + if Z.(lt n (pow z_two 63)) then int63_of_pos_bigint ?loc n else error_overflow ?loc n else error_negative ?loc -- cgit v1.2.3