uds/ASDS/Lens.icl

   1 implementation module ASDS.Lens
   2
   3 import StdEnv
   4 import Data.Func
   5 import Data.Functor
   6 import Data.List
   7 import Data.Maybe
   8 import Control.Monad
   9 import Control.Monad.Fail
  10 from Data.Map import :: Map(..), get, put
  11
  12 import ASDS, ASDS.Source
  13
  14 lens :: (p -> p1) (LensRead m p r r1) (LensWrite m p w r1 w1) (sds m p1 r1 w1) -> Lens sds m p r w | TC r1 & TC w1 & TC p1
  15 lens param mapr mapw lens = Lens {param=param,mapr=mapr,mapw=mapw,lens=lens}
  16
  17 instance read (Lens sds) | read sds
  18 where
  19         read (Lens t=:{mapr=LensReadConst f}) p = Read <$> f p
  20         read (Lens t=:{param,mapr=LensRead mapr,lens}) p = read lens (param p) >>= \v->case v of
  21                 Reading s = pure $ Reading $ Lens {t & lens=s}
  22                 Read r = Read <$> mapr p r
  23
  24 instance write (Lens sds) | read sds & write sds
  25 where
  26         //First read the child when necessary
  27         write (Lens t=:{param,mapw=LensWrite mapw,lens}) p w = read lens (param p) >>= \v->case v of
  28                 Reading s = pure $ Writing $ Lens {t & lens=rwpair s lens}
  29                 Read r = write (Lens {t & mapw=LensWriteConst \p w->mapw p w r}) p w
  30         //Then do the actual writing
  31         write (Lens t=:{param,mapw=LensWriteConst mapw,lens}) p w = mapw p w >>= \v->case v of
  32                 ?None = pure $ Written ()
  33                 ?Just w = write lens (param p) w >>= \v->case v of
  34                         Writing s = pure $ Writing $ Lens {t & lens=rwpair lens s}
  35                         Written () = pure $ Written ()
  36
  37 mapRead :: (r -> m r`) (sds m p r w) -> Lens sds m p r` w | TC r` & TC r & TC w & TC p & Monad m
  38 mapRead f sds = lens id (LensRead \p->f) (LensWrite \p w r->pure $ ?Just w) sds
  39
  40 mapWrite :: (w` r -> m (? w)) (sds m p r w) -> Lens sds m p r w` | TC r & TC w & TC w` & TC p & Monad m
  41 mapWrite f sds = lens id (LensRead \p r->pure r) (LensWrite \_ w r->f w r) sds
  42
  43 translate :: (p -> ps) (sds m ps r w) -> Lens sds m p r w | TC r & TC w & TC p & TC ps & Monad m
  44 translate param sds = lens param (LensRead \p r->pure r) (LensWriteConst \p w->pure $ ?Just w) sds
  45
  46 fromDynStore :: (sds m p Dynamic Dynamic) -> Lens sds m p r w | TC r & TC w & TC p & MonadFail m
  47 fromDynStore sds = lens id (LensRead read) (LensWriteConst write) sds
  48 where
  49         read p (r :: r^) = pure r
  50         read p r = fail $ "fromDynStore: " +++ typeMismatchError r (dynamic undef :: r^)
  51         write p w = pure $ ?Just (dynamic w)
  52
  53 toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m
  54 toDynStore sds = lens id (LensRead read) (LensWriteConst write) sds
  55 where
  56         read p r = pure (dynamic r)
  57         write p (w :: w^) = pure $ ?Just w
  58         write p w = fail $ "toDynStore: " +++ typeMismatchError w (dynamic undef :: w^)
  59
  60 typeMismatchError :: Dynamic Dynamic -> String
  61 typeMismatchError a b = "type mismatch " +++ toString (typeCodeOfDynamic a) +++ " and" +++ toString (typeCodeOfDynamic b)
  62
  63 indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m
  64 indexedStore sds = lens param (LensRead read) (LensWrite write) sds
  65 where
  66         param (p, _) = p
  67         read (_, idx) r = case r !? idx of
  68                 ?None = fail "indexedStore: index out of range"
  69                 ?Just a = pure a
  70         write (_, idx) w r = pure $ ?Just $ updateAt idx w r
  71
  72 assocStore :: (sds m p [(k, v)] [(k, v)]) -> Lens sds m (p, k) v v | TC v & TC k & Eq k & TC p & MonadFail m
  73 assocStore sds = lens param (LensRead read) (LensWrite write) sds
  74 where
  75         param (p, _) = p
  76         read (_, k) r = case lookup k r of
  77                 ?None = fail "assocStore: key not present"
  78                 ?Just a = pure a
  79         write (_, k) w r = pure $ ?Just [(k, w):filter ((<>) k o fst) r]
  80
  81 keyedStore :: (sds m p (Map k v) (Map k v)) -> Lens sds m (p, k) v v | TC v & TC k & < k & TC p & MonadFail m
  82 keyedStore sds = lens param (LensRead read) (LensWrite write) sds
  83 where
  84         param (p, _) = p
  85         read (_, k) r = case get k r of
  86                 ?None = fail "keyedStore: key not present"
  87                 ?Just a = pure a
  88         write (_, k) w r = pure $ ?Just $ put k w r