0 | module Cont
 1 |
 2 | -- from http://www.vex.net/~trebla/haskell/cont.xhtml
 3 |
 4 | public export
 5 | data Cont : (r : Type) -> (a : Type) -> Type where
 6 |   ContOf : ((a -> r) -> r) -> Cont r a
 7 |
 8 | export
 9 | Functor (Cont r) where
10 |   map f (ContOf a_cps) = ContOf (\k => a_cps (k . f))
11 |
12 | export
13 | Applicative (Cont r) where
14 |   pure x = ContOf (\f => f x)
15 |   (ContOf f) <*> (ContOf v) = ContOf (\c => f (\g => v (c . g)))
16 |
17 | export
18 | Monad (Cont r) where
19 |   (ContOf a_cps) >>= arrb = ContOf (\k => a_cps (\a => let ContOf unCont = arrb a in unCont k))
20 |
21 | public export
22 | data DIterator : (i : Type)
23 |               -> (o : Type)
24 |               -> (i2 : Type)
25 |               -> (o2 : Type)
26 |               -> (r : Type)
27 |               -> Type
28 |               where
29 |   Result : r -> DIterator i o i2 o2 r
30 |   Susp  : o ->  ( i ->  DIterator i o i2 o2 r) -> DIterator i o i2 o2 r
31 |   Susp2 : o2 -> ( i2 -> DIterator i o i2 o2 r) -> DIterator i o i2 o2 r
32 |
33 | public export
34 | Iterator: Type -> Type -> Type -> Type
35 | Iterator i o r = DIterator i o Void Void r
36 |
37 | export
38 | toIterator : Cont (DIterator i o i2 o2 r) r -> DIterator i o i2 o2 r
39 | toIterator (ContOf unCont) = unCont Result
40 |
41 | export
42 | yieldGet : o -> Cont (DIterator i o i2 o2 r) i
43 | yieldGet = ContOf . Susp
44 |
45 | export
46 | yieldGet2 : o2 -> Cont (DIterator i o i2 o2 r) i2
47 | yieldGet2 = ContOf . Susp2
48 |