module Generics.Pointless.Lenses.Examples.Recs where
import Generics.Pointless.Combinators
import Generics.Pointless.Functors
import Generics.Pointless.Lenses
import Generics.Pointless.Lenses.Combinators
innNat :: Either One Nat -> Nat
innNat (Left _) = Zero
innNat (Right n) = Succ n
outNat :: Nat -> Either One Nat
outNat Zero = Left _L
outNat (Succ n) = Right n
innNat_lns :: Lens (Either One Nat) Nat
innNat_lns = Lens innNat (outNat . fst) outNat
outNat_lns :: Lens Nat (Either One Nat)
outNat_lns = Lens outNat (innNat . fst) innNat
innMaybe :: Either One a -> Maybe a
innMaybe (Left _) = Nothing
innMaybe (Right x) = Just x
outMaybe :: Maybe a -> Either One a
outMaybe (Nothing) = Left _L
outMaybe (Just x) = Right x
innMaybe_lns :: Lens (Either One a) (Maybe a)
innMaybe_lns = Lens innMaybe (outMaybe . fst) outMaybe
outMaybe_lns :: Lens (Maybe a) (Either One a)
outMaybe_lns = Lens outMaybe (innMaybe . fst) innMaybe
innList :: Either One (a,[a]) -> [a]
innList (Left _) = []
innList (Right (x,xs)) = x:xs
outList :: [a] -> Either One (a,[a])
outList [] = Left _L
outList (x:xs) = Right (x,xs)
innList_lns :: Lens (Either One (a,[a])) [a]
innList_lns = Lens innList (outList . fst) outList
outList_lns :: Lens [a] (Either One (a,[a]))
outList_lns = Lens outList (innList . fst) innList
outNeList :: (NeList a b) -> Either a (b,NeList a b)
outNeList (NeNil a) = Left a
outNeList (NeCons b n) = Right (b,n)
innNeList :: Either a (b,NeList a b) -> NeList a b
innNeList (Left a) = NeNil a
innNeList (Right (b,n)) = NeCons b n
cataList :: (Either One (a,b) -> b) -> [a] -> b
cataList g [] = g $ Left _L
cataList g (x:xs) = g $ Right (x,cataList g xs)
anaList :: (b -> Either One (a,b)) -> b -> [a]
anaList g b = aux (g b)
where
aux (Left _L) = []
aux (Right (x,xs)) = x : anaList g xs
fmapList :: (x -> y) -> Either z (a,x) -> Either z (a,y)
fmapList f = id -|- id >< f
fmapNat :: (x -> y) -> Either a x -> Either a y
fmapNat f = id -|- f
fzipList :: (a -> c) -> (Either z (x,a),Either z (x,c)) -> Either z (x,(a,c))
fzipList f (Left z,_) = Left z
fzipList f (Right (x,a),Left _) = Right $ (x,(a,f a))
fzipList f (Right (x,a),Right (y,c)) = Right $ (x,(a,c))
fzipNat :: (a -> c) -> (Either z a,Either z c) -> Either z (a,c)
fzipNat f (Left z,_) = Left z
fzipNat f (Right a,Left _) = Right (a,f a)
fzipNat f (Right a,Right c) = Right (a,c)
cataList_lns :: (Lens (Either One (a,b)) b) -> Lens [a] b
cataList_lns g = Lens get' put' create'
where get' = cataList (get g)
create' = anaList (create g)
put' = anaList $ fzipList create' . (put g . (id >< fmapList get') /\ snd) . (id >< outList)
hyloList :: (Either x (y,c) -> c) -> (a -> Either x (y,a)) -> (a -> c)
hyloList g h = g . (id -|- id >< hyloList g h) . h
outNeNat :: NeNat a -> Either a (NeNat a)
outNeNat (NNil x) = Left x
outNeNat (NCons n) = Right n
data NeNat a = NNil a | NCons (NeNat a)
cataNeNat :: (Either a c -> c) -> NeNat a -> c
cataNeNat f (NNil x) = f (Left x)
cataNeNat f (NCons n) = f (Right $ cataNeNat f n)
anaNeNat :: (c -> Either a c) -> c -> NeNat a
anaNeNat f c = aux (f c)
where
aux (Left x) = NNil x
aux (Right n) = NCons (anaNeNat f n)
accumNeNat :: ((Either a y,x) -> y) -> ((Either a (NeNat a),x) -> Either a (NeNat a,x)) -> ((NeNat a,x) -> y)
accumNeNat g tau (NNil a,x) = g (Left a,x)
accumNeNat g tau (NCons ne,x) = g ((id -|- accumNeNat g tau) aux,x)
where aux = tau (Right ne,x)
cataNeNat_lns :: (Lens (Either a c) c) -> Lens (NeNat a) c
cataNeNat_lns f = Lens get' put' create'
where
get' = cataNeNat (get f)
create' = anaNeNat (create f)
put' = anaNeNat $ fzipNat create' . (put f . (id >< fmapNat get') /\ snd) . (id >< outNeNat)
anaNeNat_lns :: (Lens c (Either a c)) -> Lens c (NeNat a)
anaNeNat_lns g = Lens get' put' create'
where get' = anaNeNat (get g)
create' = cataNeNat (create g)
put' = accumNeNat (put g) (fzipNat create' . (id >< get g))
hyloNeNat_lns :: (Lens (Either x b) b) -> (Lens a (Either x a)) -> Lens a b
hyloNeNat_lns g h = cataNeNat_lns g .< anaNeNat_lns h
data NeList a b = NeNil a | NeCons b (NeList a b)
cataNeList :: (Either a (b,c) -> c) -> NeList a b -> c
cataNeList f (NeNil x) = f (Left x)
cataNeList f (NeCons x xs) = f (Right (x,cataNeList f xs))
anaNeList :: (c -> Either a (b,c)) -> c -> NeList a b
anaNeList f c = aux (f c)
where
aux (Left x) = NeNil x
aux (Right (x,xs)) = NeCons x (anaNeList f xs)
accumNeList :: ((Either a (b,y),x) -> y) -> ((Either a (b,NeList a b),x) -> Either a (b,(NeList a b,x))) -> ((NeList a b,x) -> y)
accumNeList g tau (NeNil a,x) = g (Left a,x)
accumNeList g tau (NeCons b ne,x) = g ((id -|- id >< accumNeList g tau) aux,x)
where aux = tau (Right (b,ne),x)
cataNeList_lns :: (Lens (Either a (b,c)) c) -> Lens (NeList a b) c
cataNeList_lns g = Lens get' put' create'
where get' = cataNeList (get g)
create' = anaNeList (create g )
put' = anaNeList $ fzipList create' . (put g . (id >< fmapList get') /\ snd) . (id >< outNeList)
anaNeList_lns :: (Lens c (Either a (b,c))) -> Lens c (NeList a b)
anaNeList_lns g = Lens get' put' create'
where get' = anaNeList (get g)
create' = cataNeList (create g)
put' = accumNeList (put g) (fzipList create' . (id >< get g))
hyloNeList_lns :: (Lens (Either x (y,b)) b) -> (Lens a (Either x (y,a))) -> Lens a b
hyloNeList_lns g h = cataNeList_lns g .< anaNeList_lns h
length_pf :: a -> Lens [a] Nat
length_pf v = cataList_lns (innNat_lns .< (id_lns -|-< snd_lns (v!)))
plus_pf :: Lens (Nat,Nat) Nat
plus_pf = hyloNeNat_lns f g
where f = innNat_lns .< (outNat_lns \/$< id_lns)
g = (snd_lns bang -|-< id_lns) .< distl_lns .< (outNat_lns ><< id_lns)
suml_pf :: Lens [Nat] Nat
suml_pf = cataList_lns (innNat_lns .< (id_lns #\/< (outNat_lns .< plus_pf)))
cat_pf :: Lens ([a],[a]) [a]
cat_pf = hyloNeList_lns g h
where g = innList_lns .< (outList_lns \/$< id_lns)
h = (snd_lns bang -|-< assocr_lns) .< distl_lns .< (outList_lns ><< id_lns)
concat_pf :: Lens [[a]] [a]
concat_pf = cataList_lns (innList_lns .< (id_lns #\/< (outList_lns .< cat_pf)))
map_pf :: Lens a b -> Lens [a] [b]
map_pf l = cataList_lns (innList_lns .< (id_lns -|-< l ><< id_lns))
filter_left_pf :: Lens [Either a b] [a]
filter_left_pf = cataList_lns ((innList_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< distl_lns))
filter_right_pf :: Lens [Either a b] [b]
filter_right_pf = cataList_lns ((innList_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< coswap_lns .< distl_lns))