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

feat: expose new float/byte array primitives

Browse source
This commit is contained in:
Leonardo de Moura 2021-10-18 16:00:11 -07:00
parent 998bec0dd3
commit d03aaec944
2 changed files with 27 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Init/Data/ByteArray/Basic.lean
View file

@ -33,14 +33,30 @@ def push : ByteArray → UInt8 → ByteArray
def size : (@& ByteArray) → Nat
| ⟨bs⟩ => bs.size
@[extern "lean_byte_array_uget"]
def uget : (a : @& ByteArray) → (i : USize) → i.toNat < a.size → UInt8
| ⟨bs⟩, i, h => bs.uget i h
@[extern "lean_byte_array_get"]
def get! : (@& ByteArray) → (@& Nat) → UInt8
| ⟨bs⟩, i => bs.get! i
@[extern "lean_byte_array_fget"]
def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
| ⟨bs⟩, i => bs.get i
@[extern "lean_byte_array_set"]
def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
| ⟨bs⟩, i, b => ⟨bs.set! i b⟩
@[extern "lean_byte_array_fset"]
def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
| ⟨bs⟩, i, b => ⟨bs.set i b⟩
@[extern "lean_byte_array_uset"]
def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray
| ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
def isEmpty (s : ByteArray) : Bool :=
s.size == 0

16
src/Init/Data/FloatArray/Basic.lean
View file

@ -33,9 +33,12 @@ def push : FloatArray → Float → FloatArray
def size : (@& FloatArray) → Nat
| ⟨ds⟩ => ds.size
@[extern "lean_float_array_uget"]
def uget : (a : @& FloatArray) → (i : USize) → i.toNat < a.size → Float
| ⟨ds⟩, i, h => ds.uget i h
@[extern "lean_float_array_fget"]
def get (ds : @& FloatArray) (i : @& Fin ds.size) : Float :=
match ds, i with
def get : (ds : @& FloatArray) → (@& Fin ds.size) → Float
| ⟨ds⟩, i => ds.get i
@[extern "lean_float_array_get"]
@ -48,10 +51,13 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
else
none
@[extern "lean_float_array_uset"]
def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
| ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩
@[extern "lean_float_array_fset"]
def set (ds : FloatArray) (i : @& Fin ds.size) (d : Float) : FloatArray :=
match ds, i with
| ⟨ds⟩, i=> ⟨ds.set i d⟩
def set : (ds : FloatArray) → (@& Fin ds.size) → Float → FloatArray
| ⟨ds⟩, i, d => ⟨ds.set i d⟩
@[extern "lean_float_array_set"]
def set! : FloatArray → (@& Nat) → Float → FloatArray