diff options
| author | Pierre-Marie Pédrot | 2020-12-11 13:18:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-11 13:18:45 +0100 |
| commit | 6ce1c1d1b661a6cbb4a415f9f7960b2ff53b32c5 (patch) | |
| tree | 5049e6475c9b554146264e64b6d8efb7d01b8ace /interp/notation.ml | |
| parent | d40ef2467b8e84115b027200aff61becdd899f57 (diff) | |
| parent | f4dcd1d9f696972e7cbdaa8d70e5abb1a18820ef (diff) | |
Merge PR #13540: Clean support of primitive integers
Reviewed-by: ppedrot
Reviewed-by: proux01
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index c35ba44aa5..912e52cec8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -782,13 +782,7 @@ 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_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) +let int63_of_pos_bigint i = Uint63.of_int64 (Z.to_int64 i) module Numbers = struct (** * Number notation *) @@ -1041,7 +1035,7 @@ let interp_int63 ?loc n = let bigint_of_int63 c = match Constr.kind c with - | Int i -> Z.of_string (Uint63.to_string i) + | Int i -> Z.of_int64 (Uint63.to_int64 i) | _ -> raise NotAValidPrimToken let interp o ?loc n = |