From b55d5d3534ae99b8ff7b655003a941dce9e49799 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 19 Sep 2023 15:05:33 -0700 Subject: [PATCH 1/4] Introduce FStar.Parse: with int_of_string and bool_of_string --- src/parser/FStar.Parser.Const.fst | 2 ++ src/typechecker/FStar.TypeChecker.Cfg.fst | 24 +++++++++++++++++++ src/typechecker/FStar.TypeChecker.NBETerm.fst | 13 ++++++++++ .../FStar.TypeChecker.NBETerm.fsti | 2 ++ ulib/FStar.Parse.fst | 24 +++++++++++++++++++ 5 files changed, 65 insertions(+) create mode 100644 ulib/FStar.Parse.fst diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index f8f45e8e1ce..63488d3dd2c 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/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"] diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst index 19f6fe59061..dcb66eb7dd6 100644 --- a/src/typechecker/FStar.TypeChecker.Cfg.fst +++ b/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, diff --git a/src/typechecker/FStar.TypeChecker.NBETerm.fst b/src/typechecker/FStar.TypeChecker.NBETerm.fst index 79f09fd85a9..1fcc4b96a04 100644 --- a/src/typechecker/FStar.TypeChecker.NBETerm.fst +++ b/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) diff --git a/src/typechecker/FStar.TypeChecker.NBETerm.fsti b/src/typechecker/FStar.TypeChecker.NBETerm.fsti index 44baf2ce0f4..2bb5b9d6e3e 100644 --- a/src/typechecker/FStar.TypeChecker.NBETerm.fsti +++ b/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 diff --git a/ulib/FStar.Parse.fst b/ulib/FStar.Parse.fst new file mode 100644 index 00000000000..b3835bc746c --- /dev/null +++ b/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) From d041fb3dd1a664f2bf9709585751411315115f38 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 19 Sep 2023 15:14:45 -0700 Subject: [PATCH 2/4] Add a test --- tests/micro-benchmarks/Test.FStar.Parse.fst | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 tests/micro-benchmarks/Test.FStar.Parse.fst diff --git a/tests/micro-benchmarks/Test.FStar.Parse.fst b/tests/micro-benchmarks/Test.FStar.Parse.fst new file mode 100644 index 00000000000..04b1ece18b3 --- /dev/null +++ b/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) From 994d914921f66fb4b1df9b12d5ec91baf0da4f29 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 19 Sep 2023 15:14:58 -0700 Subject: [PATCH 3/4] Compiler.Util: do not interpret "" as zero --- ocaml/fstar-lib/FStar_Compiler_Util.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/ocaml/fstar-lib/FStar_Compiler_Util.ml b/ocaml/fstar-lib/FStar_Compiler_Util.ml index a8ba578b631..d423983e43c 100644 --- a/ocaml/fstar-lib/FStar_Compiler_Util.ml +++ b/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) From 0c779031e3254cbbfd1a64332802d15e47974f87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 19 Sep 2023 09:40:42 -0700 Subject: [PATCH 4/4] snap --- ocaml/fstar-lib/generated/FStar_Parse.ml | 7 + .../fstar-lib/generated/FStar_Parser_Const.ml | 4 + .../generated/FStar_TypeChecker_Cfg.ml | 350 ++++++++++-------- .../generated/FStar_TypeChecker_NBETerm.ml | 16 + 4 files changed, 226 insertions(+), 151 deletions(-) create mode 100644 ocaml/fstar-lib/generated/FStar_Parse.ml diff --git a/ocaml/fstar-lib/generated/FStar_Parse.ml b/ocaml/fstar-lib/generated/FStar_Parse.ml new file mode 100644 index 00000000000..b535928f437 --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_Parse.ml @@ -0,0 +1,7 @@ +open Prims +let (bool_of_string : + Prims.string -> Prims.bool FStar_Pervasives_Native.option) = + fun uu___ -> failwith "Not yet implemented:bool_of_string" +let (int_of_string : + Prims.string -> Prims.int FStar_Pervasives_Native.option) = + fun uu___ -> failwith "Not yet implemented:int_of_string" \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index 21261f83e99..96879194b4d 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -126,6 +126,10 @@ let (let_in_typ : FStar_Ident.lident) = p2l ["Prims"; "Let"] let (string_of_int_lid : FStar_Ident.lident) = p2l ["Prims"; "string_of_int"] let (string_of_bool_lid : FStar_Ident.lident) = p2l ["Prims"; "string_of_bool"] +let (int_of_string_lid : FStar_Ident.lident) = + p2l ["FStar"; "Parse"; "int_of_string"] +let (bool_of_string_lid : FStar_Ident.lident) = + p2l ["FStar"; "Parse"; "bool_of_string"] let (string_compare : FStar_Ident.lident) = p2l ["FStar"; "String"; "compare"] let (order_lid : FStar_Ident.lident) = p2l ["FStar"; "Order"; "order"] diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml index 25e224bfda2..1de46a578ea 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml @@ -2264,6 +2264,20 @@ let (built_in_primitive_steps : primitive_step FStar_Compiler_Util.psmap) = let string_of_bool rng b = embed_simple FStar_Syntax_Embeddings.e_string rng (if b then "true" else "false") in + let int_of_string rng s = + let r = FStar_Compiler_Util.safe_int_of_string s in + let uu___ = + FStar_Syntax_Embeddings.e_option FStar_Syntax_Embeddings.e_fsint in + embed_simple uu___ rng r in + let bool_of_string rng s = + let r = + match s with + | "true" -> FStar_Pervasives_Native.Some true + | "false" -> FStar_Pervasives_Native.Some false + | uu___ -> FStar_Pervasives_Native.None in + let uu___ = + FStar_Syntax_Embeddings.e_option FStar_Syntax_Embeddings.e_bool in + embed_simple uu___ rng r in let lowercase rng s = embed_simple FStar_Syntax_Embeddings.e_string rng (FStar_String.lowercase s) in @@ -2640,199 +2654,233 @@ let (built_in_primitive_steps : primitive_step FStar_Compiler_Util.psmap) = let uu___31 = FStar_TypeChecker_NBETerm.unary_op FStar_TypeChecker_NBETerm.arg_as_string - FStar_TypeChecker_NBETerm.list_of_string' in - (FStar_Parser_Const.string_list_of_string_lid, + FStar_TypeChecker_NBETerm.bool_of_string in + (FStar_Parser_Const.bool_of_string_lid, Prims.int_one, Prims.int_zero, (unary_op arg_as_string - list_of_string'), uu___31) in + bool_of_string), uu___31) in let uu___31 = let uu___32 = let uu___33 = FStar_TypeChecker_NBETerm.unary_op - (FStar_TypeChecker_NBETerm.arg_as_list - FStar_TypeChecker_NBETerm.e_char) - FStar_TypeChecker_NBETerm.string_of_list' in - (FStar_Parser_Const.string_string_of_list_lid, + FStar_TypeChecker_NBETerm.arg_as_string + FStar_TypeChecker_NBETerm.int_of_string in + (FStar_Parser_Const.int_of_string_lid, Prims.int_one, Prims.int_zero, - (unary_op - (arg_as_list - FStar_Syntax_Embeddings.e_char) - string_of_list'), uu___33) in + (unary_op arg_as_string + int_of_string), uu___33) in let uu___33 = let uu___34 = let uu___35 = - let uu___36 = - let uu___37 = - FStar_TypeChecker_NBETerm.binary_string_op - (fun x -> - fun y -> - FStar_String.op_Hat x - y) in - (FStar_Parser_Const.prims_strcat_lid, - (Prims.of_int (2)), - Prims.int_zero, - (binary_string_op - (fun x -> - fun y -> - FStar_String.op_Hat x - y)), uu___37) in + FStar_TypeChecker_NBETerm.unary_op + FStar_TypeChecker_NBETerm.arg_as_string + FStar_TypeChecker_NBETerm.list_of_string' in + (FStar_Parser_Const.string_list_of_string_lid, + Prims.int_one, Prims.int_zero, + (unary_op arg_as_string + list_of_string'), uu___35) in + let uu___35 = + let uu___36 = let uu___37 = - let uu___38 = - let uu___39 = - let uu___40 = - FStar_TypeChecker_NBETerm.binary_op - FStar_TypeChecker_NBETerm.arg_as_string - FStar_TypeChecker_NBETerm.string_compare' in - (FStar_Parser_Const.string_compare_lid, - (Prims.of_int (2)), - Prims.int_zero, - (binary_op arg_as_string - string_compare'), - uu___40) in + FStar_TypeChecker_NBETerm.unary_op + (FStar_TypeChecker_NBETerm.arg_as_list + FStar_TypeChecker_NBETerm.e_char) + FStar_TypeChecker_NBETerm.string_of_list' in + (FStar_Parser_Const.string_string_of_list_lid, + Prims.int_one, Prims.int_zero, + (unary_op + (arg_as_list + FStar_Syntax_Embeddings.e_char) + string_of_list'), uu___37) in + let uu___37 = + let uu___38 = + let uu___39 = let uu___40 = let uu___41 = - let uu___42 = - FStar_TypeChecker_NBETerm.unary_op - FStar_TypeChecker_NBETerm.arg_as_string - FStar_TypeChecker_NBETerm.string_lowercase in - (FStar_Parser_Const.string_lowercase_lid, - Prims.int_one, - Prims.int_zero, - (unary_op arg_as_string - lowercase), uu___42) in + FStar_TypeChecker_NBETerm.binary_string_op + (fun x -> + fun y -> + FStar_String.op_Hat + x y) in + (FStar_Parser_Const.prims_strcat_lid, + (Prims.of_int (2)), + Prims.int_zero, + (binary_string_op + (fun x -> + fun y -> + FStar_String.op_Hat + x y)), uu___41) in + let uu___41 = let uu___42 = let uu___43 = let uu___44 = - FStar_TypeChecker_NBETerm.unary_op + FStar_TypeChecker_NBETerm.binary_op FStar_TypeChecker_NBETerm.arg_as_string - FStar_TypeChecker_NBETerm.string_uppercase in - (FStar_Parser_Const.string_uppercase_lid, - Prims.int_one, + FStar_TypeChecker_NBETerm.string_compare' in + (FStar_Parser_Const.string_compare_lid, + (Prims.of_int (2)), Prims.int_zero, - (unary_op + (binary_op arg_as_string - uppercase), + string_compare'), uu___44) in let uu___44 = let uu___45 = let uu___46 = - let uu___47 = - let uu___48 = - let uu___49 = - let uu___50 = - let uu___51 + FStar_TypeChecker_NBETerm.unary_op + FStar_TypeChecker_NBETerm.arg_as_string + FStar_TypeChecker_NBETerm.string_lowercase in + (FStar_Parser_Const.string_lowercase_lid, + Prims.int_one, + Prims.int_zero, + (unary_op + arg_as_string + lowercase), + uu___46) in + let uu___46 = + let uu___47 = + let uu___48 = + FStar_TypeChecker_NBETerm.unary_op + FStar_TypeChecker_NBETerm.arg_as_string + FStar_TypeChecker_NBETerm.string_uppercase in + (FStar_Parser_Const.string_uppercase_lid, + Prims.int_one, + Prims.int_zero, + (unary_op + arg_as_string + uppercase), + uu___48) in + let uu___48 = + let uu___49 = + let uu___50 = + let uu___51 = + let uu___52 = + let uu___53 + = + let uu___54 + = + let uu___55 = FStar_Parser_Const.p2l ["FStar"; "Range"; "mk_range"] in - (uu___51, + (uu___55, (Prims.of_int (5)), Prims.int_zero, mk_range, + (fun + uu___56 + -> + FStar_TypeChecker_NBETerm.mk_range)) in + [uu___54] in + (FStar_Parser_Const.op_notEq, + (Prims.of_int (3)), + Prims.int_zero, + ( + decidable_eq + true), ( fun - uu___52 + uu___54 -> - FStar_TypeChecker_NBETerm.mk_range)) in - [uu___50] in - (FStar_Parser_Const.op_notEq, + FStar_TypeChecker_NBETerm.decidable_eq + true)) :: + uu___53 in + (FStar_Parser_Const.op_Eq, + (Prims.of_int (3)), + Prims.int_zero, + (decidable_eq + false), + (fun + uu___53 + -> + FStar_TypeChecker_NBETerm.decidable_eq + false)) + :: uu___52 in + (FStar_Parser_Const.string_sub_lid, (Prims.of_int (3)), Prims.int_zero, - (decidable_eq - true), - (fun uu___50 + string_substring', + (fun uu___52 -> - FStar_TypeChecker_NBETerm.decidable_eq - true)) - :: uu___49 in - (FStar_Parser_Const.op_Eq, - (Prims.of_int (3)), + FStar_TypeChecker_NBETerm.string_substring')) + :: uu___51 in + (FStar_Parser_Const.string_index_of_lid, + (Prims.of_int (2)), Prims.int_zero, - (decidable_eq - false), - (fun uu___49 -> - FStar_TypeChecker_NBETerm.decidable_eq - false)) - :: uu___48 in - (FStar_Parser_Const.string_sub_lid, - (Prims.of_int (3)), + string_index_of, + (fun uu___51 -> + FStar_TypeChecker_NBETerm.string_index_of)) + :: uu___50 in + (FStar_Parser_Const.string_index_lid, + (Prims.of_int (2)), Prims.int_zero, - string_substring', - (fun uu___48 -> - FStar_TypeChecker_NBETerm.string_substring')) - :: uu___47 in - (FStar_Parser_Const.string_index_of_lid, - (Prims.of_int (2)), - Prims.int_zero, - string_index_of, - (fun uu___47 -> - FStar_TypeChecker_NBETerm.string_index_of)) - :: uu___46 in - (FStar_Parser_Const.string_index_lid, - (Prims.of_int (2)), - Prims.int_zero, - string_index, - (fun uu___46 -> - FStar_TypeChecker_NBETerm.string_index)) - :: uu___45 in + string_index, + (fun uu___50 -> + FStar_TypeChecker_NBETerm.string_index)) + :: uu___49 in + uu___47 :: uu___48 in + uu___45 :: uu___46 in uu___43 :: uu___44 in - uu___41 :: uu___42 in - uu___39 :: uu___40 in - (FStar_Parser_Const.string_concat_lid, + (FStar_Parser_Const.string_concat_lid, + (Prims.of_int (2)), + Prims.int_zero, + string_concat', + (fun uu___43 -> + FStar_TypeChecker_NBETerm.string_concat')) + :: uu___42 in + uu___40 :: uu___41 in + (FStar_Parser_Const.string_split_lid, (Prims.of_int (2)), Prims.int_zero, - string_concat', - (fun uu___39 -> - FStar_TypeChecker_NBETerm.string_concat')) - :: uu___38 in - uu___36 :: uu___37 in - (FStar_Parser_Const.string_split_lid, - (Prims.of_int (2)), - Prims.int_zero, string_split', - (fun uu___36 -> - FStar_TypeChecker_NBETerm.string_split')) - :: uu___35 in - (FStar_Parser_Const.string_make_lid, - (Prims.of_int (2)), Prims.int_zero, - (mixed_binary_op - (fun x -> arg_as_int x) - (fun x -> arg_as_char x) - (fun r -> - fun s -> - embed_simple - FStar_Syntax_Embeddings.e_string - r s) - (fun r -> - fun _us -> - fun x -> - fun y -> - let uu___35 = - let uu___36 = - FStar_BigInt.to_int_fs - x in - FStar_String.make - uu___36 y in - FStar_Pervasives_Native.Some - uu___35)), - (FStar_TypeChecker_NBETerm.mixed_binary_op - FStar_TypeChecker_NBETerm.arg_as_int - FStar_TypeChecker_NBETerm.arg_as_char - (FStar_TypeChecker_NBETerm.embed - FStar_TypeChecker_NBETerm.e_string - bogus_cbs) - (fun _us -> - fun x -> - fun y -> - let uu___35 = - let uu___36 = - FStar_BigInt.to_int_fs - x in - FStar_String.make - uu___36 y in - FStar_Pervasives_Native.Some - uu___35))) - :: uu___34 in + string_split', + (fun uu___40 -> + FStar_TypeChecker_NBETerm.string_split')) + :: uu___39 in + (FStar_Parser_Const.string_make_lid, + (Prims.of_int (2)), + Prims.int_zero, + (mixed_binary_op + (fun x -> arg_as_int x) + (fun x -> arg_as_char x) + (fun r -> + fun s -> + embed_simple + FStar_Syntax_Embeddings.e_string + r s) + (fun r -> + fun _us -> + fun x -> + fun y -> + let uu___39 = + let uu___40 = + FStar_BigInt.to_int_fs + x in + FStar_String.make + uu___40 y in + FStar_Pervasives_Native.Some + uu___39)), + (FStar_TypeChecker_NBETerm.mixed_binary_op + FStar_TypeChecker_NBETerm.arg_as_int + FStar_TypeChecker_NBETerm.arg_as_char + (FStar_TypeChecker_NBETerm.embed + FStar_TypeChecker_NBETerm.e_string + bogus_cbs) + (fun _us -> + fun x -> + fun y -> + let uu___39 = + let uu___40 = + FStar_BigInt.to_int_fs + x in + FStar_String.make + uu___40 y in + FStar_Pervasives_Native.Some + uu___39))) + :: uu___38 in + uu___36 :: uu___37 in + uu___34 :: uu___35 in uu___32 :: uu___33 in uu___30 :: uu___31 in uu___28 :: uu___29 in diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml index 21efac237c4..2644ea406a5 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml @@ -940,6 +940,9 @@ let (e_int : FStar_BigInt.t embedding) = let uu___1 = FStar_Syntax_Embeddings_Base.emb_typ_of FStar_Syntax_Embeddings.e_int in mk_emb' em un uu___ uu___1 +let (e_fsint : Prims.int embedding) = + embed_as e_int FStar_BigInt.to_int_fs FStar_BigInt.of_int_fs + FStar_Pervasives_Native.None let e_option : 'a . 'a embedding -> 'a FStar_Pervasives_Native.option embedding = fun ea -> @@ -1948,6 +1951,19 @@ let (string_of_int : FStar_BigInt.t -> t) = embed e_string bogus_cbs uu___ let (string_of_bool : Prims.bool -> t) = fun b -> embed e_string bogus_cbs (if b then "true" else "false") +let (int_of_string : Prims.string -> t) = + fun s -> + let uu___ = e_option e_fsint in + let uu___1 = FStar_Compiler_Util.safe_int_of_string s in + embed uu___ bogus_cbs uu___1 +let (bool_of_string : Prims.string -> t) = + fun s -> + let r = + match s with + | "true" -> FStar_Pervasives_Native.Some true + | "false" -> FStar_Pervasives_Native.Some false + | uu___ -> FStar_Pervasives_Native.None in + let uu___ = e_option e_bool in embed uu___ bogus_cbs r let (string_lowercase : Prims.string -> t) = fun s -> embed e_string bogus_cbs (FStar_String.lowercase s) let (string_uppercase : Prims.string -> t) =