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

fix: UInt ctors/fields in generated code

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-14 12:50:32 -08:00
parent 9acbc7bb7d
commit cc7d7422db
3 changed files with 71 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Prelude.lean
View file

@ -600,6 +600,9 @@ def UInt8.size : Nat := 256
structure UInt8 :=
(val : Fin UInt8.size)
attribute [extern "lean_uint8_of_nat"] UInt8.mk
attribute [extern "lean_uint8_to_nat"] UInt8.val
@[extern "lean_uint8_of_nat"]
def UInt8.ofNatCore (n : @& Nat) (h : Less n UInt8.size) : UInt8 := {
val := { val := n, isLt := h }
@ -622,6 +625,9 @@ def UInt16.size : Nat := 65536
structure UInt16 :=
(val : Fin UInt16.size)
attribute [extern "lean_uint16_of_nat"] UInt16.mk
attribute [extern "lean_uint16_to_nat"] UInt16.val
@[extern "lean_uint16_of_nat"]
def UInt16.ofNatCore (n : @& Nat) (h : Less n UInt16.size) : UInt16 := {
val := { val := n, isLt := h }
@ -644,6 +650,9 @@ def UInt32.size : Nat := 4294967296
structure UInt32 :=
(val : Fin UInt32.size)
attribute [extern "lean_uint32_of_nat"] UInt32.mk
attribute [extern "lean_uint32_to_nat"] UInt32.val
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatCore (n : @& Nat) (h : Less n UInt32.size) : UInt32 := {
val := { val := n, isLt := h }
@ -690,6 +699,9 @@ def UInt64.size : Nat := 18446744073709551616
structure UInt64 :=
(val : Fin UInt64.size)
attribute [extern "lean_uint64_of_nat"] UInt64.mk
attribute [extern "lean_uint64_to_nat"] UInt64.val
@[extern "lean_uint64_of_nat"]
def UInt64.ofNatCore (n : @& Nat) (h : Less n UInt64.size) : UInt64 := {
val := { val := n, isLt := h }
@ -719,6 +731,9 @@ theorem usizeSzEq : Or (Eq USize.size 4294967296) (Eq USize.size 184467440737095
structure USize :=
(val : Fin USize.size)
attribute [extern "lean_usize_of_nat"] USize.mk
attribute [extern "lean_usize_to_nat"] USize.val
@[extern "lean_usize_of_nat"]
def USize.ofNatCore (n : @& Nat) (h : Less n USize.size) : USize := {
val := { val := n, isLt := h }

34
tests/lean/uintCtors.lean Normal file
View file

@ -0,0 +1,34 @@
def UInt32.ofNatCore' (n : Nat) (h : Less n UInt32.size) : UInt32 := {
val := { val := n, isLt := h }
}
#eval UInt32.ofNatCore' 10 decide!
def UInt64.ofNatCore' (n : Nat) (h : Less n UInt64.size) : UInt64 := {
val := { val := n, isLt := h }
}
#eval UInt64.ofNatCore' 3 decide!
#eval toString $ { val := { val := 3, isLt := decide! } : UInt8 }
#eval (3 : UInt8).val
#eval toString $ { val := { val := 3, isLt := decide! } : UInt16 }
#eval (3 : UInt16).val
#eval toString $ { val := { val := 3, isLt := decide! } : UInt32 }
#eval (3 : UInt32).val
#eval toString $ { val := { val := 3, isLt := decide! } : UInt64 }
#eval (3 : UInt64).val
#eval toString $ { val := { val := 3, isLt := (match USize.size, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide!) } : USize }
#eval (3 : USize).val
#eval toString $ { val := { val := 4, isLt := decide! } : UInt8 }
#eval (4 : UInt8).val
#eval toString $ { val := { val := 4, isLt := decide! } : UInt16 }
#eval (4 : UInt16).val
#eval toString $ { val := { val := 4, isLt := decide! } : UInt32 }
#eval (4 : UInt32).val
#eval toString $ { val := { val := 4, isLt := decide! } : UInt64 }
#eval (4 : UInt64).val
#eval toString $ { val := { val := 4, isLt := (match USize.size, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide!) } : USize }
#eval (4 : USize).val

22
tests/lean/uintCtors.lean.expected.out Normal file
View file

@ -0,0 +1,22 @@
10
3
"3"
3
"3"
3
"3"
3
"3"
3
"3"
3
"4"
4
"4"
4
"4"
4
"4"
4
"4"
4