diff options
Diffstat (limited to 'src/Soat/Data')
| -rw-r--r-- | src/Soat/Data/Product.idr | 32 |
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 |