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