{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} module Data.RAVec.NonEmpty.Optics.Internal where import Control.Applicative ((<$>)) import Data.BinP.PosP (PosP (..), PosP' (..)) import Data.RAVec.Tree (Tree (..)) import Data.Wrd (Wrd (..)) import Prelude (Functor) import Data.RAVec.NonEmpty type LensLikeVL f s t a b = (a -> f b) -> s -> f t type LensLikeVL' f s a = LensLikeVL f s s a a ixVL :: Functor f => PosP b -> LensLikeVL' f (NERAVec b a) a ixVL :: PosP b -> LensLikeVL' f (NERAVec b a) a ixVL (PosP PosP' 'Z b i) a -> f a f (NE NERAVec' 'Z b a xs) = NERAVec' 'Z b a -> NERAVec b a forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a NE (NERAVec' 'Z b a -> NERAVec b a) -> f (NERAVec' 'Z b a) -> f (NERAVec b a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> PosP' 'Z b -> LensLikeVL' f (NERAVec' 'Z b a) a forall (f :: * -> *) (n :: Nat) (b :: BinP) a. Functor f => PosP' n b -> LensLikeVL' f (NERAVec' n b a) a ixVL' PosP' 'Z b i a -> f a f NERAVec' 'Z b a xs ixVL' :: Functor f => PosP' n b -> LensLikeVL' f (NERAVec' n b a) a ixVL' :: PosP' n b -> LensLikeVL' f (NERAVec' n b a) a ixVL' (AtEnd Wrd n i) a -> f a f (Last Tree n a t) = Tree n a -> NERAVec' n 'BE a forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a Last (Tree n a -> NERAVec' n 'BE a) -> f (Tree n a) -> f (NERAVec' n 'BE a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Wrd n -> LensLikeVL' f (Tree n a) a forall (f :: * -> *) (n :: Nat) a. Functor f => Wrd n -> LensLikeVL' f (Tree n a) a treeIxVL Wrd n i a -> f a f Tree n a t ixVL' (There0 PosP' ('S n) b1 i) a -> f a f (Cons0 NERAVec' ('S n) b1 a r) = NERAVec' ('S n) b1 a -> NERAVec' n ('B0 b1) a forall (n :: Nat) (b1 :: BinP) a. NERAVec' ('S n) b1 a -> NERAVec' n ('B0 b1) a Cons0 (NERAVec' ('S n) b1 a -> NERAVec' n ('B0 b1) a) -> f (NERAVec' ('S n) b1 a) -> f (NERAVec' n ('B0 b1) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> PosP' ('S n) b1 -> LensLikeVL' f (NERAVec' ('S n) b1 a) a forall (f :: * -> *) (n :: Nat) (b :: BinP) a. Functor f => PosP' n b -> LensLikeVL' f (NERAVec' n b a) a ixVL' PosP' ('S n) b1 i a -> f a f NERAVec' ('S n) b1 a NERAVec' ('S n) b1 a r ixVL' (There1 PosP' ('S n) b1 i) a -> f a f (Cons1 Tree n a t NERAVec' ('S n) b1 a r) = (Tree n a t Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a forall (n :: Nat) a (b1 :: BinP). Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a `Cons1`) (NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a) -> f (NERAVec' ('S n) b1 a) -> f (NERAVec' n ('B1 b1) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> PosP' ('S n) b1 -> LensLikeVL' f (NERAVec' ('S n) b1 a) a forall (f :: * -> *) (n :: Nat) (b :: BinP) a. Functor f => PosP' n b -> LensLikeVL' f (NERAVec' n b a) a ixVL' PosP' ('S n) b1 i a -> f a f NERAVec' ('S n) b1 a NERAVec' ('S n) b1 a r ixVL' (Here Wrd n i) a -> f a f (Cons1 Tree n a t NERAVec' ('S n) b1 a r) = (Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a forall (n :: Nat) a (b1 :: BinP). Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a `Cons1` NERAVec' ('S n) b1 a r) (Tree n a -> NERAVec' n ('B1 b1) a) -> f (Tree n a) -> f (NERAVec' n ('B1 b1) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Wrd n -> LensLikeVL' f (Tree n a) a forall (f :: * -> *) (n :: Nat) a. Functor f => Wrd n -> LensLikeVL' f (Tree n a) a treeIxVL Wrd n i a -> f a f Tree n a t treeIxVL :: Functor f => Wrd n -> LensLikeVL' f (Tree n a) a treeIxVL :: Wrd n -> LensLikeVL' f (Tree n a) a treeIxVL Wrd n WE a -> f a f (Leaf a x) = a -> Tree 'Z a forall a. a -> Tree 'Z a Leaf (a -> Tree 'Z a) -> f a -> f (Tree 'Z a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> f a f a x treeIxVL (W0 Wrd n1 is) a -> f a f (Node Tree n1 a x Tree n1 a y) = (Tree n1 a -> Tree n1 a -> Tree ('S n1) a forall (n1 :: Nat) a. Tree n1 a -> Tree n1 a -> Tree ('S n1) a `Node` Tree n1 a y) (Tree n1 a -> Tree ('S n1) a) -> f (Tree n1 a) -> f (Tree ('S n1) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Wrd n1 -> LensLikeVL' f (Tree n1 a) a forall (f :: * -> *) (n :: Nat) a. Functor f => Wrd n -> LensLikeVL' f (Tree n a) a treeIxVL Wrd n1 is a -> f a f Tree n1 a Tree n1 a x treeIxVL (W1 Wrd n1 is) a -> f a f (Node Tree n1 a x Tree n1 a y) = (Tree n1 a x Tree n1 a -> Tree n1 a -> Tree ('S n1) a forall (n1 :: Nat) a. Tree n1 a -> Tree n1 a -> Tree ('S n1) a `Node`) (Tree n1 a -> Tree ('S n1) a) -> f (Tree n1 a) -> f (Tree ('S n1) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Wrd n1 -> LensLikeVL' f (Tree n1 a) a forall (f :: * -> *) (n :: Nat) a. Functor f => Wrd n -> LensLikeVL' f (Tree n a) a treeIxVL Wrd n1 is a -> f a f Tree n1 a Tree n1 a y