/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Data.Array.Basic
import Init.Data.Float
import Init.Data.Option.Basic
universes u

structure FloatArray :=
(data : Array Float)

attribute [extern "lean_float_array_mk"] FloatArray.mk
attribute [extern "lean_float_array_data"] FloatArray.data

namespace FloatArray
@[extern "lean_mk_empty_float_array"]
def mkEmpty (c : @& Nat) : FloatArray :=
{ data := #[] }

def empty : FloatArray :=
mkEmpty 0

instance : Inhabited FloatArray :=
⟨empty⟩

@[extern "lean_float_array_push"]
def push : FloatArray → Float → FloatArray
| ⟨ds⟩, b => ⟨ds.push b⟩

@[extern "lean_float_array_size"]
def size : (@& FloatArray) → Nat
| ⟨ds⟩ => ds.size

@[extern "lean_float_array_fget"]
def get (ds : @& FloatArray) (i : @& Fin ds.size) : Float :=
match ds, i with
| ⟨ds⟩, i => ds.get i

@[extern "lean_float_array_get"]
def get! : (@& FloatArray) → (@& Nat) → Float
| ⟨ds⟩, i => ds.get! i

def get? (ds : FloatArray) (i : Nat) : Option Float :=
if h : i < ds.size then
  ds.get ⟨i, h⟩
else
  none

@[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⟩

@[extern "lean_float_array_set"]
def set! : FloatArray → (@& Nat) → Float → FloatArray
| ⟨ds⟩, i, d => ⟨ds.set! i d⟩

def isEmpty (s : FloatArray) : Bool :=
s.size == 0

partial def toListAux (ds : FloatArray) : Nat → List Float → List Float
| i, r =>
  if h : i < ds.size then
    toListAux (i+1) (ds.get ⟨i, h⟩ :: r)
  else
    r.reverse

def toList (ds : FloatArray) : List Float :=
toListAux ds 0 []

end FloatArray

def List.toFloatArrayAux : List Float → FloatArray → FloatArray
| [],    r => r
| b::ds, r => List.toFloatArrayAux ds (r.push b)

def List.toFloatArray (ds : List Float) : FloatArray :=
ds.toFloatArrayAux FloatArray.empty

instance : HasToString FloatArray :=
⟨fun ds => ds.toList.toString⟩