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

fix: UInt* and USize Inhabited instances

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-13 16:30:48 -08:00
parent b9f1999e32
commit ffc4abed32
7 changed files with 58 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -30,7 +30,7 @@ instance (a b : Char) : Decidable (a ≤ b) :=
abbrev isValidCharNat (n : Nat) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < uint32Sz := by
theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
match h with
| Or.inl h =>
apply Nat.ltTrans h

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

@ -111,7 +111,7 @@ instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
@[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⟩⟩
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩
abbrev Nat.toUInt32 := UInt32.ofNat
@[extern c inline "#1 + #2"]
def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩
@ -215,7 +215,7 @@ def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
theorem usizeSzGt0 : usizeSz > 0 :=
theorem usizeSzGt0 : USize.size > 0 :=
Nat.posPowOfPos System.Platform.numBits (Nat.zeroLtSucc _)
@[extern "lean_usize_of_nat"]

12
src/Init/Fix.lean
View file

@ -13,7 +13,7 @@ def bfix1 {α β : Type u} (base : α → β) (rec : (α → β) → α → β)
@[extern c inline "lean_fixpoint(#4, #5)"]
def fixCore1 {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β :=
bfix1 base rec usizeSz
bfix1 base rec USize.size
@[inline] def fixCore {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β :=
fixCore1 base rec
@ -30,7 +30,7 @@ def bfix2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α
@[extern c inline "lean_fixpoint2(#5, #6, #7)"]
def fixCore2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
bfix2 base rec usizeSz
bfix2 base rec USize.size
@[inline] def fix2 {α₁ α₂ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
fixCore2 (fun _ _ => arbitrary β) rec
@ -41,7 +41,7 @@ def bfix3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ →
@[extern c inline "lean_fixpoint3(#6, #7, #8, #9)"]
def fixCore3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
bfix3 base rec usizeSz
bfix3 base rec USize.size
@[inline] def fix3 {α₁ α₂ α₃ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
fixCore3 (fun _ _ _ => arbitrary β) rec
@ -52,7 +52,7 @@ def bfix4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α
@[extern c inline "lean_fixpoint4(#7, #8, #9, #10, #11)"]
def fixCore4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
bfix4 base rec usizeSz
bfix4 base rec USize.size
@[inline] def fix4 {α₁ α₂ α₃ α₄ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
fixCore4 (fun _ _ _ _ => arbitrary β) rec
@ -63,7 +63,7 @@ def bfix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂
@[extern c inline "lean_fixpoint5(#8, #9, #10, #11, #12, #13)"]
def fixCore5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
bfix5 base rec usizeSz
bfix5 base rec USize.size
@[inline] def fix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
fixCore5 (fun _ _ _ _ _ => arbitrary β) rec
@ -74,7 +74,7 @@ def bfix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α
@[extern c inline "lean_fixpoint6(#9, #10, #11, #12, #13, #14, #15)"]
def fixCore6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
bfix6 base rec usizeSz
bfix6 base rec USize.size
@[inline] def fix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
fixCore6 (fun _ _ _ _ _ _ => arbitrary β) rec

75
src/Init/Prelude.lean
View file

@ -596,9 +596,14 @@ instance {n} : HasLessEq (Fin n) := ⟨Fin.le⟩
instance Fin.decLt {n} (a b : Fin n) : Decidable (Less a b) := Nat.decLt ..
instance Fin.decLe {n} (a b : Fin n) : Decidable (LessEq a b) := Nat.decLe ..
def uint8Sz : Nat := 256
def UInt8.size : Nat := 256
structure UInt8 :=
(val : Fin uint8Sz)
(val : Fin UInt8.size)
@[extern "lean_uint8_of_nat"]
def UInt8.ofNatCore (n : @& Nat) (h : Less n UInt8.size) : UInt8 := {
val := { val := n, isLt := h }
}
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 == #2"]
@ -610,12 +615,17 @@ def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
instance : DecidableEq UInt8 := UInt8.decEq
instance : Inhabited UInt8 := {
default := { val := { val := 0, isLt := decide! } }
default := UInt8.ofNatCore 0 decide!
}
def uint16Sz : Nat := 65536
def UInt16.size : Nat := 65536
structure UInt16 :=
(val : Fin uint16Sz)
(val : Fin UInt16.size)
@[extern "lean_uint16_of_nat"]
def UInt16.ofNatCore (n : @& Nat) (h : Less n UInt16.size) : UInt16 := {
val := { val := n, isLt := h }
}
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 == #2"]
@ -627,12 +637,17 @@ def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
instance : DecidableEq UInt16 := UInt16.decEq
instance : Inhabited UInt16 := {
default := { val := { val := 0, isLt := decide! } }
default := UInt16.ofNatCore 0 decide!
}
def uint32Sz : Nat := 4294967296
def UInt32.size : Nat := 4294967296
structure UInt32 :=
(val : Fin uint32Sz)
(val : Fin UInt32.size)
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatCore (n : @& Nat) (h : Less n UInt32.size) : UInt32 := {
val := { val := n, isLt := h }
}
@[extern "lean_uint32_to_nat"]
def UInt32.toNat (n : UInt32) : Nat := n.val.val
@ -647,7 +662,7 @@ def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
instance : DecidableEq UInt32 := UInt32.decEq
instance : Inhabited UInt32 := {
default := { val := { val := 0, isLt := decide! } }
default := UInt32.ofNatCore 0 decide!
}
def UInt32.lt (a b : UInt32) : Prop := Less a.val b.val
@ -671,15 +686,15 @@ def UInt32.decLe (a b : UInt32) : Decidable (LessEq a b) :=
instance (a b : UInt32) : Decidable (Less a b) := UInt32.decLt a b
instance (a b : UInt32) : Decidable (LessEq a b) := UInt32.decLe a b
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatCore (n : @& Nat) (h : Less n uint32Sz) : UInt32 := {
def UInt64.size : Nat := 18446744073709551616
structure UInt64 :=
(val : Fin UInt64.size)
@[extern "lean_uint64_of_nat"]
def UInt64.ofNatCore (n : @& Nat) (h : Less n UInt64.size) : UInt64 := {
val := { val := n, isLt := h }
}
def uint64Sz : Nat := 18446744073709551616
structure UInt64 :=
(val : Fin uint64Sz)
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 == #2"]
def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
@ -690,19 +705,24 @@ def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
instance : DecidableEq UInt64 := UInt64.decEq
instance : Inhabited UInt64 := {
default := { val := { val := 0, isLt := decide! } }
default := UInt64.ofNatCore 0 decide!
}
def usizeSz : Nat := pow 2 System.Platform.numBits
def USize.size : Nat := pow 2 System.Platform.numBits
theorem usizeSzEq : Or (Eq usizeSz 4294967296) (Eq usizeSz 18446744073709551616) :=
theorem usizeSzEq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
show Or (Eq (pow 2 System.Platform.numBits) 4294967296) (Eq (pow 2 System.Platform.numBits) 18446744073709551616) from
match System.Platform.numBits, System.Platform.numBitsEq with
| _, Or.inl rfl => Or.inl (decide! : (Eq (pow 2 32) (4294967296:Nat)))
| _, Or.inr rfl => Or.inr (decide! : (Eq (pow 2 64) (18446744073709551616:Nat)))
structure USize :=
(val : Fin usizeSz)
(val : Fin USize.size)
@[extern "lean_usize_of_nat"]
def USize.ofNatCore (n : @& Nat) (h : Less n USize.size) : USize := {
val := { val := n, isLt := h }
}
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 == #2"]
@ -714,24 +734,19 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) :=
instance : DecidableEq USize := USize.decEq
instance : Inhabited USize := {
default := { val := { val := 0, isLt := match usizeSz, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide! } }
default := USize.ofNatCore 0 (match USize.size, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide!)
}
@[extern "lean_usize_of_nat"]
def USize.ofNat32 (n : @& Nat) (h : Less n 4294967296) : USize := {
val := {
val := n,
isLt := match usizeSz, usizeSzEq with
isLt := match USize.size, usizeSzEq with
| _, Or.inl rfl => h
| _, Or.inr rfl => Nat.ltTrans h (decide! : Less 4294967296 18446744073709551616)
}
}
@[extern "lean_usize_of_nat"]
def USize.ofNatCore (n : @& Nat) (h : Less n usizeSz) : USize := {
val := { val := n, isLt := h }
}
abbrev Nat.isValidChar (n : Nat) : Prop :=
Or (Less n 0xd800) (And (Less 0xdfff n) (Less n 0x110000))
@ -744,10 +759,10 @@ structure Char :=
(val : UInt32)
(valid : val.isValidChar)
private theorem validCharIsUInt32 {n : Nat} (h : n.isValidChar) : Less n uint32Sz :=
private theorem validCharIsUInt32 {n : Nat} (h : n.isValidChar) : Less n UInt32.size :=
match h with
| Or.inl h => Nat.ltTrans h (decide! : Less 55296 uint32Sz)
| Or.inr ⟨_, h⟩ => Nat.ltTrans h (decide! : Less 1114112 uint32Sz)
| Or.inl h => Nat.ltTrans h (decide! : Less 55296 UInt32.size)
| Or.inr ⟨_, h⟩ => Nat.ltTrans h (decide! : Less 1114112 UInt32.size)
@[extern "lean_uint32_of_nat"]
private def Char.ofNatAux (n : Nat) (h : n.isValidChar) : Char :=
@ -1366,7 +1381,7 @@ def mkStr (p : Name) (s : String) : Name :=
@[export lean_name_mk_numeral]
def mkNum (p : Name) (v : Nat) : Name :=
Name.num p v (mixHash (hash p) (dite (Less v usizeSz) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 decide!)))
Name.num p v (mixHash (hash p) (dite (Less v USize.size) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 decide!)))
def mkSimple (s : String) : Name :=
mkStr Name.anonymous s

2
src/Lean/Compiler/IR/EmitC.lean
View file

@ -474,7 +474,7 @@ def quoteString (s : String) : String :=
def emitNumLit (t : IRType) (v : Nat) : M Unit := do
if t.isObj then
if v < uint32Sz then
if v < UInt32.size then
emit "lean_unsigned_to_nat("; emit v; emit "u)"
else
emit "lean_cstr_to_nat(\""; emit v; emit "\")"

4
src/Lean/Data/Json/Parser.lean
View file

@ -203,7 +203,7 @@ def num : Quickparse JsonNumber := do
if c? = some '.' then
skip
let (n, d) ← natNumDigits
if d > usizeSz then fail "too many decimals"
if d > USize.size then fail "too many decimals"
let mantissa' := res.mantissa * (10^d : Nat) + n
let exponent' := res.exponent + d
pure $ JsonNumber.mk mantissa' exponent'
@ -220,7 +220,7 @@ def num : Quickparse JsonNumber := do
else do
if c = '+' then skip
let n ← natMaybeZero
if n > usizeSz then fail "exp too large"
if n > USize.size then fail "exp too large"
pure (res.shiftl n)
else
pure res

2
src/Std/Data/PersistentArray.lean
View file

@ -129,7 +129,7 @@ def mkNewTail (t : PersistentArray α) : PersistentArray α :=
shift := t.shift + initShift,
tailOff := t.size }
def tooBig : Nat := usizeSz / 8
def tooBig : Nat := USize.size / 8
def push (t : PersistentArray α) (a : α) : PersistentArray α :=
let r := { t with tail := t.tail.push a, size := t.size + 1 }