From bb0a0ceccead6afaafac531d80e7022b959aa585 Mon Sep 17 00:00:00 2001 From: Michael Morgan Date: Fri, 25 Aug 2017 22:02:20 -0500 Subject: [PATCH] add Interfaces.Correlatable interface --- libs/contrib/Interfaces/Correlatable.idr | 32 ++++++++++++++++++++++++ libs/contrib/contrib.ipkg | 1 + 2 files changed, 33 insertions(+) create mode 100644 libs/contrib/Interfaces/Correlatable.idr diff --git a/libs/contrib/Interfaces/Correlatable.idr b/libs/contrib/Interfaces/Correlatable.idr new file mode 100644 index 0000000000..bc2d353eb9 --- /dev/null +++ b/libs/contrib/Interfaces/Correlatable.idr @@ -0,0 +1,32 @@ +module Interfaces.Correlatable + +import Data.Vect + +%access public export +%default total + +interface Functor f => Correlatable (f : Type -> Type) where + correlateWith : (a -> b -> c) -> (a -> c) -> (b -> c) -> f a -> f b -> f c + +correlate : Correlatable f => f a -> f b -> f (Either (Either a b) (a, b)) +correlate xs ys = correlateWith (\x, y => Right (x, y)) + (\x => Left (Left x)) + (\y => Left (Right y)) + xs ys + +Correlatable List where + correlateWith f fx fy [] [] = [] + correlateWith f fx fy [] ys = map fy ys + correlateWith f fx fy xs [] = map fx xs + correlateWith f fx fy (x :: xs) (y :: ys) = f x y :: correlateWith f fx fy xs ys + +zipWith : (a -> b -> c) -> List a -> List b -> List c +zipWith f xs ys = map (uncurry f) (rights (correlate xs ys)) + + +Correlatable Stream where + correlateWith f fx fy (x :: xs) (y :: ys) = f x y :: correlateWith f fx fy xs ys + +Correlatable (Vect n) where + correlateWith f fx fy [] [] = [] + correlateWith f fx fy (x :: xs) (y :: ys) = f x y :: correlateWith f fx fy xs ys diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index ee0d7d8e19..bc27d47b63 100644 --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -11,6 +11,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory, Control.Pipeline, Control.ST, Control.ST.ImplicitCall, Control.ST.Exception, + Interfaces.Correlatable, Interfaces.Verified, Interfaces.Zippable,