Merge pull request #3053 from mtzguido/int_of_string

Introducing int_of_string / bool_of_string

ocaml/fstar-lib/FStar_Compiler_Util.ml

@@ -612,7 +612,9 @@ let base64_encode s = BatBase64.str_encode s
 let base64_decode s = BatBase64.str_decode s
 let char_of_int i = Z.to_int i
 let int_of_string = Z.of_string
-let safe_int_of_string x = try Some (int_of_string x) with Invalid_argument _ -> None
+let safe_int_of_string x =
+  if x = "" then None else
+  try Some (int_of_string x) with Invalid_argument _ -> None
 let int_of_char x = Z.of_int x
 let int_of_byte x = x
 let int_of_uint8 x = Z.of_int (Char.code x)

src/parser/FStar.Parser.Const.fst

@@ -161,6 +161,8 @@ let prims_op_Hat_lid = pconst "op_Hat"
 let let_in_typ      = p2l ["Prims"; "Let"]
 let string_of_int_lid = p2l ["Prims"; "string_of_int"]
 let string_of_bool_lid = p2l ["Prims"; "string_of_bool"]
+let int_of_string_lid = p2l ["FStar"; "Parse"; "int_of_string"]
+let bool_of_string_lid = p2l ["FStar"; "Parse"; "bool_of_string"]
 let string_compare = p2l ["FStar"; "String"; "compare"]
 let order_lid       = p2l ["FStar"; "Order"; "order"]
 let vconfig_lid     = p2l ["FStar"; "VConfig"; "vconfig"]

src/typechecker/FStar.TypeChecker.Cfg.fst

@@ -448,6 +448,19 @@ let built_in_primitive_steps : prim_step_set =
     let string_of_bool rng (b:bool) : term =
         embed_simple EMB.e_string rng (if b then "true" else "false")
     in
+    let int_of_string rng (s:string) : term =
+      let r = safe_int_of_string s in
+      embed_simple EMB.(e_option e_fsint) rng r
+    in
+    let bool_of_string rng (s:string) : term =
+      let r =
+        match s with
+        | "true" -> Some true
+        | "false" -> Some false
+        | _ -> None
+      in
+      embed_simple EMB.(e_option e_bool) rng r
+    in
     let lowercase rng (s:string) : term =
         embed_simple EMB.e_string rng (String.lowercase s)
     in
@@ -673,6 +686,17 @@ let built_in_primitive_steps : prim_step_set =
              0,
              unary_op arg_as_bool string_of_bool,
              NBETerm.unary_op NBETerm.arg_as_bool NBETerm.string_of_bool);
+
+         (PC.bool_of_string_lid,
+             1,
+             0,
+             unary_op arg_as_string bool_of_string,
+             NBETerm.unary_op NBETerm.arg_as_string NBETerm.bool_of_string);
+         (PC.int_of_string_lid,
+             1,
+             0,
+             unary_op arg_as_string int_of_string,
+             NBETerm.unary_op NBETerm.arg_as_string NBETerm.int_of_string);
 (* Operations from FStar.String *)
          (PC.string_list_of_string_lid,
              1,

src/typechecker/FStar.TypeChecker.NBETerm.fst

@@ -351,6 +351,8 @@ let e_int : embedding Z.t =
     in
     mk_emb' em un (lid_as_typ PC.int_lid [] [])  (SE.emb_typ_of SE.e_int)
 
+let e_fsint = embed_as e_int Z.to_int_fs Z.of_int_fs None
+
 // Embedding at option type
 let e_option (ea : embedding 'a) =
     let etyp =
@@ -798,6 +800,17 @@ let string_of_int (i:Z.t) : t =
 let string_of_bool (b:bool) : t =
     embed e_string bogus_cbs (if b then "true" else "false")
 
+let int_of_string (s:string) : t =
+    embed (e_option e_fsint) bogus_cbs (BU.safe_int_of_string s)
+
+let bool_of_string (s:string) : t =
+    let r = match s with
+            | "true" -> Some true
+            | "false" -> Some false
+            | _ -> None
+    in
+    embed (e_option e_bool) bogus_cbs r
+
 let string_lowercase (s:string) : t =
     embed e_string bogus_cbs (String.lowercase s)
 

src/typechecker/FStar.TypeChecker.NBETerm.fsti

@@ -331,6 +331,8 @@ val binary_string_op : (string -> string -> string) -> (universes -> args -> opt
 
 val string_of_int : Z.t -> t
 val string_of_bool : bool -> t
+val int_of_string : string -> t
+val bool_of_string : string -> t
 val string_of_list' : list char -> t
 val string_compare' : string -> string -> t
 val string_concat' : args -> option t

tests/micro-benchmarks/Test.FStar.Parse.fst

@@ -0,0 +1,15 @@
+module Test.FStar.Parse
+
+open FStar.Parse
+
+let _ = assert (int_of_string "" == None)
+let _ = assert (int_of_string "1" == Some 1)
+let _ = assert (int_of_string "-1" == Some (-1))
+let _ = assert (int_of_string "1234567890" == Some 1234567890)
+
+let _ = assert (int_of_string "15x1" == None)
+let _ = assert (int_of_string "x1" == None)
+
+// Hex and binary also work.
+let _ = assert (int_of_string "0x100" == Some 256)
+let _ = assert (int_of_string "0b100" == Some 4)

ulib/FStar.Parse.fst

@@ -0,0 +1,24 @@
+(*
+   Copyright 2008-2020 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module FStar.Parse
+
+(** A primitive parser for booleans *)
+assume
+val bool_of_string: string -> Tot (option bool)
+
+(** A primitive parser for [int] *)
+assume
+val int_of_string: string -> Tot (option int)