
  0 | module Syntax.E1
  1 | 
  2 | import public Data.Linear.ELift1
  3 | 
  4 | %default total
  5 | 
  6 | export %inline
  7 | map1 : (a -> b) -> E1 s es a -> E1 s es b
  8 | map1 f g t =
  9 |  let R v t := g t | E e t => E e t
 10 |   in R (f v) t
 11 | 
 12 | export %inline
 13 | (<$>) : (a -> b) -> E1 s es a -> E1 s es b
 14 | (<$>) = map1
 15 | 
 16 | export %inline
 17 | (<&>) : E1 s es a -> (a -> b) -> E1 s es b
 18 | (<&>) = flip map1
 19 | 
 20 | export %inline
 21 | ignore1 : E1 s es a -> E1' s es
 22 | ignore1 f t =
 23 |  let R _ t := f t | E e t => E e t
 24 |   in R () t
 25 | 
 26 | export %inline
 27 | pure : a -> E1 s es a
 28 | pure = R
 29 | 
 30 | export %inline
 31 | (>>=) : E1 s es a -> (a -> E1 s es b) -> E1 s es b
 32 | (>>=) f g t1 =
 33 |  let R v t2 := f t1 | E e t2 => E e t2
 34 |   in g v t2
 35 | 
 36 | export %inline
 37 | (>>) : E1' s es -> E1 s es b -> E1 s es b
 38 | (>>) f g = E1.(>>=) f (\(),t => g t)
 39 | 
 40 | export %inline
 41 | (<*) : E1 s es b -> E1' s es -> E1 s es b
 42 | (<*) f g t =
 43 |   let R v t := f t | E e t => E e t
 44 |       R _ t := g t | E e t => E e t
 45 |    in R v t
 46 | 
 47 | export %inline
 48 | (<*>) : E1 s es (a -> b) -> E1 s es a -> E1 s es b
 49 | (<*>) f g = E1.do
 50 |   fn <- f
 51 |   v  <- g
 52 |   pure (fn v)
 53 |