Strengthen static types of Inst lattice functions

Use parametricity and higher-rank types to force the lop-sided callbacks to
use only non-recursive Insts.

diff --git a/src/Dyna/Analysis/Mode/Execution/Functions.hs b/src/Dyna/Analysis/Mode/Execution/Functions.hs
index cb4a93dd7565cd31240f21816b26e23b577ba7ee..a1a1f3c0701379ec67594034f46204e5ddce1117 100644 (file)
--- a/src/Dyna/Analysis/Mode/Execution/Functions.hs
+++ b/src/Dyna/Analysis/Mode/Execution/Functions.hs
@@ -173,29 +173,44 @@ leqYK yl kr = clookup kr >>= either (leqYN yl) (leqYQ yl)
 -- 'nShallow', rather than expanding the named inst with 'nExpose'.  Since
 -- the right hand side is not getting smaller in such a case, the latter
 -- strategy would lead divergence.
-leqNY :: (LeqC m f n k) => n -> InstF f (VR f n k) -> m Bool
+leqNY :: forall m f n k . (LeqC m f n k) => n -> InstF f (VR f n k) -> m Bool
 leqNY nl (nShallow -> Just nr) = leqNN nl nr
-leqNY nl yr                    = iLeq_ leqNY leqNX (nExpose nl) yr
+leqNY nl yr                    = iLeq_ leqNL leqNX (nExpose nl) yr
+ where
+  leqNL :: NIX f -> (forall i_ . InstF f i_) -> m Bool
+  leqNL nl' yr' = leqNY nl' (ly yr')
+
+  -- What a mess.  Necessary that it is written and scoped under here to
+  -- avoid ambiguous tyvars.
+  ly :: (forall i_ . InstF f i_) -> InstF f (VR f n k)
+  ly x = x
 
 -- | Induction hypothesis YN
 --
 -- Induction is similarly funny as in 'leqNY'
 leqYN :: (LeqC m f n k) => InstF f (VR f n k) -> n -> m Bool
 leqYN (nShallow -> Just nl) nr = leqNN nl nr
-leqYN yl                    nr = iLeq_ leqXI leqXN yl (nExpose nr)
+leqYN yl                    nr = iLeq_ leqXL leqXN yl (nExpose nr)
 
 -- | Induction hypothesis YY
 leqYY :: (LeqC m f n k) => InstF f (VR f n k) -> InstF f (VR f n k) -> m Bool
-leqYY = iLeq_ leqXY leqXX
+leqYY = iLeq_ leqXL leqXX
 
+leqXL :: (LeqC m f n k) => VR f n k -> (forall i_ . InstF f i_) -> m Bool
+leqXL xl yr = leqXX xl (VRStruct yr)
+
+{-
 -- | Repackage Y as X and invoke generic dispatch.  Despite the growth of
 -- the RHS, this is guaranteed to then step to one of the induction
 -- hypotheses, which will reduce both sides.
 leqXY :: (LeqC m f n k) => VR f n k -> InstF f (VR f n k) -> m Bool
 leqXY xl yr = leqXX xl (VRStruct yr)
+-}
 
+{-
 leqXI :: (LeqC m f n k) => VR f n k -> InstF f n -> m Bool
 leqXI xl ir = leqXX xl (VRName $ nHide ir)
+-}
 
 leqXN :: (LeqC m f n k) => VR f n k -> n -> m Bool
 leqXN xl nr = leqXX xl (VRName nr)
@@ -414,7 +429,8 @@ unifyNQ' u n q = unifyNQ u n q
                             (liftM Right . cnew . const . return . Right)
 
 -- | Induction hypothesis QQ
-unifyQQ :: (UnifC m f n, UnifKC m f n k)
+unifyQQ :: forall m f n k .
+           (UnifC m f n, UnifKC m f n k)
         => Uniq
         -> KRI f n k
         -> KRI f n k
@@ -423,6 +439,7 @@ unifyQQ u ya yb = selUnifI >>= \f ->
     f jUpUniq jUpUniq fJQ fJQ unifyJJ u ya yb
     >>= either throwError return
  where
+  fJQ :: Uniq -> (forall i_. InstF f i_) -> Either n k -> m (Either n k)
   fJQ u' q' j' = unifyJQ u' j' q'
 
 -- | Name-on-Name unification, which computes a new name for the result.

