more accurate parse_nat/parse_int: avoid corner cases of Int.fromString (e.g. "1.0");
authorwenzelm
Sat Dec 16 20:02:40 2017 +0100 (17 months ago)
changeset 67218e62d72699666
parent 67217 53867014e299
child 67219 81e9804b2014
more accurate parse_nat/parse_int: avoid corner cases of Int.fromString (e.g. "1.0");
src/Pure/General/value.ML
     1.1 --- a/src/Pure/General/value.ML	Sat Dec 16 17:23:00 2017 +0100
     1.2 +++ b/src/Pure/General/value.ML	Sat Dec 16 20:02:40 2017 +0100
     1.3 @@ -31,19 +31,21 @@
     1.4  
     1.5  (* nat and int *)
     1.6  
     1.7 +val zero = ord "0";
     1.8 +val nine = ord "9";
     1.9 +
    1.10  fun parse_nat s =
    1.11 -  let val i = Int.fromString s in
    1.12 -    if is_none i orelse the i < 0
    1.13 -    then raise Fail ("Bad natural number " ^ quote s)
    1.14 -    else the i
    1.15 -  end;
    1.16 +  fold_string (fn c => fn n =>
    1.17 +    let val i = ord c in
    1.18 +      if zero <= i andalso i <= nine then 10 * n + (i - zero)
    1.19 +      else raise Fail ("Bad natural number " ^ quote s)
    1.20 +    end) s 0;
    1.21  
    1.22  fun parse_int s =
    1.23 -  let val i = Int.fromString s in
    1.24 -    if is_none i orelse String.isPrefix "~" s
    1.25 -    then raise Fail ("Bad integer " ^ quote s)
    1.26 -    else the i
    1.27 -  end;
    1.28 +  (case try (unprefix "-") s of
    1.29 +    NONE => parse_nat s
    1.30 +  | SOME s' => ~ (parse_nat s'))
    1.31 +  handle Fail _ => raise Fail ("Bad integer " ^ quote s);
    1.32  
    1.33  val print_int = signed_string_of_int;
    1.34