From 77668976339818ec534c32a660538f4c52ab9e45 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Tue, 28 May 2013 13:50:32 -0400 Subject: [PATCH] Snapshot of work in progress Notably, this marks the first commit to fix an externally filed bug report; thanks to Abram Demski for reporting! Dyna should now build with ghc 7.4 and its Platform releases. :) (This commit is a little bigger than just the fix as I had already changed some of the code in my working tree and there seemed to be no reason not to just commit things.) --- src/Dyna/Analysis/ANF.hs | 9 +- src/Dyna/Analysis/ANFSelftest.hs | 2 +- src/Dyna/Analysis/Mode/Execution/NamedInst.hs | 214 ++++++++++-------- .../Analysis/Mode/Execution/NoAliasContext.hs | 46 ++-- .../Mode/Execution/NoAliasFunctions.hs | 75 +++--- src/Dyna/Analysis/Mode/Inst.hs | 11 +- src/Dyna/Analysis/Mode/InstPretty.hs | 32 +++ src/Dyna/Analysis/Mode/Unification.hs | 23 +- src/Dyna/Analysis/RuleMode.hs | 189 ++++++++-------- src/Dyna/Backend/Python/Backend.hs | 28 +-- src/Dyna/Main/Driver.hs | 9 +- src/Dyna/Term/TTerm.hs | 3 + src/Dyna/XXX/DataUtils.hs | 44 +++- 13 files changed, 412 insertions(+), 273 deletions(-) create mode 100644 src/Dyna/Analysis/Mode/InstPretty.hs diff --git a/src/Dyna/Analysis/ANF.hs b/src/Dyna/Analysis/ANF.hs index c145868..57c1ff0 100644 --- a/src/Dyna/Analysis/ANF.hs +++ b/src/Dyna/Analysis/ANF.hs @@ -72,7 +72,7 @@ {-# OPTIONS_GHC -Wall #-} module Dyna.Analysis.ANF ( - Crux, EvalCrux(..), UnifCrux(..), cruxIsEval, cruxVars, + Crux, EvalCrux(..), UnifCrux(..), cruxIsEval, cruxVars, allCruxVars, Rule(..), ANFAnnots, ANFWarns, normTerm, normRule, runNormalize, @@ -101,7 +101,7 @@ import qualified Dyna.ParserHS.Parser as P import Dyna.Term.TTerm import Dyna.Term.Normalized import Dyna.Term.SurfaceSyntax -import Dyna.XXX.DataUtils (mapInOrApp) +import Dyna.XXX.DataUtils (mapInOrCons) -- import Dyna.Test.Trifecta -- XXX import qualified Text.Trifecta as T @@ -172,6 +172,9 @@ cruxVars = either evalVars unifVars CEquals o i -> S.fromList [o,i] CNotEqu o i -> S.fromList [o,i] +allCruxVars :: S.Set (Crux DVar TBase) -> S.Set DVar +allCruxVars = S.unions . map cruxVars . S.toList + ------------------------------------------------------------------------}}} -- ANF State {{{ @@ -217,7 +220,7 @@ newAssign pfx t = newAnnot :: (MonadState ANFState m) => DVar -> Annotation (T.Spanned P.Term) -> m () -newAnnot v a = as_annot %= mapInOrApp v a +newAnnot v a = as_annot %= mapInOrCons v a {- newAssignNT :: (MonadState ANFState m) => String -> NTV -> m DVar diff --git a/src/Dyna/Analysis/ANFSelftest.hs b/src/Dyna/Analysis/ANFSelftest.hs index c717098..08b2fc7 100644 --- a/src/Dyna/Analysis/ANFSelftest.hs +++ b/src/Dyna/Analysis/ANFSelftest.hs @@ -27,7 +27,7 @@ import Dyna.Term.TTerm import Dyna.XXX.TrifectaTest -testNormRule :: B.ByteString -> Rule +testNormRule :: B.ByteString -> (Rule, ANFWarns) testNormRule = normRule . unsafeParse P.rawDRule {- diff --git a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs index 157fe47..77806ed 100644 --- a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs +++ b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs @@ -13,6 +13,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wall #-} module Dyna.Analysis.Mode.Execution.NamedInst ( @@ -21,7 +22,9 @@ module Dyna.Analysis.Mode.Execution.NamedInst ( -- * Well-formedness predicates nWellFormedUniq, nWellFormedOC, -- * Unary functions - nNotEmpty, nGround, nUpUniq, nPrune, nExpose, nHide, + nNotEmpty, nGround, nUpUniq, nExpose, nHide, nShallow, + -- * Unary functions on internals + nPrune, -- * Binary comparators nCmp, nEq, nLeq, nSub, -- * Total binary functions @@ -30,11 +33,15 @@ module Dyna.Analysis.Mode.Execution.NamedInst ( nPBin, nLeqGLBRD, nLeqGLBRL, -- nSubLUB, -- * Mode functions mWellFormed, + + -- * XXX + eml, ) where import Control.Applicative import qualified Control.Arrow as A import Control.Lens +-- import Control.Monad.Identity import Control.Monad.State import Control.Monad.Trans.Either import qualified Data.Foldable as F @@ -44,12 +51,14 @@ import qualified Data.Set as S import qualified Data.Traversable as T -- import qualified Debug.Trace as XT import Dyna.Analysis.Mode.Inst +import qualified Dyna.Analysis.Mode.InstPretty as IP import Dyna.Analysis.Mode.Mode import Dyna.Analysis.Mode.Unification import Dyna.Analysis.Mode.Uniq import Dyna.Main.Exception +-- import Dyna.XXX.DataUtils import Dyna.XXX.MonadUtils -import System.IO.Unsafe (unsafePerformIO) +-- import System.IO.Unsafe (unsafePerformIO) import System.Mem.StableName (makeStableName) import Text.PrettyPrint.Free @@ -66,9 +75,15 @@ type NIXM a f = M.Map a (Either (NIX f) (InstF f a)) -- | A closed, mu-recursive inst. -- +-- The existential captures a @Show f@ as well for use by 'panicwf' below. +-- This requires that all terms constructing NIXes afresh (e.g. 'nHide' and +-- 'nShallow') have a @Show f@ constraint, but means that we don't need to +-- annotate the whole universe. The trade-off, of course, is that we +-- potentially carry those dictionaries around at runtime. +-- -- The accessors and constructor is exported solely for the selftests' -- benefits and SHOULD NOT be used elsewhere in the code! -data NIX f = forall a . (Ord a,Show a) => +data NIX f = forall a . (Ord a,Show a,Show f) => NIX { -- | The top InstF ply in this term. @@ -82,41 +97,14 @@ data NIX f = forall a . (Ord a,Show a) => , nix_map :: NIXM a f } +-- | Semantic, not structural, equality +instance (Ord f) => Eq (NIX f) where + n1 == n2 = nEq n1 n2 + -- XXX This is hideously ugly, but we can clean it up later instance (Show f) => Show (NIX f) where show (NIX r m) = "(NIX ("++ (show r) ++ ") (" ++ (show m) ++ "))" -instance (Pretty f) => Pretty (NIX f) where - pretty (NIX r m) = ri r <> if M.null m - then empty - else align $ indent 2 - ( (text "where") - <+> (vsep $ map rme $ M.toList m)) - where - -- render index - rix = angles . text . show - - -- render map entry - rme (k,v) = rix k <+> equals <+> either pretty ri v - - -- render uniq (XXX own pretty instance instead?) - ru u = text $ case u of - UUnique -> "un" - UMostlyUnique -> "mu" - UShared -> "sh" - UMostlyClobbered -> "mc" - UClobbered -> "cl" - - -- render inst - ri IFree = text "F" - ri (IAny u) = text "A@" <> ru u - ri (IUniv u) = text "U@" <> ru u - ri (IBound u bm b) = (semiBraces $ if b then (text "B"):rm else rm) - <> char '@' <> ru u - where - rm = map (\(k,vs) -> pretty k <> tupled (map rix vs)) (M.toList bm) - - ------------------------------------------------------------------------}}} -- Utilities {{{ @@ -124,7 +112,8 @@ instance (Pretty f) => Pretty (NIX f) where -- -- XXX Should attempt to do something with the 'NIX' passed in! panicwf :: NIX f -> a -panicwf _ = dynacPanicStr "NIX not well formed" +panicwf n = dynacPanic (text "NIX not well-formed" + `above` indent 2 (pretty n)) -- | Often we want to check a set cache for membership, returning true if -- so, or assume this case and run some action to obtain a boolean. This is @@ -142,13 +131,13 @@ tsc l e miss = (uses l $ S.member e) (l %= S.insert e >> miss) -- | Either of Maybe of Lookup. A common pattern found in implementation. -eml :: (Monad m, Ord k) +eml :: (Ord k) => NIX f -- ^ For debugging - -> (a -> m c) - -> (b -> m c) + -> (a -> c) + -> (b -> c) -> M.Map k (Either a b) -> k - -> m c + -> c eml n al ar m x = either al ar (ml n m x) -- | Our particular version of 'fromJust' which panics appropriately. @@ -186,21 +175,24 @@ nWellFormedUniq u0 n0@(NIX i0 m) = evalState (iWellFormed_ q u0 i0) -- debugging nontermination of the compiler. There's nothing that can save -- us from an evil NIX which generates additional NIXes on the fly, tho'. -- -nWellFormedOC :: forall f . (Ord f) => NIX f -> () -nWellFormedOC = go H.empty +nWellFormedOC :: (Ord f) => NIX f -> IO () +nWellFormedOC n0 = evalStateT (go n0) H.empty where - mksp x = x `seq` unsafePerformIO (makeStableName x) + mksp x = x `seq` makeStableName x visit q i = F.mapM_ (F.mapM_ q) (i ^. inst_rec) - go vis n0@(NIX i m) = - let sn0 = mksp n0 - in if sn0 `H.member` vis - then dynacPanicStr "Named inst occurs check!" - else evalState (visit (q vis) i) S.empty + go n@(NIX i m) = do + sn <- liftIO $ mksp n + vis <- get + if sn `H.member` vis + then dynacPanicStr "Named inst occurs check!" + else do + put (H.insert sn vis) + evalStateT (visit q i) S.empty where - q v a = tsc id a - (eml n0 (return . go v) (visit (q v)) m a >> return True) + q a = tsc id a + (eml n0 (lift . go) (visit q) m a >> return True) -- | Is a named inst ground? nGround :: forall f . NIX f -> Bool @@ -230,44 +222,14 @@ nNotEmpty n0@(NIX i0 m0) = evalState (visit i0) S.empty already `orM1` eml n0 (return . nNotEmpty) (\v -> modify (S.insert idx) >> visit v) m0 idx -nCrawl :: forall f . (Ord f) - => (forall a . Uniq -> InstF f a) -- ^ Replace free variables - -> Uniq -- ^ Minimum uniqueness - -> NIX f - -> NIX f -nCrawl fv u0 n0@(NIX i0 m) = - let i0' = reall u0 i0 in NIX i0' $ execState (T.traverse (evac u0) i0') M.empty - where - reun = over inst_uniq (max u0) - refv u IFree = fv u - refv _ x = x - - reall u = reun . refv u - - evac u i = gets (M.lookup i) >>= maybe (go u i) (const $ return ()) - - go u i = do - let l = ml n0 m i - case l of - Left n -> id %= M.insert i (Left $ nCrawl fv u n) - Right x -> do - id %= M.insert i (Right $ reall u x) - F.traverse_ (evac (maybe u (max u) $ iUniq x)) x - return () - --- | Prune the internals of a 'NIX'. This really ought not be needed, but --- it's handy for test generation. -nPrune :: forall f . (Ord f) => NIX f -> NIX f -nPrune = nCrawl (const IFree) UUnique -- | Increase the nonuniqueness of a particular named inst to at least the -- given level. +-- +-- This is equivalent to unification with 'IANy' at the given 'Uniq' level, +-- but may be slightly more efficient than actually performing that work. nUpUniq :: forall f . (Ord f) => Uniq -> NIX f -> NIX f - --- XXX a simplistic, cruft-removing, but inefficient solution. --- nUpUniq = nCrawl (const IFree) - {- - XXX The beginnings of a possibly more efficient implementation nUpUniq u0 n0@(NIX i0 m) = uncurry NIX $ runState (T.traverse visit i0) m @@ -286,12 +248,14 @@ nUpUniq u0 n0@(NIX i0 m0) = -- | Expose the root ply of a 'NIX' as an Inst which recurses as additional -- 'NIX' elements. +-- +-- Note that recursive use of this function may well diverge! nExpose :: NIX f -> InstF f (NIX f) nExpose n@(NIX r m) = fmap (\a -> either id (\i -> NIX i m) (ml n m a)) r {-# INLINABLE nExpose #-} -- | An inefficient \"inverse\" (up to isomorphism) of nExpose. -nHide :: InstF f (NIX f) -> NIX f +nHide :: (Show f) => InstF f (NIX f) -> NIX f nHide i = uncurry NIX $ runState (T.mapM next i) M.empty where next n = do @@ -301,10 +265,17 @@ nHide i = uncurry NIX $ runState (T.mapM next i) M.empty return n' {-# INLINABLE nHide #-} +nShallow :: (Show f) => InstF f a -> Maybe (NIX f) +nShallow IFree = Just $ nHide $ IFree +nShallow (IAny u) = Just $ nHide $ (IAny u) +nShallow (IUniv u) = Just $ nHide $ (IUniv u) +nShallow (IBound _ _ _) = Nothing + ------------------------------------------------------------------------}}} -- Binary predicates {{{ -nCmp :: forall f . (Ord f, Show f) +nCmp :: forall f . + (Ord f) => (forall a b m . (Monad m) => (a -> InstF f b -> m Bool) @@ -331,7 +302,7 @@ nCmp q l0@(NIX li0 lm) r0@(NIX ri0 rm) = (flip (q qop qip) ri) lm l -nEq, nLeq, nSub :: (Ord f, Show f) => NIX f -> NIX f -> Bool +nEq, nLeq, nSub :: (Ord f) => NIX f -> NIX f -> Bool nEq = nCmp (\_ -> iEq_) nLeq = nCmp iLeq_ nSub = nCmp iSub_ @@ -339,15 +310,15 @@ nSub = nCmp iSub_ ------------------------------------------------------------------------}}} -- Binary functions {{{ -data NBinState a b f = NBS { _nbs_next :: Int +data NBinState a b f u = NBS { _nbs_next :: Int , _nbs_ctx :: NIXM Int f - , _nbs_cache_symm :: M.Map (Uniq,a,b) Int - , _nbs_cache_lsml :: M.Map (Uniq,InstF f b,a) Int - , _nbs_cache_lsmr :: M.Map (Uniq,InstF f a,b) Int + , _nbs_cache_symm :: M.Map (u,a,b) Int + , _nbs_cache_lsml :: M.Map (u,InstF f b,a) Int + , _nbs_cache_lsmr :: M.Map (u,InstF f a,b) Int } $(makeLenses ''NBinState) -iNBS :: NBinState a b f +iNBS :: NBinState a b f u iNBS = NBS 0 M.empty M.empty M.empty M.empty @@ -441,7 +412,9 @@ nTBin f l0@(NIX li0 lm) r0@(NIX ri0 rm) = evalState (tlq li0 ri0) iNBS return k -- | Total lattice functions -nLeqGLB, nSubGLB :: forall f . (Ord f, Show f) => NIX f -> NIX f -> NIX f +nLeqGLB, nSubGLB :: forall f . + (Ord f, Show f) + => NIX f -> NIX f -> NIX f nLeqGLB = nTBin iLeqGLB_ nSubGLB = nTBin (\_ _ fl fr fm _ -> iSubGLB_ (fl UUnique) (fr UUnique) (fm UUnique)) @@ -543,7 +516,9 @@ nPBin f l0@(NIX li0 lm) r0@(NIX ri0 rm) = evalState (runEitherT (tlq li0 ri0)) i -- | Partial lattice functions. These raise unification failures if -- the runtime would fail. -nLeqGLBRD, nLeqGLBRL :: forall f . (Ord f, Show f) => NIX f -> NIX f -> Either UnifFail (NIX f) +nLeqGLBRD, nLeqGLBRL :: forall f . + (Ord f, Show f) + => NIX f -> NIX f -> Either UnifFail (NIX f) nLeqGLBRD = nPBin iLeqGLBRD_ nLeqGLBRL = nPBin iLeqGLBRL_ @@ -576,4 +551,59 @@ mWellFormed (QMode ats vm@(vti,vto) _) = && (all (uncurry (flip nLeq)) $ vm:ats) +------------------------------------------------------------------------}}} +-- Cleanup and minimization {{{ + +nCrawl :: forall f . + (forall a . Uniq -> InstF f a) -- ^ Replace free variables + -> Uniq -- ^ Minimum uniqueness + -> NIX f + -> NIX f +nCrawl fv u0 n0@(NIX i0 m) = + let i0' = reall u0 i0 in NIX i0' $ execState (T.traverse (evac u0) i0') M.empty + where + reun = over inst_uniq (max u0) + + refv u IFree = fv u + refv _ x = x + + reall u = reun . refv u + + evac u i = gets (M.lookup i) >>= maybe (go u i) (const $ return ()) + + go u i = do + let l = ml n0 m i + case l of + Left n -> id %= M.insert i (Left $ nCrawl fv u n) + Right x -> do + id %= M.insert i (Right $ reall u x) + F.traverse_ (evac (maybe u (max u) $ iUniq x)) x + return () + +-- | Prune the internals of a 'NIX'. This really ought not be needed, but +-- it's handy for test generation. +nPrune :: forall f . NIX f -> NIX f +nPrune = nCrawl (const IFree) UUnique + +------------------------------------------------------------------------}}} +-- Pretty-printing {{{ + +instance Pretty (NIX f) where + pretty (nPrune -> NIX r m) = align $ + ri r <> if M.null m + then empty + else line <> (indent 2 $ + text "where" + <+> (align $ vsep $ map rme $ M.toList m)) + where + -- render index + rix = angles . text . show + + -- render map entry + rme (k,v) = rix k <+> equals <+> either pretty ri v + + ri = IP.compactly (text . show) rix + + + ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/NoAliasContext.hs b/src/Dyna/Analysis/Mode/Execution/NoAliasContext.hs index a45e67c..2c92ad9 100644 --- a/src/Dyna/Analysis/Mode/Execution/NoAliasContext.hs +++ b/src/Dyna/Analysis/Mode/Execution/NoAliasContext.hs @@ -33,8 +33,8 @@ module Dyna.Analysis.Mode.Execution.NoAliasContext ( -- ** Monad SIMCT(..), runSIMCT, -- *** And its context - SIMCtx(..), emptySIMCtx, -)where + SIMCtx(..), emptySIMCtx, allFreeSIMCtx, +) where -- import Control.Exception(assert) import Control.Lens @@ -42,21 +42,22 @@ import Control.Lens import Control.Monad.Error.Class import Control.Monad.State import Control.Monad.Trans.Either -import qualified Control.Monad.Trans.State as CMTS -import qualified Control.Monad.Trans.Reader as CMTR +import qualified Control.Monad.Trans.State as CMTS +import qualified Control.Monad.Trans.Reader as CMTR -- import Data.Function -import qualified Data.Map as M --- import qualified Data.Traversable as T +import qualified Data.Map as M +-- import qualified Data.Traversable as T -- import Data.Unique import Dyna.Analysis.Mode.Execution.NamedInst import Dyna.Analysis.Mode.Inst +import qualified Dyna.Analysis.Mode.InstPretty as IP import Dyna.Analysis.Mode.Unification -- import Dyna.Main.Exception import Dyna.Term.TTerm -- import Dyna.XXX.DataUtils import Dyna.XXX.MonadContext --- import qualified Debug.Trace as XT --- import qualified Text.PrettyPrint.Free as PP +-- import qualified Debug.Trace as XT +import qualified Text.PrettyPrint.Free as PP ------------------------------------------------------------------------}}} -- Variables {{{ @@ -69,8 +70,17 @@ data VR f n = | VRStruct (InstF f (VR f n)) deriving (Eq,Ord,Show) --- XXX Boy this is bad -vrToNIX :: VR f (NIX f) -> NIX f +instance (PP.Pretty f, PP.Pretty n) => PP.Pretty (VR f n) where + pretty (VRName n) = PP.pretty n + pretty (VRStruct y) = IP.compactly PP.pretty PP.pretty y + +-- This is used during rule analysis to capture the state of the binding +-- chart into the generated DOpAMine. +-- +-- XXX Ick. We should probably try to generate one NIX, not a cluster of +-- them, but... This is going to be replaced with the thesis's more general +-- 'extract' anyway. +vrToNIX :: (Show f) => VR f (NIX f) -> NIX f vrToNIX (VRName n) = n vrToNIX (VRStruct i) = nHide $ fmap vrToNIX i @@ -94,6 +104,13 @@ instance (Monad m) => MonadError UnifFail (SIMCT m f) where instance MonadIO m => MonadIO (SIMCT m f) where liftIO m = SIMCT $ lift (liftIO m) +instance (PP.Pretty f) => PP.Pretty (SIMCtx f) where + pretty (SIMCtx vm) = PP.vcat + $ flip map (M.toAscList vm) + $ \(v,vr) -> PP.pretty v + PP.<+> PP.text "=>" + PP.<+> PP.pretty vr + {- - XXX maybe @@ -106,6 +123,9 @@ instance (Monad m) => MonadState (SIMCtx f) (SIMCT m f) where emptySIMCtx :: SIMCtx f emptySIMCtx = SIMCtx M.empty +allFreeSIMCtx :: [DVar] -> SIMCtx f +allFreeSIMCtx fs = SIMCtx $ M.fromList $ map (\x -> (x, VRStruct IFree)) fs + runSIMCT :: SIMCT m f a -> SIMCtx f -> m (Either UnifFail (a, SIMCtx f)) runSIMCT q x = runEitherT (runStateT (unSIMCT q) x) @@ -178,13 +198,13 @@ instance (MCW (SIMCT m f) k) => MCW (CMTR.ReaderT r (SIMCT m f)) k where -- -- * @N@ -- 'NIX' f -- --- * @I@ -- @'InstF' f ('NI' f)@ +-- * @I@ -- @'InstF' f ('NIX' f)@ -- -- * @V@ -- 'VV' -- --- * @X@ -- 'VR' f 'NI' +-- * @X@ -- 'VR' f 'NIX' -- --- * @Y@ -- @InstF f (VR f 'NI')@ +-- * @Y@ -- @InstF f (VR f 'NIX')@ ------------------------------------------------------------------------}}} ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/NoAliasFunctions.hs b/src/Dyna/Analysis/Mode/Execution/NoAliasFunctions.hs index 1b34abd..8dbe269 100644 --- a/src/Dyna/Analysis/Mode/Execution/NoAliasFunctions.hs +++ b/src/Dyna/Analysis/Mode/Execution/NoAliasFunctions.hs @@ -25,7 +25,7 @@ module Dyna.Analysis.Mode.Execution.NoAliasFunctions ( -- * Unification - UnifParams(..), unifyVV, unifyVF, unifyUnaliasedNV, + unifyVV, unifyVF, unifyUnaliasedNV, -- * Matching, subVN, -- * Modes @@ -60,7 +60,7 @@ import Dyna.Term.TTerm import Dyna.XXX.DataUtils import Dyna.XXX.MonadContext -- import Dyna.XXX.MonadUtils -import qualified Debug.Trace as XT +-- import qualified Debug.Trace as XT ------------------------------------------------------------------------}}} -- Leq {{{ @@ -68,6 +68,7 @@ import qualified Debug.Trace as XT type LeqC m f n = (Ord f, Show f, Monad m, n ~ NIX f) + leqXX :: (LeqC m f n) => VR f n -> VR f n -> m Bool leqXX (VRStruct yl) (VRStruct yr) = iLeq_ leqXY leqXX yl yr @@ -87,7 +88,8 @@ leqNX nl (VRStruct yr) = iLeq_ leqNY leqNX (nExpose nl) yr leqNY :: (LeqC m f n) => NIX f -> InstF f (VR f n) -> m Bool -leqNY nl ir = iLeq_ leqNY leqNX (nExpose nl) ir +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 leqYN :: (LeqC m f n) => InstF f (VR f n) -> NIX f -> m Bool @@ -119,22 +121,6 @@ leqVX vl xr = do ------------------------------------------------------------------------}}} -- Unification {{{ -data UnifParams = UnifParams - { _up_live :: Bool - -- ^ Are we engaged in a live unification? See §3.2.1, - -- p43 and definition 3.2.19, p53 - - , _up_fake :: Bool - -- ^ Absent from the thesis but present in the Mercury - -- implementation is the consideration of "fake" - -- unifications, which are used when refining the - -- outputs of method calls and must be allowed to - -- descend through (Mostly)'Clobbered' material. - -- - -- See @compiler/prog_data.m@'s @unify_is_real@ type. - } -$(makeLenses ''UnifParams) - -- XXX Ought to have a MonadWriter to produce -- the actual opcode sequence for unification! -- the determinism information @@ -159,7 +145,7 @@ type UnifC m f n = (UnifC' m f n, -- applicable. unifyNN :: UnifC m f n => Uniq -> n -> n -> m n -unifyNN u a b = do +unifyNN u a b = {- XT.traceShow ("NN",a,b) $-} do live <- view up_live fake <- view up_fake either throwError (return . nUpUniq u) $ @@ -184,7 +170,7 @@ unifyVV :: forall f m n . MCVT m DVar ~ VR f n, MCR m DVar, MCA m DVar) => DVar -> DVar -> m DVar unifyVV vl vr | vl == vr = return vl -unifyVV vl vr = do +unifyVV vl vr = {- XT.traceShow ("VV", vl, vr) $-} do live <- view up_live calias (go live) vl vr where @@ -194,7 +180,7 @@ unifyVV vl vr = do checkAndReunif :: forall f m n . (UnifC m f n) => VR f n -> m (VR f n) -checkAndReunif x = do +checkAndReunif x = {- XT.trace "CAR" $-} do err <- leqXX x (VRStruct $ IAny UUnique) if err then unifyXX UUnique x (VRStruct $ IAny UShared) @@ -212,7 +198,7 @@ unifyXX u0 (VRStruct ya) (VRStruct yb) = unifyYY u0 ya yb -- to this one (or 'unifyNN'). unifyYY :: (UnifC m f n) => Uniq -> InstF f (VR f n) -> InstF f (VR f n) -> m (VR f n) -unifyYY u0 ya yb = do +unifyYY u0 ya yb = {- XT.traceShow ("YY", ya, yb) $-} do live <- view up_live fake <- view up_fake let f = if (live && not fake) then iLeqGLBRL_ else iLeqGLBRD_ @@ -226,8 +212,9 @@ unifyYY u0 ya yb = do unifyXY :: (UnifC m f n) => Uniq -> VR f n -> InstF f (VR f n) -> m (VR f n) -unifyXY u0 (VRStruct ya) yb = unifyYY u0 ya yb -unifyXY u0 (VRName nl) yr = unifyIY u0 (nExpose nl) yr +unifyXY u0 (VRStruct ya) yb = {- XT.trace "XY1" $-} unifyYY u0 ya yb +unifyXY u0 (VRName nl) (nShallow -> Just nr) = {- XT.trace "XY2" $ -} liftM VRName $ unifyNN u0 nl nr +unifyXY u0 (VRName nl) yr = {- XT.trace "XY3" $-} unifyIY u0 (nExpose nl) yr unifyNX :: (UnifC m f n) => Uniq -> n -> VR f n -> m (VR f n) @@ -240,8 +227,8 @@ unifyIY u0 ia yb = unifyYY u0 (fmap VRName ia) yb -- XXX Should stop earlier than it does xUpUniq :: (Ord f, n ~ NIX f) => Uniq -> VR f n -> VR f n -xUpUniq u (VRName n) = VRName $ nUpUniq u n -xUpUniq u (VRStruct y) = VRStruct $ over inst_uniq (max u) +xUpUniq u (VRName n) = {- XT.trace "XUU1" $ -} VRName $ nUpUniq u n +xUpUniq u (VRStruct y) = {- XT.trace "XUU2" $ -} VRStruct $ over inst_uniq (max u) $ fmap (xUpUniq u) y -- | Name-on-Variable unification. This should not be called on names @@ -279,32 +266,36 @@ unifyVF :: forall m f n . => (DVar -> m Bool) -> DVar -> f -> [DVar] -> m DVar unifyVF lf v f vs = do vl <- lf v - vi <- clookup v - vis <- mapM clookup vs + vy <- clookup v + vys <- mapM clookup vs - let vvis = zip vs vis + let vvys = zip vs vys - i'' <- runReaderT (unifyXY UUnique vi (IBound UUnique (M.singleton f vis) False)) + -- Perform a fake, dead unification of the variable's old inst and + -- bound(unique, f(...)). This gets us just the join on the lattice. + i'' <- runReaderT (unifyXY UUnique vy (IBound UUnique + (M.singleton f vys) + False)) (UnifParams False True) - -- Unification was successful; now, rip through the results and do the - -- second unification pass. + -- If we arrive here, unification was successful; + -- now, rip through the results and do the second unification pass. - (u,vis') <- case i'' of + (u,vys') <- case i'' of VRName n'' -> case nExpose n'' of IBound u (M.toList -> [(f',ris)]) False | f == f' -> do - x <- go unifyNX vl vvis u ris + x <- go unifyNX vl vvys u ris return (u,x) _ -> dynacPanicStr "unifyVF impossible NIX result" VRStruct (IBound u (M.toList -> [(f',ris)]) False) | f == f' -> do - x <- go unifyXX vl vvis u ris + x <- go unifyXX vl vvys u ris return (u,x) _ -> dynacPanicStr "unifyVF impossible result" -- Store back into the context - () <- sequence_ $ zipWith (cassign) vs vis' - cassign v (VRStruct $ IBound u (M.singleton f vis') False) + () <- sequence_ $ zipWith (cassign) vs vys' + cassign v (VRStruct $ IBound u (M.singleton f vys') False) return v where @@ -312,14 +303,14 @@ unifyVF lf v f vs = do (m' ~ ReaderT UnifParams m) => (Uniq -> a -> b -> m' (VR f (NIX f))) -> Bool -> [(DVar,b)] -> Uniq -> [a] -> m [VR f (NIX f)] - go uf vl vvis u ris = sequence $ zipWithTails + go uf vl vvys u ris = sequence $ zipWithTails (\ri (v',oi) -> do l <- lf v' runReaderT (uf u ri oi >>= checkAndReunif) (UnifParams (l && vl) True)) (\_ -> dynacPanicStr "unifyVF length mismatch") (\_ -> dynacPanicStr "unifyVF length mismatch") - ris vvis + ris vvys ------------------------------------------------------------------------}}} -- Matching {{{ @@ -330,7 +321,7 @@ type SubC m f n = (Ord f, Show f, subNN :: (SubC m f n) => n -> n -> m Bool -subNN a b = XT.traceShow ("SNN",a,b) $ return $ nSub a b +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 @@ -352,7 +343,7 @@ subVN :: forall f m n . => DVar -> n -> m Bool -subVN v n = XT.traceShow ("SVN",v,n) $ do +subVN v n = {- XT.traceShow ("SVN",v,n) $-} do vx <- clookup v subXN vx n diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs index baf7998..6593499 100644 --- a/src/Dyna/Analysis/Mode/Inst.hs +++ b/src/Dyna/Analysis/Mode/Inst.hs @@ -26,13 +26,14 @@ {-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -Wall #-} module Dyna.Analysis.Mode.Inst( - InstF(..), inst_uniq, inst_rec, + InstF(..), inst_uniq, inst_rec, inst_recps, iNotReached, iIsNotReached, iUniq, iIsFree, iWellFormed_, iEq_, iGround_, iLeq_, iLeqGLB_, iSub_, iSubGLB_, iSubLUB_, ) where +import Control.Applicative (Applicative) import Control.Lens -- import Control.Monad import qualified Data.Foldable as F @@ -152,7 +153,11 @@ $(makeLensesFor [("_inst_uniq","inst_uniq") ] ''InstF) --- XXX class (Pretty f, Pretty i) => Pretty (InstF f i) where +-- | 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 ------------------------------------------------------------------------}}} -- Instantiation States: Unary predicates {{{ @@ -514,7 +519,7 @@ iSubLUB_ _ _ l r q (IBound u m b) (IBound u' m' b') = do ------------------------------------------------------------------------}}} -- Instantiation States: Utility Functions {{{ - +-- | const $ return False crf :: (Monad m) => a -> m Bool crf = const $ return False diff --git a/src/Dyna/Analysis/Mode/InstPretty.hs b/src/Dyna/Analysis/Mode/InstPretty.hs new file mode 100644 index 0000000..98bbad3 --- /dev/null +++ b/src/Dyna/Analysis/Mode/InstPretty.hs @@ -0,0 +1,32 @@ +--------------------------------------------------------------------------- +-- | Functions for pretty-printing Insts +-- +-- Intended to be imported qualified + +-- Header material {{{ +{-# LANGUAGE OverloadedStrings #-} +module Dyna.Analysis.Mode.InstPretty where + +import qualified Data.Map as M +import Data.String +import Dyna.Analysis.Mode.Inst +import Dyna.Analysis.Mode.Uniq +import Text.PrettyPrint.Free + +compactUniq :: (IsString a) => Uniq -> a +compactUniq UUnique = "un" +compactUniq UMostlyUnique = "mu" +compactUniq UShared = "sh" +compactUniq UMostlyClobbered = "mc" +compactUniq UClobbered = "cl" + +compactly :: (f -> Doc e) + -> (a -> Doc e) + -> InstF f a -> Doc e +compactly _ _ IFree = "F" +compactly _ _ (IAny u) = "A@" <> compactUniq u +compactly _ _ (IUniv u) = "U@" <> compactUniq u +compactly f a (IBound u bm b) = (semiBraces $ if b then (text "B"):rm else rm) + <> char '@' <> compactUniq u + where + rm = map (\(k,vs) -> f k <> tupled (map a vs)) (M.toList bm) diff --git a/src/Dyna/Analysis/Mode/Unification.hs b/src/Dyna/Analysis/Mode/Unification.hs index f1c4866..3ebc4bf 100644 --- a/src/Dyna/Analysis/Mode/Unification.hs +++ b/src/Dyna/Analysis/Mode/Unification.hs @@ -2,11 +2,13 @@ -- | Wrappers around 'InstF' primitives that are useful during unification. -- Header material {{{ +{-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -Wall #-} module Dyna.Analysis.Mode.Unification {-( )-} where +import Control.Lens.TH import qualified Data.Maybe as MA import Dyna.Analysis.Mode.Inst import Dyna.Analysis.Mode.Uniq @@ -21,6 +23,25 @@ data UnifFail = | UFExDomain -- ^ A partial function was applied outside its domain deriving (Eq,Ord,Show) +------------------------------------------------------------------------}}} +-- Unification-wide Read-only Parameters {{{ + +data UnifParams = UnifParams + { _up_live :: Bool + -- ^ Are we engaged in a live unification? See §3.2.1, + -- p43 and definition 3.2.19, p53 + + , _up_fake :: Bool + -- ^ Absent from the thesis but present in the Mercury + -- implementation is the consideration of "fake" + -- unifications, which are used when refining the + -- outputs of method calls and must be allowed to + -- descend through (Mostly)'Clobbered' material. + -- + -- See @compiler/prog_data.m@'s @unify_is_real@ type. + } +$(makeLenses ''UnifParams) + ------------------------------------------------------------------------}}} -- Unification {{{ @@ -41,7 +62,7 @@ data UnifFail = -- predicate can run with a clobbered input, and if not, we'll fail at that -- point. A semidet unification, on the other hand, cannot run with a -- clobbered input. - +-- -- Definition 3.2.19, p53 -- -- XXX In contrast to the thesis, we ignore the size of the sets represented diff --git a/src/Dyna/Analysis/RuleMode.hs b/src/Dyna/Analysis/RuleMode.hs index 72d5e08..5fb34f3 100644 --- a/src/Dyna/Analysis/RuleMode.hs +++ b/src/Dyna/Analysis/RuleMode.hs @@ -41,7 +41,6 @@ import Control.Monad.Trans.Reader import Control.Monad.Identity import qualified Data.ByteString as B import qualified Data.ByteString.Char8 as BC -import qualified Data.Either as E import qualified Data.IntMap as IM -- import qualified Data.List as L import qualified Data.Map as M @@ -57,7 +56,7 @@ import Dyna.Analysis.Mode.Execution.NoAliasFunctions import Dyna.Term.TTerm import Dyna.Term.Normalized import Dyna.Main.Exception -import Dyna.XXX.DataUtils(argmin,mapInOrApp,mapMinRepView) +import Dyna.XXX.DataUtils(argmin,mapInOrCons,mapMinRepView) import Dyna.XXX.MonadContext import Dyna.XXX.Trifecta (prettySpanLoc) -- import Dyna.XXX.TrifectaTest @@ -134,20 +133,19 @@ mapMaybeModeCompat mis mo = return (d,f)) -} --- | Free, Universal, or Panic. A rather simplistic take on unification. +-- | Free, Ground, or Neither. A rather simplistic take on unification. -- -- XXX There is nothing good about this. -fup :: forall a m . (Monad m, MCVT m DVar ~ VR DFunct (NIX DFunct), MCR m DVar) - => DVar -> m a -> m a -> m a -fup v cf cu = do - vr <- clookup v - let vi = case vr of - VRName vn -> fmap VRName $ nExpose vn - VRStruct vx -> vx - case vi of - IFree -> cf - IUniv _ -> cu - _ -> dynacPanic "Unexpected instantiation state while planning" +fgn :: forall a m . (Monad m, MCVT m DVar ~ VR DFunct (NIX DFunct), MCR m DVar) + => DVar -> m a -> m a -> m a -> m a +fgn v cf cg cn = do + ff <- v `subVN` (nHide IFree) + gf <- v `subVN` (nHide $ IUniv UShared) + case (ff,gf) of + (True ,True ) -> dynacPanicStr "Variable is both free and ground" + (True ,False) -> cf + (False,True ) -> cg + (False,False) -> cn possible :: (Monad m) => BackendPossible fbs @@ -166,17 +164,21 @@ possible fp cr = -- Assign or check Right (CAssign o i) -> - fup o (runReaderT (unifyVU o) (UnifParams True False) + fgn o (runReaderT (unifyVU o) (UnifParams True False) >> return [ OPAsgn o (NTBase i) ]) (let chk = "_chk" in return [ OPAsgn chk (NTBase i), OPCheq chk o]) + (throwError UFExDomain) Right (CEquals o i) -> - fup o (fup i (throwError UFExDomain) + fgn o (fgn i (throwError UFExDomain) (runReaderT (unifyVV i o) (UnifParams True False) - >> return [ OPAsgn o (NTVar i) ])) - (fup i (runReaderT (unifyVV i o) (UnifParams True False) + >> return [ OPAsgn o (NTVar i) ]) + (throwError UFExDomain)) + (fgn i (runReaderT (unifyVV i o) (UnifParams True False) >> return [ OPAsgn i (NTVar o) ]) - (return [ OPCheq o i ])) + (return [ OPCheq o i ]) + (throwError UFExDomain)) + (throwError UFExDomain) {- case i of @@ -185,22 +187,28 @@ possible fp cr = -} -- Structure building or unbuilding - Right (CStruct o is funct) -> fup o (mapM_ isBound is >> bind o >> return [ OPWrap o is funct ]) - (buildPeel) - where - buildPeel = do - (is', mcis) <- zipWithM maybeCheck is newvars >>= return . unzip - let cis = MA.catMaybes mcis - return ([ OPPeel is' o funct ] ++ map (uncurry OPCheq) cis) + Right (CStruct o is funct) -> + fgn o (mapM_ ensureBound is >> bind o >> return [ OPWrap o is funct ]) + buildPeel + (throwError UFExDomain) + where + buildPeel = do + (is', mcis) <- zipWithM maybeCheck is newvars >>= return . unzip + let cis = MA.catMaybes mcis + return ([ OPPeel is' o funct ] ++ map (uncurry OPCheq) cis) - newvars = map (\n -> BC.pack $ "_chk_" ++ (show n)) [0::Int ..] + newvars = map (\n -> BC.pack $ "_chk_" ++ (show n)) [0::Int ..] - maybeCheck v nv = fup v (return (v,Nothing)) (return (nv, Just (nv,v))) + maybeCheck v nv = fgn v (return (v,Nothing)) + (return (nv, Just (nv,v))) + (throwError UFExDomain) -- Disequality constraints require that both inputs be brought to ground - Right (CNotEqu o i) -> fup o (throwError UFExDomain) - (fup i (throwError UFExDomain) - (return [ OPCkne o i ])) + Right (CNotEqu o i) -> fgn o (throwError UFExDomain) + (fgn i (throwError UFExDomain) + (return [ OPCkne o i ]) + (throwError UFExDomain)) + (throwError UFExDomain) -- XXX Indirect evaluation is not yet supported Left (_, CEval _ _) -> dynacSorry "Indir eval" @@ -225,15 +233,14 @@ possible fp cr = vi <- clookup v return $ MV v (vrToNIX vi) mo - isBound v = fup v (throwError UFExDomain) (return ()) + ensureBound v = fgn v (throwError UFExDomain) + (return ()) + (throwError UFExDomain) bind x = runReaderT (unifyVU x) (UnifParams False False) ------------------------------------------------------------------------}}} -- ANF to Cruxes {{{ -allCruxVars :: S.Set (Crux DVar TBase) -> S.Set DVar -allCruxVars = S.unions . map cruxVars . S.toList - {- anfVars :: ANFState -> S.Set DVar anfVars (AS { as_evals = evals, as_unifs = unifs, as_assgn = assgns } ) = @@ -309,34 +316,6 @@ simpleCost (PP { pp_score = osc, pp_plan = pfx }) act = ------------------------------------------------------------------------}}} -- Planning {{{ --- $dupcrux --- --- Consider a rule like @a += b(X) * b(Y).@ This desugars into an ANF with --- two separate evaluations of @b(_)@. This is problematic, since we will --- plan each evaluation separately. (Note that CSE won't help; we really do --- mean to compute the cross-product in this case, but not double-count the --- diagonal!) The workaround here is to /order/ the evaluations (by their --- ANF temporary variables, for the moment). --- --- For replacement updates, the correct action is to @continue@ the --- evaluation loop when an eariler (by the intrinsic ordering) iterator --- within a update to a later (by the intrinsic ordering) evaluation --- lands at the same position. --- --- For delta updates, the ordering is used for the Blatz-Eisner update --- propagation strategy -- new values are used in earlier evaluations (than --- the one being updated) and old values are used in later evaluations. --- --- When backward chaining, we get to ignore all of this, since we only --- produce one backward chaining plan. --- --- XXX It's unclear that this is really the right solution. Maybe we should --- be planning a single stream of instructions for each dfuctar, rather than --- each evalution arc, but it's not quite clear that there's a nice --- graphical story to be told in that case? --- --- XXX What do we do in the CEval case?? We need to check every evaluation --- inside a CEval update? data PartialPlan fbs = PP { pp_cruxes :: S.Set (Crux DVar TBase) , pp_binds :: BindChart @@ -346,7 +325,7 @@ data PartialPlan fbs = PP { pp_cruxes :: S.Set (Crux DVar TBase) } pp_liveVars :: PartialPlan fbs -> S.Set DVar -pp_liveVars p = S.unions $ map cruxVars $ S.toList (pp_cruxes p) +pp_liveVars p = allCruxVars (pp_cruxes p) -- XXX This does not have a way to signal UFNotReached back to its caller. -- That is particularly disappointing since any unification producing that @@ -432,19 +411,13 @@ planner_ :: (Crux DVar TBase -> SIMCT Identity DFunct (Actions fbs)) -- ^ Maybe the updated evaluation crux, the interned -- representation of the term being updated, and -- result variable. - -> S.Set DVar - -- ^ Any variables bound on the way in, in addition to - -- the two given for an initial crux - -> S.Set DVar + -> SIMCtx DVar -- ^ Unbound variables in the rule -> [(Cost, Actions fbs)] -- ^ Plans and their costs -planner_ st sc cr mic bv fv = runAgenda +planner_ st sc cr mic ictx = runAgenda $ PP { pp_cruxes = cr - , pp_binds = SIMCtx $ M.fromSet (const $ VRStruct (IUniv UShared)) - (S.unions [bv,bi]) - `M.union` - M.fromSet (const $ VRStruct IFree) fv + , pp_binds = ctx' , pp_restrictSearch = False , pp_score = 0 , pp_plan = ip @@ -455,7 +428,7 @@ planner_ st sc cr mic bv fv = runAgenda mioaPlan :: PartialPlan fbs -> M.Map Cost [PartialPlan fbs] -> M.Map Cost [PartialPlan fbs] - mioaPlan p@(PP{pp_score=psc}) = mapInOrApp psc p + mioaPlan p@(PP{pp_score=psc}) = mapInOrCons psc p go pq = maybe [] go' $ mapMinRepView pq where @@ -463,15 +436,22 @@ planner_ st sc cr mic bv fv = runAgenda Left df -> df : (go pq') Right ps' -> go (foldr mioaPlan pq' ps') + ctx' = either (const $ dynacPanicStr "Unable to bind input variable") + snd + $ runIdentity + $ flip runSIMCT ictx + $ flip runReaderT (UnifParams True False) + (mapM_ (unifyUnaliasedNV (nHide $ IUniv UShared)) bis) + -- XREF:INITPLAN - (ip,bi) = case mic of - Nothing -> ([],S.empty) + (ip,bis) = case mic of + Nothing -> ([],[]) Just (CCall o is f, hi, ho) -> ( [ OPPeel is hi f , OPAsgn o (NTVar ho)] - , S.fromList $ o:is) + , o:is) Just (CEval o i, hi, ho) -> ( [ OPAsgn i (NTVar hi) , OPAsgn o (NTVar ho)] - , S.fromList $ [o,i] ) + , [o,i] ) -- | Pick the best plan, but stop the planner from going off the rails by -- considering at most a constant number of plans. @@ -499,21 +479,47 @@ planUpdate :: BackendPossible fbs -> (PartialPlan fbs -> Actions fbs -> Cost) -> S.Set (Crux DVar TBase) -- ^ Normal form -> (EvalCrux DVar, DVar, DVar) - -> S.Set DVar + -> SIMCtx DVar -> Maybe (Cost, Actions fbs) -planUpdate bp sc anf mi fv = - bestPlan $ planner_ (possible bp) sc anf (Just mi) S.empty fv +planUpdate bp sc anf mi ictx = + bestPlan $ planner_ (possible bp) sc anf (Just mi) ictx planInitializer :: BackendPossible fbs -> Rule -> Maybe (Cost, Actions fbs) planInitializer bp r = let cruxes = r_cruxes r in - bestPlan $ planner_ (possible bp) simpleCost cruxes Nothing S.empty (allCruxVars cruxes) + bestPlan $ planner_ (possible bp) simpleCost cruxes Nothing + (allFreeSIMCtx $ S.toList $ allCruxVars cruxes) -- | Given a particular crux and the remaining evaluation cruxes in a rule, -- find all the \"later\" evaluations which will need special handling and -- generate the cruxes necessary to prevent double-counting. -- --- See $dupcrux. +-- Consider a rule like @a += b(X) * b(Y).@ This desugars into an ANF with +-- two separate evaluations of @b(_)@. This is problematic, since we will +-- plan each evaluation separately. (Note that CSE won't help; we really do +-- mean to compute the cross-product in this case, but not double-count the +-- diagonal!) The workaround here is to /order/ the evaluations, thus why +-- ANF gives a numeric identifier to each evaluation. +-- +-- For replacement updates, the correct action is to @continue@ the +-- evaluation loop when an eariler (by the intrinsic ordering) iterator +-- within a update to a later (by the intrinsic ordering) evaluation +-- lands at the same position. +-- +-- For delta updates, the ordering is used for the Blatz-Eisner update +-- propagation strategy -- new values are used in earlier evaluations (than +-- the one being updated) and old values are used in later evaluations. +-- +-- When backward chaining, we get to ignore all of this, since we only +-- produce one backward chaining plan. +-- +-- XXX It's unclear that this is really the right solution. Maybe we should +-- be planning a single stream of instructions for each dfunctar, rather than +-- each evalution arc, but it's not quite clear that there's a nice +-- graphical story to be told in that case? +-- +-- XXX What do we do in the CEval case?? We need to check every evaluation +-- inside a CEval update? handleDoubles :: (Ord a, Ord b) => (Int -> a -> a -> a) -> (Int,EvalCrux a) @@ -540,6 +546,9 @@ handleDoubles vc e r = S.fold (go e) S.empty r $ S.insert (CStruct qcv qis qf) $ S.insert (CNotEqu ecv qcv) s +-- XXX Split into two functions, one which wraps handleDoubles and one which +-- feeds that to the planner. The former will also be useful in dumping +-- more accurate ANF. planEachEval :: BackendPossible fbs -- ^ The backend's primitive support -> (DFunctAr -> Bool) -- ^ Indicator for constant function -> Rule @@ -547,13 +556,15 @@ planEachEval :: BackendPossible fbs -- ^ The backend's primitive support -- planEachEval _ _ _ = [] planEachEval bp cs r = map (\(n,cr) -> - let cruxes' = S.union cruxes + let cruxes' = S.union (r_cruxes r) (S.map Right $ handleDoubles mkvar cr (S.delete cr $ S.fromList ecs)) in (n, varify $ planUpdate bp simpleCost cruxes' (mic $ snd cr) - (allCruxVars cruxes'))) + (allFreeSIMCtx + $ S.toList + $ allCruxVars cruxes'))) -- Filter out non-constant evaluations -- -- XXX This instead should look at the update modes of each evaluation @@ -566,11 +577,9 @@ planEachEval bp cs r = -- Grab all evaluations $ ecs where - cruxes = r_cruxes r - mkvar n v1 v2 = B.concat ["chk",v1,"_",v2,"_",BC.pack $ show n] - ecs = fst $ E.partitionEithers $ S.toList cruxes + ecs = IM.toList $ r_ecruxes r -- XXX I am not terribly happy about these, but it'll do for the moment. -- @@ -628,7 +637,7 @@ combineUpdatePlans = go (M.empty) <+> group (pretty fa) <+> "in rule at" <+> (prettySpanLoc $ r_span fr) - Just (c,v1,v2,a) -> go' xs fr ys $ mapInOrApp fa (fr,n,c,v1,v2,a) m + Just (c,v1,v2,a) -> go' xs fr ys $ mapInOrCons fa (fr,n,c,v1,v2,a) m where fa = evalCruxFA ev ev = maybe (dynacPanic $ "Eval index without eval crux in rule " @@ -653,7 +662,7 @@ combineQueryPlans = go (M.empty) go' _ fr Nothing _ = dynacUserErr $ "No query plan for rule at" <+> (prettySpanLoc $ r_span fr) - go' xs fr (Just (c,v,a)) m = go (mapInOrApp (findHeadFA fr) + go' xs fr (Just (c,v,a)) m = go (mapInOrCons (findHeadFA fr) (fr,c,v,a) m) xs diff --git a/src/Dyna/Backend/Python/Backend.hs b/src/Dyna/Backend/Python/Backend.hs index 34571eb..8ce945d 100644 --- a/src/Dyna/Backend/Python/Backend.hs +++ b/src/Dyna/Backend/Python/Backend.hs @@ -11,36 +11,35 @@ module Dyna.Backend.Python.Backend (pythonBackend) where -import Control.Applicative ((<*)) -import qualified Control.Arrow as A -import Control.Exception +-- import Control.Applicative ((<*)) +-- import qualified Control.Arrow as A +-- import Control.Exception import Control.Lens ((^.)) import Control.Monad -import qualified Data.ByteString as B -import qualified Data.ByteString.UTF8 as BU -import Data.Char +-- import qualified Data.ByteString as B +-- import qualified Data.ByteString.UTF8 as BU +-- import Data.Char -- import Data.Either -import qualified Data.List as L +-- import qualified Data.List as L import qualified Data.Map as M import qualified Data.Maybe as MA -import qualified Data.Ord as O -import qualified Data.Set as S -import qualified Debug.Trace as XT +-- import qualified Data.Ord as O +-- import qualified Data.Set as S +-- import qualified Debug.Trace as XT import Dyna.Analysis.ANF -import Dyna.Analysis.Aggregation +-- import Dyna.Analysis.Aggregation import Dyna.Analysis.DOpAMine import Dyna.Analysis.Mode import Dyna.Analysis.RuleMode import Dyna.Backend.BackendDefn import Dyna.Main.Exception import Dyna.Term.TTerm -import qualified Dyna.ParserHS.Parser as P -import Dyna.XXX.DataUtils (mapInOrApp) +-- import qualified Dyna.ParserHS.Parser as P import Dyna.XXX.PPrint import Dyna.XXX.Trifecta (prettySpanLoc) import System.IO import Text.PrettyPrint.Free -import qualified Text.Trifecta as T +-- import qualified Text.Trifecta as T ------------------------------------------------------------------------}}} -- DOpAMine Backend Information {{{ @@ -50,6 +49,7 @@ import qualified Text.Trifecta as T -- generation without having to re-probe the modes. newtype PyDopeBS = PDBS (forall e . ModedVar -> [ModedVar] -> Doc e) +nfree, nuniv :: NIX DFunct nfree = nHide IFree nuniv = nHide (IUniv UShared) diff --git a/src/Dyna/Main/Driver.hs b/src/Dyna/Main/Driver.hs index f053703..ab77526 100644 --- a/src/Dyna/Main/Driver.hs +++ b/src/Dyna/Main/Driver.hs @@ -307,7 +307,7 @@ main_ argv = do _ -> dynacSorry "We can't do more than one file" main :: IO () -main = catch (getArgs >>= main_) printerr +main = handle someExnPanic $ handle printerr (getArgs >>= main_) where printerr x = pe x >> exitFailure @@ -328,7 +328,12 @@ main = catch (getArgs >>= main_) printerr taMsg PP.hPutDoc stderr d hPutStrLn stderr "" - pe (Panic d) = do + pe (Panic d) = panic d + + someExnPanic (e :: SomeException) = panic $ "Uncaught Haskell exception:" + <+> text (show e) + + panic d = do hPutStrLn stderr "Compiler panic!" taMsg PP.hPutDoc stderr d diff --git a/src/Dyna/Term/TTerm.hs b/src/Dyna/Term/TTerm.hs index ca401c0..c2c63ca 100644 --- a/src/Dyna/Term/TTerm.hs +++ b/src/Dyna/Term/TTerm.hs @@ -37,6 +37,9 @@ import qualified Data.Foldable as F import qualified Data.Traversable as T import qualified Text.PrettyPrint.Free as PP +-- This is needed to work with ghc 7.4 and bytestring 0.9.2.1 +import qualified Data.ByteString.Char8() + ------------------------------------------------------------------------}}} -- Term Base Cases {{{ diff --git a/src/Dyna/XXX/DataUtils.hs b/src/Dyna/XXX/DataUtils.hs index f8f18e8..261a83b 100644 --- a/src/Dyna/XXX/DataUtils.hs +++ b/src/Dyna/XXX/DataUtils.hs @@ -10,9 +10,9 @@ module Dyna.XXX.DataUtils ( -- ** Upsertion mapUpsert, -- ** Maps of lists - mapInOrApp, mapMinRepView, + mapInOrCons, mapMinRepView, -- ** Unification-style utilities - mapSemiprune, + mapSemiprune, intmapSemiprune, -- ** Backports mergeWithKey, -- * 'Data.Set' utilities @@ -21,10 +21,11 @@ module Dyna.XXX.DataUtils ( ) where -import qualified Data.List as L -import qualified Data.Map as M -import qualified Data.Ord as O -import qualified Data.Set as S +import qualified Data.List as L +import qualified Data.Map as M +import qualified Data.IntMap as IM +import qualified Data.Ord as O +import qualified Data.Set as S argmax :: (Ord b) => (a -> b) -> [a] -> a argmax = L.maximumBy . O.comparing @@ -59,8 +60,8 @@ mapUpsert k v m = -- 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 +mapInOrCons :: (Ord k) => k -> v -> M.Map k [v] -> M.Map k [v] +mapInOrCons k v m = M.alter (\mv -> Just $ v:nel mv) k m where nel Nothing = [] nel (Just x) = x @@ -83,12 +84,12 @@ mapMinRepView m = do -- leave the map with identity mappings, which should be carefully -- interpreted by the user (probably as a free variable) mapSemiprune :: (Ord k) - => (v -> Maybe k) -- ^ Is this a variable link? - -> (k -> v) -- ^ What should we store to indicate + => (v -> Maybe k) -- ^ Is this a variable link? + -> (k -> v) -- ^ What should we store to indicate -- a pointer to this variable? -> k -- ^ Initial variable - -> M.Map k v -- ^ In this map - -> (k, M.Map k v) -- ^ (terminus of chain, pruned map) + -> M.Map k v -- ^ In this map + -> (k, M.Map k v) -- ^ (terminus of chain, pruned map) mapSemiprune q p k m = case M.lookup k m >>= q of Nothing -> (k, m) Just k' -> go (S.singleton k) k' @@ -102,6 +103,25 @@ 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' +-- | 'mapSemiprune' for the special case of 'IntMap's. +intmapSemiprune :: (v -> Maybe Int) + -> (Int -> v) + -> Int + -> IM.IntMap v + -> (Int, IM.IntMap v) +intmapSemiprune q p k m = case IM.lookup k m >>= q of + Nothing -> (k, m) + Just k' -> go (S.singleton k) k' + where + go v k' = + case IM.lookup k' m >>= q of + Nothing -> (k', setAll m v k') + Just k'' | k'' `S.member` v -> (k'', setAll m v k'') -- (M.delete k'' m) (S.delete k'' v) k'') + Just k'' -> go (k' `S.insert` v) k'' + + setAll m' v k' = IM.fromList (map (\x -> (x,p k')) $ S.toList v) + `IM.union` m' + -- | A generalized version of 'zipWith' that gives access to tail elements -- as well. -- 2.50.1