blob: c11acdc8bdce23a55dd79158f485973d6dd09465 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
type t = {
int : string;
frac : string;
exp : string
}
let equal n1 n2 =
String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
let int s = { int = s; frac = ""; exp = "" }
let to_string n = n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.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
| _ -> len in
fun s ->
let i = get_buff (number 0 s) in
let f =
match Stream.npeek 2 s with
| '.' :: (('0'..'9' | '_') as c) :: _ ->
Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
| _ -> "" in
let e =
match (Stream.npeek 2 s) with
| (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
| (('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 of_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
|
