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 +44/−0
- Data/BffMono/Base.hs +214/−0
- Data/BffMono/CheckHistory.hs +25/−0
- Data/BffMono/EquivMap.hs +145/−0
- Data/BffMono/EquivWitness.hs +32/−0
- Data/BffMono/Utility.hs +155/−0
- LICENSE +30/−0
- Setup.hs +2/−0
- bff-mono.cabal +37/−0
+ 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