{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE EmptyCase            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Intended for qualified import
--
-- > import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Telescope as Telescope
module Ouroboros.Consensus.HardFork.Combinator.Util.Telescope (
    -- * Telescope
    Telescope (..)
  , sequence
    -- ** Utilities
  , fromTZ
  , fromTip
  , tip
  , toAtMost
    -- ** Bifunctor analogues of SOP functions
  , bihap
  , bihczipWith
  , bihmap
  , bihzipWith
    -- * Extension, retraction, alignment
  , Extend (..)
  , Retract (..)
  , align
  , extend
  , retract
    -- ** Simplified API
  , alignExtend
  , alignExtendNS
  , extendIf
  , retractIf
    -- * Additional API
  , ScanNext (..)
  , SimpleTelescope (..)
  , scanl
  ) where

import           Prelude hiding (scanl, sequence, zipWith)

import           Data.Functor.Product
import           Data.Kind
import           Data.SOP.Strict
import           GHC.Stack
import           NoThunks.Class (NoThunks (..), allNoThunks)

import           Ouroboros.Consensus.Util.Counting
import           Ouroboros.Consensus.Util.SOP

import           Ouroboros.Consensus.HardFork.Combinator.Util.InPairs
                     (InPairs (..), Requiring (..))
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.InPairs as InPairs
import           Ouroboros.Consensus.HardFork.Combinator.Util.Tails (Tails (..))
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Tails as Tails

{-------------------------------------------------------------------------------
  Telescope
-------------------------------------------------------------------------------}

-- | Telescope
--
-- A telescope is an extension of an 'NS', where every time we "go right" in the
-- sum we have an additional value.
--
-- Blockchain intuition: think of @g@ as representing some kind of past state,
-- and @f@ some kind of current state. Then depending on how many hard fork
-- transitions we have had, we might either have, say
--
-- > TZ currentByronState
-- > TS pastByronState $ TZ currentShelleyState
-- > TS pastByronState $ TS pastShelleyState $ TZ currentGoguenState
--
-- The 'Telescope' API mostly follows @sop-core@ conventions, supporting
-- functor ('hmap', 'hcmap'), applicative ('hap', 'hpure'), foldable
-- ('hcollapse') and traversable ('hsequence''). However, since 'Telescope'
-- is a bi-functor, it cannot reuse the @sop-core@ classes. The naming scheme
-- of the functions is adopted from @sop-core@ though; for example:
--
-- > bi h (c) zipWith
-- > |  |  |    |
-- > |  |  |    \ zipWith: the name from base
-- > |  |  |
-- > |  |  \ constrained: version of the function with a constraint parameter
-- > |  |
-- > |  \ higher order: 'Telescope' (like 'NS'/'NP') is a /higher order/ functor
-- > |
-- > \ bifunctor: 'Telescope' (unlike 'NS'/'NP') is a higher order /bifunctor/
--
-- In addition to the standard SOP operators, the new operators that make
-- a 'Telescope' a telescope are 'extend', 'retract' and 'align'; see their
-- documentation for details.
data Telescope (g :: k -> Type) (f :: k -> Type) (xs :: [k]) where
  TZ :: !(f x) ->                        Telescope g f (x ': xs)
  TS :: !(g x) -> !(Telescope g f xs) -> Telescope g f (x ': xs)

{-------------------------------------------------------------------------------
  SOP class instances for 'Telescope'
-------------------------------------------------------------------------------}

type instance Prod    (Telescope g)   = NP
type instance SListIN (Telescope g)   = SListI
type instance AllN    (Telescope g) c = All c

instance HAp (Telescope g) where
  hap :: Prod (Telescope g) (f -.-> g) xs
-> Telescope g f xs -> Telescope g g xs
hap = (Telescope g f xs -> NP (f -.-> g) xs -> Telescope g g xs)
-> NP (f -.-> g) xs -> Telescope g f xs -> Telescope g g xs
forall a b c. (a -> b -> c) -> b -> a -> c
flip Telescope g f xs -> NP (f -.-> g) xs -> Telescope g g xs
forall (f :: k -> *) (xs :: [k]) (f' :: k -> *).
Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs
go
    where
      -- We could define this in terms of 'bihap' but we lack 'SListI'
      go :: Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs
      go :: Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs
go (TZ f x
fx)   ((-.->) f f' x
f :* NP (f -.-> f') xs
_)  = f' x -> Telescope g f' (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ ((-.->) f f' x -> f x -> f' x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) f f' x
f f x
f x
fx)
      go (TS g x
gx Telescope g f xs
t) ((-.->) f f' x
_ :* NP (f -.-> f') xs
fs) = g x -> Telescope g f' xs -> Telescope g f' (x : xs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
gx (Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs
forall (f :: k -> *) (xs :: [k]) (f' :: k -> *).
Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs
go Telescope g f xs
t NP (f -.-> f') xs
NP (f -.-> f') xs
fs)

instance HTraverse_ (Telescope g) where
  hctraverse_ :: proxy c
-> (forall (a :: k). c a => f a -> g ())
-> Telescope g f xs
-> g ()
hctraverse_ proxy c
p = proxy c
-> (forall (x :: k). c x => g x -> g ())
-> (forall (a :: k). c a => f a -> g ())
-> Telescope g f xs
-> g ()
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *).
(All c xs, Applicative m) =>
proxy c
-> (forall (x :: k). c x => g x -> m ())
-> (forall (x :: k). c x => f x -> m ())
-> Telescope g f xs
-> m ()
bihctraverse_ proxy c
p (\g x
_ -> () -> g ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  htraverse_ :: (forall (a :: k). f a -> g ()) -> Telescope g f xs -> g ()
htraverse_    = (forall (x :: k). g x -> g ())
-> (forall (a :: k). f a -> g ()) -> Telescope g f xs -> g ()
forall k (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *).
(SListI xs, Applicative m) =>
(forall (x :: k). g x -> m ())
-> (forall (x :: k). f x -> m ()) -> Telescope g f xs -> m ()
bihtraverse_    (\g x
_ -> () -> g ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

instance HSequence (Telescope g) where
  hsequence' :: Telescope g (f :.: g) xs -> f (Telescope g g xs)
hsequence'    = Telescope (f :.: g) (f :.: g) xs -> f (Telescope g g xs)
forall k (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]).
(SListI xs, Applicative m) =>
Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs)
bihsequence' (Telescope (f :.: g) (f :.: g) xs -> f (Telescope g g xs))
-> (Telescope g (f :.: g) xs -> Telescope (f :.: g) (f :.: g) xs)
-> Telescope g (f :.: g) xs
-> f (Telescope g g xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: k). g x -> (:.:) f g x)
-> (forall (x :: k). (:.:) f g x -> (:.:) f g x)
-> Telescope g (f :.: g) xs
-> Telescope (f :.: g) (f :.: g) xs
forall k (xs :: [k]) (g :: k -> *) (g' :: k -> *) (f :: k -> *)
       (f' :: k -> *).
SListI xs =>
(forall (x :: k). g x -> g' x)
-> (forall (x :: k). f x -> f' x)
-> Telescope g f xs
-> Telescope g' f' xs
bihmap (f (g x) -> (:.:) f g x
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (f (g x) -> (:.:) f g x) -> (g x -> f (g x)) -> g x -> (:.:) f g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> f (g x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure) forall (x :: k). (:.:) f g x -> (:.:) f g x
forall a. a -> a
id
  hctraverse' :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> Telescope g f xs
-> g (Telescope g f' xs)
hctraverse' proxy c
p = proxy c
-> (forall (x :: k). c x => g x -> g (g x))
-> (forall (a :: k). c a => f a -> g (f' a))
-> Telescope g f xs
-> g (Telescope g f' xs)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *)
       (f' :: k -> *) (xs :: [k]).
(All c xs, Applicative m) =>
proxy c
-> (forall (x :: k). c x => g x -> m (g' x))
-> (forall (x :: k). c x => f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
bihctraverse' proxy c
p forall (x :: k). c x => g x -> g (g x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  htraverse' :: (forall (a :: k). f a -> g (f' a))
-> Telescope g f xs -> g (Telescope g f' xs)
htraverse'    = (forall (x :: k). g x -> g (g x))
-> (forall (a :: k). f a -> g (f' a))
-> Telescope g f xs
-> g (Telescope g f' xs)
forall k (xs :: [k]) (m :: * -> *) (g :: k -> *) (g' :: k -> *)
       (f :: k -> *) (f' :: k -> *).
(SListI xs, Applicative m) =>
(forall (x :: k). g x -> m (g' x))
-> (forall (x :: k). f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
bihtraverse'    forall (x :: k). g x -> g (g x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Specialization of 'hsequence'' with weaker constraints
-- ('Functor' rather than 'Applicative')
sequence :: forall m g f xs. Functor m
         => Telescope g (m :.: f) xs -> m (Telescope g f xs)
sequence :: Telescope g (m :.: f) xs -> m (Telescope g f xs)
sequence = Telescope g (m :.: f) xs -> m (Telescope g f xs)
forall (xs' :: [k]).
Telescope g (m :.: f) xs' -> m (Telescope g f xs')
go
  where
    go :: Telescope g (m :.: f) xs' -> m (Telescope g f xs')
    go :: Telescope g (m :.: f) xs' -> m (Telescope g f xs')
go (TZ (Comp m (f x)
fx)) = f x -> Telescope g f (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ (f x -> Telescope g f (x : xs))
-> m (f x) -> m (Telescope g f (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (f x)
fx
    go (TS g x
gx Telescope g (m :.: f) xs
t)      = g x -> Telescope g f xs -> Telescope g f (x : xs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
gx (Telescope g f xs -> Telescope g f (x : xs))
-> m (Telescope g f xs) -> m (Telescope g f (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope g (m :.: f) xs -> m (Telescope g f xs)
forall (xs' :: [k]).
Telescope g (m :.: f) xs' -> m (Telescope g f xs')
go Telescope g (m :.: f) xs
t

{-------------------------------------------------------------------------------
  Bifunctor analogues of class methods
-------------------------------------------------------------------------------}

-- | Bifunctor analogue of 'hap'
bihap :: NP (g -.-> g') xs
      -> NP (f -.-> f') xs
      -> Telescope g f xs -> Telescope g' f' xs
bihap :: NP (g -.-> g') xs
-> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
bihap = \NP (g -.-> g') xs
gs NP (f -.-> f') xs
fs Telescope g f xs
t -> Telescope g f xs
-> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs
forall k (g :: k -> *) (f :: k -> *) (xs :: [k]) (g' :: k -> *)
       (f' :: k -> *).
Telescope g f xs
-> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs
go Telescope g f xs
t NP (g -.-> g') xs
gs NP (f -.-> f') xs
fs
  where
    go :: Telescope g f xs
       -> NP (g -.-> g') xs
       -> NP (f -.-> f') xs
       -> Telescope g' f' xs
    go :: Telescope g f xs
-> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs
go (TZ f x
fx)   NP (g -.-> g') xs
_         ((-.->) f f' x
f :* NP (f -.-> f') xs
_)  = f' x -> Telescope g' f' (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ ((-.->) f f' x -> f x -> f' x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) f f' x
f f x
f x
fx)
    go (TS g x
gx Telescope g f xs
t) ((-.->) g g' x
g :* NP (g -.-> g') xs
gs) ((-.->) f f' x
_ :* NP (f -.-> f') xs
fs) = g' x -> Telescope g' f' xs -> Telescope g' f' (x : xs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS ((-.->) g g' x -> g x -> g' x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) g g' x
g g x
g x
gx) (Telescope g f xs
-> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs
forall k (g :: k -> *) (f :: k -> *) (xs :: [k]) (g' :: k -> *)
       (f' :: k -> *).
Telescope g f xs
-> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs
go Telescope g f xs
t NP (g -.-> g') xs
NP (g -.-> g') xs
gs NP (f -.-> f') xs
NP (f -.-> f') xs
fs)

-- | Bifunctor analogue of 'hctraverse''
bihctraverse' :: forall proxy c m g g' f f' xs. (All c xs, Applicative m)
              => proxy c
              -> (forall x. c x => g x -> m (g' x))
              -> (forall x. c x => f x -> m (f' x))
              -> Telescope g f xs -> m (Telescope g' f' xs)
bihctraverse' :: proxy c
-> (forall (x :: k). c x => g x -> m (g' x))
-> (forall (x :: k). c x => f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
bihctraverse' proxy c
_ forall (x :: k). c x => g x -> m (g' x)
g forall (x :: k). c x => f x -> m (f' x)
f = Telescope g f xs -> m (Telescope g' f' xs)
forall (xs' :: [k]).
All c xs' =>
Telescope g f xs' -> m (Telescope g' f' xs')
go
  where
    go :: All c xs' => Telescope g f xs' -> m (Telescope g' f' xs')
    go :: Telescope g f xs' -> m (Telescope g' f' xs')
go (TZ f x
fx)   = f' x -> Telescope g' f' (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ (f' x -> Telescope g' f' (x : xs))
-> m (f' x) -> m (Telescope g' f' (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> m (f' x)
forall (x :: k). c x => f x -> m (f' x)
f f x
fx
    go (TS g x
gx Telescope g f xs
t) = g' x -> Telescope g' f' xs -> Telescope g' f' (x : xs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS (g' x -> Telescope g' f' xs -> Telescope g' f' (x : xs))
-> m (g' x) -> m (Telescope g' f' xs -> Telescope g' f' (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g x -> m (g' x)
forall (x :: k). c x => g x -> m (g' x)
g g x
gx m (Telescope g' f' xs -> Telescope g' f' (x : xs))
-> m (Telescope g' f' xs) -> m (Telescope g' f' (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Telescope g f xs -> m (Telescope g' f' xs)
forall (xs' :: [k]).
All c xs' =>
Telescope g f xs' -> m (Telescope g' f' xs')
go Telescope g f xs
t

-- | Bifunctor analogue of 'htraverse''
bihtraverse' :: (SListI xs, Applicative m)
             => (forall x. g x -> m (g' x))
             -> (forall x. f x -> m (f' x))
             -> Telescope g f xs -> m (Telescope g' f' xs)
bihtraverse' :: (forall (x :: k). g x -> m (g' x))
-> (forall (x :: k). f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
bihtraverse' = Proxy Top
-> (forall (x :: k). Top x => g x -> m (g' x))
-> (forall (x :: k). Top x => f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *)
       (f' :: k -> *) (xs :: [k]).
(All c xs, Applicative m) =>
proxy c
-> (forall (x :: k). c x => g x -> m (g' x))
-> (forall (x :: k). c x => f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
bihctraverse' (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

-- | Bifunctor analogue of 'hsequence''
bihsequence' :: forall m g f xs. (SListI xs, Applicative m)
             => Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs)
bihsequence' :: Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs)
bihsequence' = (forall (x :: k). (:.:) m g x -> m (g x))
-> (forall (x :: k). (:.:) m f x -> m (f x))
-> Telescope (m :.: g) (m :.: f) xs
-> m (Telescope g f xs)
forall k (xs :: [k]) (m :: * -> *) (g :: k -> *) (g' :: k -> *)
       (f :: k -> *) (f' :: k -> *).
(SListI xs, Applicative m) =>
(forall (x :: k). g x -> m (g' x))
-> (forall (x :: k). f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
bihtraverse' forall (x :: k). (:.:) m g x -> m (g x)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp forall (x :: k). (:.:) m f x -> m (f x)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp

-- | Bifunctor analogue of 'hctraverse_'
bihctraverse_ :: forall proxy c xs m g f. (All c xs, Applicative m)
              => proxy c
              -> (forall x. c x => g x -> m ())
              -> (forall x. c x => f x -> m ())
              -> Telescope g f xs -> m ()
bihctraverse_ :: proxy c
-> (forall (x :: k). c x => g x -> m ())
-> (forall (x :: k). c x => f x -> m ())
-> Telescope g f xs
-> m ()
bihctraverse_ proxy c
_ forall (x :: k). c x => g x -> m ()
g forall (x :: k). c x => f x -> m ()
f = Telescope g f xs -> m ()
forall (xs' :: [k]). All c xs' => Telescope g f xs' -> m ()
go
  where
    go :: All c xs' => Telescope g f xs' -> m ()
    go :: Telescope g f xs' -> m ()
go (TZ f x
fx)   = f x -> m ()
forall (x :: k). c x => f x -> m ()
f f x
fx
    go (TS g x
gx Telescope g f xs
t) = g x -> m ()
forall (x :: k). c x => g x -> m ()
g g x
gx m () -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Telescope g f xs -> m ()
forall (xs' :: [k]). All c xs' => Telescope g f xs' -> m ()
go Telescope g f xs
t

bihtraverse_ :: (SListI xs, Applicative m)
             => (forall x. g x -> m ())
             -> (forall x. f x -> m ())
             -> Telescope g f xs -> m ()
bihtraverse_ :: (forall (x :: k). g x -> m ())
-> (forall (x :: k). f x -> m ()) -> Telescope g f xs -> m ()
bihtraverse_ = Proxy Top
-> (forall (x :: k). Top x => g x -> m ())
-> (forall (x :: k). Top x => f x -> m ())
-> Telescope g f xs
-> m ()
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *).
(All c xs, Applicative m) =>
proxy c
-> (forall (x :: k). c x => g x -> m ())
-> (forall (x :: k). c x => f x -> m ())
-> Telescope g f xs
-> m ()
bihctraverse_ (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

{-------------------------------------------------------------------------------
  Bifunctor analogues of derived functions
-------------------------------------------------------------------------------}

-- | Bifunctor analogue of 'hmap'
bihmap :: SListI xs
       => (forall x. g x -> g' x)
       -> (forall x. f x -> f' x)
       -> Telescope g f xs -> Telescope g' f' xs
bihmap :: (forall (x :: k). g x -> g' x)
-> (forall (x :: k). f x -> f' x)
-> Telescope g f xs
-> Telescope g' f' xs
bihmap = Proxy Top
-> (forall (x :: k). Top x => g x -> g' x)
-> (forall (x :: k). Top x => f x -> f' x)
-> Telescope g f xs
-> Telescope g' f' xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (g :: k -> *) (g' :: k -> *)
       (f :: k -> *) (f' :: k -> *).
All c xs =>
proxy c
-> (forall (x :: k). c x => g x -> g' x)
-> (forall (x :: k). c x => f x -> f' x)
-> Telescope g f xs
-> Telescope g' f' xs
bihcmap (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

-- | Bifunctor analogue of 'hcmap'
bihcmap :: All c xs
        => proxy c
        -> (forall x. c x => g x -> g' x)
        -> (forall x. c x => f x -> f' x)
        -> Telescope g f xs -> Telescope g' f' xs
bihcmap :: proxy c
-> (forall (x :: k). c x => g x -> g' x)
-> (forall (x :: k). c x => f x -> f' x)
-> Telescope g f xs
-> Telescope g' f' xs
bihcmap proxy c
p forall (x :: k). c x => g x -> g' x
g forall (x :: k). c x => f x -> f' x
f = NP (g -.-> g') xs
-> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
forall k (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *)
       (f' :: k -> *).
NP (g -.-> g') xs
-> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
bihap (proxy c
-> (forall (a :: k). c a => (-.->) g g' a) -> NP (g -.-> g') xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure proxy c
p ((g a -> g' a) -> (-.->) g g' a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn g a -> g' a
forall (x :: k). c x => g x -> g' x
g)) (proxy c
-> (forall (a :: k). c a => (-.->) f f' a) -> NP (f -.-> f') xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure proxy c
p ((f a -> f' a) -> (-.->) f f' a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn f a -> f' a
forall (x :: k). c x => f x -> f' x
f))

-- | Bifunctor equivalent of 'hzipWith'
bihzipWith :: SListI xs
           => (forall x. h x -> g x -> g' x)
           -> (forall x. h x -> f x -> f' x)
           -> NP h xs -> Telescope g f xs -> Telescope g' f' xs
bihzipWith :: (forall (x :: k). h x -> g x -> g' x)
-> (forall (x :: k). h x -> f x -> f' x)
-> NP h xs
-> Telescope g f xs
-> Telescope g' f' xs
bihzipWith forall (x :: k). h x -> g x -> g' x
g forall (x :: k). h x -> f x -> f' x
f NP h xs
ns = NP (g -.-> g') xs
-> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
forall k (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *)
       (f' :: k -> *).
NP (g -.-> g') xs
-> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
bihap ((forall (a :: k). h a -> (-.->) g g' a)
-> NP h xs -> NP (g -.-> g') xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap ((g a -> g' a) -> (-.->) g g' a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn ((g a -> g' a) -> (-.->) g g' a)
-> (h a -> g a -> g' a) -> h a -> (-.->) g g' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h a -> g a -> g' a
forall (x :: k). h x -> g x -> g' x
g) NP h xs
ns) ((forall (a :: k). h a -> (-.->) f f' a)
-> NP h xs -> NP (f -.-> f') xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap ((f a -> f' a) -> (-.->) f f' a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn ((f a -> f' a) -> (-.->) f f' a)
-> (h a -> f a -> f' a) -> h a -> (-.->) f f' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h a -> f a -> f' a
forall (x :: k). h x -> f x -> f' x
f) NP h xs
ns)

-- | Bifunctor equivalent of 'hczipWith'
bihczipWith :: All c xs
            => proxy c
            -> (forall x. c x => h x -> g x -> g' x)
            -> (forall x. c x => h x -> f x -> f' x)
            -> NP h xs -> Telescope g f xs -> Telescope g' f' xs
bihczipWith :: proxy c
-> (forall (x :: k). c x => h x -> g x -> g' x)
-> (forall (x :: k). c x => h x -> f x -> f' x)
-> NP h xs
-> Telescope g f xs
-> Telescope g' f' xs
bihczipWith proxy c
p forall (x :: k). c x => h x -> g x -> g' x
g forall (x :: k). c x => h x -> f x -> f' x
f NP h xs
ns = NP (g -.-> g') xs
-> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
forall k (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *)
       (f' :: k -> *).
NP (g -.-> g') xs
-> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
bihap (proxy c
-> (forall (a :: k). c a => h a -> (-.->) g g' a)
-> NP h xs
-> NP (g -.-> g') xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap proxy c
p ((g a -> g' a) -> (-.->) g g' a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn ((g a -> g' a) -> (-.->) g g' a)
-> (h a -> g a -> g' a) -> h a -> (-.->) g g' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h a -> g a -> g' a
forall (x :: k). c x => h x -> g x -> g' x
g) NP h xs
ns) (proxy c
-> (forall (a :: k). c a => h a -> (-.->) f f' a)
-> NP h xs
-> NP (f -.-> f') xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap proxy c
p ((f a -> f' a) -> (-.->) f f' a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn ((f a -> f' a) -> (-.->) f f' a)
-> (h a -> f a -> f' a) -> h a -> (-.->) f f' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h a -> f a -> f' a
forall (x :: k). c x => h x -> f x -> f' x
f) NP h xs
ns)

{-------------------------------------------------------------------------------
  Simple telescope

  This is an internal type that is useful primarily useful as a sanity check
  of our bifunctor generalizations.
-------------------------------------------------------------------------------}

-- | 'Telescope' with both functors set to the same @f@
newtype SimpleTelescope f xs = SimpleTelescope {
      SimpleTelescope f xs -> Telescope f f xs
getSimpleTelescope :: Telescope f f xs
    }

type instance Prod       SimpleTelescope   = NP
type instance SListIN    SimpleTelescope   = SListI
type instance AllN       SimpleTelescope c = All c
type instance CollapseTo SimpleTelescope a = [a]

instance HAp SimpleTelescope where
  hap :: Prod SimpleTelescope (f -.-> g) xs
-> SimpleTelescope f xs -> SimpleTelescope g xs
hap Prod SimpleTelescope (f -.-> g) xs
fs = Telescope g g xs -> SimpleTelescope g xs
forall k (f :: k -> *) (xs :: [k]).
Telescope f f xs -> SimpleTelescope f xs
SimpleTelescope (Telescope g g xs -> SimpleTelescope g xs)
-> (SimpleTelescope f xs -> Telescope g g xs)
-> SimpleTelescope f xs
-> SimpleTelescope g xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (f -.-> g) xs
-> NP (f -.-> g) xs -> Telescope f f xs -> Telescope g g xs
forall k (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *)
       (f' :: k -> *).
NP (g -.-> g') xs
-> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
bihap Prod SimpleTelescope (f -.-> g) xs
NP (f -.-> g) xs
fs Prod SimpleTelescope (f -.-> g) xs
NP (f -.-> g) xs
fs (Telescope f f xs -> Telescope g g xs)
-> (SimpleTelescope f xs -> Telescope f f xs)
-> SimpleTelescope f xs
-> Telescope g g xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleTelescope f xs -> Telescope f f xs
forall k (f :: k -> *) (xs :: [k]).
SimpleTelescope f xs -> Telescope f f xs
getSimpleTelescope

instance HTraverse_ SimpleTelescope where
  hctraverse_ :: proxy c
-> (forall (a :: k). c a => f a -> g ())
-> SimpleTelescope f xs
-> g ()
hctraverse_ proxy c
p forall (a :: k). c a => f a -> g ()
f = proxy c
-> (forall (a :: k). c a => f a -> g ())
-> (forall (a :: k). c a => f a -> g ())
-> Telescope f f xs
-> g ()
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *).
(All c xs, Applicative m) =>
proxy c
-> (forall (x :: k). c x => g x -> m ())
-> (forall (x :: k). c x => f x -> m ())
-> Telescope g f xs
-> m ()
bihctraverse_ proxy c
p forall (a :: k). c a => f a -> g ()
f forall (a :: k). c a => f a -> g ()
f (Telescope f f xs -> g ())
-> (SimpleTelescope f xs -> Telescope f f xs)
-> SimpleTelescope f xs
-> g ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleTelescope f xs -> Telescope f f xs
forall k (f :: k -> *) (xs :: [k]).
SimpleTelescope f xs -> Telescope f f xs
getSimpleTelescope
  htraverse_ :: (forall (a :: k). f a -> g ()) -> SimpleTelescope f xs -> g ()
htraverse_    forall (a :: k). f a -> g ()
f = (forall (a :: k). f a -> g ())
-> (forall (a :: k). f a -> g ()) -> Telescope f f xs -> g ()
forall k (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *).
(SListI xs, Applicative m) =>
(forall (x :: k). g x -> m ())
-> (forall (x :: k). f x -> m ()) -> Telescope g f xs -> m ()
bihtraverse_    forall (a :: k). f a -> g ()
f forall (a :: k). f a -> g ()
f (Telescope f f xs -> g ())
-> (SimpleTelescope f xs -> Telescope f f xs)
-> SimpleTelescope f xs
-> g ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleTelescope f xs -> Telescope f f xs
forall k (f :: k -> *) (xs :: [k]).
SimpleTelescope f xs -> Telescope f f xs
getSimpleTelescope

instance HSequence SimpleTelescope where
  hsequence' :: SimpleTelescope (f :.: g) xs -> f (SimpleTelescope g xs)
hsequence'      = (Telescope g g xs -> SimpleTelescope g xs)
-> f (Telescope g g xs) -> f (SimpleTelescope g xs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Telescope g g xs -> SimpleTelescope g xs
forall k (f :: k -> *) (xs :: [k]).
Telescope f f xs -> SimpleTelescope f xs
SimpleTelescope (f (Telescope g g xs) -> f (SimpleTelescope g xs))
-> (SimpleTelescope (f :.: g) xs -> f (Telescope g g xs))
-> SimpleTelescope (f :.: g) xs
-> f (SimpleTelescope g xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope (f :.: g) (f :.: g) xs -> f (Telescope g g xs)
forall k (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]).
(SListI xs, Applicative m) =>
Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs)
bihsequence'        (Telescope (f :.: g) (f :.: g) xs -> f (Telescope g g xs))
-> (SimpleTelescope (f :.: g) xs
    -> Telescope (f :.: g) (f :.: g) xs)
-> SimpleTelescope (f :.: g) xs
-> f (Telescope g g xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleTelescope (f :.: g) xs -> Telescope (f :.: g) (f :.: g) xs
forall k (f :: k -> *) (xs :: [k]).
SimpleTelescope f xs -> Telescope f f xs
getSimpleTelescope
  hctraverse' :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> SimpleTelescope f xs
-> g (SimpleTelescope f' xs)
hctraverse' proxy c
p forall (a :: k). c a => f a -> g (f' a)
f = (Telescope f' f' xs -> SimpleTelescope f' xs)
-> g (Telescope f' f' xs) -> g (SimpleTelescope f' xs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Telescope f' f' xs -> SimpleTelescope f' xs
forall k (f :: k -> *) (xs :: [k]).
Telescope f f xs -> SimpleTelescope f xs
SimpleTelescope (g (Telescope f' f' xs) -> g (SimpleTelescope f' xs))
-> (SimpleTelescope f xs -> g (Telescope f' f' xs))
-> SimpleTelescope f xs
-> g (SimpleTelescope f' xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> (forall (a :: k). c a => f a -> g (f' a))
-> Telescope f f xs
-> g (Telescope f' f' xs)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *)
       (f' :: k -> *) (xs :: [k]).
(All c xs, Applicative m) =>
proxy c
-> (forall (x :: k). c x => g x -> m (g' x))
-> (forall (x :: k). c x => f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
bihctraverse' proxy c
p forall (a :: k). c a => f a -> g (f' a)
f forall (a :: k). c a => f a -> g (f' a)
f (Telescope f f xs -> g (Telescope f' f' xs))
-> (SimpleTelescope f xs -> Telescope f f xs)
-> SimpleTelescope f xs
-> g (Telescope f' f' xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleTelescope f xs -> Telescope f f xs
forall k (f :: k -> *) (xs :: [k]).
SimpleTelescope f xs -> Telescope f f xs
getSimpleTelescope
  htraverse' :: (forall (a :: k). f a -> g (f' a))
-> SimpleTelescope f xs -> g (SimpleTelescope f' xs)
htraverse'    forall (a :: k). f a -> g (f' a)
f = (Telescope f' f' xs -> SimpleTelescope f' xs)
-> g (Telescope f' f' xs) -> g (SimpleTelescope f' xs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Telescope f' f' xs -> SimpleTelescope f' xs
forall k (f :: k -> *) (xs :: [k]).
Telescope f f xs -> SimpleTelescope f xs
SimpleTelescope (g (Telescope f' f' xs) -> g (SimpleTelescope f' xs))
-> (SimpleTelescope f xs -> g (Telescope f' f' xs))
-> SimpleTelescope f xs
-> g (SimpleTelescope f' xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). f a -> g (f' a))
-> (forall (a :: k). f a -> g (f' a))
-> Telescope f f xs
-> g (Telescope f' f' xs)
forall k (xs :: [k]) (m :: * -> *) (g :: k -> *) (g' :: k -> *)
       (f :: k -> *) (f' :: k -> *).
(SListI xs, Applicative m) =>
(forall (x :: k). g x -> m (g' x))
-> (forall (x :: k). f x -> m (f' x))
-> Telescope g f xs
-> m (Telescope g' f' xs)
bihtraverse'    forall (a :: k). f a -> g (f' a)
f forall (a :: k). f a -> g (f' a)
f (Telescope f f xs -> g (Telescope f' f' xs))
-> (SimpleTelescope f xs -> Telescope f f xs)
-> SimpleTelescope f xs
-> g (Telescope f' f' xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleTelescope f xs -> Telescope f f xs
forall k (f :: k -> *) (xs :: [k]).
SimpleTelescope f xs -> Telescope f f xs
getSimpleTelescope

instance HCollapse SimpleTelescope where
  hcollapse :: SimpleTelescope (K a) xs -> CollapseTo SimpleTelescope a
hcollapse (SimpleTelescope Telescope (K a) (K a) xs
t) = Telescope (K a) (K a) xs -> [a]
forall k a (xs :: [k]). Telescope (K a) (K a) xs -> [a]
go Telescope (K a) (K a) xs
t
    where
      go :: Telescope (K a) (K a) xs -> [a]
      go :: Telescope (K a) (K a) xs -> [a]
go (TZ (K a
x))    = [a
x]
      go (TS (K a
x) Telescope (K a) (K a) xs
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Telescope (K a) (K a) xs -> [a]
forall k a (xs :: [k]). Telescope (K a) (K a) xs -> [a]
go Telescope (K a) (K a) xs
xs

{-------------------------------------------------------------------------------
  Utilities
-------------------------------------------------------------------------------}

tip :: Telescope g f xs -> NS f xs
tip :: Telescope g f xs -> NS f xs
tip (TZ   f x
l) = f x -> NS f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z f x
l
tip (TS g x
_ Telescope g f xs
r) = NS f xs -> NS f (x : xs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (Telescope g f xs -> NS f xs
forall k (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
tip Telescope g f xs
r)

fromTip :: NS f xs -> Telescope (K ()) f xs
fromTip :: NS f xs -> Telescope (K ()) f xs
fromTip (Z f x
l) = f x -> Telescope (K ()) f (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ f x
l
fromTip (S NS f xs
r) = K () x -> Telescope (K ()) f xs -> Telescope (K ()) f (x : xs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS (() -> K () x
forall k a (b :: k). a -> K a b
K ()) (NS f xs -> Telescope (K ()) f xs
forall k (f :: k -> *) (xs :: [k]).
NS f xs -> Telescope (K ()) f xs
fromTip NS f xs
r)

toAtMost :: Telescope (K a) (K (Maybe a)) xs -> AtMost xs a
toAtMost :: Telescope (K a) (K (Maybe a)) xs -> AtMost xs a
toAtMost = Telescope (K a) (K (Maybe a)) xs -> AtMost xs a
forall a (xs :: [*]).
Telescope (K a) (K (Maybe a)) xs -> AtMost xs a
go
  where
    go :: Telescope (K a) (K (Maybe a)) xs -> AtMost xs a
    go :: Telescope (K a) (K (Maybe a)) xs -> AtMost xs a
go (TZ (K Maybe a
ma))  = AtMost (x : xs) a
-> (a -> AtMost (x : xs) a) -> Maybe a -> AtMost (x : xs) a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe AtMost (x : xs) a
forall (xs :: [*]) a. AtMost xs a
AtMostNil a -> AtMost (x : xs) a
forall a x (xs :: [*]). a -> AtMost (x : xs) a
atMostOne Maybe a
ma
    go (TS (K a
a) Telescope (K a) (K (Maybe a)) xs
t) = a -> AtMost xs a -> AtMost (x : xs) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
a (Telescope (K a) (K (Maybe a)) xs -> AtMost xs a
forall a (xs :: [*]).
Telescope (K a) (K (Maybe a)) xs -> AtMost xs a
go Telescope (K a) (K (Maybe a)) xs
t)

fromTZ :: Telescope g f '[x] -> f x
fromTZ :: Telescope g f '[x] -> f x
fromTZ (TZ f x
fx)  = f x
f x
fx

{-------------------------------------------------------------------------------
  Extension and retraction
-------------------------------------------------------------------------------}

newtype Extend m g f x y = Extend { Extend m g f x y -> f x -> m (g x, f y)
extendWith :: f x -> m (g x, f y) }

-- | Extend the telescope
--
-- We will not attempt to extend the telescope past its final segment.
--
-- Blockchain intuition: suppose we have a telescope containing the ledger
-- state. The "how to extend" argument would take, say, the final Byron
-- state to the initial Shelley state; and "where to extend from" argument
-- would indicate when we want to extend: when the current slot number has
-- gone past the end of the Byron era.
extend :: forall m h g f xs. Monad m
       => InPairs (Requiring h (Extend m g f)) xs -- ^ How to extend
       -> NP (f -.-> Maybe :.: h) xs              -- ^ Where to extend /from/
       -> Telescope g f xs -> m (Telescope g f xs)
extend :: InPairs (Requiring h (Extend m g f)) xs
-> NP (f -.-> (Maybe :.: h)) xs
-> Telescope g f xs
-> m (Telescope g f xs)
extend = InPairs (Requiring h (Extend m g f)) xs
-> NP (f -.-> (Maybe :.: h)) xs
-> Telescope g f xs
-> m (Telescope g f xs)
forall (xs' :: [k]).
InPairs (Requiring h (Extend m g f)) xs'
-> NP (f -.-> (Maybe :.: h)) xs'
-> Telescope g f xs'
-> m (Telescope g f xs')
go
  where
    go :: InPairs (Requiring h (Extend m g f)) xs'
       -> NP (f -.-> Maybe :.: h) xs'
       -> Telescope g f xs' -> m (Telescope g f xs')
    go :: InPairs (Requiring h (Extend m g f)) xs'
-> NP (f -.-> (Maybe :.: h)) xs'
-> Telescope g f xs'
-> m (Telescope g f xs')
go InPairs (Requiring h (Extend m g f)) xs'
PNil NP (f -.-> (Maybe :.: h)) xs'
_ (TZ f x
fx) =
        Telescope g f '[x] -> m (Telescope g f '[x])
forall (m :: * -> *) a. Monad m => a -> m a
return (f x -> Telescope g f '[x]
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ f x
fx)
    go (PCons Requiring h (Extend m g f) x y
e InPairs (Requiring h (Extend m g f)) (y : zs)
es) ((-.->) f (Maybe :.: h) x
p :* NP (f -.-> (Maybe :.: h)) xs
ps) (TZ f x
fx) =
        case (:.:) Maybe h x -> Maybe (h x)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp ((:.:) Maybe h x -> Maybe (h x)) -> (:.:) Maybe h x -> Maybe (h x)
forall a b. (a -> b) -> a -> b
$ (-.->) f (Maybe :.: h) x -> f x -> (:.:) Maybe h x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) f (Maybe :.: h) x
p f x
f x
fx of
          Maybe (h x)
Nothing ->
            Telescope g f (x : y : zs) -> m (Telescope g f (x : y : zs))
forall (m :: * -> *) a. Monad m => a -> m a
return (f x -> Telescope g f (x : y : zs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ f x
fx)
          Just h x
hx -> do
            (g x
gx, f y
fy) <- Extend m g f x y -> f x -> m (g x, f y)
forall (m :: * -> *) k (g :: k -> *) (f :: k -> *) (x :: k)
       (y :: k).
Extend m g f x y -> f x -> m (g x, f y)
extendWith (Requiring h (Extend m g f) x y -> h x -> Extend m g f x y
forall k1 (h :: k1 -> *) k2 (f :: k1 -> k2 -> *) (x :: k1)
       (y :: k2).
Requiring h f x y -> h x -> f x y
provide Requiring h (Extend m g f) x y
e h x
h x
hx) f x
f x
fx
            g x -> Telescope g f (y : zs) -> Telescope g f (x : y : zs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
gx (Telescope g f (y : zs) -> Telescope g f (x : y : zs))
-> m (Telescope g f (y : zs)) -> m (Telescope g f (x : y : zs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InPairs (Requiring h (Extend m g f)) (y : zs)
-> NP (f -.-> (Maybe :.: h)) (y : zs)
-> Telescope g f (y : zs)
-> m (Telescope g f (y : zs))
forall (xs' :: [k]).
InPairs (Requiring h (Extend m g f)) xs'
-> NP (f -.-> (Maybe :.: h)) xs'
-> Telescope g f xs'
-> m (Telescope g f xs')
go InPairs (Requiring h (Extend m g f)) (y : zs)
es NP (f -.-> (Maybe :.: h)) xs
NP (f -.-> (Maybe :.: h)) (y : zs)
ps (f y -> Telescope g f (y : zs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ f y
fy)
    go (PCons Requiring h (Extend m g f) x y
_ InPairs (Requiring h (Extend m g f)) (y : zs)
es) ((-.->) f (Maybe :.: h) x
_ :* NP (f -.-> (Maybe :.: h)) xs
ps) (TS g x
gx Telescope g f xs
fx) =
        g x -> Telescope g f (y : zs) -> Telescope g f (x : y : zs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
gx (Telescope g f (y : zs) -> Telescope g f (x : y : zs))
-> m (Telescope g f (y : zs)) -> m (Telescope g f (x : y : zs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InPairs (Requiring h (Extend m g f)) (y : zs)
-> NP (f -.-> (Maybe :.: h)) (y : zs)
-> Telescope g f (y : zs)
-> m (Telescope g f (y : zs))
forall (xs' :: [k]).
InPairs (Requiring h (Extend m g f)) xs'
-> NP (f -.-> (Maybe :.: h)) xs'
-> Telescope g f xs'
-> m (Telescope g f xs')
go InPairs (Requiring h (Extend m g f)) (y : zs)
es NP (f -.-> (Maybe :.: h)) xs
NP (f -.-> (Maybe :.: h)) (y : zs)
ps Telescope g f xs
Telescope g f (y : zs)
fx

newtype Retract m g f x y = Retract { Retract m g f x y -> g x -> f y -> m (f x)
retractWith :: g x -> f y -> m (f x) }

-- | Retract a telescope
--
-- Blockchain intuition: suppose we have a telescope containing the consensus
-- state. When we rewind the consensus state, we might cross a hard fork
-- transition point. So we first /retract/ the telescope /to/ the era containing
-- the slot number that we want to rewind to, and only then call
-- 'rewindChainDepState' on that era. Of course, retraction may fail (we
-- might not /have/ past consensus state to rewind to anymore); this failure
-- would require a choice for a particular monad @m@.
retract :: forall m h g f xs. Monad m
        => Tails (Requiring h (Retract m g f)) xs  -- ^ How to retract
        -> NP (g -.-> Maybe :.: h) xs              -- ^ Where to retract /to/
        -> Telescope g f xs -> m (Telescope g f xs)
retract :: Tails (Requiring h (Retract m g f)) xs
-> NP (g -.-> (Maybe :.: h)) xs
-> Telescope g f xs
-> m (Telescope g f xs)
retract =
    \Tails (Requiring h (Retract m g f)) xs
tails NP (g -.-> (Maybe :.: h)) xs
np ->
       NP (g -.-> (Maybe :.: h)) xs
-> (SListI xs => Telescope g f xs -> m (Telescope g f xs))
-> Telescope g f xs
-> m (Telescope g f xs)
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (g -.-> (Maybe :.: h)) xs
np ((SListI xs => Telescope g f xs -> m (Telescope g f xs))
 -> Telescope g f xs -> m (Telescope g f xs))
-> (SListI xs => Telescope g f xs -> m (Telescope g f xs))
-> Telescope g f xs
-> m (Telescope g f xs)
forall a b. (a -> b) -> a -> b
$ Tails (Requiring h (Retract m g f)) xs
-> NP (g -.-> (Maybe :.: h)) xs
-> Telescope g f xs
-> m (Telescope g f xs)
forall (xs' :: [k]).
SListI xs' =>
Tails (Requiring h (Retract m g f)) xs'
-> NP (g -.-> (Maybe :.: h)) xs'
-> Telescope g f xs'
-> m (Telescope g f xs')
go Tails (Requiring h (Retract m g f)) xs
tails NP (g -.-> (Maybe :.: h)) xs
np
  where
    go :: SListI xs'
       => Tails (Requiring h (Retract m g f)) xs'
       -> NP (g -.-> Maybe :.: h) xs'
       -> Telescope g f xs' -> m (Telescope g f xs')
    go :: Tails (Requiring h (Retract m g f)) xs'
-> NP (g -.-> (Maybe :.: h)) xs'
-> Telescope g f xs'
-> m (Telescope g f xs')
go Tails (Requiring h (Retract m g f)) xs'
_            NP (g -.-> (Maybe :.: h)) xs'
_         (TZ f x
fx)   = Telescope g f (x : xs) -> m (Telescope g f (x : xs))
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope g f (x : xs) -> m (Telescope g f (x : xs)))
-> Telescope g f (x : xs) -> m (Telescope g f (x : xs))
forall a b. (a -> b) -> a -> b
$ f x -> Telescope g f (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ f x
fx
    go (TCons NP (Requiring h (Retract m g f) x) xs
r Tails (Requiring h (Retract m g f)) xs
rs) ((-.->) g (Maybe :.: h) x
p :* NP (g -.-> (Maybe :.: h)) xs
ps) (TS g x
gx Telescope g f xs
t) =
        case (:.:) Maybe h x -> Maybe (h x)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp ((-.->) g (Maybe :.: h) x -> g x -> (:.:) Maybe h x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) g (Maybe :.: h) x
p g x
g x
gx) of
          Just h x
hx ->
            (NS (K (f x)) xs -> Telescope g f (x : xs))
-> m (NS (K (f x)) xs) -> m (Telescope g f (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f x -> Telescope g f (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ (f x -> Telescope g f (x : xs))
-> (NS (K (f x)) xs -> f x)
-> NS (K (f x)) xs
-> Telescope g f (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS (K (f x)) xs -> f x
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse) (m (NS (K (f x)) xs) -> m (Telescope g f (x : xs)))
-> m (NS (K (f x)) xs) -> m (Telescope g f (x : xs))
forall a b. (a -> b) -> a -> b
$ NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: * -> *)
       (g :: k -> *).
(HSequence h, SListIN h xs, Applicative f) =>
h (f :.: g) xs -> f (h g xs)
hsequence' (NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs))
-> NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs)
forall a b. (a -> b) -> a -> b
$
              (forall (a :: k).
 Requiring h (Retract m g f) x a -> f a -> (:.:) m (K (f x)) a)
-> Prod NS (Requiring h (Retract m g f) x) xs
-> NS f xs
-> NS (m :.: K (f x)) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith (h x
-> g x
-> Requiring h (Retract m g f) x a
-> f a
-> (:.:) m (K (f x)) a
forall k (m :: * -> *) (h :: k -> *) (x :: k) (g :: k -> *)
       (f :: k -> *) (z :: k).
Functor m =>
h x
-> g x
-> Requiring h (Retract m g f) x z
-> f z
-> (:.:) m (K (f x)) z
retractAux h x
hx g x
g x
gx) Prod NS (Requiring h (Retract m g f) x) xs
NP (Requiring h (Retract m g f) x) xs
r (Telescope g f xs -> NS f xs
forall k (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
tip Telescope g f xs
t)
          Maybe (h x)
Nothing ->
            g x -> Telescope g f xs -> Telescope g f (x : xs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
gx (Telescope g f xs -> Telescope g f (x : xs))
-> m (Telescope g f xs) -> m (Telescope g f (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tails (Requiring h (Retract m g f)) xs
-> NP (g -.-> (Maybe :.: h)) xs
-> Telescope g f xs
-> m (Telescope g f xs)
forall (xs' :: [k]).
SListI xs' =>
Tails (Requiring h (Retract m g f)) xs'
-> NP (g -.-> (Maybe :.: h)) xs'
-> Telescope g f xs'
-> m (Telescope g f xs')
go Tails (Requiring h (Retract m g f)) xs
rs NP (g -.-> (Maybe :.: h)) xs
NP (g -.-> (Maybe :.: h)) xs
ps Telescope g f xs
Telescope g f xs
t

-- | Internal auxiliary to 'retract' and 'alignWith'
retractAux :: Functor m
           => h x  -- Proof that we need to retract
           -> g x  -- Era we are retracting to
           -> Requiring h (Retract m g f) x z
           -> f z  -- Current tip (what we are retracting from)
           -> (m :.: K (f x)) z
retractAux :: h x
-> g x
-> Requiring h (Retract m g f) x z
-> f z
-> (:.:) m (K (f x)) z
retractAux h x
hx g x
gx Requiring h (Retract m g f) x z
r f z
fz = m (K (f x) z) -> (:.:) m (K (f x)) z
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (m (K (f x) z) -> (:.:) m (K (f x)) z)
-> m (K (f x) z) -> (:.:) m (K (f x)) z
forall a b. (a -> b) -> a -> b
$ f x -> K (f x) z
forall k a (b :: k). a -> K a b
K (f x -> K (f x) z) -> m (f x) -> m (K (f x) z)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Retract m g f x z -> g x -> f z -> m (f x)
forall (m :: * -> *) k (g :: k -> *) (f :: k -> *) (x :: k)
       (y :: k).
Retract m g f x y -> g x -> f y -> m (f x)
retractWith (Requiring h (Retract m g f) x z -> h x -> Retract m g f x z
forall k1 (h :: k1 -> *) k2 (f :: k1 -> k2 -> *) (x :: k1)
       (y :: k2).
Requiring h f x y -> h x -> f x y
provide Requiring h (Retract m g f) x z
r h x
hx) g x
gx f z
fz

-- | Align a telescope with another, then apply a function to the tips
--
-- Aligning is a combination of extension and retraction, extending or
-- retracting the telescope as required to match up with the other telescope.
--
-- Blockchain intuition: suppose we have one telescope containing the
-- already-ticked ledger state, and another telescope containing the consensus
-- state. Since the ledger state has already been ticked, it might have been
-- advanced to the next era. If this happens, we should then align the
-- consensus state with the ledger state, moving /it/ also to the next era,
-- before we can do the consensus header validation check. Note that in this
-- particular example, the ledger state will always be ahead of the consensus
-- state, never behind; 'alignExtend' can be used in this case.
align :: forall m g' g f' f f'' xs. Monad m
      => InPairs (Requiring g' (Extend  m g f)) xs  -- ^ How to extend
      -> Tails   (Requiring f' (Retract m g f)) xs  -- ^ How to retract
      -> NP (f' -.-> f -.-> f'') xs  -- ^ Function to apply at the tip
      -> Telescope g' f' xs          -- ^ Telescope we are aligning with
      -> Telescope g f xs -> m (Telescope g f'' xs)
align :: InPairs (Requiring g' (Extend m g f)) xs
-> Tails (Requiring f' (Retract m g f)) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
align = \InPairs (Requiring g' (Extend m g f)) xs
es Tails (Requiring f' (Retract m g f)) xs
rs NP (f' -.-> (f -.-> f'')) xs
atTip ->
    NP (f' -.-> (f -.-> f'')) xs
-> (SListI xs =>
    Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs))
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (f' -.-> (f -.-> f'')) xs
atTip ((SListI xs =>
  Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs))
 -> Telescope g' f' xs
 -> Telescope g f xs
 -> m (Telescope g f'' xs))
-> (SListI xs =>
    Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs))
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall a b. (a -> b) -> a -> b
$ InPairs (Requiring g' (Extend m g f)) xs
-> Tails (Requiring f' (Retract m g f)) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall (xs' :: [k]).
SListI xs' =>
InPairs (Requiring g' (Extend m g f)) xs'
-> Tails (Requiring f' (Retract m g f)) xs'
-> NP (f' -.-> (f -.-> f'')) xs'
-> Telescope g' f' xs'
-> Telescope g f xs'
-> m (Telescope g f'' xs')
go InPairs (Requiring g' (Extend m g f)) xs
es Tails (Requiring f' (Retract m g f)) xs
rs NP (f' -.-> (f -.-> f'')) xs
atTip
  where
    go :: SListI xs'
       => InPairs (Requiring g' (Extend  m g f)) xs'
       -> Tails   (Requiring f' (Retract m g f)) xs'
       -> NP (f' -.-> f -.-> f'') xs'
       -> Telescope g' f' xs' -> Telescope g f xs' -> m (Telescope g f'' xs')
    go :: InPairs (Requiring g' (Extend m g f)) xs'
-> Tails (Requiring f' (Retract m g f)) xs'
-> NP (f' -.-> (f -.-> f'')) xs'
-> Telescope g' f' xs'
-> Telescope g f xs'
-> m (Telescope g f'' xs')
go InPairs (Requiring g' (Extend m g f)) xs'
_ Tails (Requiring f' (Retract m g f)) xs'
_ ((-.->) f' (f -.-> f'') x
f :* NP (f' -.-> (f -.-> f'')) xs
_) (TZ f' x
f'x) (TZ f x
fx) =
        Telescope g f'' (x : xs) -> m (Telescope g f'' (x : xs))
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope g f'' (x : xs) -> m (Telescope g f'' (x : xs)))
-> Telescope g f'' (x : xs) -> m (Telescope g f'' (x : xs))
forall a b. (a -> b) -> a -> b
$ f'' x -> Telescope g f'' (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ ((-.->) f' (f -.-> f'') x
f (-.->) f' (f -.-> f'') x -> f' x -> (-.->) f f'' x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
`apFn` f' x
f' x
f'x (-.->) f f'' x -> f x -> f'' x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
`apFn` f x
f x
fx)
    go (PCons Requiring g' (Extend m g f) x y
_ InPairs (Requiring g' (Extend m g f)) (y : zs)
es) (TCons NP (Requiring f' (Retract m g f) x) xs
_ Tails (Requiring f' (Retract m g f)) xs
rs) ((-.->) f' (f -.-> f'') x
_ :* NP (f' -.-> (f -.-> f'')) xs
fs) (TS g' x
_ Telescope g' f' xs
f'x) (TS g x
gx Telescope g f xs
fx) =
        g x -> Telescope g f'' (y : zs) -> Telescope g f'' (x : y : zs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
gx (Telescope g f'' (y : zs) -> Telescope g f'' (x : y : zs))
-> m (Telescope g f'' (y : zs)) -> m (Telescope g f'' (x : y : zs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InPairs (Requiring g' (Extend m g f)) (y : zs)
-> Tails (Requiring f' (Retract m g f)) (y : zs)
-> NP (f' -.-> (f -.-> f'')) (y : zs)
-> Telescope g' f' (y : zs)
-> Telescope g f (y : zs)
-> m (Telescope g f'' (y : zs))
forall (xs' :: [k]).
SListI xs' =>
InPairs (Requiring g' (Extend m g f)) xs'
-> Tails (Requiring f' (Retract m g f)) xs'
-> NP (f' -.-> (f -.-> f'')) xs'
-> Telescope g' f' xs'
-> Telescope g f xs'
-> m (Telescope g f'' xs')
go InPairs (Requiring g' (Extend m g f)) (y : zs)
es Tails (Requiring f' (Retract m g f)) xs
Tails (Requiring f' (Retract m g f)) (y : zs)
rs NP (f' -.-> (f -.-> f'')) xs
NP (f' -.-> (f -.-> f'')) (y : zs)
fs Telescope g' f' xs
Telescope g' f' (y : zs)
f'x Telescope g f xs
Telescope g f (y : zs)
fx
    go InPairs (Requiring g' (Extend m g f)) xs'
_ (TCons NP (Requiring f' (Retract m g f) x) xs
r Tails (Requiring f' (Retract m g f)) xs
_) ((-.->) f' (f -.-> f'') x
f :* NP (f' -.-> (f -.-> f'')) xs
_) (TZ f' x
f'x) (TS g x
gx Telescope g f xs
fx) =
        (NS (K (f x)) xs -> Telescope g f'' (x : xs))
-> m (NS (K (f x)) xs) -> m (Telescope g f'' (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f'' x -> Telescope g f'' (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ (f'' x -> Telescope g f'' (x : xs))
-> (NS (K (f x)) xs -> f'' x)
-> NS (K (f x)) xs
-> Telescope g f'' (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\f x
fx' -> (-.->) f' (f -.-> f'') x
f (-.->) f' (f -.-> f'') x -> f' x -> (-.->) f f'' x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
`apFn` f' x
f' x
f'x (-.->) f f'' x -> f x -> f'' x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
`apFn` f x
fx') (f x -> f'' x)
-> (NS (K (f x)) xs -> f x) -> NS (K (f x)) xs -> f'' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS (K (f x)) xs -> f x
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse) (m (NS (K (f x)) xs) -> m (Telescope g f'' (x : xs)))
-> m (NS (K (f x)) xs) -> m (Telescope g f'' (x : xs))
forall a b. (a -> b) -> a -> b
$ NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: * -> *)
       (g :: k -> *).
(HSequence h, SListIN h xs, Applicative f) =>
h (f :.: g) xs -> f (h g xs)
hsequence' (NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs))
-> NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs)
forall a b. (a -> b) -> a -> b
$
          (forall (a :: k).
 Requiring f' (Retract m g f) x a -> f a -> (:.:) m (K (f x)) a)
-> Prod NS (Requiring f' (Retract m g f) x) xs
-> NS f xs
-> NS (m :.: K (f x)) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith (f' x
-> g x
-> Requiring f' (Retract m g f) x a
-> f a
-> (:.:) m (K (f x)) a
forall k (m :: * -> *) (h :: k -> *) (x :: k) (g :: k -> *)
       (f :: k -> *) (z :: k).
Functor m =>
h x
-> g x
-> Requiring h (Retract m g f) x z
-> f z
-> (:.:) m (K (f x)) z
retractAux f' x
f'x g x
g x
gx) Prod NS (Requiring f' (Retract m g f) x) xs
NP (Requiring f' (Retract m g f) x) xs
r (Telescope g f xs -> NS f xs
forall k (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
tip Telescope g f xs
fx)
    go (PCons Requiring g' (Extend m g f) x y
e InPairs (Requiring g' (Extend m g f)) (y : zs)
es) (TCons NP (Requiring f' (Retract m g f) x) xs
_ Tails (Requiring f' (Retract m g f)) xs
rs) ((-.->) f' (f -.-> f'') x
_ :* NP (f' -.-> (f -.-> f'')) xs
fs) (TS g' x
g'x Telescope g' f' xs
t'x) (TZ f x
fx) = do
        (g x
gx, f y
fy) <- Extend m g f x y -> f x -> m (g x, f y)
forall (m :: * -> *) k (g :: k -> *) (f :: k -> *) (x :: k)
       (y :: k).
Extend m g f x y -> f x -> m (g x, f y)
extendWith (Requiring g' (Extend m g f) x y -> g' x -> Extend m g f x y
forall k1 (h :: k1 -> *) k2 (f :: k1 -> k2 -> *) (x :: k1)
       (y :: k2).
Requiring h f x y -> h x -> f x y
provide Requiring g' (Extend m g f) x y
e g' x
g' x
g'x) f x
f x
fx
        g x -> Telescope g f'' (y : zs) -> Telescope g f'' (x : y : zs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
gx (Telescope g f'' (y : zs) -> Telescope g f'' (x : y : zs))
-> m (Telescope g f'' (y : zs)) -> m (Telescope g f'' (x : y : zs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InPairs (Requiring g' (Extend m g f)) (y : zs)
-> Tails (Requiring f' (Retract m g f)) (y : zs)
-> NP (f' -.-> (f -.-> f'')) (y : zs)
-> Telescope g' f' (y : zs)
-> Telescope g f (y : zs)
-> m (Telescope g f'' (y : zs))
forall (xs' :: [k]).
SListI xs' =>
InPairs (Requiring g' (Extend m g f)) xs'
-> Tails (Requiring f' (Retract m g f)) xs'
-> NP (f' -.-> (f -.-> f'')) xs'
-> Telescope g' f' xs'
-> Telescope g f xs'
-> m (Telescope g f'' xs')
go InPairs (Requiring g' (Extend m g f)) (y : zs)
es Tails (Requiring f' (Retract m g f)) xs
Tails (Requiring f' (Retract m g f)) (y : zs)
rs NP (f' -.-> (f -.-> f'')) xs
NP (f' -.-> (f -.-> f'')) (y : zs)
fs Telescope g' f' xs
Telescope g' f' (y : zs)
t'x (f y -> Telescope g f (y : zs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ f y
fy)

{-------------------------------------------------------------------------------
  Derived API
-------------------------------------------------------------------------------}

-- | Version of 'extend' where the evidence is a simple 'Bool'
extendIf :: Monad m
         => InPairs (Extend m g f) xs -- ^ How to extend
         -> NP (f -.-> K Bool) xs     -- ^ Where to extend /from/
         -> Telescope g f xs -> m (Telescope g f xs)
extendIf :: InPairs (Extend m g f) xs
-> NP (f -.-> K Bool) xs
-> Telescope g f xs
-> m (Telescope g f xs)
extendIf InPairs (Extend m g f) xs
es NP (f -.-> K Bool) xs
ps = NP (f -.-> K Bool) xs
-> (SListI xs => Telescope g f xs -> m (Telescope g f xs))
-> Telescope g f xs
-> m (Telescope g f xs)
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (f -.-> K Bool) xs
ps ((SListI xs => Telescope g f xs -> m (Telescope g f xs))
 -> Telescope g f xs -> m (Telescope g f xs))
-> (SListI xs => Telescope g f xs -> m (Telescope g f xs))
-> Telescope g f xs
-> m (Telescope g f xs)
forall a b. (a -> b) -> a -> b
$
    InPairs (Requiring (K ()) (Extend m g f)) xs
-> NP (f -.-> (Maybe :.: K ())) xs
-> Telescope g f xs
-> m (Telescope g f xs)
forall k (m :: * -> *) (h :: k -> *) (g :: k -> *) (f :: k -> *)
       (xs :: [k]).
Monad m =>
InPairs (Requiring h (Extend m g f)) xs
-> NP (f -.-> (Maybe :.: h)) xs
-> Telescope g f xs
-> m (Telescope g f xs)
extend
      ((forall (x :: k) (y :: k).
 Extend m g f x y -> Requiring (K ()) (Extend m g f) x y)
-> InPairs (Extend m g f) xs
-> InPairs (Requiring (K ()) (Extend m g f)) xs
forall k (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *).
SListI xs =>
(forall (x :: k) (y :: k). f x y -> g x y)
-> InPairs f xs -> InPairs g xs
InPairs.hmap ((K () x -> Extend m g f x y) -> Requiring (K ()) (Extend m g f) x y
forall k1 k2 (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1)
       (y :: k2).
(h x -> f x y) -> Requiring h f x y
Require ((K () x -> Extend m g f x y)
 -> Requiring (K ()) (Extend m g f) x y)
-> (Extend m g f x y -> K () x -> Extend m g f x y)
-> Extend m g f x y
-> Requiring (K ()) (Extend m g f) x y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Extend m g f x y -> K () x -> Extend m g f x y
forall a b. a -> b -> a
const) InPairs (Extend m g f) xs
es)
      ((forall (a :: k).
 (-.->) f (K Bool) a -> (-.->) f (Maybe :.: K ()) a)
-> NP (f -.-> K Bool) xs -> NP (f -.-> (Maybe :.: K ())) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap (\(-.->) f (K Bool) a
f -> (f a -> (:.:) Maybe (K ()) a) -> (-.->) f (Maybe :.: K ()) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn ((f a -> (:.:) Maybe (K ()) a) -> (-.->) f (Maybe :.: K ()) a)
-> (f a -> (:.:) Maybe (K ()) a) -> (-.->) f (Maybe :.: K ()) a
forall a b. (a -> b) -> a -> b
$ K Bool a -> (:.:) Maybe (K ()) a
forall k (x :: k). K Bool x -> (:.:) Maybe (K ()) x
fromBool (K Bool a -> (:.:) Maybe (K ()) a)
-> (f a -> K Bool a) -> f a -> (:.:) Maybe (K ()) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (-.->) f (K Bool) a -> f a -> K Bool a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) f (K Bool) a
f) NP (f -.-> K Bool) xs
ps)

-- | Version of 'retract' where the evidence is a simple 'Bool'
retractIf :: Monad m
          => Tails (Retract m g f) xs  -- ^ How to retract
          -> NP (g -.-> K Bool) xs     -- ^ Where to retract /to/
          -> Telescope g f xs -> m (Telescope g f xs)
retractIf :: Tails (Retract m g f) xs
-> NP (g -.-> K Bool) xs
-> Telescope g f xs
-> m (Telescope g f xs)
retractIf Tails (Retract m g f) xs
rs NP (g -.-> K Bool) xs
ps = NP (g -.-> K Bool) xs
-> (SListI xs => Telescope g f xs -> m (Telescope g f xs))
-> Telescope g f xs
-> m (Telescope g f xs)
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (g -.-> K Bool) xs
ps ((SListI xs => Telescope g f xs -> m (Telescope g f xs))
 -> Telescope g f xs -> m (Telescope g f xs))
-> (SListI xs => Telescope g f xs -> m (Telescope g f xs))
-> Telescope g f xs
-> m (Telescope g f xs)
forall a b. (a -> b) -> a -> b
$
    Tails (Requiring (K ()) (Retract m g f)) xs
-> NP (g -.-> (Maybe :.: K ())) xs
-> Telescope g f xs
-> m (Telescope g f xs)
forall k (m :: * -> *) (h :: k -> *) (g :: k -> *) (f :: k -> *)
       (xs :: [k]).
Monad m =>
Tails (Requiring h (Retract m g f)) xs
-> NP (g -.-> (Maybe :.: h)) xs
-> Telescope g f xs
-> m (Telescope g f xs)
retract
      ((forall (x :: k) (y :: k).
 Retract m g f x y -> Requiring (K ()) (Retract m g f) x y)
-> Tails (Retract m g f) xs
-> Tails (Requiring (K ()) (Retract m g f)) xs
forall k (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *).
SListI xs =>
(forall (x :: k) (y :: k). f x y -> g x y)
-> Tails f xs -> Tails g xs
Tails.hmap ((K () x -> Retract m g f x y)
-> Requiring (K ()) (Retract m g f) x y
forall k1 k2 (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1)
       (y :: k2).
(h x -> f x y) -> Requiring h f x y
Require ((K () x -> Retract m g f x y)
 -> Requiring (K ()) (Retract m g f) x y)
-> (Retract m g f x y -> K () x -> Retract m g f x y)
-> Retract m g f x y
-> Requiring (K ()) (Retract m g f) x y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Retract m g f x y -> K () x -> Retract m g f x y
forall a b. a -> b -> a
const) Tails (Retract m g f) xs
rs)
      ((forall (a :: k).
 (-.->) g (K Bool) a -> (-.->) g (Maybe :.: K ()) a)
-> NP (g -.-> K Bool) xs -> NP (g -.-> (Maybe :.: K ())) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap (\(-.->) g (K Bool) a
f -> (g a -> (:.:) Maybe (K ()) a) -> (-.->) g (Maybe :.: K ()) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn ((g a -> (:.:) Maybe (K ()) a) -> (-.->) g (Maybe :.: K ()) a)
-> (g a -> (:.:) Maybe (K ()) a) -> (-.->) g (Maybe :.: K ()) a
forall a b. (a -> b) -> a -> b
$ K Bool a -> (:.:) Maybe (K ()) a
forall k (x :: k). K Bool x -> (:.:) Maybe (K ()) x
fromBool (K Bool a -> (:.:) Maybe (K ()) a)
-> (g a -> K Bool a) -> g a -> (:.:) Maybe (K ()) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (-.->) g (K Bool) a -> g a -> K Bool a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) g (K Bool) a
f) NP (g -.-> K Bool) xs
ps)

-- | Version of 'align' that never retracts, only extends
--
-- PRE: The telescope we are aligning with cannot be behind us.
alignExtend :: (Monad m, HasCallStack)
            => InPairs (Requiring g' (Extend m g f)) xs  -- ^ How to extend
            -> NP (f' -.-> f -.-> f'') xs  -- ^ Function to apply at the tip
            -> Telescope g' f' xs          -- ^ Telescope we are aligning with
            -> Telescope g f xs -> m (Telescope g f'' xs)
alignExtend :: InPairs (Requiring g' (Extend m g f)) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
alignExtend InPairs (Requiring g' (Extend m g f)) xs
es NP (f' -.-> (f -.-> f'')) xs
atTip = NP (f' -.-> (f -.-> f'')) xs
-> (SListI xs =>
    Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs))
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (f' -.-> (f -.-> f'')) xs
atTip ((SListI xs =>
  Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs))
 -> Telescope g' f' xs
 -> Telescope g f xs
 -> m (Telescope g f'' xs))
-> (SListI xs =>
    Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs))
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall a b. (a -> b) -> a -> b
$
    InPairs (Requiring g' (Extend m g f)) xs
-> Tails (Requiring f' (Retract m g f)) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall k (m :: * -> *) (g' :: k -> *) (g :: k -> *) (f' :: k -> *)
       (f :: k -> *) (f'' :: k -> *) (xs :: [k]).
Monad m =>
InPairs (Requiring g' (Extend m g f)) xs
-> Tails (Requiring f' (Retract m g f)) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
align InPairs (Requiring g' (Extend m g f)) xs
es ((forall (x :: k) (y :: k). Requiring f' (Retract m g f) x y)
-> Tails (Requiring f' (Retract m g f)) xs
forall k (xs :: [k]) (f :: k -> k -> *).
SListI xs =>
(forall (x :: k) (y :: k). f x y) -> Tails f xs
Tails.hpure ((forall (x :: k) (y :: k). Requiring f' (Retract m g f) x y)
 -> Tails (Requiring f' (Retract m g f)) xs)
-> (forall (x :: k) (y :: k). Requiring f' (Retract m g f) x y)
-> Tails (Requiring f' (Retract m g f)) xs
forall a b. (a -> b) -> a -> b
$ (f' x -> Retract m g f x y) -> Requiring f' (Retract m g f) x y
forall k1 k2 (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1)
       (y :: k2).
(h x -> f x y) -> Requiring h f x y
Require ((f' x -> Retract m g f x y) -> Requiring f' (Retract m g f) x y)
-> (f' x -> Retract m g f x y) -> Requiring f' (Retract m g f) x y
forall a b. (a -> b) -> a -> b
$ \f' x
_ -> [Char] -> Retract m g f x y
forall a. HasCallStack => [Char] -> a
error [Char]
precondition) NP (f' -.-> (f -.-> f'')) xs
atTip
  where
    precondition :: String
    precondition :: [Char]
precondition = [Char]
"alignExtend: precondition violated"

-- | Version of 'alignExtend' that extends with an NS instead
alignExtendNS :: (Monad m, HasCallStack)
              => InPairs (Extend m g f) xs   -- ^ How to extend
              -> NP (f' -.-> f -.-> f'') xs  -- ^ Function to apply at the tip
              -> NS f' xs                    -- ^ NS we are aligning with
              -> Telescope g f xs -> m (Telescope g f'' xs)
alignExtendNS :: InPairs (Extend m g f) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> NS f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
alignExtendNS InPairs (Extend m g f) xs
es NP (f' -.-> (f -.-> f'')) xs
atTip NS f' xs
ns = NP (f' -.-> (f -.-> f'')) xs
-> (SListI xs => Telescope g f xs -> m (Telescope g f'' xs))
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (f' -.-> (f -.-> f'')) xs
atTip ((SListI xs => Telescope g f xs -> m (Telescope g f'' xs))
 -> Telescope g f xs -> m (Telescope g f'' xs))
-> (SListI xs => Telescope g f xs -> m (Telescope g f'' xs))
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall a b. (a -> b) -> a -> b
$
   InPairs (Requiring (K ()) (Extend m g f)) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> Telescope (K ()) f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
forall k (m :: * -> *) (g' :: k -> *) (g :: k -> *) (f :: k -> *)
       (xs :: [k]) (f' :: k -> *) (f'' :: k -> *).
(Monad m, HasCallStack) =>
InPairs (Requiring g' (Extend m g f)) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
alignExtend
     ((forall (x :: k) (y :: k).
 Extend m g f x y -> Requiring (K ()) (Extend m g f) x y)
-> InPairs (Extend m g f) xs
-> InPairs (Requiring (K ()) (Extend m g f)) xs
forall k (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *).
SListI xs =>
(forall (x :: k) (y :: k). f x y -> g x y)
-> InPairs f xs -> InPairs g xs
InPairs.hmap ((K () x -> Extend m g f x y) -> Requiring (K ()) (Extend m g f) x y
forall k1 k2 (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1)
       (y :: k2).
(h x -> f x y) -> Requiring h f x y
Require ((K () x -> Extend m g f x y)
 -> Requiring (K ()) (Extend m g f) x y)
-> (Extend m g f x y -> K () x -> Extend m g f x y)
-> Extend m g f x y
-> Requiring (K ()) (Extend m g f) x y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Extend m g f x y -> K () x -> Extend m g f x y
forall a b. a -> b -> a
const) InPairs (Extend m g f) xs
es)
     NP (f' -.-> (f -.-> f'')) xs
atTip
     (NS f' xs -> Telescope (K ()) f' xs
forall k (f :: k -> *) (xs :: [k]).
NS f xs -> Telescope (K ()) f xs
fromTip NS f' xs
ns)

-- | Internal auxiliary to 'extendIf' and 'retractIf'
fromBool :: K Bool x -> (Maybe :.: K ()) x
fromBool :: K Bool x -> (:.:) Maybe (K ()) x
fromBool (K Bool
True)  = Maybe (K () x) -> (:.:) Maybe (K ()) x
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (Maybe (K () x) -> (:.:) Maybe (K ()) x)
-> Maybe (K () x) -> (:.:) Maybe (K ()) x
forall a b. (a -> b) -> a -> b
$ K () x -> Maybe (K () x)
forall a. a -> Maybe a
Just (K () x -> Maybe (K () x)) -> K () x -> Maybe (K () x)
forall a b. (a -> b) -> a -> b
$ () -> K () x
forall k a (b :: k). a -> K a b
K ()
fromBool (K Bool
False) = Maybe (K () x) -> (:.:) Maybe (K ()) x
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (Maybe (K () x) -> (:.:) Maybe (K ()) x)
-> Maybe (K () x) -> (:.:) Maybe (K ()) x
forall a b. (a -> b) -> a -> b
$ Maybe (K () x)
forall a. Maybe a
Nothing

{-------------------------------------------------------------------------------
  Additional API
-------------------------------------------------------------------------------}

newtype ScanNext h g x y = ScanNext { ScanNext h g x y -> h x -> g x -> h y
getNext :: h x -> g x -> h y }

-- | Telescope analogue of 'scanl' on lists
--
-- This function is modelled on
--
-- > scanl :: (b -> a -> b) -> b -> [a] -> [b]
--
-- but there are a few differences:
--
-- * Since every seed has a different type, we must be given a function
--   for each transition.
-- * Unlike 'scanl', we preserve the length of the telescope
--   ('scanl' prepends the initial seed)
-- * Instead of generating a telescope containing only the seeds, we
--   instead pair the seeds with the elements.
scanl :: InPairs (ScanNext h g) (x ': xs)
      -> h x
      -> Telescope g f (x ': xs)
      -> Telescope (Product h g) (Product h f) (x ': xs)
scanl :: InPairs (ScanNext h g) (x : xs)
-> h x
-> Telescope g f (x : xs)
-> Telescope (Product h g) (Product h f) (x : xs)
scanl = InPairs (ScanNext h g) (x : xs)
-> h x
-> Telescope g f (x : xs)
-> Telescope (Product h g) (Product h f) (x : xs)
forall a (h :: a -> *) (g :: a -> *) (x' :: a) (xs' :: [a])
       (f :: a -> *).
InPairs (ScanNext h g) (x' : xs')
-> h x'
-> Telescope g f (x' : xs')
-> Telescope (Product h g) (Product h f) (x' : xs')
go
  where
    go :: InPairs (ScanNext h g) (x' ': xs')
       -> h x'
       -> Telescope g f (x' ': xs')
       -> Telescope (Product h g) (Product h f) (x' ': xs')
    go :: InPairs (ScanNext h g) (x' : xs')
-> h x'
-> Telescope g f (x' : xs')
-> Telescope (Product h g) (Product h f) (x' : xs')
go InPairs (ScanNext h g) (x' : xs')
_            h x'
hx (TZ f x
fx)   = Product h f x' -> Telescope (Product h g) (Product h f) (x' : xs')
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ (h x' -> f x' -> Product h f x'
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair h x'
hx f x'
f x
fx)
    go (PCons ScanNext h g x y
f InPairs (ScanNext h g) (y : zs)
fs) h x'
hx (TS g x
gx Telescope g f xs
t) = Product h g x'
-> Telescope (Product h g) (Product h f) (y : zs)
-> Telescope (Product h g) (Product h f) (x' : y : zs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS (h x' -> g x' -> Product h g x'
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair h x'
hx g x'
g x
gx) (Telescope (Product h g) (Product h f) (y : zs)
 -> Telescope (Product h g) (Product h f) (x' : y : zs))
-> Telescope (Product h g) (Product h f) (y : zs)
-> Telescope (Product h g) (Product h f) (x' : y : zs)
forall a b. (a -> b) -> a -> b
$ InPairs (ScanNext h g) (y : zs)
-> h y
-> Telescope g f (y : zs)
-> Telescope (Product h g) (Product h f) (y : zs)
forall a (h :: a -> *) (g :: a -> *) (x' :: a) (xs' :: [a])
       (f :: a -> *).
InPairs (ScanNext h g) (x' : xs')
-> h x'
-> Telescope g f (x' : xs')
-> Telescope (Product h g) (Product h f) (x' : xs')
go InPairs (ScanNext h g) (y : zs)
fs (ScanNext h g x y -> h x -> g x -> h y
forall k (h :: k -> *) (g :: k -> *) (x :: k) (y :: k).
ScanNext h g x y -> h x -> g x -> h y
getNext ScanNext h g x y
f h x'
h x
hx g x
g x
gx) Telescope g f xs
Telescope g f (y : zs)
t

{-------------------------------------------------------------------------------
  Standard type class instances
-------------------------------------------------------------------------------}

deriving instance ( All (Compose Eq g) xs
                  , All (Compose Eq f) xs
                  ) => Eq (Telescope g f xs)

deriving instance ( All (Compose Eq  g) xs
                  , All (Compose Ord g) xs
                  , All (Compose Eq  f) xs
                  , All (Compose Ord f) xs
                  ) => Ord (Telescope g f xs)

deriving instance ( All (Compose Show g) xs
                  , All (Compose Show f) xs
                  ) => Show (Telescope g f xs)

instance ( All (Compose NoThunks g) xs
         , All (Compose NoThunks f) xs
         ) => NoThunks (Telescope g f xs) where
  showTypeOf :: Proxy (Telescope g f xs) -> [Char]
showTypeOf Proxy (Telescope g f xs)
_ = [Char]
"Telescope"
  wNoThunks :: Context -> Telescope g f xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt = \case
      TZ f x
f   -> Context -> f x -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks ([Char]
"TZ" [Char] -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) f x
f
      TS g x
g Telescope g f xs
t -> [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo)
allNoThunks [
                   Context -> g x -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks ([Char]
"g" [Char] -> Context -> Context
forall a. a -> [a] -> [a]
: [Char]
"TS" [Char] -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) g x
g
                 , Context -> Telescope g f xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks ([Char]
"t" [Char] -> Context -> Context
forall a. a -> [a] -> [a]
: [Char]
"TS" [Char] -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) Telescope g f xs
t
                 ]