From 3ca15ac2f6d7677dc07b7fbf9bd66f4bdbf81d75 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Wed, 8 Mar 2023 15:58:54 -0500 Subject: [PATCH] Document LArray a bit more --- src/Data/NumIdr/LArray.idr | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/src/Data/NumIdr/LArray.idr b/src/Data/NumIdr/LArray.idr index 1360e34..31df81a 100644 --- a/src/Data/NumIdr/LArray.idr +++ b/src/Data/NumIdr/LArray.idr @@ -7,22 +7,43 @@ import Data.NumIdr.Array %default total +||| An array type that is guaranteed to be unique through linear types. +||| +||| This type can be used to operate on an array value without it being copied +||| on every mutation. export data LArray : Vect rk Nat -> Type -> Type where MkLArray : (ord : Order) -> (sts : Vect rk Nat) -> (s : Vect rk Nat) -> PrimArray a -> LArray s a +||| A vector that is guaranteed to be unique through linear types. +export +LVector : Nat -> Type -> Type +LVector n = LArray [n] + +||| A matrix that is guaranteed to be unique through linear types. +export +LMatrix : (m, n : Nat) -> Type -> Type +LMatrix m n = LArray [m,n] + +||| A matrix that is guaranteed to be unique through linear types. +export +LMatrix' : Nat -> Type -> Type +LMatrix' n = LArray [n,n] + + thaw : Array s a -> LArray s a thaw {s} arr with (viewShape arr) _ | Shape s = MkLArray (getOrder arr) (strides arr) s (getPrim arr) +||| Freeze a linear array into an immutable array. export freeze : (1 _ : LArray s a) -> Array s a freeze (MkLArray ord sts s arr) = unsafeMkArray ord sts s arr -------------------------------------------------------------------------------- --- Constructor +-- Constructors --------------------------------------------------------------------------------