From 61274c7d357ea5bd5de9428095b5cea4739770ae Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Feb 2019 18:07:55 -0800 Subject: [PATCH] feat(library/init/data/char): use `uint32` instead of `nat` for defining `char` --- library/init/data/char/basic.lean | 48 ++++---------------- library/init/lean/extern.lean | 2 +- library/init/lean/name_mangling.lean | 2 +- library/init/lean/parser/string_literal.lean | 6 +-- src/library/string.cpp | 1 + 5 files changed, 14 insertions(+), 45 deletions(-) diff --git a/library/init/data/char/basic.lean b/library/init/data/char/basic.lean index 386c09970a..b7598c5bbb 100644 --- a/library/init/data/char/basic.lean +++ b/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 diff --git a/library/init/lean/extern.lean b/library/init/lean/extern.lean index 7a538d2686..19b715c56a 100644 --- a/library/init/lean/extern.lean +++ b/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] diff --git a/library/init/lean/name_mangling.lean b/library/init/lean/name_mangling.lean index b2505e14bc..88c6337c6c 100644 --- a/library/init/lean/name_mangling.lean +++ b/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 diff --git a/library/init/lean/parser/string_literal.lean b/library/init/lean/parser/string_literal.lean index 99560063c6..1aee40f1d8 100644 --- a/library/init/lean/parser/string_literal.lean +++ b/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 := diff --git a/src/library/string.cpp b/src/library/string.cpp index 723e963350..747d1a30ad 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -130,6 +130,7 @@ optional to_char_core(expr const & e) { buffer 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(n->get_unsigned_int()); } else {