From ffc4abed32d3a5069d87fb098ce3d2d42eaa3d84 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Nov 2020 16:30:48 -0800 Subject: [PATCH] fix: `UInt*` and `USize` `Inhabited` instances --- src/Init/Data/Char/Basic.lean | 2 +- src/Init/Data/UInt.lean | 4 +- src/Init/Fix.lean | 12 ++--- src/Init/Prelude.lean | 75 ++++++++++++++++++------------- src/Lean/Compiler/IR/EmitC.lean | 2 +- src/Lean/Data/Json/Parser.lean | 4 +- src/Std/Data/PersistentArray.lean | 2 +- 7 files changed, 58 insertions(+), 43 deletions(-) diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean index 1806d82c0b..0712b64c26 100644 --- a/src/Init/Data/Char/Basic.lean +++ b/src/Init/Data/Char/Basic.lean @@ -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 diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean index 0cecf19817..77f4e0fbff 100644 --- a/src/Init/Data/UInt.lean +++ b/src/Init/Data/UInt.lean @@ -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"] diff --git a/src/Init/Fix.lean b/src/Init/Fix.lean index a01a955208..c626917df3 100644 --- a/src/Init/Fix.lean +++ b/src/Init/Fix.lean @@ -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 diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 7716792a95..ce6c0a536f 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -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 diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 4ede1d8a0f..78a87f0f61 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -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 "\")" diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean index af895eef2d..eef92ed91d 100644 --- a/src/Lean/Data/Json/Parser.lean +++ b/src/Lean/Data/Json/Parser.lean @@ -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 diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean index 17a6b3c770..6634da3be3 100644 --- a/src/Std/Data/PersistentArray.lean +++ b/src/Std/Data/PersistentArray.lean @@ -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 }