FStar.Char: move type into smaller FStar.Char.Type module

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
 

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)

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]

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

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

src/ml/bare/FStarC_Parser_Parse.mly

@@ -87,7 +87,7 @@ let parse_use_lang_blob (extension_name:string)
 %token <string> UINT64
 %token <string> SIZET
 %token <string> REAL
-%token <FStar_Char.char> CHAR
+%token <FStar_Char_Type.char> CHAR
 %token <bool> LET
 %token <string> LET_OP
 %token <string> AND_OP

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"]
 

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)))

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

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`"]}
 >>]

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
 
 >>]

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

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)]

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

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
 }

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 *)

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

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
 

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

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

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