From a3f678bfb666867045a0fdefb45470c2d0aab5bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 25 Aug 2024 02:53:10 -0700 Subject: [PATCH 1/3] FStar.Char: move type into smaller FStar.Char.Type module This also tweaks the dependency analysis to only introduce a dependency to FStar.Char.Type when a character literal appears. --- src/basic/FStarC.Char.fsti | 3 +- src/extraction/FStarC.Extraction.Krml.fst | 2 +- src/ml/bare/FStarC_BaseTypes.ml | 2 +- src/ml/bare/FStarC_Compiler_String.ml | 2 +- src/ml/bare/FStarC_Getopt.ml | 2 +- src/ml/bare/FStarC_Parser_Parse.mly | 2 +- src/parser/FStarC.Parser.Const.fst | 2 +- src/parser/FStarC.Parser.Dep.fst | 2 +- .../FStarC.SMTEncoding.EncodeTerm.fst | 2 +- ulib/FStar.Char.Type.fsti | 36 +++++++++++++++++++ ulib/FStar.Char.fsti | 30 ++++++---------- ulib/FStar.Pprint.fsti | 3 +- ulib/ml/app/FStar_Char.ml | 12 +++---- ulib/ml/app/FStar_Char_Type.ml | 4 +++ ulib/ml/app/FStar_String.ml | 2 +- 15 files changed, 66 insertions(+), 40 deletions(-) create mode 100644 ulib/FStar.Char.Type.fsti create mode 100644 ulib/ml/app/FStar_Char_Type.ml diff --git a/src/basic/FStarC.Char.fsti b/src/basic/FStarC.Char.fsti index 271b643db3b..cb2b97e5162 100644 --- a/src/basic/FStarC.Char.fsti +++ b/src/basic/FStarC.Char.fsti @@ -20,8 +20,7 @@ module FStarC.Char same ML implementation. It is here to prevent dependencies from the compiler into the UInt32 module. *) -new -val char:eqtype +include FStar.Char.Type type char_code diff --git a/src/extraction/FStarC.Extraction.Krml.fst b/src/extraction/FStarC.Extraction.Krml.fst index 9f95efe8086..3b6fb5d90ba 100644 --- a/src/extraction/FStarC.Extraction.Krml.fst +++ b/src/extraction/FStarC.Extraction.Krml.fst @@ -1302,7 +1302,7 @@ and translate_constant c: expr = let i = BU.int_of_char c in let s = BU.string_of_int i in let c = EConstant (CInt, s) in - let char_of_int = EQualified (["FStar"; "Char"], "char_of_int") in + let char_of_int = EQualified (["FStar"; "Char"; "Type"], "char_of_int") in EApp(char_of_int, [c]) | MLC_Int (s, Some (sg, wd)) -> EConstant (translate_width (Some (sg, wd)), s) diff --git a/src/ml/bare/FStarC_BaseTypes.ml b/src/ml/bare/FStarC_BaseTypes.ml index 66b018bd10c..6c8a79eba55 100644 --- a/src/ml/bare/FStarC_BaseTypes.ml +++ b/src/ml/bare/FStarC_BaseTypes.ml @@ -1,4 +1,4 @@ -type char = FStar_Char.char[@@deriving yojson,show] +type char = FStar_Char_Type.char[@@deriving yojson,show] type float = FStar_Float.float[@@deriving yojson,show] type double = FStar_Float.double[@@deriving yojson,show] type byte = FStar_UInt8.byte[@@deriving yojson,show] diff --git a/src/ml/bare/FStarC_Compiler_String.ml b/src/ml/bare/FStarC_Compiler_String.ml index 9dcff4a94df..5805aefee26 100644 --- a/src/ml/bare/FStarC_Compiler_String.ml +++ b/src/ml/bare/FStarC_Compiler_String.ml @@ -16,7 +16,7 @@ let split seps s = repeat_split l seps in repeat_split [s] seps let compare x y = Z.of_int (BatString.compare x y) -type char = FStar_Char.char +type char = FStar_Char_Type.char let concat = BatString.concat let length s = Z.of_int (BatUTF8.length s) let strlen s = length s diff --git a/src/ml/bare/FStarC_Getopt.ml b/src/ml/bare/FStarC_Getopt.ml index a7bad22b6c4..aaa125f4177 100644 --- a/src/ml/bare/FStarC_Getopt.ml +++ b/src/ml/bare/FStarC_Getopt.ml @@ -2,7 +2,7 @@ let noshort = 0 type 'a opt_variant = | ZeroArgs of (unit -> 'a) | OneArg of (string -> 'a) * string -type 'a opt' = FStar_Char.char * string * 'a opt_variant +type 'a opt' = FStar_Char_Type.char * string * 'a opt_variant type opt = unit opt' type parse_cmdline_res = | Empty diff --git a/src/ml/bare/FStarC_Parser_Parse.mly b/src/ml/bare/FStarC_Parser_Parse.mly index ccf4d38af78..7be7cb10e6a 100644 --- a/src/ml/bare/FStarC_Parser_Parse.mly +++ b/src/ml/bare/FStarC_Parser_Parse.mly @@ -87,7 +87,7 @@ let parse_use_lang_blob (extension_name:string) %token UINT64 %token SIZET %token REAL -%token CHAR +%token CHAR %token LET %token LET_OP %token AND_OP diff --git a/src/parser/FStarC.Parser.Const.fst b/src/parser/FStarC.Parser.Const.fst index d698f4819b7..eaf799259d4 100644 --- a/src/parser/FStarC.Parser.Const.fst +++ b/src/parser/FStarC.Parser.Const.fst @@ -84,7 +84,7 @@ let real_lid = p2l ["FStar"; "Real"; "real"] let float_lid = p2l ["FStar"; "Float"; "float"] -let char_lid = p2l ["FStar"; "Char"; "char"] +let char_lid = p2l ["FStar"; "Char"; "Type"; "char"] let heap_lid = p2l ["FStar"; "Heap"; "heap"] diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index 1d535975038..190f0739af9 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -956,7 +956,7 @@ let collect_one let w = match width with | Int8 -> "8" | Int16 -> "16" | Int32 -> "32" | Int64 -> "64" in add_to_parsing_data (P_dep (false, (Util.format2 "fstar.%sint%s" u w |> Ident.lid_of_str))) | Const_char _ -> - add_to_parsing_data (P_dep (false, ("fstar.char" |> Ident.lid_of_str))) + add_to_parsing_data (P_dep (false, ("fstar.char.type" |> Ident.lid_of_str))) | Const_range_of | Const_set_range_of -> add_to_parsing_data (P_dep (false, ("fstar.range" |> Ident.lid_of_str))) diff --git a/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst b/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst index a151568d04a..b47c7a24ad5 100644 --- a/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst +++ b/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst @@ -359,7 +359,7 @@ let rec encode_const c env = | Const_unit -> mk_Term_unit, [] | Const_bool true -> boxBool mkTrue, [] | Const_bool false -> boxBool mkFalse, [] - | Const_char c -> mkApp("FStar.Char.__char_of_int", [boxInt (mkInteger' (BU.int_of_char c))]), [] + | Const_char c -> mkApp("FStar.Char.Type.char_of_int", [boxInt (mkInteger' (BU.int_of_char c))]), [] | Const_int (i, None) -> boxInt (mkInteger i), [] | Const_int (repr, Some sw) -> let syntax_term = FStarC.ToSyntax.ToSyntax.desugar_machine_integer env.tcenv.dsenv repr sw Range.dummyRange in diff --git a/ulib/FStar.Char.Type.fsti b/ulib/FStar.Char.Type.fsti new file mode 100644 index 00000000000..b0b7bd77f17 --- /dev/null +++ b/ulib/FStar.Char.Type.fsti @@ -0,0 +1,36 @@ +(* + Copyright 2008-2018 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.Char.Type + +(** [char] represents a Unicode codepoint. *) +new +val char : eqtype + +let valid_codepoint (i:nat) : prop = i < 0xd7ff \/ (i >= 0xe000 /\ i <= 0x10ffff) + +(* Chars are in a bijection with codepoints. See FStar.Char module for +machine integer versions of these two functions. *) +val char_of_int (i: nat{valid_codepoint i}) : Tot char +val int_of_char (c: char) : Tot (i:nat{valid_codepoint i}) + +val char_of_int_of_char (c:char) + : Lemma (char_of_int (int_of_char c) == c) + [SMTPat (int_of_char c)] + +val int_of_char_of_int (i:nat{valid_codepoint i}) + : Lemma (int_of_char (char_of_int i) == i) + [SMTPat (char_of_int i)] diff --git a/ulib/FStar.Char.fsti b/ulib/FStar.Char.fsti index 8e87b73ad3d..aa4d01ac884 100644 --- a/ulib/FStar.Char.fsti +++ b/ulib/FStar.Char.fsti @@ -26,42 +26,35 @@ module FStar.Char /// See https://en.wikipedia.org/wiki/UTF-8 and /// https://erratique.ch/software/uucp/doc/unicode.html -module U32 = FStar.UInt32 +(* The type definition is here. The rest of this module is properties. +Clients who only need the name of the type can import this smaller +Char.Type module. *) +include FStar.Char.Type -(** [char] is a new primitive type with decidable equality *) -new -val char:eqtype +module U32 = FStar.UInt32 (** A [char_code] is the representation of a UTF-8 char code in an unsigned 32-bit integer whose value is at most 0x110000, and not between 0xd800 and 0xe000 *) -type char_code = n: U32.t{U32.v n < 0xd7ff \/ (U32.v n >= 0xe000 /\ U32.v n <= 0x10ffff)} +type char_code = n: U32.t{valid_codepoint (U32.v n)} (** A primitive to extract the [char_code] of a [char] *) -val u32_of_char: char -> Tot char_code +val u32_of_char: c:char -> Tot (n:char_code{U32.v n == int_of_char c}) (** A primitive to promote a [char_code] to a [char] *) -val char_of_u32: char_code -> Tot char +val char_of_u32: n:char_code -> Tot (c:char{c == char_of_int (U32.v n)}) -(** Encoding and decoding from [char] to [char_code] is the identity *) +(* These two are provable from the lemmas in FStar.Char.Type. *) val char_of_u32_of_char (c: char) : Lemma (ensures (char_of_u32 (u32_of_char c) == c)) [SMTPat (u32_of_char c)] - -(** Encoding and decoding from [char] to [char_code] is the identity *) val u32_of_char_of_u32 (c: char_code) : Lemma (ensures (u32_of_char (char_of_u32 c) == c)) [SMTPat (char_of_u32 c)] -(** A couple of utilities to use mathematical integers rather than [U32.t] - to represent a [char_code] *) -let int_of_char (c: char) : nat = U32.v (u32_of_char c) -let char_of_int (i: nat{i < 0xd7ff \/ (i >= 0xe000 /\ i <= 0x10ffff)}) : char = char_of_u32 (U32.uint_to_t i) - (** Case conversion *) val lowercase: char -> Tot char val uppercase: char -> Tot char -#set-options "--admit_smt_queries true" - +#push-options "--admit_smt_queries true" (** This private primitive is used internally by the compiler to translate character literals with a desugaring-time check of the size of the number, rather than an expensive verification check. @@ -71,5 +64,4 @@ val uppercase: char -> Tot char private unfold let __char_of_int (x: int) : char = char_of_int x -#reset-options - +#pop-options diff --git a/ulib/FStar.Pprint.fsti b/ulib/FStar.Pprint.fsti index 7ac5c135064..f43a0c6fc87 100644 --- a/ulib/FStar.Pprint.fsti +++ b/ulib/FStar.Pprint.fsti @@ -15,8 +15,7 @@ *) module FStar.Pprint -(* Unfortunate *) -open FStar.Char +open FStar.Char.Type open FStar.Float (* The rest of this file is taken almost verbatim from src/prettyprint/FStar.Pprint.fsti *) diff --git a/ulib/ml/app/FStar_Char.ml b/ulib/ml/app/FStar_Char.ml index 2727e723626..84f0496bd2d 100644 --- a/ulib/ml/app/FStar_Char.ml +++ b/ulib/ml/app/FStar_Char.ml @@ -1,10 +1,12 @@ module UChar = BatUChar - module U32 = FStar_UInt32 +open FStar_Char_Type -type char = int[@@deriving yojson,show] type char_code = U32.t +let u32_of_char (x:char) : char_code = U32.of_native_int x +let char_of_u32 (x:char_code) : char = U32.to_native_int x + (* FIXME(adl) UChar.lowercase/uppercase removed from recent Batteries. Use Camomile? *) let lowercase (x:char) : char = try Char.code (Char.lowercase_ascii (Char.chr x)) @@ -13,9 +15,3 @@ let lowercase (x:char) : char = let uppercase (x:char) : char = try Char.code (Char.uppercase_ascii (Char.chr x)) with _ -> x - -let int_of_char (x:char) : Z.t= Z.of_int x -let char_of_int (i:Z.t) : char = Z.to_int i - -let u32_of_char (x:char) : char_code = U32.of_native_int x -let char_of_u32 (x:char_code) : char = U32.to_native_int x diff --git a/ulib/ml/app/FStar_Char_Type.ml b/ulib/ml/app/FStar_Char_Type.ml new file mode 100644 index 00000000000..7397cc95488 --- /dev/null +++ b/ulib/ml/app/FStar_Char_Type.ml @@ -0,0 +1,4 @@ +type char = int[@@deriving yojson,show] + +let int_of_char (x:char) : Z.t = Z.of_int x +let char_of_int (i:Z.t) : char = Z.to_int i diff --git a/ulib/ml/app/FStar_String.ml b/ulib/ml/app/FStar_String.ml index 45c7ba41578..27a34d42a65 100644 --- a/ulib/ml/app/FStar_String.ml +++ b/ulib/ml/app/FStar_String.ml @@ -16,7 +16,7 @@ let split seps s = repeat_split l seps in repeat_split [s] seps let compare x y = Z.of_int (BatString.compare x y) -type char = FStar_Char.char +type char = FStar_Char_Type.char let concat = BatString.concat let length s = Z.of_int (BatUTF8.length s) let strlen s = length s From 87369fa08719720dcc12f0be4d30db5b1d448acd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 25 Aug 2024 02:59:52 -0700 Subject: [PATCH 2/3] lib: tightening FStar.Char -> FStar.Char.Type --- ulib/FStar.Bytes.fsti | 1 - ulib/FStar.Class.Printable.fst | 2 +- ulib/FStar.String.fsti | 2 +- ulib/legacy/FStar.Pointer.Base.fsti | 2 +- 4 files changed, 3 insertions(+), 4 deletions(-) diff --git a/ulib/FStar.Bytes.fsti b/ulib/FStar.Bytes.fsti index 5092aa1e02e..3e31f591f38 100644 --- a/ulib/FStar.Bytes.fsti +++ b/ulib/FStar.Bytes.fsti @@ -35,7 +35,6 @@ module U16 = FStar.UInt16 module U32 = FStar.UInt32 module U64 = FStar.UInt64 module Str = FStar.String -module Chr = FStar.Char unfold let u8 = U8.t unfold let u16 = U16.t diff --git a/ulib/FStar.Class.Printable.fst b/ulib/FStar.Class.Printable.fst index 8f781012915..4d54cc6a033 100644 --- a/ulib/FStar.Class.Printable.fst +++ b/ulib/FStar.Class.Printable.fst @@ -80,7 +80,7 @@ instance printable_either #a #b {| printable a |} {| printable b |} : printable (* Then the base types. *) -instance printable_char : printable FStar.Char.char = +instance printable_char : printable FStar.Char.Type.char = { to_string = string_of_char } diff --git a/ulib/FStar.String.fsti b/ulib/FStar.String.fsti index ba6245670af..f11e3b8b4cf 100644 --- a/ulib/FStar.String.fsti +++ b/ulib/FStar.String.fsti @@ -33,7 +33,7 @@ open FStar.List.Tot For strings in Low*, see LowStar.String, LowStar.Literal etc. *) -type char = FStar.Char.char +type char = FStar.Char.Type.char /// `list_of_string` and `string_of_list`: A pair of coercions to /// expose and pack a string as a list of characters diff --git a/ulib/legacy/FStar.Pointer.Base.fsti b/ulib/legacy/FStar.Pointer.Base.fsti index 82e8d8e72be..1e9bcc62bb3 100644 --- a/ulib/legacy/FStar.Pointer.Base.fsti +++ b/ulib/legacy/FStar.Pointer.Base.fsti @@ -208,7 +208,7 @@ let type_of_base_typ | TInt16 -> FStar.Int16.t | TInt32 -> FStar.Int32.t | TInt64 -> FStar.Int64.t - | TChar -> FStar.Char.char + | TChar -> FStar.Char.Type.char | TBool -> bool | TUnit -> unit From 58693ea928111b89f0287d87b077acba2143e2b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 25 Aug 2024 09:58:03 -0700 Subject: [PATCH 3/3] Update expected output Char type moved --- .../ExpectFailure.fst.json_output.expected | 10 +++++----- tests/error-messages/ExpectFailure.fst.output.expected | 10 +++++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/tests/error-messages/ExpectFailure.fst.json_output.expected b/tests/error-messages/ExpectFailure.fst.json_output.expected index dd69a2e413b..708f065563f 100644 --- a/tests/error-messages/ExpectFailure.fst.json_output.expected +++ b/tests/error-messages/ExpectFailure.fst.json_output.expected @@ -1,8 +1,8 @@ >> Got issues: [ -{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} >>] >> Got issues: [ -{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} >>] >> Got issues: [ {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":28,"col":15},"end_pos":{"line":28,"col":20}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":28,"col":8},"end_pos":{"line":28,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} @@ -11,11 +11,11 @@ {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":30,"col":15},"end_pos":{"line":30,"col":20}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":30,"col":8},"end_pos":{"line":30,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} >>] >> Got issues: [ -{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} >>] >> Got issues: [ -{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} >>] >> Got issues: [ -{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} >>] diff --git a/tests/error-messages/ExpectFailure.fst.output.expected b/tests/error-messages/ExpectFailure.fst.output.expected index 58e223f85ce..b870eb71ec1 100644 --- a/tests/error-messages/ExpectFailure.fst.output.expected +++ b/tests/error-messages/ExpectFailure.fst.output.expected @@ -2,14 +2,14 @@ * Error 189 at ExpectFailure.fst(20,12-20,15): - Expected expression of type Prims.int got expression 'a' - of type FStar.Char.char + of type FStar.Char.Type.char >>] >> Got issues: [ * Error 189 at ExpectFailure.fst(24,12-24,15): - Expected expression of type Prims.int got expression 'a' - of type FStar.Char.char + of type FStar.Char.Type.char >>] >> Got issues: [ @@ -32,20 +32,20 @@ * Error 189 at ExpectFailure.fst(43,12-43,15): - Expected expression of type Prims.int got expression 'a' - of type FStar.Char.char + of type FStar.Char.Type.char >>] >> Got issues: [ * Error 189 at ExpectFailure.fst(50,12-50,15): - Expected expression of type Prims.int got expression 'a' - of type FStar.Char.char + of type FStar.Char.Type.char >>] >> Got issues: [ * Error 189 at ExpectFailure.fst(61,12-61,15): - Expected expression of type Prims.int got expression 'a' - of type FStar.Char.char + of type FStar.Char.Type.char >>]