From dd634b024b78a61142e5c8cfae98575ed2fe68a4 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Wed, 26 Jun 2013 21:54:53 -0400 Subject: [PATCH] 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. --- src/Dyna/Analysis/Mode/Execution/Functions.hs | 27 ++++++++++--- .../Mode/Execution/FunctionsNoAlias.hs | 24 +++++++++--- src/Dyna/Analysis/Mode/Execution/NamedInst.hs | 20 ++++++---- src/Dyna/Analysis/Mode/Inst.hs | 39 ++++++++++++------- 4 files changed, 77 insertions(+), 33 deletions(-) diff --git a/src/Dyna/Analysis/Mode/Execution/Functions.hs b/src/Dyna/Analysis/Mode/Execution/Functions.hs index cb4a93d..a1a1f3c 100644 --- 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 d9cabff..30786fd 100644 --- 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 caec2d1..87e48ff 100644 --- 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 b00cc44..52ed1aa 100644 --- 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' -- 2.50.1