(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** We keep the string to preserve the user representation,
e.g. "e"/"E" or the presence of leading 0s, or the presence of a +
in the exponent *)
type num_class = CDec | CHex
let string_del_head n s = String.sub s n (String.length s - n)
module UnsignedNat =
struct
type t = string
let of_string s =
assert (String.length s > 0);
assert (s.[0] >= '0' && s.[0] <= '9');
s
let to_string s =
String.(map Char.lowercase_ascii (concat "" (split_on_char '_' s)))
let sprint s = s
let print s = Pp.str (sprint s)
let classify s =
if String.length s >= 2 && (s.[1] = 'x' || s.[1] = 'X') then CHex else CDec
(** Comparing two raw numbers (base 10 or 16, big-endian, non-negative).
A bit nasty, but not critical: used e.g. to decide when a number
is considered as large (see threshold warnings in notation.ml). *)
exception Comp of int
let rec compare s s' =
let l = String.length s and l' = String.length s' in
if l < l' then - compare s' s
else
let d = l-l' in
try
for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
for i = d to l-1 do
let c = Util.pervasives_compare s.[i] s'.[i-d] in
if c != 0 then raise (Comp c)
done;
0
with Comp c -> c
let compare n d =
assert (classify d = CDec);
match classify n with
| CDec -> compare (to_string n) (to_string d)
| CHex -> compare (string_del_head 2 (to_string n)) (to_string d)
let is_zero s =
compare s "0" = 0
end
type sign = SPlus | SMinus
type 'a exp = EDec of 'a | EBin of 'a
module SignedNat =
struct
type t = sign * UnsignedNat.t
let of_string s =
assert (String.length s > 0);
let sign,n =
match s.[0] with
| '-' -> (SMinus,string_del_head 1 s)
| '+' -> (SPlus,string_del_head 1 s)
| _ -> (SPlus,s) in
(sign,UnsignedNat.of_string n)
let to_string (sign,n) =
(match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
let classify (_,n) = UnsignedNat.classify n
let bigint_of_string (sign,n) = Z.of_string (to_string (sign,n))
let to_bigint n = bigint_of_string n
let string_of_nonneg_bigint c n =
match c with
| CDec -> Z.format "%d" n
| CHex -> Z.format "%#x" n
let of_bigint c n =
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
module Unsigned =
struct
type t = {
int : string;
frac : string;
exp : string
}
(**
- int: \[0-9\]\[0-9_\]*
- frac: empty or \[0-9_\]+
- exp: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]*
or
- int: 0\[xX\]\[0-9a-fA-F\]\[0-9a-fA-F_\]*
- frac: empty or \[0-9a-fA-F_\]+
- exp: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *)
let equal n1 n2 =
String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
let parse =
let buff = ref (Bytes.create 80) in
let store len x =
let open Bytes in
if len >= length !buff then
buff := cat !buff (create (length !buff));
set !buff len x;
succ len in
let get_buff len = Bytes.sub_string !buff 0 len in
(* reads [0-9_]* *)
let rec number len s = match Stream.peek s with
| Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
| Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s
| _ -> len in
(* reads [0-9a-fA-F_]* *)
let rec hex_number len s = match Stream.peek s with
| Some (('0'..'9' | 'a'..'f' | 'A'..'F') as c) ->
Stream.junk s; hex_number (store len c) s
| Some ('_' as c) when len > 0 ->
Stream.junk s; hex_number (store len c) s
| _ -> len in
fun s ->
let hex, i =
match Stream.npeek 3 s with
| '0' :: (('x' | 'X') as x) :: (('0'..'9' | 'a'..'f' | 'A'..'F') as c) :: _ ->
Stream.junk s; Stream.junk s; Stream.junk s;
true, get_buff (hex_number (store (store (store 0 '0') x) c) s)
| _ -> false, get_buff (number 0 s) in
assert (i <> "");
let f =
match hex, Stream.npeek 2 s with
| true, '.' :: (('0'..'9' | 'a'..'f' | 'A'..'F' | '_') as c) :: _ ->
Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s)
| false, '.' :: (('0'..'9' | '_') as c) :: _ ->
Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
| _ -> "" in
let e =
match hex, Stream.npeek 2 s with
| true, (('p'|'P') as e) :: ('0'..'9' as c) :: _
| false, (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
| true, (('p'|'P') as e) :: (('+'|'-') as sign) :: _
| false, (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
begin match Stream.npeek 3 s with
| _ :: _ :: ('0'..'9' as c) :: _ ->
Stream.junk s; Stream.junk s; Stream.junk s;
get_buff (number (store (store (store 0 e) sign) c) s)
| _ -> ""
end
| _ -> "" in
{ int = i; frac = f; exp = e }
let sprint n =
n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp
let print n =
Pp.str (sprint n)
let parse_string s =
if s = "" || s.[0] < '0' || s.[0] > '9' then None else
let strm = Stream.of_string (s ^ " ") in
let n = parse strm in
if Stream.count strm >= String.length s then Some n else None
let of_string s =
match parse_string s with
| None -> assert false
| Some s -> s
let to_string =
sprint (* We could remove the '_' but not necessary for float_of_string *)
let to_nat = function
| { int = i; frac = ""; exp = "" } -> Some i
| _ -> None
let is_nat = function
| { int = _; frac = ""; exp = "" } -> true
| _ -> false
let classify n = UnsignedNat.classify n.int
end
open Unsigned
module Signed =
struct
type t = sign * Unsigned.t
let equal (s1,n1) (s2,n2) =
s1 = s2 && equal n1 n2
let is_zero = function
| (SPlus,{int;frac;exp}) -> UnsignedNat.is_zero int && UnsignedNat.is_zero frac
| _ -> false
let of_int_frac_and_exponent (sign,int) f e =
assert (match e with None -> true | Some e -> SignedNat.classify e = CDec);
let c = UnsignedNat.classify int in
let exp = match e with None -> "" | Some e ->
let e = SignedNat.to_string e in
match c with CDec -> "e" ^ e | CHex -> "p" ^ e in
let frac = match f with None -> "" | Some f ->
assert (c = UnsignedNat.classify f);
let f = UnsignedNat.to_string f in
match c with CDec -> f | CHex -> string_del_head 2 f in
sign, { int; frac; exp }
let to_int_frac_and_exponent (sign, { int; frac; exp }) =
let e =
if exp = "" then None else
Some (match exp.[1] with
| '-' -> SMinus, string_del_head 2 exp
| '+' -> SPlus, string_del_head 2 exp
| _ -> SPlus, string_del_head 1 exp) in
let f =
if frac = "" then None else
Some (match UnsignedNat.classify int with
| CDec -> frac
| CHex -> "0x" ^ frac) in
(sign, int), f, e
let of_nat i =
(SPlus,{ int = i; frac = ""; exp = "" })
let of_int (s,i) =
(s,{ int = i; frac = ""; exp = "" })
let of_int_string s = of_int (SignedNat.of_string s)
let to_int = function
| (s, { int = i; frac = ""; exp = "" }) -> Some (s,i)
| _ -> None
let is_int n = match to_int n with None -> false | Some _ -> true
let sprint (s,i) =
(match s with SPlus -> "" | SMinus -> "-") ^ Unsigned.sprint i
let print i =
Pp.str (sprint i)
let parse_string s =
if s = "" || s = "-" || s = "+" ||
(s.[0] < '0' || s.[0] > '9') && ((s.[0] <> '-' && s.[0] <> '+') || s.[1] < '0' || s.[1] > '9') then None else
let strm = Stream.of_string (s ^ " ") in
let sign = match s.[0] with
| '-' -> (Stream.junk strm; SMinus)
| '+' -> (Stream.junk strm; SPlus)
| _ -> SPlus in
let n = parse strm in
if Stream.count strm >= String.length s then Some (sign,n) else None
let of_string s =
assert (s <> "");
let sign,u = match s.[0] with
| '-' -> (SMinus, string_del_head 1 s)
| '+' -> (SPlus, string_del_head 1 s)
| _ -> (SPlus, s) in
(sign, Unsigned.of_string u)
let to_string (sign,u) =
(match sign with SPlus -> "" | SMinus -> "-") ^ Unsigned.to_string u
let to_bigint = function
| (sign, { int = n; frac = ""; exp = "" }) ->
Some (SignedNat.to_bigint (sign,UnsignedNat.to_string n))
| _ -> None
let of_bigint c n =
of_int (SignedNat.of_bigint c n)
let to_bigint_and_exponent (s, { int; frac; exp }) =
let c = UnsignedNat.classify int in
let int = UnsignedNat.to_string int in
let frac = UnsignedNat.to_string frac in
let i = SignedNat.to_bigint (s, int ^ frac) in
let e =
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
Z.(sub e (of_int l)) in
(i, match c with CDec -> EDec e | CHex -> EBin e)
let of_bigint_and_exponent i e =
let c = match e with EDec _ -> CDec | EBin _ -> CHex in
let e = match e with EDec e | EBin e -> Some (SignedNat.of_bigint CDec e) in
of_int_frac_and_exponent (SignedNat.of_bigint c i) None e
let is_bigger_int_than (s, { int; frac; exp }) i =
frac = "" && exp = "" && UnsignedNat.compare int i >= 0
let classify (_, n) = Unsigned.classify n
end