uds/test.icl

   1 module test
   2
   3 import StdEnv
   4 import Data.Maybe
   5 import Data.Functor
   6 import Data.Func
   7 import Data.Tuple
   8 import Data.List
   9 import Control.Applicative
  10 import Control.Monad
  11 import qualified Data.Map
  12
  13 class get v ~st :: (v r w) .st -> .(Maybe r, .st) | TC r
  14 class put v ~st :: w (v r w) .st -> .(Maybe (), .st) | TC w
  15
  16 :: SDS sds a :== sds a a
  17
  18 :: Source r w = Source String
  19 :: St :== 'Data.Map'.Map String Dynamic
  20
  21 instance get Source St
  22 where
  23         get (Source n) st = case 'Data.Map'.get n st of
  24                 Just (a :: a^) = (Just a, st)
  25                 _ = (Nothing, st)
  26
  27 instance put Source St
  28 where
  29         put w (Source n) st = (Just (), 'Data.Map'.put n (dynamic w) st)
  30
  31 :: Par sdsl sdsr r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
  32 :: ParOpts sdsl sdsr r1 r2 w1 w2 r w =
  33         { read  :: r1 r2 -> Maybe r
  34         , write :: w -> Maybe (w1, w2)
  35         , left  :: sdsl r1 w1
  36         , right :: sdsr r2 w2
  37         }
  38 (>*<) infixl 6 :: (sdsl r1 w1) (sdsr r2 w2) -> Par sdsl sdsr (r1, r2) (w1, w2) | get sdsl St & put sdsr St & TC r1 & TC r2 & TC w1 & TC w2
  39 (>*<) l r = Par {read= \x y->Just (x, y), write=Just, left=l, right=r}
  40
  41 instance get (Par sdsl sdsr) St | get sdsl St & get sdsr St
  42 where
  43         get (Par {read,left,right}) st
  44                 # (ml, st) = get left st
  45                 # (mr, st) = get right st
  46                 = (join $ read <$> ml <*> mr, st)
  47 instance put (Par sdsl sdsr) St | put sdsl St & put sdsr St
  48 where
  49         put w (Par {write,left,right}) st
  50                 = case write w of
  51                         Just (w1, w2)
  52                                 # (ml, st) = put w1 left st
  53                                 # (mr, st) = put w2 right st
  54                                 = (ml *> mr, st)
  55                         Nothing = (Nothing, st)
  56
  57 :: Lens sds r w = E.r1 w1: Lens (LensOpts sds r1 w1 r w) & TC r1 & TC w1
  58 :: LensOpts sds r1 w1 r w =
  59         { mapr :: r1   -> Maybe r
  60         , mapw :: w r1 -> Maybe w1
  61         , lens :: sds r1 w1
  62         }
  63
  64 instance get (Lens sds) St | get sds St
  65 where
  66         get (Lens {mapr,lens}) st = appFst ((=<<) mapr) $ get lens st
  67 instance put (Lens sds) St | get sds St & put sds St
  68 where
  69         put w (Lens {mapw,lens}) st
  70                 # (mv, st) = get lens st
  71                 = case mv of
  72                         Just r = case mapw w r of
  73                                 Just w = put w lens st
  74                                 Nothing = (Nothing, st)
  75                         Nothing = (Nothing, st)
  76
  77 :: Select sdsl sdsr r w = E.r1 w1: Select (SelectOpts sdsl sdsr r1 w1 r w) & TC r1 & TC w1
  78 :: SelectOpts sdsl sdsr r1 w1 r w =
  79         { select :: sdsl r1 w1
  80         , bind   :: r1 -> (sdsr r w)
  81         }
  82
  83 instance get (Select sdsl sdsr) St | get sdsl St & get sdsr St
  84 where
  85         get (Select {select,bind}) st
  86                 = case get select st of
  87                         (Just r, st)  = get (bind r) st
  88                         (Nothing, st) = (Nothing, st)
  89 instance put (Select sdsl sdsr) St | get sdsl St & put sdsr St
  90 where
  91         put w (Select {select,bind}) st
  92                 = case get select st of
  93                         (Just r, st) = put w (bind r) st
  94                         (Nothing, st) = (Nothing, st)
  95
  96 mapRead :: (r -> r`) (sds r w) -> Lens sds r` w | TC r` & TC r & TC w
  97 mapRead f sds = Lens {mapr=Just o f, mapw=const o Just, lens=sds}
  98 (>?@) infixl 6
  99 (>?@) :== mapRead
 100
 101 mapWrite :: (w` r -> Maybe w) (sds r w) -> Lens sds r w` | TC r & TC w & TC w`
 102 mapWrite f sds = Lens {mapr=Just, mapw=f, lens=sds}
 103 (>!@) infixl 6
 104 (>!@) :== mapWrite
 105
 106 indexedStore :: Int (SDS sds [a]) -> SDS (Lens sds) a | TC a
 107 indexedStore idx sds
 108         = Lens
 109                 { mapr = \r->r !? idx
 110                 , mapw = \w->Just o updateAt idx w
 111                 , lens = sds
 112                 }
 113
 114 indexedSelect :: (sdsl Int z) (SDS sdsr [a]) -> SDS (Select sdsl (Lens sdsr)) a | TC a & TC z
 115 indexedSelect l r = Select {select=l, bind=flip indexedStore r}
 116
 117 keyedSelect :: (sdsl k z) (SDS sdsr ('Data.Map'.Map k v)) -> SDS (Select sdsl (Lens sdsr)) v | TC z & TC v & TC k & < k
 118 keyedSelect l r = Select {select=l, bind=flip keyedStore r}
 119
 120 keyedStore :: k (SDS sds ('Data.Map'.Map k v)) -> SDS (Lens sds) v | TC v & TC k & < k
 121 keyedStore key sds
 122         = Lens
 123                 { mapr = 'Data.Map'.get key
 124                 , mapw = \r->Just o 'Data.Map'.put key r
 125                 , lens = sds
 126                 }
 127
 128 Start = appSnd 'Data.Map'.toList
 129         $ put (42, "blurp") (store "foo" >*< store "bar") 'Data.Map'.newMap
 130
 131 store :: (String -> Source a a) | TC a
 132 store = Source