feat(library/init/data/char): use uint32 instead of nat for defining char

library/init/data/char/basic.lean

@@ -4,25 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.nat.basic
-
-open nat
-@[inline, reducible] def is_valid_char (n : nat) : Prop :=
+import init.data.uint
+@[inline, reducible] def is_valid_char (n : uint32) : Prop :=
 n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
 
-lemma is_valid_char_range_1 (n : nat) (h : n < 0xd800) : is_valid_char n :=
-or.inl h
-
-lemma is_valid_char_range_2 (n : nat) (h₁ : 0xdfff < n) (h₂ : n < 0x110000) : is_valid_char n :=
-or.inr ⟨h₁, h₂⟩
-
 /-- The `char` type represents an unicode scalar value.
     See http://www.unicode.org/glossary/#unicode_scalar_value). -/
 structure char :=
-(val : nat) (valid : is_valid_char val)
+(val : uint32) (valid : is_valid_char val)
 
 instance : has_sizeof char :=
-⟨λ c, c.val⟩
+⟨λ c, c.val.to_nat⟩
 
 namespace char
 protected def lt (a b : char) : Prop := a.val < b.val
@@ -32,26 +24,16 @@ instance : has_lt char := ⟨char.lt⟩
 instance : has_le char := ⟨char.le⟩
 
 instance dec_lt (a b : char) :  decidable (a < b) :=
-nat.dec_lt _ _
+uint32.dec_lt _ _
 
 instance dec_le (a b : char) : decidable (a ≤ b) :=
-nat.dec_le _ _
-
-/-
-We cannot use tactics dec_trivial or comp_val here because the tactic framework has not been defined yet.
-We also do not use `zero_lt_succ _` as a proof term because this proof may not be trivial to check by
-external type checkers. See discussion at: https://github.com/leanprover/tc/issues/8
--/
-lemma zero_lt_d800 : 0 < 0xd800 :=
-nat.zero_lt_bit0 $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $
-nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $
-nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit1_ne_zero 13
+uint32.dec_le _ _
 
 @[inline, pattern] def of_nat (n : nat) : char :=
-if h : is_valid_char n then {val := n, valid := h} else {val := 0, valid := or.inl zero_lt_d800}
+if h : is_valid_char (uint32.of_nat n) then {val := uint32.of_nat n, valid := h} else {val := 0, valid := sorry}
 
 @[inline] def to_nat (c : char) : nat :=
-c.val
+c.val.to_nat
 
 lemma eq_of_veq : ∀ {c d : char}, c.val = d.val → c = d
 | ⟨v, h⟩ ⟨_, _⟩ rfl := rfl
@@ -94,18 +76,4 @@ def to_lower (c : char) : char :=
 let n := to_nat c in
 if n >= 65 ∧ n <= 90 then of_nat (n + 32) else c
 
-theorem val_of_nat_eq_of_is_valid {n : nat} : is_valid_char n → (of_nat n).val = n :=
-λ h, show (if h' : is_valid_char n then {char . val := n, valid := h'} else {val := 0, valid := or.inl zero_lt_d800}).val = n, from
-(@dif_pos _ _ h _ (λ h', {char . val := n, valid := h'}) (λ _, {val := 0, valid := or.inl zero_lt_d800})).symm ▸ rfl
-
-theorem val_of_nat_eq_of_not_is_valid {n : nat} : ¬ is_valid_char n → (of_nat n).val = 0 :=
-λ h, show (if h' : is_valid_char n then {char . val := n, valid := h'} else {val := 0, valid := or.inl zero_lt_d800}).val = 0, from
-(@dif_neg _ _ h _ (λ h', {char . val := n, valid := h'}) (λ _, {val := 0, valid := or.inl zero_lt_d800})).symm ▸ rfl
-
-theorem of_nat_eq_of_not_is_valid {n : nat} : ¬ is_valid_char n → of_nat n = of_nat 0 :=
-λ h, eq_of_veq ((val_of_nat_eq_of_not_is_valid h).symm ▸ rfl)
-
-theorem of_nat_ne_of_ne {n₁ n₂ : nat} (h₁ : n₁ ≠ n₂) (h₂ : is_valid_char n₁) (h₃ : is_valid_char n₂) : of_nat n₁ ≠ of_nat n₂ :=
-ne_of_vne ((val_of_nat_eq_of_is_valid h₂).symm ▸ (val_of_nat_eq_of_is_valid h₃).symm ▸ h₁)
-
 end char

library/init/lean/extern.lean

@@ -52,7 +52,7 @@ def expand_extern_pattern_aux (args : list string) : nat → string.iterator →
     else
       let it  := it.next in
       let c   := it.curr in
-      let j   := c.val - '0'.val - 1 in
+      let j   := c.to_nat - '0'.to_nat - 1 in
       expand_extern_pattern_aux i it.next (r ++ (args.nth j).get_or_else "")
 
 @[export lean.expand_extern_pattern_core]

library/init/lean/name_mangling.lean

@@ -17,7 +17,7 @@ private def string.mangle_aux : nat → string.iterator → string → string
     string.mangle_aux i it.next (r.push c)
   else if c = '_' then
     string.mangle_aux i it.next (r ++ "__")
-  else if c.val < 255 then
+  else if c.to_nat < 255 then
     let n := c.to_nat in
     let r := r ++ "_x" in
     let r := r.push $ nat.digit_char (n / 16) in

library/init/lean/parser/string_literal.lean

@@ -12,9 +12,9 @@ open monad_parsec
 variables {m : Type → Type} {μ : Type} [monad m] [monad_parsec μ m] [alternative m]
 
 def parse_hex_digit : m nat :=
-(    (do d ← digit, pure $ d.val - '0'.val)
- <|> (do c ← satisfy (λ c, 'a'.val ≤ c.val && c.val ≤ 'f'.val), pure $ 10 + (c.val - 'a'.val))
- <|> (do c ← satisfy (λ c, 'A'.val ≤ c.val && c.val ≤ 'F'.val), pure $ 10 + (c.val - 'A'.val)))
+(    (do d ← digit, pure $ d.to_nat - '0'.to_nat)
+ <|> (do c ← satisfy (λ c, 'a'.val ≤ c.val && c.val ≤ 'f'.val), pure $ 10 + (c.to_nat - 'a'.to_nat))
+ <|> (do c ← satisfy (λ c, 'A'.val ≤ c.val && c.val ≤ 'F'.val), pure $ 10 + (c.to_nat - 'A'.to_nat)))
 <?> "hexadecimal"
 
 def parse_quoted_char : m char :=

src/library/string.cpp

@@ -130,6 +130,7 @@ optional<unsigned> to_char_core(expr const & e) {
     buffer<expr> args;
     expr const & fn = get_app_args(e, args);
     if (fn == *g_char_mk && args.size() == 2) {
+        /* TODO(Leo): FIX, we are now using uint32 instead of nat */
         if (auto n = to_num(args[0])) {
             return optional<unsigned>(n->get_unsigned_int());
         } else {