D2[Array] now has a Maybe instead of zero-size for zero

Remaining problem: 'add' in Compile doesn't use the D2 stuff

1 files changed, 5 insertions, 0 deletions

diff --git a/src/Data.hs b/src/Data.hs
index 60afdd0..e7b3148 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -11,6 +11,7 @@
 module Data (module Data, (:~:)(Refl)) where
 
 import Data.Functor.Product
+import Data.Some
 import Data.Type.Equality
 import Unsafe.Coerce (unsafeCoerce)
 
@@ -85,6 +86,10 @@ unSNat :: SNat n -> Nat
 unSNat SZ = Z
 unSNat (SS n) = S (unSNat n)
 
+reSNat :: Nat -> Some SNat
+reSNat Z = Some SZ
+reSNat (S n) | Some n' <- reSNat n = Some (SS n')
+
 fromNat :: Nat -> Int
 fromNat Z = 0
 fromNat (S m) = succ (fromNat m)