max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make sure Char.ofNat can be efficiently reduced in the kernel and WHNF

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-18 16:41:19 -07:00
parent 736925bbce
commit cd8bd55311
2 changed files with 17 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Init/Data/Char/Basic.lean
View file

@ -39,10 +39,23 @@ UInt32.decLt _ _
instance decLe (a b : Char) : Decidable (a ≤ b) :=
UInt32.decLe _ _
axiom isValidChar0 : isValidChar 0
abbrev isValidCharNat (n : Nat) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < uint32Sz :=
sorry -- TODO: waiting for new frontend
theorem isValidCharOfValidNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
sorry -- TODO: waiting for new frontend
theorem isValidChar0 : isValidChar 0 :=
sorry -- TODO: waiting for new frontend
@[noinline, matchPattern] def ofNat (n : Nat) : Char :=
if h : isValidChar n.toUInt32 then {val := n.toUInt32, valid := h} else {val := 0, valid := isValidChar0}
if h : isValidCharNat n then
{ val := UInt32.ofNat' n (isValidUInt32 n h), valid := isValidCharOfValidNat n h }
else
{ val := 0, valid := isValidChar0 }
@[inline] def toNat (c : Char) : Nat :=
c.val.toNat

2
src/Init/Data/UInt.lean
View file

@ -136,6 +136,8 @@ structure UInt32 :=
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat' (n : Nat) (h : n < uint32Sz) : UInt32 := ⟨⟨n, h⟩⟩
abbrev Nat.toUInt32 := UInt32.ofNat
@[extern "lean_uint32_to_nat"]
def UInt32.toNat (n : UInt32) : Nat := n.val.val