
  0 | module Pipeline.Basic
  1 | 
  2 | import public Data.Vect
  3 | import public Data.Vect.Utils
  4 | import public Data.Vect.Quantifiers
  5 | import Debug.Trace
  6 | 
  7 | public export
  8 | Pipeline : Nat -> Type
  9 | Pipeline length = Vect length Type
 10 | 
 11 | public export
 12 | Fn : Type -> Type -> Type
 13 | Fn x y = x -> y
 14 | 
 15 | public export
 16 | KleisliFn : (Type -> Type) -> Type -> Type -> Type
 17 | KleisliFn m x y = x -> m y
 18 | 
 19 | public export
 20 | Impl : Pipeline (2 + n) -> Type
 21 | Impl cs = All (uncurry Fn) (pairUp cs)
 22 | 
 23 | export
 24 | Run : (p : Pipeline (2 + n)) -> Impl p -> head p -> last p
 25 | Run [x, y] [f] v = f v
 26 | Run (s :: t :: x :: xs) (f :: cont) v = Run (t :: x :: xs) cont (f v)
 27 | 
 28 | export
 29 | RunTrace : (p : Pipeline (2 + n)) -> (print : All Show p) => Impl p -> head p -> last p
 30 | RunTrace {print = [p, q]} [x, y] [f] v = traceValBy show (f v)
 31 | RunTrace {print = p :: q :: ps} (s :: t :: x :: xs) (f :: cont) v =
 32 |   Run (t :: x :: xs) cont (traceValBy show (f v))
 33 | 
 34 | parameters {m : Type -> Type}
 35 | 
 36 |   public export
 37 |   ImplM : Pipeline (2 + n) -> Type
 38 |   ImplM cs = All (uncurry (KleisliFn m)) (pairUp cs)
 39 | 
 40 |   export
 41 |   RunM : (mon : Monad m) => (p : Pipeline (2 + n)) -> ImplM p -> Vect.head p -> m (Vect.last p)
 42 |   RunM [x, y]  [f] = f
 43 |   RunM (x :: y :: z :: xs) (f :: c) = RunM (y :: z :: xs) c <=< f
 44 | 
 45 | export
 46 | RunTraceM : Monad m => (p : Pipeline (2 + n)) -> (print : All Show p) => ImplM {m} p -> Vect.head p -> m (Vect.last p)
 47 | RunTraceM [x, y] {print = [p1, p2]} [f] = f >=> pure . traceValBy show
 48 | RunTraceM (x :: y :: z :: xs) {print = p :: q :: ps} (f :: c) =
 49 |   f >=> pure . traceValBy show >=> RunTraceM (y :: z :: xs) c
 50 | 
 51 |