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

ocaml/fstar-lib/FStar_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]

ocaml/fstar-lib/FStar_Char.ml

@@ -2,7 +2,8 @@ module UChar = BatUChar
 
 module U32 = FStar_UInt32
 
-type char = int[@@deriving yojson,show]
+open FStar_Char_Type
+
 type char_code = U32.t
 
 (* FIXME(adl) UChar.lowercase/uppercase removed from recent Batteries. Use Camomile? *)

ocaml/fstar-lib/FStar_Char_Type.ml

@@ -0,0 +1 @@
+type char = int[@@deriving yojson,show]

ocaml/fstar-lib/FStar_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

ocaml/fstar-lib/FStar_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

ocaml/fstar-lib/FStar_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

ocaml/fstar-lib/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

src/basic/FStar.Char.fsti

@@ -20,8 +20,7 @@ module FStar.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/FStar.Extraction.Krml.fst

@@ -1094,7 +1094,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/parser/FStar.Parser.Const.fst

@@ -82,7 +82,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/FStar.Parser.Dep.fst

@@ -934,7 +934,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/FStar.SMTEncoding.EncodeTerm.fst

@@ -360,7 +360,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 = FStar.ToSyntax.ToSyntax.desugar_machine_integer env.tcenv.dsenv repr sw Range.dummyRange in

tests/error-messages/ExpectFailure.fst.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,21 +32,21 @@
 * 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
 
 >>]
 Verified module: ExpectFailure

tests/ide/emacs/fstarmode_gh73.out.expected

@@ -1,5 +1,5 @@
 {"kind": "protocol-info", "rest": "[...]"}
-{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "- Pattern uses these theory symbols or terms that should not be in an SMT\n  pattern:\n    Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [434, 8], "end": [434, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
+{"kind": "response", "query-id": "1", "response": [], "status": "success"}
 {"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "success"}
 {"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "failure"}
 {"kind": "response", "query-id": "4", "response": [], "status": "success"}

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,25 @@
+(*
+   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] is a new primitive type with decidable equality *)
+new
+val char : eqtype
+
+let valid_codepoint (i:nat) : prop = i < 0xd7ff \/ (i >= 0xe000 /\ i <= 0x10ffff)
+
+val char_of_int (i: nat{valid_codepoint i}) : char

ulib/FStar.Char.fsti

@@ -26,16 +26,17 @@ 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
@@ -51,10 +52,13 @@ val char_of_u32_of_char (c: char)
 val u32_of_char_of_u32 (c: char_code)
     : Lemma (ensures (u32_of_char (char_of_u32 c) == c)) [SMTPat (char_of_u32 c)]
 
+val char_of_u32_char_of_int (x:nat{valid_codepoint x})
+    : Lemma (ensures (char_of_u32 (U32.uint_to_t x) == char_of_int x))
+            [SMTPat (char_of_int x)]
+
 (** 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

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.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/FStar.Stubs.Pprint.fsti

@@ -15,8 +15,7 @@
 *)
 module FStar.Stubs.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/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/Makefile.realized

@@ -1,7 +1,7 @@
 # You should include this Makefile in your Makefile to make sure you remain
 # future-proof w.r.t. realized modules!
 
-FSTAR_REALIZED_MODULES=All Buffer Bytes Char CommonST Constructive Dyn Float Ghost Heap Monotonic.Heap \
+FSTAR_REALIZED_MODULES=All Buffer Bytes Char Char.Type CommonST Constructive Dyn Float Ghost Heap Monotonic.Heap \
 	HyperStack.All HyperStack.ST HyperStack.IO Int16 Int32 Int64 Int8 IO \
 	List List.Tot.Base Mul Option Pervasives.Native ST Exn String \
 	UInt16 UInt32 UInt64 UInt8 \