aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/dune2
-rw-r--r--interp/notation.ml44
-rw-r--r--interp/notation.mli8
-rw-r--r--interp/numTok.ml41
-rw-r--r--interp/numTok.mli12
5 files changed, 56 insertions, 51 deletions
diff --git a/interp/dune b/interp/dune
index e9ef7ba99a..6d73d5724c 100644
--- a/interp/dune
+++ b/interp/dune
@@ -3,4 +3,4 @@
(synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
(public_name coq.interp)
(wrapped false)
- (libraries pretyping))
+ (libraries zarith pretyping))
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 =
diff --git a/interp/notation.mli b/interp/notation.mli
index 05ddd25a62..948831b317 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -101,7 +101,7 @@ val register_rawnumeral_interpretation :
?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
val register_bignumeral_interpretation :
- ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+ ?allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit
val register_string_interpretation :
?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
@@ -196,8 +196,8 @@ val enable_prim_token_interpretation : prim_token_infos -> unit
*)
val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module ->
- Bigint.bigint prim_token_interpreter ->
- glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit
+ Z.t prim_token_interpreter ->
+ glob_constr list * Z.t prim_token_uninterpreter * bool -> unit
val declare_string_interpreter : ?local:bool -> scope_name -> required_module ->
string prim_token_interpreter ->
glob_constr list * string prim_token_uninterpreter * bool -> unit
@@ -349,4 +349,4 @@ val level_of_notation : notation -> level
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
(** Conversion from bigint to int63 *)
-val int63_of_pos_bigint : Bigint.bigint -> Uint63.t
+val int63_of_pos_bigint : Z.t -> Uint63.t
diff --git a/interp/numTok.ml b/interp/numTok.ml
index bb14649b91..e90e4d25d3 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -62,6 +62,13 @@ struct
compare s "0" = 0
end
+(* Helper function *)
+let div2_with_rest =
+ let two = Z.of_int 2 in
+ fun n ->
+ let res, rem = Z.div_rem n two in
+ res, Z.equal rem Z.one
+
type sign = SPlus | SMinus
type 'a exp = EDec of 'a | EBin of 'a
@@ -84,31 +91,31 @@ struct
(* nasty code to remove when switching to zarith
since zarith's of_string handles hexadecimal *)
match UnsignedNat.classify n with
- | CDec -> Bigint.of_string (to_string (sign,n))
+ | CDec -> Z.of_string (to_string (sign,n))
| CHex ->
let int_of_char c = match c with
| 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
| _ -> int_of_char c - int_of_char '0' in
- let c16 = Bigint.of_int 16 in
+ let c16 = Z.of_int 16 in
let s = UnsignedNat.to_string n in
- let n = ref Bigint.zero in
+ let n = ref Z.zero in
let len = String.length s in
for d = 2 to len - 1 do
- n := Bigint.(add (mult !n c16) (of_int (int_of_char s.[d])))
+ n := Z.(add (mul !n c16) (of_int (int_of_char s.[d])))
done;
- match sign with SPlus -> !n | SMinus -> Bigint.neg !n
+ match sign with SPlus -> !n | SMinus -> Z.neg !n
let to_bigint n = bigint_of_string n
let string_of_nonneg_bigint c n =
(* nasty code to remove when switching to zarith
since zarith's format handles hexadecimal *)
match c with
- | CDec -> Bigint.to_string n
+ | CDec -> Z.to_string n
| CHex ->
let div16 n =
- let n, r0 = Bigint.div2_with_rest n in
- let n, r1 = Bigint.div2_with_rest n in
- let n, r2 = Bigint.div2_with_rest n in
- let n, r3 = Bigint.div2_with_rest n in
+ let n, r0 = div2_with_rest n in
+ let n, r1 = div2_with_rest n in
+ let n, r2 = div2_with_rest n in
+ let n, r3 = div2_with_rest n in
let r = match r3, r2, r1, r0 with
| false, false, false, false -> "0"
| false, false, false, true -> "1"
@@ -129,14 +136,14 @@ struct
n, r in
let n = ref n in
let l = ref [] in
- while Bigint.is_strictly_pos !n do
+ while Int.equal 1 (Z.sign !n) do
let n', r = div16 !n in
n := n';
l := r :: !l
done;
"0x" ^ String.concat "" (List.rev !l)
let of_bigint c n =
- let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in
+ let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in
(sign, string_of_nonneg_bigint c n)
end
@@ -339,13 +346,13 @@ struct
let frac = UnsignedNat.to_string frac in
let i = SignedNat.to_bigint (s, int ^ frac) in
let e =
- let e = if exp = "" then Bigint.zero else match exp.[1] with
- | '+' -> Bigint.of_string (UnsignedNat.to_string (string_del_head 2 exp))
- | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
- | _ -> Bigint.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
+ let e = if exp = "" then Z.zero else match exp.[1] with
+ | '+' -> Z.of_string (UnsignedNat.to_string (string_del_head 2 exp))
+ | '-' -> Z.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
+ | _ -> Z.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
let l = String.length frac in
let l = match c with CDec -> l | CHex -> 4 * l in
- Bigint.(sub e (of_int l)) in
+ Z.(sub e (of_int l)) in
(i, match c with CDec -> EDec e | CHex -> EBin e)
let of_bigint_and_exponent i e =
diff --git a/interp/numTok.mli b/interp/numTok.mli
index 11d5a0f980..bcfe663dd2 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -65,8 +65,8 @@ sig
val classify : t -> num_class
- val of_bigint : num_class -> Bigint.bigint -> t
- val to_bigint : t -> Bigint.bigint
+ val of_bigint : num_class -> Z.t -> t
+ val to_bigint : t -> Z.t
end
(** {6 Unsigned decimal numerals } *)
@@ -131,8 +131,8 @@ sig
val to_string : t -> string
(** Returns a string in the syntax of OCaml's float_of_string *)
- val of_bigint : num_class -> Bigint.bigint -> t
- val to_bigint : t -> Bigint.bigint option
+ val of_bigint : num_class -> Z.t -> t
+ val to_bigint : t -> Z.t option
(** Convert from and to bigint when the denotation of a bigint *)
val of_int_frac_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
@@ -140,8 +140,8 @@ sig
(** n, p and q such that the number is n.p*10^q or n.p*2^q
pre/postcondition: classify n = classify p, classify q = CDec *)
- val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint exp -> t
- val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint exp
+ val of_bigint_and_exponent : Z.t -> Z.t exp -> t
+ val to_bigint_and_exponent : t -> Z.t * Z.t exp
(** n and p such that the number is n*10^p or n*2^p *)
val classify : t -> num_class
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:05:01 +0000