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 fc77bc4db498f260ba706fb6fc9ae5a691a816ac..79f15125f214c24a0b7765c561abbff85d3478d8 100644 (file)
--- 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 a8d7f18bbf896c4889cc4ef043ecd4c14f46e8a0..bf1382db5fbeab3c7400aff8e01ce357ff6c9efb 100644 (file)
--- 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 4b636429d04f3c7a2d33d8cae5c052161127f310..f6ab533d767a3eb50dbb8617b45fe0a772763ccf 100644 (file)
--- 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