From: Nathaniel Wesley Filardo Date: Tue, 12 Feb 2013 07:12:57 +0000 (-0500) Subject: Fix and expand Analysis.Mode.Inst X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=913b9da50ad28b746631dd86f099c1a4a122ebaa;p=dyna2 Fix and expand Analysis.Mode.Inst Correct iSubGLB_ definition Add iEq_ and iSubLUB_ Expand commentary Better IBound-vs-IBound cases in GLB functions Some additional utilities appeared in XXX.DataUtils and XXX.MonadUtils. --- diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs index fc77bc4..79f1512 100644 --- a/src/Dyna/Analysis/Mode/Inst.hs +++ b/src/Dyna/Analysis/Mode/Inst.hs @@ -18,7 +18,9 @@ module Dyna.Analysis.Mode.Inst( InstF(..), iNotReached, iIsNotReached, - iUniq, iWellFormed_, iGround_, iSub_, iSubGLB_, iLeq_, iLeqGLB_, + iUniq, iWellFormed_, iEq_, iGround_, + iLeq_, iLeqGLB_, + iSub_, iSubGLB_, iSubLUB_, ) where -- import Control.Monad @@ -26,6 +28,7 @@ import qualified Data.Foldable as F import qualified Data.Traversable as T import qualified Data.Map as M -- import qualified Data.Set as S +import Dyna.XXX.DataUtils import Dyna.XXX.MonadUtils import Dyna.Analysis.Mode.Uniq @@ -170,14 +173,47 @@ iGround_ _ _ = return False ------------------------------------------------------------------------}}} -- Instantiation States: Binary predicates {{{ --- | Instantiatedness partial order with uniqueness +-- | Equality of two insts +iEq_ :: (Ord f, Monad m) + => (i -> i -> m Bool) + -> InstF f i -> InstF f i -> m Bool +iEq_ _ IFree IFree = return $ True +iEq_ _ _ IFree = return $ False +iEq_ _ IFree _ = return $ False + +iEq_ _ (IAny u) (IAny v) | u == v = return True +iEq_ _ _ (IAny _) = return False +iEq_ _ (IAny _) _ = return False + +iEq_ _ (IUniv u) (IUniv v) | u == v = return True +iEq_ _ _ (IUniv _) = return False +iEq_ _ (IUniv _) _ = return False + +iEq_ q (IBound u b c) (IBound u' b' c') + | u == u' && c == c' && (M.null $ M.difference b' b) = + flip mapForallM b $ + \f is -> case M.lookup f b' of + Nothing -> return False + Just is' -> allM $ zipWith q is is' +iEq_ _ (IBound _ _ _) (IBound _ _ _) + | otherwise = return False + +-- | Instantiatedness partial order with uniqueness (≼) +-- +-- The purpose of iLeq is two-fold: +-- 1. To describe the allowable transitions during forward execution +-- of some predicate. (prose, p32, \"A major rôle...\"). +-- Specifically, a binding may move from @i'@ to @i@ if @i `iLeq` i'@. +-- 2. Defining the abstract unification lattice; see definitions +-- 3.1.18 (p38), 3.2.2 (p44), 3.2.6 (p46), 3.2.19 (p53), and +-- 5.3.8 (p98). -- -- IAny `iLeq` IAny is declared (prose, p46, \"We allow...\") to be unsafe -- in general but safe for reasoning about forward execution (recall defn -- 3.1.10, p34). XXX I do not understand. -- --- Definition 3.2.14, p51 -iLeq_ :: (Eq f, Monad m) +-- Definition 3.2.14, p51 (see also definitions 3.1.4 (p32) and 3.2.5 (p46)) +iLeq_ :: (Ord f, Monad m) => (i -> InstF f i -> m Bool) -> (i -> i -> m Bool) -> InstF f i -> InstF f i -> m Bool @@ -192,11 +228,11 @@ iLeq_ q _ (IBound u b _) r@(IAny u') = andM1 (u' <= u) $ mfmamm (flip q r) b iLeq_ q _ (IBound u b _) r@(IUniv u') = andM1 (u' <= u) $ mfmamm (flip q r) b -iLeq_ _ q (IBound u b _) (IBound u' b' _) = andM1 (u' <= u) $ - mapForallM (\f is -> mapExistsM (\f' is' -> andM1 (f == f') $ - allM $ zipWith q is is' - ) b' - ) b +iLeq_ _ q (IBound u m b) (IBound u' m' b') = andM1 (b <= b' && u' <= u) $ + flip mapForallM m $ + \f is -> case M.lookup f m' of + Nothing -> return False + Just is' -> allM $ zipWithTails q crf crf is is' -- XXX Ought to assert that length is == length is' {- iLeq_ _ (INotReached u) (IAny u') = return $ u' <= u @@ -206,7 +242,9 @@ iLeq_ _ (INotReached u) (INotReached u') = return $ u' <= u {-# INLINE iLeq_ #-} --- | Compute the GLB under iLeq_ +-- | Compute the GLB under iLeq_ (⋏) +-- +-- Since iLeq (≼) is a lattice, this is a total function. iLeqGLB_ :: (Monad m, Ord f) => (i -> i -> m i) -> InstF f i @@ -235,10 +273,17 @@ iLeqGLB_ q (IBound u m b) (IBound u' m' b') = do -- iLeqGLB_ _ a@(INotReached _) _ = return $ Just a -- iLeqGLB_ _ _ a@(INotReached _) = return $ Just a --- | Matches partial order with uniqueness +-- | Matches partial order with uniqueness (⊑) +-- +-- Matching specifies the intersubstitutability of insts: if @i `iSub` i'@ +-- then we may use anything with binding @i@ wherever the predicate would +-- require @i'@. +-- +-- Note that this is not a full lattice. -- --- Definition 3.2.15, p51 -iSub_ :: (Eq f, Monad m) +-- Definition 3.2.15, p51 (see also definitions 3.1.11 (p35) and 3.2.7 +-- (p46)) +iSub_ :: (Ord f, Monad m) => (i -> InstF f i -> m Bool) -> (i -> i -> m Bool) -> InstF f i @@ -258,54 +303,98 @@ iSub_ q _ (IBound u b _) r@(IAny u') = andM1 (u <= u') $ mfmamm (flip q r) b iSub_ q _ (IBound u b _) r@(IUniv u') = andM1 (u <= u') $ mfmamm (flip q r) b -iSub_ _ q (IBound u b _) (IBound u' b' _) = andM1 (u <= u') $ - mapForallM (\f is -> mapExistsM (\f' is' -> andM1 (f == f') $ - allM $ zipWith q is is' - ) b' - ) b +iSub_ _ q (IBound u m b) (IBound u' m' b') = andM1 (u <= u' && b <= b') $ + flip mapForallM m $ + \f is -> case M.lookup f m' of + Nothing -> return False + Just is' -> allM $ zipWithTails q crf crf is is' -- XXX Ought to assert that length is == length is' -- iSub_ _ (INotReached u) (IAny u') = return $ u <= u' -- iSub_ _ (INotReached u) (IUniv u') = return $ u <= u' -- iSub_ _ _ _ = return $ False --- | Compute the GLB under iSub_ +-- | Compute the GLB under iSub_ (⊓) iSubGLB_ :: (Ord f, Monad m) => (i -> i -> m i) - -> InstF f i -> InstF f i -> m (Maybe (InstF f i)) -iSubGLB_ _ IFree IFree = return $ Just IFree -iSubGLB_ _ IFree _ = return $ Nothing -iSubGLB_ _ _ IFree = return $ Nothing + -> InstF f i -> InstF f i -> m (InstF f i) +iSubGLB_ _ IFree IFree = return $ IFree +iSubGLB_ _ IFree b = return $ iNotReached (iUniq b) +iSubGLB_ _ a IFree = return $ iNotReached (iUniq a) -iSubGLB_ _ (IAny u) (IAny u') = return $ Just $ IAny (min u u') +iSubGLB_ _ (IAny u) (IAny u') = return $ IAny (min u u') -iSubGLB_ _ (IAny u') (IUniv u) = return $ Just $ IUniv (min u u') -iSubGLB_ _ (IUniv u) (IAny u') = return $ Just $ IUniv (min u u') -iSubGLB_ _ (IUniv u) (IUniv u') = return $ Just $ IUniv (min u u') +iSubGLB_ _ (IAny u') (IUniv u) = return $ IUniv (min u u') +iSubGLB_ _ (IUniv u) (IAny u') = return $ IUniv (min u u') +iSubGLB_ _ (IUniv u) (IUniv u') = return $ IUniv (min u u') -iSubGLB_ _ (IBound u m b) (IAny u') = return $ Just $ IBound (min u u') m b -iSubGLB_ _ (IAny u') (IBound u m b) = return $ Just $ IBound (min u u') m b +iSubGLB_ _ (IBound u m b) (IAny u') = return $ IBound (min u u') m b +iSubGLB_ _ (IAny u') (IBound u m b) = return $ IBound (min u u') m b -iSubGLB_ _ (IBound u m b) (IUniv u') = return $ Just $ IBound (min u u') m b -iSubGLB_ _ (IUniv u') (IBound u m b) = return $ Just $ IBound (min u u') m b +iSubGLB_ _ (IBound u m b) (IUniv u') = return $ IBound (min u u') m b +iSubGLB_ _ (IUniv u') (IBound u m b) = return $ IBound (min u u') m b iSubGLB_ q (IBound u m b) (IBound u' m' b') = do + let u'' = min u u' + -- NOTE: I was briefly concerned that we would have to pass u'' down + -- through q, but since the well-formedness criteria may be assumed to + -- hold for both m and m' (that is, for all insts contained in m (resp. + -- m'), their uniqueness is <= u (resp. u')), and our recursion is + -- defined by minimizing uniqueness, the uniqueness of the return is + -- guaranteed to be <= min {u, u'} with no additional effort on our + -- part. m'' <- mergeBoundLB q m m' - return $! Just $! IBound (min u u') m'' (b && b') + return $ IBound u'' m'' (b && b') -- iSubGLB_ _ a@(INotReached _) _ = return $ Just a -- iSubGLB_ _ _ a@(INotReached _) = return $ Just a -- iSubGLB_ _ _ _ = return $ Nothing +-- | Compute the LUB under iSub_ (⊔) +-- +-- Since 'iSub_' is not a full lattice, this is a partial function (thus +-- 'Maybe'). Note, however, that the recursion is defined to be total -- +-- thus it is the responsibility of the outer 'Monad' to bail out if any +-- call to 'iSubGLB_' yields 'Nothing'. +iSubLUB_ :: (Ord f, Monad m) + => (i -> i -> m i) + -> InstF f i -> InstF f i -> m (Maybe (InstF f i)) +iSubLUB_ _ IFree IFree = return $ Just IFree +iSubLUB_ _ IFree b | iIsNotReached b = return $ Just IFree +iSubLUB_ _ a IFree | iIsNotReached a = return $ Just IFree +iSubLUB_ _ IFree _ = return $ Nothing +iSubLUB_ _ _ IFree = return $ Nothing + +iSubLUB_ _ (IAny u) (IAny u') = return $ Just $ IAny (max u u') +iSubLUB_ _ (IAny u') (IUniv u) = return $ Just $ IAny (max u u') +iSubLUB_ _ (IUniv u) (IAny u') = return $ Just $ IAny (max u u') +iSubLUB_ _ (IUniv u) (IUniv u') = return $ Just $ IUniv (max u u') + +iSubLUB_ _ (IBound u _ _) (IAny u') = return $ Just $ IAny (max u u') +iSubLUB_ _ (IAny u') (IBound u _ _) = return $ Just $ IAny (max u u') + +iSubLUB_ _ (IBound u _ _) (IUniv u') = return $ Just $ IUniv (max u u') +iSubLUB_ _ (IUniv u') (IBound u _ _) = return $ Just $ IUniv (max u u') + +iSubLUB_ q (IBound u m b) (IBound u' m' b') = do + m'' <- mergeBoundUB q m m' + return $! Just $! IBound (max u u') m'' (b || b') + ------------------------------------------------------------------------}}} -- Instantiation States: Utility Functions {{{ +-- | The bottom of the 'iLeq' lattice and 'iSub' semi-lattice, representing +-- the empty set of (non-ground) terms. iNotReached :: Uniq -> InstF f i iNotReached u = IBound u M.empty False +-- | Indicator function for 'iNotReached' iIsNotReached :: InstF f i -> Bool iIsNotReached (IBound _ m False) = M.null m iIsNotReached _ = False +crf :: (Monad m) => a -> m Bool +crf = const $ return False + -- | A common pattern we encounter in unary predicates, so let's just pull -- it out. mfmamm :: Monad m => (a -> m Bool) -> M.Map k [a] -> m Bool @@ -313,14 +402,17 @@ mfmamm f = mapForallM (\_ -> allM . map f) -- | Compute the lower bound of two guts of IBound constructors. mergeBoundLB :: (Monad m, Ord f) + => (i -> i -> m a) + -> M.Map f [i] -> M.Map f [i] -> m (M.Map f [a]) +mergeBoundLB q lm rm = T.sequence $ M.intersectionWith (\a b -> sequence $ zipWith q a b) lm rm + +-- | Compute the upper bound of two guts of IBound constructors. +mergeBoundUB :: (Monad m, Ord f) => (i -> i -> m i) -> M.Map f [i] -> M.Map f [i] -> m (M.Map f [i]) -mergeBoundLB q lm rm = M.foldrWithKey fold (return M.empty) - $ M.intersectionWith (,) lm rm - where - fold f (lis,ris) mm = do - m <- mm - is <- sequence $ zipWith q lis ris - return $ M.insert f is m +mergeBoundUB q lm rm = T.sequence + $ M.mergeWithKey (\_ a b -> Just $ sequence $ zipWith q a b) + (fmap return) (fmap return) + lm rm ------------------------------------------------------------------------}}} diff --git a/src/Dyna/XXX/DataUtils.hs b/src/Dyna/XXX/DataUtils.hs index a8d7f18..bf1382d 100644 --- a/src/Dyna/XXX/DataUtils.hs +++ b/src/Dyna/XXX/DataUtils.hs @@ -2,6 +2,8 @@ module Dyna.XXX.DataUtils ( -- * 'Data.List' utilities -- ** Argmin/argmax idiom argmax, argmin, + -- ** A more faithful zipWith + zipWithTails, -- * 'Data.Map' utilities -- ** Quantification mapExists, mapForall, @@ -51,6 +53,10 @@ mapUpsert k v m = r = Right m' in maybe r (\o -> if o == v then r else Left o) mo + +-- | Add @v@ to the list of values at @k@, possibly after creating an empty +-- bucket there. + -- XXX maybe consider generalizing this to any collection type? mapInOrApp :: (Ord k) => k -> v -> M.Map k [v] -> M.Map k [v] mapInOrApp k v m = M.alter (\mv -> Just $ v:nel mv) k m @@ -82,3 +88,14 @@ mapSemiprune q p k m = case M.lookup k m >>= q of setAll m' v k' = M.fromList (map (\x -> (x,p k')) $ S.toList v) `M.union` m' + + +-- | A generalized version of 'zipWith' that gives access to tail elements +-- as well. +zipWithTails :: (a -> b -> c) -> (a -> c) -> (b -> c) -> [a] -> [b] -> [c] +zipWithTails fb fl fr = go + where + go [] [] = [] + go [] (r:rs) = fr r : map fr rs + go (l:ls) [] = fl l : map fl ls + go (l:ls) (r:rs) = fb l r : go ls rs diff --git a/src/Dyna/XXX/MonadUtils.hs b/src/Dyna/XXX/MonadUtils.hs index 4b63642..f6ab533 100644 --- a/src/Dyna/XXX/MonadUtils.hs +++ b/src/Dyna/XXX/MonadUtils.hs @@ -1,20 +1,22 @@ {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MultiParamTypeClasses #-} module Dyna.XXX.MonadUtils( -- * Data utilities generalizing 'Dyna.XXX.DataUtils' - mapForallM, mapExistsM, + mapForallM, mapExistsM, setForallM, setExistsM, -- * Logic utilities andM, andM1, orM, orM1, allM, anyM, -- * MonadState utilities bracketState, incState, -- * Context classes - MC(..), + MCR(..), MCW(..), MCF(..), ) where import Control.Applicative import Control.Monad.State import qualified Data.Map as M +import qualified Data.Set as S andM :: Monad m => m Bool -> m Bool -> m Bool andM x y = x >>= flip andM1 y @@ -41,6 +43,12 @@ mapForallM, mapExistsM :: (Monad m) mapForallM p m = M.foldrWithKey (\k v -> (andM $ p k v)) (return True ) m mapExistsM p m = M.foldrWithKey (\k v -> (orM $ p k v)) (return False) m +setForallM, setExistsM :: (Monad m) + => (e -> m Bool) -> S.Set e -> m Bool +setForallM p m = S.foldr (\e -> (andM $ p e)) (return True ) m +setExistsM p m = S.foldr (\e -> (orM $ p e)) (return False) m + + bracketState :: (MonadState s m) => s -> m t -> m (t, s) bracketState bs m = do s <- get @@ -56,8 +64,12 @@ incState = do put $! (s+1) return s --- | Assert the the monad @m@ has a context of type @k -> v@. -class (Monad m) => MC m k v where +-- | Assert the the monad @m@ has a readable context of type @k -> v@ +class (Monad m) => MCR m k v | m k -> v where clookup :: k -> m v + +class (MCR m k v) => MCW m k v | m k -> v where cassign :: k -> v -> m () + +class (Monad m) => MCF m k where cfresh :: m k