
  0 | module Stellar.API.Kleene
  1 | 
  2 | import Stellar.API
  3 | import Stellar.API.Morphism
  4 | 
  5 | %hide Prelude.Ops.infixl.(|>)
  6 | 
  7 | -- λ x : API -> μy . I + x ○ y
  8 | public export
  9 | data StarShp : API -> Type where
 10 |   Done : StarShp c
 11 |   More : Ex c (StarShp c) -> StarShp c
 12 | 
 13 | public export
 14 | data StarPos : (c : API) -> StarShp c -> Type where
 15 |   StarU : StarPos c Done
 16 |   StarM : (x : c.response x1) -> StarPos c (x2 x) -> StarPos c (More (MkEx x1 x2))
 17 | 
 18 | public export
 19 | (.star) : API -> API
 20 | (.star) c = (!>) (StarShp c) (StarPos c)
 21 | 
 22 | public export
 23 | Kleene : API -> API
 24 | Kleene c = (!>) (StarShp c) (StarPos c)
 25 | 
 26 | public export
 27 | mapStarShp : (a =&> b) -> StarShp a -> StarShp b
 28 | mapStarShp x Done = Done
 29 | mapStarShp x (More p1) =
 30 |   let xx = x.continuation p1.req
 31 |   in More (MkEx xx.π1 (\y => assert_total $ mapStarShp x (p1.cont (xx.π2 y))))
 32 | 
 33 | public export
 34 | mapStarPos : (mor : a =&> b) -> (x : StarShp a) -> StarPos b (mapStarShp mor x) -> StarPos a x
 35 | mapStarPos y Done z = StarU
 36 | mapStarPos y (More (MkEx p1 p2)) (StarM z1 z2) =  ?fixLater
 37 |   -- let yy = y.continuation z1
 38 |   -- in StarM (y.bwd p1 z1) (mapStarPos y (p2 (y.bwd p1 z1)) z2)
 39 | 
 40 | public export
 41 | map_kleene : a =&> b -> a.star =&> b.star
 42 | map_kleene mor = !! \x => mapStarShp mor x ## mapStarPos mor x
 43 | 
 44 | public export
 45 | join_star : forall a. StarShp a.star -> StarShp a
 46 | join_star Done = Done
 47 | join_star (More (MkEx Done p2)) = Done
 48 | join_star (More (MkEx (More p2) p3)) = More p2
 49 | 
 50 | public export
 51 | single : a.message -> StarShp a
 52 | single x = More (MkEx x (\_ => Done))
 53 | 
 54 | public export
 55 | pure_kleene : a =&> a.star
 56 | pure_kleene =
 57 |     !! \x => single {a} x ## \(StarM y1 y2) => y1
 58 | 
 59 | public export
 60 | unit_kleene : (End).star =&> End
 61 | unit_kleene = !! \x => () ## bwd x
 62 | 
 63 |   where
 64 |     bwd : (x : StarShp End) -> Unit -> StarPos End x
 65 |     bwd Done y = StarU
 66 |     bwd (More (MkEx () p2)) () = StarM () (bwd (p2 ()) ())
 67 | 
 68 | export
 69 | kleeneCounit : a =&> End -> a.star =&> End
 70 | kleeneCounit c = map_kleene c |&> unit_kleene
 71 | 
 72 | export
 73 | runStar : a =&> b.star -> b =&> End -> a =&> End
 74 | runStar m1 m2 = m1 |&> map_kleene m2 |&> unit_kleene
 75 | 
 76 | -- export
 77 | -- absorb : a &> a.star =&> a.star
 78 | -- absorb = !! \x => More x ## \(MkEx e1 e2), (StarM y1 y2) => y1 ## y2
 79 | 
 80 |