From 1e7660b1f253760cb5c5a6a13e1244b2448e2bd5 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 20 May 2022 10:53:29 -0400 Subject: [PATCH] Create Show instance for Array --- src/Data/NumIdr/Array/Array.idr | 33 ++++++++++++++++++++++++++++----- 1 file changed, 28 insertions(+), 5 deletions(-) diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 8e2f4b7..361c856 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -1,5 +1,6 @@ module Data.NumIdr.Array.Array +import Data.List import Data.List1 import Data.Vect import Data.Zippable @@ -259,10 +260,6 @@ display = printLn . PrimArray.toList . getPrim -- reordered to match one. -export -Functor (Array s) where - map f (MkArray ord sts s arr) = MkArray ord sts s (map f arr) - export Zippable (Array s) where zipWith f a b = rewrite shapeEq a @@ -289,6 +286,10 @@ Zippable (Array s) where MkArray (getOrder arr) (strides arr) _ b, MkArray (getOrder arr) (strides arr) _ c) +export +Functor (Array s) where + map f (MkArray ord sts s arr) = MkArray ord sts s (map f arr) + export {s : _} -> Applicative (Array s) where pure = constant s @@ -329,12 +330,34 @@ export {s : _} -> Monoid a => Monoid (Array s a) where neutral = constant s neutral - -- the shape must be known at runtime due to `fromInteger`. If `fromInteger` -- were moved into its own interface, this constraint could be removed. + +export {s : _} -> Num a => Num (Array s a) where (+) = zipWith (+) (*) = zipWith (*) fromInteger = constant s . fromInteger + +export +Show a => Show (Array s a) where + showPrec d arr = let orderedElems = PrimArray.toList $ getPrim $ + if getOrder arr == COrder then arr else reorder COrder arr + in showCon d "array " $ concat $ insertPunct (shape arr) $ map show orderedElems + where + splitWindow : Nat -> List String -> List (List String) + splitWindow n xs = case splitAt n xs of + (xs, []) => [xs] + (l1, l2) => l1 :: splitWindow n (assert_smaller xs l2) + + insertPunct : Vect rk Nat -> List String -> List String + insertPunct [] strs = strs + insertPunct [d] strs = "[" :: intersperse ", " strs `snoc` "]" + insertPunct (Z :: s) strs = ["[","]"] + insertPunct (d :: s) strs = + let secs = if null strs + then List.replicate d ("[]" :: Prelude.Nil) + else map (insertPunct s) $ splitWindow (length strs `div` d) strs + in "[" :: (concat $ intersperse [", "] secs) `snoc` "]"