diff --git a/src/Dyna/Analysis/Mode/Execution/FunctionsNoAlias.hs b/src/Dyna/Analysis/Mode/Execution/FunctionsNoAlias.hs
index d9cabff0d3361f28597a65c803a3cd7d8e93555a..30786fd5bbac17f1c622659f122aade65837e1ed 100644 (file)
--- a/src/Dyna/Analysis/Mode/Execution/FunctionsNoAlias.hs
+++ b/src/Dyna/Analysis/Mode/Execution/FunctionsNoAlias.hs
@@ -89,34 +89,48 @@ type LeqC m f n = (Ord f, Show f,
 
 leqXX :: (LeqC m f n)
       => VR f n -> VR f n -> m Bool
-leqXX (VRStruct yl) (VRStruct yr) = iLeq_ leqXY leqXX yl yr
+leqXX (VRStruct yl) (VRStruct yr) = iLeq_ leqXL leqXX yl yr
 leqXX (VRName   nl) (VRStruct yr) = leqNY nl yr
 leqXX (VRStruct yl) (VRName   nr) = leqYN yl nr
 leqXX (VRName   nl) (VRName   nr) = return $ nLeq nl nr
 
+leqXL :: (LeqC m f n)
+      => VR f n -> (forall i_ . InstF f i_) -> m Bool
+leqXL (VRName   nl) yr = iLeq_ leqNL leqNX (nExpose nl) yr
+leqXL (VRStruct yl) yr = iLeq_ leqXL leqXX yl yr
+
+{-
 leqXY :: (LeqC m f n)
       => VR f n -> InstF f (VR f n) -> m Bool
 leqXY (VRName   nl) yr = iLeq_ leqNY leqNX (nExpose nl) yr
 leqXY (VRStruct yl) yr = iLeq_ leqXY leqXX yl yr
+-}
 
 leqNX :: (LeqC m f n)
       => NIX f -> VR f n -> m Bool
 leqNX nl (VRName   nr) = return $ nLeq nl nr
-leqNX nl (VRStruct yr) = iLeq_ leqNY leqNX (nExpose nl) yr
+leqNX nl (VRStruct yr) = iLeq_ leqNL leqNX (nExpose nl) yr
 
 leqNY :: (LeqC m f n)
       => NIX f -> InstF f (VR f n) -> m Bool
 leqNY nl (nShallow -> Just nr) = {- XT.trace "LNYS" $-} return $ nLeq nl nr
-leqNY nl ir = {-XT.traceShow ("LNY",nl,ir) $-} iLeq_ leqNY leqNX (nExpose nl) ir
+leqNY nl ir = {-XT.traceShow ("LNY",nl,ir) $-} iLeq_ leqNL leqNX (nExpose nl) ir
+
+-- XXX I am uncertain why this is necessary.
+leqNL :: (LeqC m f n)
+      => NIX f -> (forall i_ . InstF f i_) -> m Bool
+leqNL n l = leqNY n l
 
 leqYN :: (LeqC m f n)
       => InstF f (VR f n) -> NIX f -> m Bool
-leqYN il nr = iLeq_ leqXI leqXN il (nExpose nr)
+leqYN il nr = iLeq_ leqXL leqXN il (nExpose nr)
 
+{-
 leqXI :: (LeqC m f n)
       => VR f n -> InstF f (NIX f) -> m Bool
 leqXI (VRStruct yl) ir = leqYN yl (nHide ir)
 leqXI (VRName   nl) ir = return $ nLeq nl (nHide ir)
+-}
 
 leqXN :: (LeqC m f n)
       => VR f n -> NIX f -> m Bool
@@ -342,7 +356,7 @@ subNN :: (SubC m f n)
 subNN a b = {- XT.traceShow ("SNN",a,b) $-} return $ nSub a b
 
 subXI :: (SubC m f n)
-      => VR f n -> InstF f (NIX f) -> m Bool
+      => VR f n -> (forall i_ . InstF f i_) -> m Bool
 subXI (VRName   ln) ri = subNN ln (nHide ri)
 subXI (VRStruct ly) ri = subYI ly ri
 

diff --git a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs
index caec2d1d8580508dbcb213be702375fd8b04ad11..87e48ff59cc57f50f51a409ef3d629db331af4db 100644 (file)
--- a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs
+++ b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs
@@ -319,7 +319,7 @@ nCmp :: forall f .
         (Ord f)
      => (forall a b m .
             (Monad m)
-         => (a -> InstF f b -> m Bool)
+         => (a -> (forall i_ . InstF f i_) -> m Bool)
          -> (a -> b -> m Bool)
          -> InstF f a -> InstF f b -> m Bool)
      -> NIX f -> NIX f -> Bool
@@ -339,9 +339,13 @@ nCmp q l0@(NIX li0 lm) r0@(NIX ri0 rm) =
 
   -- Q Out of Phase
   qop l ri = -- XT.traceShow ("NCMP QOP",l,ri) $
-             tsc _2 (l,ri) $ eml l0 (return . flip (nCmp q) (NIX ri rm))
-                                    (flip (q qop qip) ri)
-                                    lm l
+             tsc _2 (l,downcast ri)
+               $ eml l0 (return . flip (nCmp q) (NIX ri rm))
+                        (flip (q qop qip) ri)
+                        lm l
+
+  downcast :: (forall i_ . InstF f i_) -> InstF f ()
+  downcast i = i
 
 nEq, nLeq, nSub :: (Ord f) => NIX f -> NIX f -> Bool
 nEq  = nCmp (\_ -> iEq_)
@@ -368,8 +372,8 @@ nTBin :: forall f . (Ord f, Show f)
             (Monad m)
          => (Uniq -> a -> m c)
          -> (Uniq -> b -> m c)
-         -> (Uniq -> InstF f b -> a -> m c)
-         -> (Uniq -> InstF f a -> b -> m c)
+         -> (Uniq -> (forall i_ . InstF f i_) -> a -> m c)
+         -> (Uniq -> (forall i_ . InstF f i_) -> b -> m c)
          -> (Uniq -> a -> b -> m c)
          -> Uniq
          -> InstF f a -> InstF f b -> m (InstF f c))
