Define wrap and unwrap.

1 files changed, 32 insertions, 0 deletions

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index c4a2acc..2c5d973 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -89,6 +89,38 @@ public export
 (++) []        ys = ys
 (++) (x :: xs) ys = x :: (xs ++ ys)
 
+public export
+wrap : (0 f : a -> b) -> (x . f) ^ is -> x ^ map f is
+wrap f []        = []
+wrap f (x :: xs) = x :: wrap f xs
+
+public export
+mapWrap : {0 f : IFunc x y} -> (0 g : a -> b) -> (xs : (x . g) ^ is)
+  -> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs)
+mapWrap g []        = Refl
+mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs
+
+public export
+unwrap : (0 f : a -> b) -> {is : _} -> x ^ map f is -> (x . f) ^ is
+unwrap f {is = []}        []        = []
+unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs
+
+public export
+mapUnwrap : {0 f : IFunc x y} -> (0 g : a -> b) -> {is : _} -> (xs : x ^ map g is)
+  -> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs)
+mapUnwrap g {is = []}        []        = Refl
+mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs
+
+public export
+unwrapWrap : (0 x : a -> Type) -> (xs : (x . f) ^ is) -> unwrap f (wrap {x} f xs) = xs
+unwrapWrap u []        = Refl
+unwrapWrap u (x :: xs) = cong ((::) x) $ unwrapWrap u xs
+
+public export
+wrapUnwrap : {is : _} -> (xs : x ^ map f is) -> wrap f {is} (unwrap f xs) = xs
+wrapUnwrap {is = []}        []        = Refl
+wrapUnwrap {is = (i :: is)} (x :: xs) = cong ((::) x) $ wrapUnwrap xs
+
 -- Relations
 
 namespace Pointwise