module UVMHS.Lib.Pipeline where

import UVMHS.Core

-- | A `Pipeline` is essentially just a list of annotated monadic functions. Its
--   definitions uses a GADT to capture chaining `a → m b` with `b → m c` as a
--   `Pipeline` from `a` to `c`, and where `b` ends up existentially quantified
--   in the chain.
--   
--   A `Pipeline` 𝒸 m i a b` imposes constraint `𝒸` on all intermediate result
--   types of monadic computations in the list, annotates each function in the
--   list with a value of type `i`, and ultimately consumes a value of type `a`
--   and produces a value of type `m b`.
data Pipeline 𝒸 m i a b where
  UnitPipeline ∷ Pipeline 𝒸 m i a a
  StepPipeline ∷ (𝒸 b) ⇒ Pipeline 𝒸 m i a b → i → (b → m c) → Pipeline 𝒸 m i a c

runPipeline ∷ (Monad m) ⇒ Pipeline 𝒸 m i a b → a → m b
runPipeline :: forall (m :: * -> *) (𝒸 :: * -> Constraint) i a b.
Monad m =>
Pipeline 𝒸 m i a b -> a -> m b
runPipeline = \case
  Pipeline 𝒸 m i a b
UnitPipeline → a -> m a
a -> m b
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return
  StepPipeline Pipeline 𝒸 m i a b
fs i
_ b -> m b
f → b -> m b
f (b -> m b) -> (a -> m b) -> a -> m b
forall (m :: * -> *) b c a.
Bind m =>
(b -> m c) -> (a -> m b) -> a -> m c
*∘ Pipeline 𝒸 m i a b -> a -> m b
forall (m :: * -> *) (𝒸 :: * -> Constraint) i a b.
Monad m =>
Pipeline 𝒸 m i a b -> a -> m b
runPipeline Pipeline 𝒸 m i a b
fs