diff options
| author | Tom Smeding <t.j.smeding@uu.nl> | 2024-03-28 17:30:54 +0100 |
|---|---|---|
| committer | Tom Smeding <t.j.smeding@uu.nl> | 2024-03-28 17:30:54 +0100 |
| commit | 373799f36417c086510847e4d6689bd68582e658 (patch) | |
| tree | 72ac398279c2e8bc2162ffe77f6f054b4e0d2f77 /src/Array.hs | |
| parent | ae113c0249f3fe8be7df345081b1b51451cd3fdf (diff) | |
Various improvements
Diffstat (limited to 'src/Array.hs')
| -rw-r--r-- | src/Array.hs | 11 |
1 files changed, 11 insertions, 0 deletions
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) |