From 373799f36417c086510847e4d6689bd68582e658 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Thu, 28 Mar 2024 17:30:54 +0100 Subject: Various improvements --- src/Array.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/Array.hs') diff --git a/src/Array.hs b/src/Array.hs index 29806d4..693df05 100644 --- a/src/Array.hs +++ b/src/Array.hs @@ -145,6 +145,11 @@ lemKnownNatRank IZX = Dict lemKnownNatRank (_ ::@ sh) | Dict <- lemKnownNatRank sh = Dict lemKnownNatRank (_ ::? sh) | Dict <- lemKnownNatRank sh = Dict +lemKnownNatRankSSX :: StaticShapeX sh -> Dict KnownNat (Rank sh) +lemKnownNatRankSSX SZX = Dict +lemKnownNatRankSSX (_ :$@ ssh) | Dict <- lemKnownNatRankSSX ssh = Dict +lemKnownNatRankSSX (_ :$? ssh) | Dict <- lemKnownNatRankSSX ssh = Dict + lemKnownShapeX :: StaticShapeX sh -> Dict KnownShapeX sh lemKnownShapeX SZX = Dict lemKnownShapeX (n :$@ ssh) | Dict <- lemKnownShapeX ssh, Dict <- snatKnown n = Dict @@ -196,3 +201,9 @@ index xarr i | Refl <- lemAppNil @sh = let XArray arr' = indexPartial xarr i :: XArray '[] a in U.unScalar arr' + +append :: forall sh a. (KnownShapeX sh, U.Unbox a) => XArray sh a -> XArray sh a -> XArray sh a +append (XArray a) (XArray b) + | Dict <- lemKnownNatRankSSX (knownShapeX @sh) + , Dict <- gknownNat (Proxy @(Rank sh)) + = XArray (U.append a b) -- cgit v1.2.3-70-g09d2