packages feed

bff-mono (empty) → 0.2.0

raw patch · 9 files changed

+684/−0 lines, 9 filesdep +basedep +containersdep +mtlsetup-changed

Dependencies added: base, containers, mtl

Files

+ Data/BffMono.hs view
@@ -0,0 +1,44 @@+{-| +  The module provides an automatic way to construct a bidirectional+  transformation (rougly speaking, a getter/setter pair) +  from a uni-directional transformation (or, a getter function).++  The module provides a class 'PackM'. Once we write a transformation of type ++  @+  h :: (Traversable src, Traversable tgt) => forall a m.PackM c a m => src a -> m (tgt a)+  @ ++  then applying 'fwd' to obtain a forward transformation (so-called \"get\" or \"getter\") +  +  @+  fwd h :: src c -> tgt c +  @++  and applying `bwd` to obtain a backward transformation (so-called \"put\" or \"setter\").++  @+  bwd h :: (MonadError e m, Error e) => src c -> tgt c -> m (src c)+  @++  assuming that @c@ is some concrete type and @src@ and @tgt@ are some +  concrete containers ('Data.Traversable' instances) with @Eq c@ and @Eq (tgt ())@.++  The correctness of the obtained bidirectional transformation +  (GetPut and PutGet) is guaranted for free. That is, the following laws hold+  (assuming that we use @'Either' 'String'@ for the result of 'bwd').++  prop> bwd h s (fwd h s) = Right s +  prop> bwd h s v = Right s'  implies fwd h s' = v  ++  +-}++module Data.BffMono+    (+     Pack(..), PackM(..), liftO1, liftO2, +     fwd, bwd+    ) where ++import Data.BffMono.Base+
+ Data/BffMono/Base.hs view
@@ -0,0 +1,214 @@+{-#+  LANGUAGE +    FlexibleInstances, MultiParamTypeClasses, +    FunctionalDependencies, Rank2Types,+    ImpredicativeTypes, FlexibleContexts, +    PatternGuards +  #-}+++module Data.BffMono.Base where ++import Data.Traversable hiding (mapM)++import Data.Foldable (Foldable)+import qualified Data.Foldable as Foldable ++import Data.BffMono.CheckHistory ++import Data.BffMono.EquivMap (EquivMap) +import qualified Data.BffMono.EquivMap as EM +import Data.BffMono.EquivWitness (EquivWitness)+import qualified Data.BffMono.EquivWitness as EW++-- from mtl +import Control.Monad.Error +import Control.Monad.State +import Control.Monad.Identity ++----------------------------------------------------------------+-- | @Pack conc abs@ provides a way to abstract @conc@ by @abs@. +class Pack conc abs | abs -> conc where +    new :: conc -> abs ++class (Pack conc abs, Monad m, Functor m) => +       PackM conc abs m where+    liftO :: Eq r => ([conc] -> r) -> ([abs] -> m r)+    -- ^ Lifts @conc@-level observations to @abs@ level, with +    --   recording the examined values and the observed result. ++    eqSync :: Eq conc => abs -> abs -> m Bool +    -- ^ Lifts @conc@-level equivalence with synchronization ++    compareSync :: Ord conc => abs -> abs -> m Ordering +    -- ^ Lifts @conc@-level ordering.+    --   It synchronizes the elements if the comparison result is EQ ++-- | A special version of 'liftO' for unary observations.+liftO1 :: (PackM conc abs m, Eq r) => (conc -> r) -> abs -> m r +liftO1 f x = liftO (\[a] -> f a) [x]+++-- | A special version of 'liftO' for binary observations.+liftO2 :: (PackM conc abs m, Eq r) +          => (conc -> conc -> r) -> abs -> abs -> m r +liftO2 f x y = liftO (\[a,b] -> f a b) [x,y]+++-- | Abstract pointer.+--   @InSource i@ means i-th position in the original source. +--   @InTrans@ means outside of the original source.+data Location = InSource Int | InTrans+                deriving (Show, Eq, Ord)++-- | Datum with its pointer +data Loc a = Loc { body :: a, location :: Location }+           deriving (Show, Eq, Ord)++-- | Update is a mapping from source locations to elements+-- type Update a = IntMap a+type Update a = EquivMap Int a ++----------------------------------------------------------------++++-- | @update elem@ applies the update in a state to the source element @elem@.++update :: MonadState (Update a) m => Loc a -> m (Loc a)+update (Loc a InTrans)      = return $ Loc a InTrans +update (Loc a (InSource i)) = +    do { r <- EM.lookupM i+       ; case r of +           Nothing -> return $ Loc a (InSource i)+           Just b  -> return $ Loc b (InSource i)}++++-- | 'assignIDs' assigns a distict 'Index' for each source element. +assignIDs :: Traversable f => f a -> f (Loc a) +assignIDs t = +    evalState (traverse f t) 0+        where+          f x = do { i <- get+                   ; put (i+1)+                   ; return $ Loc x (InSource i) }++errMsgInconsistent :: Error e => e +errMsgInconsistent = strMsg "Inconsistent Update!"++errMsgConstant :: Error e => e +errMsgConstant = strMsg "Update on Constant!"+++{- This version does not check the all the duplicates are updated as in +   the same way -} +matchViews :: (Eq a,Functor f,Foldable f, Eq (f ()), MonadError e m, Error e)+              => f (Loc a) -> f a -> EquivWitness Int -> m (Update a) +matchViews xview view equiv =+    if isShapeEqual xview view then +        makeUpd (EW.emptyMap equiv) $ filter hasUpdated+                    $ zip (Foldable.toList xview) (Foldable.toList view)+    else+        throwError $ strMsg "Shape Mismatch!"+    where+      hasUpdated (Loc x _, y) = x /= y +      makeUpd upd [] = return upd +      makeUpd upd ((Loc _ InTrans,y):ps) = throwError errMsgConstant +      makeUpd upd ((Loc _ (InSource i), y):ps) =+          case EM.lookup i upd of +            (Just z, upd') -> +                if z == y then +                    makeUpd upd' ps +                else+                    throwError errMsgInconsistent +            (Nothing, upd') -> +                makeUpd (EM.insert i y upd) ps +      isShapeEqual :: (Functor f, Eq (f ())) => f a -> f b -> Bool +      isShapeEqual x y =  void x == void y +          +          +++------------------------------------------------------++-- | used internally +instance Pack a (Identity a) where +    new = Identity ++-- | used internally +instance PackM a (Identity a) Identity where +    liftO obs xs = return $ obs (map runIdentity xs)+    eqSync x y  = return $ runIdentity x == runIdentity y +    compareSync x y = return $ runIdentity x `compare` runIdentity y +                 +-- | used internally +instance Pack a (Loc a) where +    new a = Loc a InTrans ++-- We record checking histories by a State-monad for efficiency, +-- unlike what written in the paper. +type B a = State ([CheckResult (Loc a)], EquivWitness Int)+++unB :: B a b -> (b, [CheckResult (Loc a)], EquivWitness Int)+unB m =+    let (x,(h,t)) = runState m ([], EW.empty)+    in (x,h,t)++-- | used internally +instance PackM a (Loc a) (B a) where +    liftO obs xs = do { modify (\(h,t) -> (CheckResult obs' xs (obs' xs):h,t))+                      ; return $ obs' xs }+        where+          obs' xs = obs (map body xs)++    eqSync x y +        | body x == body y, InSource i <- location x, InSource j <- location y = +              do { modify (\(h,t) -> (h, EW.equate i j t))+                 ; return True }+        | otherwise = liftO2 (==) x y ++    compareSync x y +        |  EQ <- compare x y, InSource i <- location x, InSource j <- location y =+              do { modify (\(h,t) -> (h, EW.equate i j t))+                 ; return EQ }+        | otherwise = liftO2 compare x y +          +                          ++------------------------------------------------------++-- | Constructs a backward transformation (or, \"put\" or+--   \"setter\") from a given function.+bwd :: (Eq (vf ()), Traversable vf, Traversable sf, Eq c,+        MonadError e n, Error e) =>+       (forall a m. (PackM c a m) => sf a -> m (vf a)) ->+           sf c -> vf c -> n (sf c)+bwd pget src view =+        do { upd <- matchViews xview view equiv +           ; let (b,upd') = runState (checkHistory update hist) upd +           ; if b then +                 let u x = evalState (update x) upd' +                 in return $ fmap (body . u) xsrc +             else+                 throwError $ strMsg "Violated Invariants"}+    where+      xsrc = assignIDs src +      (xview, hist, equiv) = unB' (pget xsrc) +      -- for type inference +      unB' = unB :: B c (sf (Loc c))+                    -> (sf (Loc c), +                        [CheckResult (Loc c)], +                        EquivWitness Int) +++-- | Constructs a forward transformation (or, \"get\" or \"getter\") from a+--   given function. +fwd :: (Traversable vf, Traversable sf) =>+       (forall a m. (PackM c a m) => sf a -> m (vf a)) ->+           sf c -> vf c+fwd pget src =+    let Identity r = pget $ fmap Identity src +    in fmap runIdentity r+
+ Data/BffMono/CheckHistory.hs view
@@ -0,0 +1,25 @@+{-# LANGUAGE Rank2Types, ExistentialQuantification #-}++module Data.BffMono.CheckHistory where +++-- | 'CheckResult' stores an observation result.  It consists of an+--   observation function, a list observed elements and an observation+--   result. We used an existential type here to store heterogeneous+--   observation results into a list.++data CheckResult a = forall b. Eq b => +                     CheckResult ([a] -> b) [a] b +                     +-- | Checks if an update does not change a recorded observation+checkResult :: Monad m => (a -> m a) -> CheckResult a -> m Bool +checkResult u (CheckResult test as r) = +    do { as' <- mapM u as +       ; return $ test as' == r }++-- | Checks if an update does not change all the recorded observation results +checkHistory :: Monad m => (a -> m a) -> [CheckResult a] -> m Bool +checkHistory u hist = +    do { bs <- mapM (checkResult u) hist +       ; return $ and bs }+
+ Data/BffMono/EquivMap.hs view
@@ -0,0 +1,145 @@+{-|++An implementation of maps based on Union-Find. ++-}+{-# LANGUAGE FlexibleContexts  #-}++module Data.BffMono.EquivMap +    (+     EquivMap+    , equals, equalsM+    , equate, equateM+    , lookup, lookupM+    , insert, insertM+    , empty+    ) +    where ++import Prelude hiding (lookup)++import Data.IntMap (IntMap) +import qualified Data.IntMap as IM+import Data.Map (Map) +import qualified Data.Map as M ++import Data.Maybe (fromJust) ++import Control.Monad.State ++data EquivMap k a =+    EquivMap {+      elemMap :: Map k Int,+       -- ^ mapping from keys to integers +      tree :: IntMap Int,+       -- ^ body of union-find tree (negative value means -rank) +      valueMap :: IntMap a+       -- ^ mapping to values (only correct for a root) +    }++-- | Checks that two keys are in the same set or not. +--   The resulting EquivMap is tuned for later queries. +equals :: Ord k => k -> k -> EquivMap k a -> (Bool, EquivMap k a) +equals x1 x2 t =+    let (r1,t1) = find x1 t +        (r2,t2) = find x2 t1 +    in (r1 == r2, t2)++-- | Monadic-version of @equals@+equalsM :: (MonadState (EquivMap k a) m, Ord k) => k -> k -> m Bool +equalsM x1 x2 =+    do { t <- get +       ; let (r,t') = equals x1 x2 t+       ; put t' +       ; return r }++-- | Empty map +empty :: EquivMap k a +empty = EquivMap M.empty IM.empty IM.empty ++-- | "find" of "Union-Find" +find :: Ord k => k -> EquivMap k a -> (Int, EquivMap k a) +find k equivMap =+    case M.lookup k (elemMap equivMap) of +      Nothing -> +          let i  = M.size (elemMap equivMap)+              equivMap' = +                  equivMap { elemMap = M.insert k i (elemMap equivMap)+                           , tree = IM.insert i (-1) (tree equivMap) }+          in (i, equivMap')+      Just i -> +          let (root, t') = findAux i (tree equivMap) +          in (root, equivMap { tree = t' } )+    where+      findAux i t =+          let p = fromJust $ IM.lookup i t +          in if p < 0 then +                 (i,t) +             else +                 let (root,t') = findAux p t +                 in (root, IM.insert i root t')++-- | Unify the set of the given two keys. This operation corresponds to +--   "Union" of "Union-Find". +--+--   FIXME: The function does not touch the values associated with the keys +--          This does not affect the correctness of our bidirectionalization, +--          which does not call @equate@ after @insert@ and @lookup@. +equate :: Ord k => k -> k -> EquivMap k a -> EquivMap k a +equate a1 a2 equivMap =+    let (root1, equivMap1) = find a1 equivMap+        (root2, equivMap2) = find a2 equivMap1+        rk1 = - (fromJust $ IM.lookup root1 $ tree equivMap2)+        rk2 = - (fromJust $ IM.lookup root2 $ tree equivMap2)+    in if root1 == root2 then +           equivMap2 +       else+           if rk1 < rk2 then +               insertUF root1 root2 rk1 rk2 (tree equivMap2) equivMap2+           else+               insertUF root2 root1 rk2 rk1 (tree equivMap2) equivMap2 +    where+      insertUF r1 r2 rk1 rk2 t em =+          let t'  = IM.insert r1 (- (rk1 + rk2)) t+              t'' = IM.insert r2 r1 t'+          in em { tree = t'' } ++-- | Monadic version of @equte@+equateM :: (MonadState (EquivMap k a) m, Ord k) => k -> k -> m ()+equateM a1 a2 = modify (equate a1 a2) +       ++-- | Associates a value to the set that contains the given key +insert :: Ord k => k -> a -> EquivMap k a -> EquivMap k a +insert k v equivMap =+    let (i, equivMap') = find k equivMap +    in equivMap' { valueMap = IM.insert i v (valueMap equivMap') }++-- | A monadic version of @insert@ +insertM :: (MonadState (EquivMap k a) m, Ord k) => k -> a -> m ()+insertM k v = modify (insert k v) +    +-- | Loops-up values associated with the set of the given key +lookup :: Ord k => k -> EquivMap k a -> (Maybe a, EquivMap k a) +lookup k equivMap =+    let (i, equivMap') = find k equivMap +    in (IM.lookup i (valueMap equivMap'), equivMap')++-- | A monadic version of @lookup@+lookupM :: (MonadState (EquivMap k a) m, Ord k) => k -> m (Maybe a)+lookupM k =+    do { t <- get +       ; let (r,t') = lookup k t+       ; put t'+       ; return r }+++++                                   +                   +                   +              +++                  
+ Data/BffMono/EquivWitness.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE FlexibleContexts, Rank2Types  #-}+{-| +  A restricted version of @EquivMap@, which just records equivalence. + -} +module Data.BffMono.EquivWitness +     (+       EquivWitness+     , equals, equate, empty+     , emptyMap +     )+    where ++import qualified Data.BffMono.EquivMap as EM +++newtype EquivWitness k = EquivWitness (forall a. EM.EquivMap k a)++emptyMap :: EquivWitness k -> EM.EquivMap k a +emptyMap (EquivWitness w) = w ++empty :: EquivWitness k +empty = EquivWitness EM.empty ++equals :: Ord k => k -> k -> EquivWitness k -> (Bool , EquivWitness k)+equals x y (EquivWitness t) =+    let (r,t') = EM.equals x y t+    in (r, EquivWitness t') ++equate :: Ord k => k -> k -> EquivWitness k -> EquivWitness k +equate x y (EquivWitness t) =+    let t' = EM.equate x y t +    in EquivWitness t'
+ Data/BffMono/Utility.hs view
@@ -0,0 +1,155 @@+{-|+  The module provides counterparts of @..By@ functions in "Data.List"+  for monadic observations. +-}+module Data.BffMono.Utility +    ( +     ifM, nubByM, deleteByM, deleteFirstByM, unionByM, +     intersectByM, elemByM, groupByM, +     sortByM, insertByM, maximumByM, minimumByM, +     traceM +     ) where +++import Control.Monad +import Debug.Trace +    +ifM :: Monad m => m Bool -> m a -> m a -> m a +ifM m x y = m >>= (\b -> if b then x else y)++traceM :: Monad m => m String -> m a -> m a +traceM m y = do { x <- m; trace x y }++nubByM :: Monad m => (a -> a -> m Bool) -> [a] -> m [a]+nubByM eq = f +    where+      f []     = return []+      f (x:xs) = do { r <- deleteByM eq x xs+                    ; y <- f r+                    ; return $ x:y }++deleteByM :: Monad m => (a -> a -> m Bool) -> a -> [a] -> m [a]+deleteByM _  _ []     = return []+deleteByM eq x (y:ys) = +    do { b <- eq x y +       ; r <- deleteByM eq x ys +       ; return (if b then r else y:r) }++deleteFirstByM :: Monad m => (a -> a -> m Bool) -> a -> [a] -> m [a]+deleteFirstByM _  _ []     = return []+deleteFirstByM eq x (y:ys) = +    do { b <- eq x y +       ; if b then +             return ys+         else +             do { r <- deleteFirstByM eq x ys+                ; return $ y:r }}++unionByM :: Monad m => (a -> a -> m Bool) -> [a] -> [a] -> m [a]+unionByM eq xs ys = +    do { ys' <- foldM (flip (deleteByM eq)) ys xs +       ; return $ xs ++ ys' }++intersectByM :: Monad m => (a -> a -> m Bool) -> [a] -> [a] -> m [a]+intersectByM eq xs ys = f xs+    where+      f [] = return []+      f (z:zs) = do { b <- elemByM eq z ys+                    ; r <- f zs +                    ; return (if b then z:r else r) }+      +    +elemByM :: Monad m => (a -> a -> m Bool) -> a -> [a] -> m Bool +elemByM _  _ []     = return False +elemByM eq x (y:ys) = +    do { b <- eq x y +       ; if b then +             return True +         else +             elemByM eq x ys}++groupByM :: Monad m => (a -> a -> m Bool) -> [a] -> m [[a]] +groupByM eq = g +    where+      g []     = return []+      g (x:xs) = f [x] xs +      f r  [] = return [reverse r] +      f (y:ys) (x:xs) =+          do { b <- eq x y +             ; if b then +                   f (x:y:ys) xs +               else+                   do { r <- f [x] xs +                      ; return $ reverse (y:ys):r }}++sortByM :: Monad m => (a -> a -> m Ordering) -> [a] -> m [a]+sortByM ord zs = ms (map (:[]) zs)+    where+      ms []  = return []+      ms [r] = return r+      ms r   = step r >>= ms ++      step []  = return []+      step [r] = return [r]+      step (xs:ys:rss) = +          do { xys  <- merge xs ys+             ; rss' <- step rss +             ; return $ xys : rss' }+    ++      merge [] ys = return ys+      merge xs [] = return xs +      merge (x:xs) (y:ys) = +          do { o <- ord x y +             ; case o of +                 EQ -> liftM ((x:) . (y:)) $ merge xs ys +                 LT -> liftM (x:) $ merge xs (y:ys)+                 GT -> liftM (y:) $ merge (x:xs) ys }++insertByM :: Monad m => (a -> a -> m Ordering) -> a -> [a] -> m [a]+insertByM ord = f +    where+      f a [] = return [a]+      f a (x:xs) =+          do { o <- ord a x  +             ; case o of +                 GT -> liftM (x:) $ f a xs +                 _  -> return (a:x:xs)}++maximumByM :: Monad m => (a -> a -> m Ordering) -> [a] -> m a+maximumByM ord = f +    where +      f []     = errorEmptyList "maximumByM"+      f (x:xs) = g x xs ++      g a []     = return a+      g a (x:xs) = +          do { o <- ord a x+             ; case o of +                 LT -> g x xs +                 _  -> g a xs}++minimumByM :: Monad m => (a -> a -> m Ordering) -> [a] -> m a+minimumByM ord = f +    where +      f []     = errorEmptyList "minimumByM"+      f (x:xs) = g x xs ++      g a []     = return a+      g a (x:xs) = +          do { o <- ord a x+             ; case o of +                 GT -> g x xs +                 _  -> g a xs}++errorEmptyList :: String -> a +errorEmptyList f = +    error ("Language.CheapB18n.Utility." ++ f ++ ": empty list")++++             +  +                         +    +    
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013, Kazutaka Matsuda++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Kazutaka Matsuda nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ bff-mono.cabal view
@@ -0,0 +1,37 @@+name:                bff-mono+version:             0.2.0+synopsis:            "Bidirectionalization for Free" for Monomorphic Transformations+description:         This package provides a way to make a bidirectional +                     transformation (a getter/setter pair, or so-called lens) +                     from a description of unidirectional transformation. +                     Like 'bff' package, the package constructs bidirectional +                     transformations based on the free theorem. +                     Unlike 'bff' package,+                     the package supports some of monomorphic transformations. +                     +                     +license:             BSD3+license-file:        LICENSE+author:              Kazutaka Matsuda, +                     Meng Wang+maintainer:          kztk@is.s.u-tokyo.ac.jp+category:            Language+build-type:          Simple+cabal-version:       >=1.8++homepage:            https://bitbucket.org/kztk/bff-mono/++library+  exposed-modules:     Data.BffMono+                       Data.BffMono.Utility++  other-modules:       Data.BffMono.Base +                       Data.BffMono.CheckHistory +                       Data.BffMono.EquivMap +                       Data.BffMono.EquivWitness +                       +  build-depends:       base >= 4 && < 5, mtl, containers+  +source-repository head+  type:   git+  location: https://bitbucket.org/kztk/bff-mono.git