@@ -465,8 +469,8 @@ nPBin :: forall e f .
             (Monad m, Show a, Show b, Show c)
          => (Uniq -> a -> m c)
          -> (Uniq -> b -> m c)
-         -> (Uniq -> InstF f b -> a -> m c)
-         -> (Uniq -> InstF f a -> b -> m c)
+         -> (Uniq -> (forall i_ . InstF f i_) -> a -> m c)
+         -> (Uniq -> (forall i_ . InstF f i_) -> b -> m c)
          -> (Uniq -> a -> b -> m c)
          -> Uniq
          -> InstF f a -> InstF f b -> m (Either e (InstF f c)))

diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs
index b00cc44dc358e249b5b2f252050c614dba793c99..52ed1aa11a09d04195e9804e42bdd571468da00f 100644 (file)
--- a/src/Dyna/Analysis/Mode/Inst.hs
+++ b/src/Dyna/Analysis/Mode/Inst.hs
@@ -26,7 +26,7 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -Wall #-}
 module Dyna.Analysis.Mode.Inst(
-  InstF(..), inst_uniq, inst_rec, inst_recps,
+  InstF(..), inst_uniq, inst_rec, inst_recps, inst_irecps,
   iNotReached, iIsNotReached,
   iUniq, iIsFree, iWellFormed_, iEq_, iGround_,
   iLeq_, iLeqGLB_, TyILeqGLB_,
@@ -152,12 +152,21 @@ $(makeLensesFor [("_inst_uniq","inst_uniq")
                 ,("_inst_rec","inst_rec")
                 ]
                 ''InstF)
+-- Note that makeLensesFor creates INLINE pragmas for its lenses, too. :)
 
 -- | Traverse all of the recursion points @a@, rather than the @M.Map f [a]@
 -- structure itself.  This provides a more robust interface to term
 -- recursion, but of course loses information about disjunctions.
 inst_recps :: (Applicative a) => (i -> a i') -> InstF f i -> a (InstF f i')
 inst_recps = inst_rec . each . each
+{-# INLINABLE inst_recps #-}
+
+-- | An indexed variant of 'inst_recps' which reveals the functor of the
+-- disjunct and the argument position being traversed right now.
+inst_irecps :: (Applicative a) => ((f, Int) -> i -> a i')
+                               -> InstF f i -> a (InstF f i')
+inst_irecps = itraverseOf (inst_rec .> each <.> each)
+{-# INLINABLE inst_irecps #-}
 
 ------------------------------------------------------------------------}}}
 -- Instantiation States: Unary predicates                               {{{
@@ -293,7 +302,7 @@ iEq_ _ (IBound _ _ _) (IBound _ _ _)
 --
 -- 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 -> (forall i_ . InstF f i_) -> m Bool)
       -> (i -> i' -> m Bool)
       -> InstF f i -> InstF f i' -> m Bool
 iLeq_ _ _  _            IFree             = return $ True
@@ -323,8 +332,8 @@ iLeq_ _ q (IBound u m b) (IBound u' m' b') = andM1 (b <= b' && u' <= u) $
 type TyILeqGLB_ f m i i' i'' r = 
             (Uniq -> i  -> m i'')               -- ^ Import left
          -> (Uniq -> i' -> m i'')               -- ^ Import right
-         -> (Uniq -> InstF f i' -> i  -> m i'') -- ^ Lopsided merge left
-         -> (Uniq -> InstF f i  -> i' -> m i'') -- ^ Lopsided merge right
+         -> (Uniq -> (forall i_ . InstF f i_) -> i  -> m i'') -- ^ Lopsided merge left
+         -> (Uniq -> (forall i_ . InstF f i_) -> i' -> m i'') -- ^ Lopsided merge right
          -> (Uniq -> i -> i' -> m i'')          -- ^ Simultaneous Merge
          -> Uniq                                -- ^ Uniq of outer context
          -> InstF f i                           -- ^ Left
@@ -397,7 +406,7 @@ iLeqGLB_ _ _ _ _ q _ (IBound u m b) (IBound u' m' b') = do
 -- 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 -> (forall i_ . InstF f i_) -> m Bool)
       -> (i -> i' -> m Bool)
       -> InstF f i
       -> InstF f i'
@@ -432,8 +441,8 @@ iSub_ _ q (IBound u m b) (IBound u' m' b') = andM1 (u <= u' && b <= b') $
 -- on 'IFree' are with 'IFree' or 'iNotReached', there is no recursion to be
 -- done.
 iSubGLB_ :: (Ord f, Monad m)
-         => (InstF f i' -> i  -> m i'')
-         -> (InstF f i  -> i' -> m i'')
+         => ((forall i_ . InstF f i_) -> i  -> m i'')
+         -> ((forall i_ . InstF f i_) -> i' -> m i'')
          -> (i -> i' -> m i'')
          -> InstF f i -> InstF f i' -> m (InstF f i'')
 iSubGLB_ _ _ _ IFree      IFree        = return $ IFree
@@ -449,15 +458,15 @@ 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_ l _ _ (IBound u m b) r@(IAny u') = (return . flip (IBound (min u u')) b)
-                                            =<< T.mapM (T.mapM (l r)) m
-iSubGLB_ _ r _ l@(IAny u') (IBound u m b) = (return . flip (IBound (min u u')) b)
-                                            =<< T.mapM (T.mapM (r l)) m
+iSubGLB_ l _ _ (IBound u m b) (IAny u') = (return . flip (IBound (min u u')) b)
+                                            =<< T.mapM (T.mapM (l (IAny u'))) m
+iSubGLB_ _ r _ (IAny u') (IBound u m b) = (return . flip (IBound (min u u')) b)
+                                            =<< T.mapM (T.mapM (r (IAny u'))) m
 
-iSubGLB_ l _ _ (IBound u m b) r@(IUniv u') = (return . flip (IBound (min u u')) b)
-                                            =<< T.mapM (T.mapM (l r)) m
-iSubGLB_ _ r _ l@(IUniv u') (IBound u m b) = (return . flip (IBound (min u u')) b)
-                                            =<< T.mapM (T.mapM (r l)) m
+iSubGLB_ l _ _ (IBound u m b) (IUniv u') = (return . flip (IBound (min u u')) b)
+                                            =<< T.mapM (T.mapM (l (IUniv u'))) m
+iSubGLB_ _ r _ (IUniv u') (IBound u m b) = (return . flip (IBound (min u u')) b)
+                                            =<< T.mapM (T.mapM (r (IUniv u'))) m
 
 iSubGLB_ _ _ q (IBound u m b) (IBound u' m' b') = do
     let u'' = min u u'