From: Nathaniel Wesley Filardo <nwf@cs.jhu.edu>
Date: Thu, 9 May 2013 05:12:19 +0000 (-0400)
Subject: Cleanup ANF frontend some more
X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=fec06556df338f3c89136c2184f32fadf383b946;p=dyna2

Cleanup ANF frontend some more

Eliminate the awkward old ANF language in favor of direct translation to
Cruxes in Dyna.Analysis.ANF.  Evaluation cruxes are now properly indexed
within rules using an Int, so we don't have to rely on the output variable
being unique.  There are more flavors of unification cruxes, including
inequality constraints.

The terrible 'handleConflictors' has been replaced with a much more
sane function which operates on cruxes, rather than on DOpAMine, which will
be welcome when we have more interesting OPIter modes.

While here, move python scripts from bin/ to src/Dyna/Backend/Python and
adjust the world.  Use this as an excuse to make ./debug invoke the dyna
compiler only once and dump everything to different files in $PROGRAM.d/
---

diff --git a/debug b/debug
index 0e66300..69ac8ec 100755
--- a/debug
+++ b/debug
@@ -1,3 +1,3 @@
 #!/usr/bin/env bash
 
-python bin/prototype.py $@
+python src/Dyna/Backend/Python/debug.py $@
diff --git a/dyna b/dyna
index abb76af..2794e6c 100755
--- a/dyna
+++ b/dyna
@@ -1,3 +1,3 @@
 #!/usr/bin/env bash
 
-python bin/interpreter.py $@
+python src/Dyna/Backend/Python/interpreter.py $@
diff --git a/dyna.cabal b/dyna.cabal
index bc5a4c8..454c015 100644
--- a/dyna.cabal
+++ b/dyna.cabal
@@ -29,9 +29,9 @@ Library
 
 
     Exposed-Modules:    Dyna.Analysis.ANF,
+                        Dyna.Analysis.ANFPretty,
                         Dyna.Analysis.Mode,
                         Dyna.Backend.BackendDefn,
-                        Dyna.Main.Driver,
                         Dyna.Main.Exception,
                         Dyna.ParserHS.Parser,
                         Dyna.XXX.Trifecta
@@ -150,6 +150,7 @@ Test-suite dyna-selftests
                         recursion-schemes >=3.0,
                         reducers >=3.0,
                         semigroups >=0.8,
+                        smallcheck >= 1.0,
                         tagged >= 0.4.4,
                         template-haskell,
                         test-framework >=0.6,
diff --git a/src/Dyna/Analysis/ANF.hs b/src/Dyna/Analysis/ANF.hs
index 490fb39..3b66b68 100644
--- a/src/Dyna/Analysis/ANF.hs
+++ b/src/Dyna/Analysis/ANF.hs
@@ -67,38 +67,45 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TupleSections #-}
+{-# OPTIONS_GHC -Wall #-}
 
 module Dyna.Analysis.ANF (
-    ANFState(..),  Rule(..),
-    normTerm, normRule, runNormalize, printANF,
+	Crux, EvalCrux(..), UnifCrux(..), cruxIsEval, cruxVars,
+	
+    Rule(..), ANFAnnots, ANFWarns,
+    normTerm, normRule, runNormalize,
 
 	-- * Internals
 	SelfDispos(..), ArgDispos(..), ECSrc(..), EvalCtx,
+
+    -- * Placeholders
+    findHeadFA,
 ) where
 
+import           Control.Lens
 import           Control.Monad.Reader
 import           Control.Monad.State
 -- import           Control.Unification
 import qualified Data.ByteString.Char8      as BC
 import qualified Data.ByteString.UTF8       as BU
 import qualified Data.ByteString            as B
-import qualified Data.Char                  as C
+-- import qualified Data.Char                  as C
+import qualified Data.Either                as E
 import qualified Data.Map                   as M
+import qualified Data.Maybe                 as MA
+-- import qualified Data.IntMap                as IM
+import qualified Data.Set                   as S
 -- import qualified Debug.Trace                as XT
 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.PPrint (valign)
 -- import           Dyna.Test.Trifecta         -- XXX
-import           Text.PrettyPrint.Free
 import qualified Text.Trifecta              as T
 
-
-import           Dyna.XXX.Trifecta (prettySpanLoc)
-
 ------------------------------------------------------------------------}}}
 -- Preliminaries                                                        {{{
 
@@ -107,6 +114,9 @@ data ECSrc = ECFunctor
 
 type EvalCtx = (ECSrc,ArgDispos)
 
+type ANFAnnots = M.Map DVar [Annotation (T.Spanned P.Term)]
+type ANFWarns  = [(BU.ByteString, [T.Span])]
+
 newtype ANFDict = AD { ad_dt :: DisposTab }
 {-
   { -- | A map from (functor,arity) to a list of bits indicating whether to
@@ -132,27 +142,67 @@ mergeDispositions = md
   md SDQuote   (ECExplicit,ADEval)  = ADEval
   md SDQuote   (_,_)                = ADQuote
 
+------------------------------------------------------------------------}}}
+-- Cruxes                                                               {{{
+
+data EvalCrux v = CCall Int v [v] DFunct
+                | CEval Int v v
+ deriving (Eq,Ord,Show)
+
+data UnifCrux v n = CStruct v [v] DFunct   -- Known structure building
+                  | CAssign v n            -- Constant loading
+                  | CEquals v v            -- Equality constraint
+                  | CNotEqu v v            -- Disequality constraint
+ deriving (Eq,Ord,Show)
+
+type Crux v n = Either (EvalCrux v) (UnifCrux v n)
+
+cruxIsEval :: Crux v n -> Bool
+cruxIsEval (Left _) = True
+cruxIsEval (Right _) = False
+
+cruxVars :: Crux DVar TBase -> S.Set DVar
+cruxVars = either evalVars unifVars
+ where
+  evalVars cr = case cr of
+    CCall _ o is        _ -> S.fromList (o:is)
+    CEval _ o i           -> S.fromList [o,i]
+  unifVars cr = case cr of
+    CStruct o is _ -> S.fromList (o:is)
+    CAssign o _    -> S.singleton o
+    CEquals o i    -> S.fromList [o,i]
+    CNotEqu o i    -> S.fromList [o,i]
+
+
+------------------------------------------------------------------------}}}
+-- ANF State                                                            {{{
+
 data ANFState = AS
-              { as_next  :: !Int
-              , as_evals :: M.Map DVar EVF
-              , as_assgn :: M.Map DVar EBF
-              , as_unifs :: [(DVar,DVar)]
-              , as_annot :: M.Map DVar [Annotation (T.Spanned P.Term)]
-              , as_warns :: [(B.ByteString, [T.Span])]
+              { _as_next_var  :: !Int
+              , _as_next_eval :: !Int
+              , _as_cruxes    :: S.Set (Crux DVar TBase)
+              -- , as_evals :: IM.IntMap (DVar,EVF)
+              -- , as_assgn :: M.Map DVar EBF
+              -- , as_unifs :: [(DVar,DVar)]
+              , _as_annot :: ANFAnnots
+              , _as_warns :: ANFWarns
               }
  deriving (Show)
+$(makeLenses ''ANFState)
+
+addCrux :: (MonadState ANFState m) => Crux DVar TBase -> m ()
+addCrux c = as_cruxes %= (S.insert c)
 
 nextVar :: (MonadState ANFState m) => String -> m DVar
 nextVar pfx = do
-    vn  <- gets as_next
-    modify (\s -> s { as_next = vn + 1 })
+    vn  <- as_next_var <<%= (+1)
     return $ BU.fromString $ pfx ++ show vn
 
 newEval :: (MonadState ANFState m) => String -> EVF -> m DVar
 newEval pfx t = do
     n   <- nextVar pfx
-    evs <- gets as_evals
-    modify (\s -> s { as_evals = M.insert n t evs })
+    ne  <- as_next_eval <<%= (+1)
+    addCrux (Left $ either (CEval ne n) (uncurry (flip (CCall ne n))) t)
     return n
 
 newAssign :: (MonadState ANFState m) => String -> ENF -> m DVar
@@ -164,14 +214,12 @@ newAssign pfx t =
  where
   go u = do
     n   <- nextVar pfx
-    uns <- gets as_assgn
-    modify (\s -> s { as_assgn = M.insert n u uns })
+    addCrux (Right $ either (CAssign n) (uncurry (flip (CStruct n))) u)
     return n
 
 newAnnot :: (MonadState ANFState m)
          => DVar -> Annotation (T.Spanned P.Term) -> m ()
-newAnnot v a = do
-    modify (\s -> s { as_annot = mapInOrApp v a (as_annot s) })
+newAnnot v a = as_annot %= mapInOrApp v a
 
 {-
 newAssignNT :: (MonadState ANFState m) => String -> NTV -> m DVar
@@ -182,10 +230,10 @@ newAssignNT pfx x             = newAssign pfx $ Left x
 doUnif :: (MonadState ANFState m) => DVar -> DVar -> m ()
 doUnif v w = if v == w
               then return ()
-              else modify (\s -> s { as_unifs = (v,w):(as_unifs s) })
+              else addCrux (Right $ CEquals v w)
 
 newWarn :: (MonadState ANFState m) => B.ByteString -> [T.Span] -> m ()
-newWarn msg loc = modify (\s -> s { as_warns = (msg,loc):(as_warns s) })
+newWarn msg loc = as_warns %= ((msg,loc):)
 
 ------------------------------------------------------------------------}}}
 -- Normalize a Term                                                     {{{
@@ -343,16 +391,19 @@ data Rule = Rule { r_index      :: Int
                  , r_aggregator :: DAgg
                  , r_result     :: DVar
                  , r_span       :: T.Span
-                 , r_anf        :: ANFState
+                 , r_annots     :: ANFAnnots
+                 , r_cruxes     :: S.Set (Crux DVar TBase)
                  }
  deriving (Show)
 
 normRule :: T.Spanned P.Rule   -- ^ Term to digest
-         -> Rule
-normRule (P.Rule i h a r dt T.:~ sp) = uncurry ($) $ runNormalize dt $ do
-    nh  <- normTerm False h >>= newAssign "_h" . Left
-    nr  <- normTerm True  r >>= newAssign "_r" . Left
-    return $ Rule i nh a nr sp
+         -> (Rule, ANFWarns)
+normRule (P.Rule i h a r dt T.:~ sp) = 
+  let (ru,s) = runNormalize dt $ do
+               nh  <- normTerm False h >>= newAssign "_h" . Left
+               nr  <- normTerm True  r >>= newAssign "_r" . Left
+               return $ Rule i nh a nr sp
+  in (ru (s^.as_annot) (s^.as_cruxes),s^.as_warns)
 
 ------------------------------------------------------------------------}}}
 -- Run the normalizer                                                   {{{
@@ -363,40 +414,20 @@ normRule (P.Rule i h a r dt T.:~ sp) = uncurry ($) $ runNormalize dt $ do
 runNormalize :: DisposTab
              -> ReaderT ANFDict (State ANFState) a -> (a, ANFState)
 runNormalize dt =
-  flip runState   (AS 0 M.empty M.empty [] M.empty []) .
+  flip runState   (AS 0 0 S.empty M.empty []) .
   flip runReaderT (AD dt)
 
 ------------------------------------------------------------------------}}}
--- Pretty Printer                                                       {{{
-
-printANF :: Rule -> Doc e
-printANF (Rule i h a result sp
-            (AS {as_evals = evals, as_assgn = assgn, as_unifs = unifs})) =
-          text ";;" <+> prettySpanLoc sp
-  `above`
-          text ";; index" <+> pretty i
-  `above`
-  ( parens $ (pretty a)
-            <+> valign [ (pretty h)
-                       , parens $ text "evals"  <+> pev
-                       , parens $ text "assign" <+> pas
-                       , parens $ text "unifs"  <+> pun
-                       , parens $ text "result" <+> (pretty result)
-                       ]
-  ) <> line
-  where
-    pft :: FDT -> Doc e
-    pft (fn,args)  = parens $ hsep $ (pretty fn : (map pretty args))
-
-    pe :: Pretty a => Either a FDT -> Doc e
-    pe = either pretty pft
-
-    pev = valign $ map (\(y,z)-> parens $ pretty y <+> pe z)
-                 $ M.toList evals
-
-    pas = valign $ map (\(y,z)-> parens $ pretty y <+> pe z)
-                       (M.toList assgn)
-    pun = valign $ map (\(y,z) -> parens $ pretty y <+> pretty z)
-                       unifs
+-- Placeholders XXX                                                     {{{
+
+-- XXX This is terrible and should be replaced with whatever type-checking
+-- work we do.
+findHeadFA :: DVar -> S.Set (Crux DVar TBase) -> Maybe DFunctAr
+findHeadFA h crs = MA.listToMaybe
+                 $ MA.mapMaybe m
+                 $ snd $ E.partitionEithers (S.toList crs)
+ where
+  m (CStruct o is f) | o == h = Just (f,length is)
+  m _                         = Nothing
 
 ------------------------------------------------------------------------}}}
diff --git a/src/Dyna/Analysis/ANFPretty.hs b/src/Dyna/Analysis/ANFPretty.hs
new file mode 100644
index 0000000..2d88e00
--- /dev/null
+++ b/src/Dyna/Analysis/ANFPretty.hs
@@ -0,0 +1,51 @@
+
+module Dyna.Analysis.ANFPretty (printANF) where
+
+import qualified Data.Either                as E
+import qualified Data.Set                   as S
+import           Dyna.Analysis.ANF
+import           Dyna.Term.Normalized
+import           Dyna.XXX.PPrint (valign)
+
+import           Text.PrettyPrint.Free
+import qualified Text.Trifecta              as T
+import           Dyna.XXX.Trifecta (prettySpanLoc)
+
+------------------------------------------------------------------------}}}
+-- Pretty Printer                                                       {{{
+
+printANF :: Rule -> Doc e
+printANF (Rule rix h a result sp _ cruxes) =
+          text ";;" <+> prettySpanLoc sp
+  `above`
+          text ";; index" <+> pretty rix
+  `above`
+  ( parens $ (pretty a)
+            <+> valign [ (pretty h)
+                       , parens $ text "evals"  <+> pevs
+                       , parens $ text "unifs"  <+> puns
+                       , parens $ text "result" <+> (pretty result)
+                       ]
+  ) <> line
+  where
+    (evals, unifs) = E.partitionEithers (S.elems cruxes)
+
+    pft :: FDT -> Doc e
+    pft (fn,args)     = hsep $ (pretty fn : (map pretty args))
+
+    pnft :: (Int,FDT) -> Doc e
+    pnft (n,(f,args))  = parens $ hsep $ (  pretty f <> char '@' <> pretty n 
+                                          : (map pretty args))
+
+    pev (CEval n o i)    = parens (pretty o <+> pretty i <> char '@' <> pretty n)
+    pev (CCall n o is f) = parens (pretty o <+> pnft (n,(f,is)))
+
+    pun (CStruct o is f) = parens (pretty o  <+> parens (pft (f,is)))
+    pun (CAssign o v   ) = parens (pretty o  <+> parens (equals   <+> pretty v))
+    pun (CEquals v1 v2 ) = parens (pretty v1 <+> parens (equals   <+> pretty v2))
+    pun (CNotEqu v1 v2 ) = parens (pretty v1 <+> parens (char '!' <+> pretty v2))
+
+    pevs = valign $ map pev evals
+    puns = valign $ map pun unifs
+
+------------------------------------------------------------------------}}}
diff --git a/src/Dyna/Analysis/ANFSelftest.hs b/src/Dyna/Analysis/ANFSelftest.hs
index 0d79bd2..c717098 100644
--- a/src/Dyna/Analysis/ANFSelftest.hs
+++ b/src/Dyna/Analysis/ANFSelftest.hs
@@ -22,16 +22,13 @@ import           Text.PrettyPrint.Free
 import           Dyna.Analysis.ANF
 import qualified Dyna.ParserHS.Parser         as P
 import           Dyna.ParserHS.Selftest
+import           Dyna.Term.Normalized
 import           Dyna.Term.TTerm
 import           Dyna.XXX.TrifectaTest
 
 
-testNormTerm :: Bool -> B.ByteString -> (NTV, ANFState)
-testNormTerm c = runNormalize . normTerm c . unsafeParse P.dterm
-
-testNormRule :: B.ByteString -> (FRule, ANFState)
-testNormRule = runNormalize . normRule . unsafeParse P.drule
-
+testNormRule :: B.ByteString -> Rule
+testNormRule = normRule . unsafeParse P.rawDRule
 
 {-
 e1 = testNormRule "f(X)."
diff --git a/src/Dyna/Analysis/Aggregation.hs b/src/Dyna/Analysis/Aggregation.hs
index 3c92691..e41159f 100644
--- a/src/Dyna/Analysis/Aggregation.hs
+++ b/src/Dyna/Analysis/Aggregation.hs
@@ -12,7 +12,9 @@ module Dyna.Analysis.Aggregation (
 ) where
 
 -- import qualified Data.ByteString            as B
+import qualified Data.Either                as E
 import qualified Data.Map                   as M
+import qualified Data.Set                   as S
 import           Dyna.Analysis.ANF
 import           Dyna.Main.Exception
 import           Dyna.Term.TTerm
@@ -29,18 +31,17 @@ type AggMap = M.Map DFunctAr DAgg
 -- Associate each item with an aggregator                               {{{
 
 procANF :: Rule -> (DFunctAr, DAgg)
-procANF r@(Rule _ h a _ sp (AS { as_assgn = as })) =
-  case M.lookup h as of
-    Nothing       -> dynacSorry $ "I can't process head-variables in rule at" <+> (prettySpanLoc sp)
-    Just t -> case t of
-                Left _       -> dynacPanic $ "Malformed head" <+> (pretty $ show r)
-                Right (f,xs) -> ((f,length xs),a)
+procANF r@(Rule _ h a _ sp _ crs) =
+  case findHeadFA h crs of
+    Nothing -> dynacSorry $ "The rule at" <+> (prettySpanLoc sp)
+                                          <+> "is beyond my abilities."
+    Just t  -> (t,a)
 
 buildAggMap :: [Rule] -> AggMap
 buildAggMap = go (M.empty)
  where
   go m []      = m
-  go m (ar@(Rule _ _ a _ sp _):xs) =
+  go m (ar@(Rule _ _ a _ sp _ _):xs) =
     let (d,a) = procANF ar
     in case mapUpsert d a m of
          Left a' -> dynacUserErr $     "Conflicting aggregators; rule"
diff --git a/src/Dyna/Analysis/RuleMode.hs b/src/Dyna/Analysis/RuleMode.hs
index 72aa29c..9747b1c 100644
--- a/src/Dyna/Analysis/RuleMode.hs
+++ b/src/Dyna/Analysis/RuleMode.hs
@@ -14,6 +14,7 @@
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# OPTIONS_GHC -Wall #-}
 
 module Dyna.Analysis.RuleMode {- (
     Mode(..), Moded(..), ModedNT, isBound, isFree,
@@ -32,7 +33,6 @@ module Dyna.Analysis.RuleMode {- (
     adornedQueries
 ) -} where
 
-import           Control.Lens ((^.))
 import           Control.Monad
 import           Control.Monad.Error.Class
 import           Control.Monad.Trans.Either
@@ -40,6 +40,7 @@ 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.List                  as L
 import qualified Data.Map                   as M
 import qualified Data.Maybe                 as MA
@@ -53,7 +54,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)
+import           Dyna.XXX.DataUtils(argmin,mapInOrApp,mapMinRepView)
 import           Dyna.XXX.MonadContext
 import           Dyna.XXX.Trifecta (prettySpanLoc)
 -- import           Dyna.XXX.TrifectaTest
@@ -85,47 +86,6 @@ modedNT b (NTVar  v)     = NTVar $ modedVar b v
 modedNT _ (NTBase b)     = NTBase b
 -}
 
-------------------------------------------------------------------------}}}
--- Cruxes                                                               {{{
-
-data EvalCrux v = CFCall v [v] DFunct
-                | CFEval v v
- deriving (Eq,Ord,Show)
-
-data UnifCrux v n = CFStruct v [v] DFunct
-                  | CFAssign v n
- deriving (Eq,Ord,Show)
-
-type Crux v n = Either (EvalCrux v) (UnifCrux v n)
-
-cruxIsEval :: Crux v n -> Bool
-cruxIsEval (Left _) = True
-cruxIsEval (Right _) = False
-
-{-
-cruxMode :: BindChart -> Crux DVar NTV -> Crux (ModedVar) (ModedNT)
-cruxMode c cr = either (Left . evalMode) (Right . unifMode) cr
- where
-  evalMode ec = case ec of
-    CFCall   o is f -> CFCall   (mv o) (map mv is) f
-    CFEval   o i    -> CFEval   (mv o) (mv i)
-  unifMode uc = case uc of
-    CFStruct o is f -> CFStruct (mv o) (map mv is) f
-    CFAssign o i    -> CFAssign (mv o) (modedNT c i)
-  mv = modedVar c
--}
-
-cruxVars :: Crux DVar NTV -> S.Set DVar
-cruxVars = either evalVars unifVars
- where
-  evalVars cr = case cr of
-    CFCall   o is        _ -> S.fromList (o:is)
-    CFEval   o i           -> S.fromList [o,i]
-  unifVars cr = case cr of
-    CFStruct o is        _ -> S.fromList (o:is)
-    CFAssign o (NTVar i)   -> S.fromList [o,i]
-    CFAssign o _           -> S.singleton o
-
 ------------------------------------------------------------------------}}}
 -- Actions                                                              {{{
 
@@ -133,6 +93,8 @@ type Actions fbs = [DOpAMine fbs]
 
 data BackendAction fbs = BAct
                           { bact_dop     :: Actions fbs
+
+                          -- XXX Does not support aliasing
                           , bact_outmode :: [(DVar,NIX DFunct)]
                           }
  deriving (Show)
@@ -186,30 +148,37 @@ fup v cf cu = do
 
 possible :: (Monad m)
          => BackendPossible fbs
-         -> Crux DVar NTV
+         -> Crux DVar TBase
          -> SIMCT m DFunct (Actions fbs)
 possible fp cr =
   case cr of
-      -- XXX Indirect evaluation is not yet supported
-    Left (CFEval _ _) -> dynacSorry "Indir eval"
-
-	-- XXX This is going to be such a pile.  We really, really should have
-	-- unification crank out a series of DOpAMine opcodes for us, but for
-	-- the moment, since everything we do is either IFree or IUniv, just use
-	-- iEq everywhere.
+    -- XXX This is going to be such a pile.  We really, really should have
+    -- unification crank out a series of DOpAMine opcodes for us, but for
+    -- the moment, since everything we do is either IFree or IUniv, just use
+    -- iEq everywhere.
 
     -- Assign or check
-    Right (CFAssign o i) ->
+    Right (CAssign o i) ->
+        fup o (runReaderT (unifyVU o) (UnifParams True False)
+                >> return [ OPAsgn o (NTBase i) ])
+              (let chk = "_chk" in return [ OPAsgn chk (NTBase i), OPCheq chk o])
+
+    Right (CEquals o i) ->
+       fup o (fup 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 i (NTVar o) ])
+                    (return [ OPCheq o i ]))
+
+{-
         case i of
           NTVar  v -> fup v (fup o (throwError UFExDomain)
-                                   (runReaderT (unifyVV v o) (UnifParams True False) >> return [ OPAsgn v (NTVar o) ]))
-                            (fup o (runReaderT (unifyVV v o) (UnifParams True False) >> return [ OPAsgn o i ])
-                               (return [ OPCheq o v ]))
-          NTBase b -> fup o (runReaderT (unifyVU o) (UnifParams True False) >> return [ OPAsgn o i ])
-                            (let chk = "_chk" in return [ OPAsgn chk i, OPCheq chk o])
+                                   
+-}
 
     -- Structure building or unbuilding
-    Right (CFStruct o is funct) -> fup o (mapM_ isBound is >> bind o >> return [ OPWrap o is funct ])
+    Right (CStruct o is funct) -> fup o (mapM_ isBound is >> bind o >> return [ OPWrap o is funct ])
                                          (buildPeel)
       where
        buildPeel = do
@@ -217,15 +186,24 @@ possible fp cr =
                     let cis = MA.catMaybes mcis
                     return ([ OPPeel is' o funct ] ++ map (uncurry OPCheq) cis)
 
-       newvars = map (\n -> BC.pack $ "_chk_" ++ (show n)) [0..]
+       newvars = map (\n -> BC.pack $ "_chk_" ++ (show n)) [0::Int ..]
 
        maybeCheck v nv = fup v (return (v,Nothing)) (return (nv, Just (nv,v)))
-                            
-    Left (CFCall vo vis funct) -> do
+
+    -- 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 ]))
+
+    -- XXX Indirect evaluation is not yet supported
+    Left (CEval _ _ _) -> dynacSorry "Indir eval"
+
+    -- Evaluation
+    Left (CCall _ vo vis funct) -> do
       is <- mapM mkMV vis 
       o  <- mkMV vo
       case fp (funct,is,o) of
-  		-- Not a built-in, so we assume that it can be iterated in full.
+          -- XXX Not a built-in, so we assume that it can be iterated in full.
         Left False      -> do mapM_ bind (vo:vis)
                               return [OPIter o is funct DetNon Nothing]
         Left True        -> throwError UFExDomain
@@ -246,6 +224,10 @@ possible fp cr =
 ------------------------------------------------------------------------}}}
 -- 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 } ) =
   S.unions [ M.foldWithKey (\k v s -> S.insert k (go1 v s)) S.empty evals
@@ -262,17 +244,18 @@ eval_cruxes :: ANFState -> [EvalCrux DVar]
 eval_cruxes = M.foldrWithKey (\o i -> (crux o i :)) [] . as_evals
  where
   crux :: DVar -> EVF -> EvalCrux DVar
-  crux o (Left v) = CFEval o v
-  crux o (Right (f,as)) = CFCall o as f
+  crux o (Left v) = CEval o v
+  crux o (Right (f,as)) = CCall o as f
 
 unif_cruxes :: ANFState -> [UnifCrux DVar NTV]
 unif_cruxes (AS { as_assgn = assigns, as_unifs = unifs }) =
      M.foldrWithKey (\o i -> (crux o i :)) [] assigns
-  ++ map (\(v1,v2) -> CFAssign v1 (NTVar v2)) unifs
+  ++ map (\(v1,v2) -> CAssign v1 (NTVar v2)) unifs
  where
   crux :: DVar -> EBF -> UnifCrux DVar NTV
-  crux o (Left  x)              = CFAssign o (NTBase x)
-  crux o (Right (f,as))         = CFStruct o as f
+  crux o (Left  x)              = CAssign o (NTBase x)
+  crux o (Right (f,as))         = CStruct o as f
+-}
 
 ------------------------------------------------------------------------}}}
 -- Costing Plans                                                        {{{
@@ -297,12 +280,15 @@ simpleCost (PP { pp_score = osc, pp_plan = pfx }) act =
     OPPeel _ _ _        -> 0
     OPWrap _ _ _        -> 1  -- Upweight building due to side-effects
                               -- in the intern table
-    OPIter o is _ d _   -> case d of
+    OPIter _ _ _ d _   -> case d of
+                             DetErroneous -> 0
+                             DetFailure   -> 0
                              Det     -> 0
                              DetSemi -> 1
                              DetNon  -> 2 {- ** (fromIntegral $ length $
                                               filter isFree (o:is))
                                         - 1 -}
+                             DetMulti -> 2
     OPIndr _ _          -> 100
 
   loops = fromIntegral . length . filter isLoop
@@ -339,10 +325,10 @@ simpleCost (PP { pp_score = osc, pp_plan = pfx }) act =
 -- 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 CFEval case??  We need to check every evaluation
--- inside a CFEval update?
+-- 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 NTV)
+data PartialPlan fbs = PP { pp_cruxes         :: S.Set (Crux DVar TBase)
                           , pp_binds          :: BindChart
                           , pp_restrictSearch :: Bool
                           , pp_score          :: Cost
@@ -350,30 +336,22 @@ data PartialPlan fbs = PP { pp_cruxes         :: S.Set (Crux DVar NTV)
                           }
 
 pp_liveVars :: PartialPlan fbs -> S.Set DVar
-pp_liveVars p = S.unions $ map lvs $ S.toList (pp_cruxes p)
- where
-  lvs (Left  (CFCall   v vs _))       = S.fromList (v:vs)
-  lvs (Left  (CFEval   v v'))         = S.fromList [v,v']
-  lvs (Right (CFStruct v vs _))       = S.fromList (v:vs)
-  lvs (Right (CFAssign v (NTVar v'))) = S.fromList [v,v']
-  lvs (Right (CFAssign v (NTBase _))) = S.singleton v
+pp_liveVars p = S.unions $ map cruxVars $ S.toList (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
 -- means that there's certainly no plan for the whole rule.
-stepPartialPlan :: (Crux DVar NTV -> SIMCT Identity DFunct (Actions fbs))
+stepPartialPlan :: (Crux DVar TBase -> SIMCT Identity DFunct (Actions fbs))
                 -- ^ Possible actions
                 -> (PartialPlan fbs -> Actions fbs -> Cost)
                 -- ^ Plan scoring function
-                -> Maybe (Maybe DFunctAr, DVar, DVar)
-                -- ^ The 'DFunctAr', intern representation, and
-                -- result variable of the
-                -- initial /evaluation/ crux, if any.  This is used to
-                -- avoid double-counting during updates.  See $dupcrux
                 -> PartialPlan fbs
                 -> Either (Cost, Actions fbs) [PartialPlan fbs]
-stepPartialPlan poss score mic p =
-  -- XT.traceShow ("SPP", mic, pp_binds p, pp_cruxes p) $
+stepPartialPlan poss score p =
+  {- XT.trace ("SPP:\n"
+             ++ "  " ++ show (pp_cruxes p) ++ "\n"
+             ++ "  " ++ show (pp_binds p) ++ "\n"
+           ) $ -}
   if S.null (pp_cruxes p)
    then Left $ (pp_score p, pp_plan p)
    else Right $
@@ -401,16 +379,17 @@ stepPartialPlan poss score mic p =
                       rc' = S.delete crux (pp_cruxes p)
                       r'  = (not $ cruxIsEval crux) || (pp_restrictSearch p)
                   in either (const ps)
-                            (\(act,bc') -> let act' = handleConflictors act
+                            (\(act,bc') -> let act' = {- handleConflictors -} act
                                            in PP rc' bc' r' (score p act') (pl ++ act')
                                               : ps)
                             plan
                 ) []
 
+{-
    handleConflictors =
      case mic of
        Nothing -> id
-       Just (mfa,i,ov) -> \p -> flip concatMap p (\dop ->
+       Just (mfa,i,ov) -> concatMap (\dop ->
          case dop of
            OPIter ov' ivs' f' _ _ |  
                 -- We must insert checks whenever this step involves
@@ -431,12 +410,13 @@ stepPartialPlan poss score mic p =
                    , OPCkne i cv
                    ]
            _ -> [dop])
+-}
 
-planner_ :: (Crux DVar NTV -> SIMCT Identity DFunct (Actions fbs))
+planner_ :: (Crux DVar TBase -> SIMCT Identity DFunct (Actions fbs))
          -- ^ Available steps
          -> (PartialPlan fbs -> Actions fbs -> Cost)
          -- ^ Scoring function
-         -> S.Set (Crux DVar NTV)
+         -> S.Set (Crux DVar TBase)
          -- ^ Cruxes to be planned over
          -> Maybe (EvalCrux DVar, DVar, DVar)
          -- ^ Maybe the updated evaluation crux, the interned
@@ -451,7 +431,8 @@ planner_ :: (Crux DVar NTV -> SIMCT Identity DFunct (Actions fbs))
          -- ^ Plans and their costs
 planner_ st sc cr mic bv fv = runAgenda
    $ PP { pp_cruxes = cr
-        , pp_binds  = SIMCtx $ M.fromSet (const $ VRStruct (IUniv UShared)) (S.unions [bv,bi])
+        , pp_binds  = SIMCtx $ M.fromSet (const $ VRStruct (IUniv UShared))
+                                         (S.unions [bv,bi])
                                `M.union`
                                M.fromSet (const $ VRStruct IFree) fv
         , pp_restrictSearch = False
@@ -459,78 +440,125 @@ planner_ st sc cr mic bv fv = runAgenda
         , pp_plan   = ip
         }
  where
-  runAgenda = go [] . (\x -> [x])
+  runAgenda = go . (flip mioaPlan M.empty)
    where
-    go [] []     = []
-    go (r:rs) [] = go rs r
-    go rs (p:ps) = case stepPartialPlan st sc mic' p of
-                     Left df -> df : (go rs ps)
-                     Right ps' -> go (ps':rs) ps
+    mioaPlan :: PartialPlan fbs
+             -> M.Map Cost [PartialPlan fbs]
+             -> M.Map Cost [PartialPlan fbs]
+    mioaPlan p@(PP{pp_score=psc}) = mapInOrApp psc p
 
-  -- XREF:INITPLAN
-  (ip,bi,mic') = case mic of
-                Nothing -> ([],S.empty,Nothing)
-                Just (CFCall o is f, hi, ho) -> ( [ OPPeel is hi f
-                                                  , OPAsgn o (NTVar ho)]
-                                                , S.fromList $ o:is
-                                                , Just (Just (f,length is),o,hi))
-                Just (CFEval o i, hi, ho) -> ( [ OPAsgn i (NTVar hi)
-                                               , OPAsgn o (NTVar ho)]
-                                             , S.fromList $ [o,i] 
-                                             , Just (Nothing,o,i))
-
-anfPlanner_ st sc anf mic bv = planner_ st sc cruxes mic bv
- where
-  cruxes =           S.fromList (map Right $ unif_cruxes anf)
-           `S.union` ( S.map Left
-                       $ maybe id (\(ic,_,_) -> S.delete ic) mic
-                       $ S.fromList $ eval_cruxes anf)
+    go pq = maybe [] go' $ mapMinRepView pq
+     where
+      go' (p, pq') = case stepPartialPlan st sc p of
+                       Left df -> df : (go pq')
+                       Right ps' -> go (foldr mioaPlan pq' ps')
 
+  -- XREF:INITPLAN
+  (ip,bi) = case mic of
+              Nothing -> ([],S.empty)
+              Just (CCall _ o is f, hi, ho) -> ( [ OPPeel is hi f
+                                                 , OPAsgn o (NTVar ho)]
+                                              , S.fromList $ o:is)
+              Just (CEval _ o i, hi, ho) -> ( [ OPAsgn i (NTVar hi)
+                                              , OPAsgn o (NTVar ho)]
+                                            , S.fromList $ [o,i] )
+
+-- | Pick the best plan, but stop the planner from going off the rails by
+-- considering at most a constant number of plans.
+--
+-- XXX This is probably not the right idea
 bestPlan :: [(Cost, a)] -> Maybe (Cost, a)
 bestPlan []    = Nothing
-bestPlan plans = Just $ argmin fst plans
+bestPlan plans = Just $ argmin fst (take 1000 plans)
 
+{-
 -- | Given a normalized form and, optionally, an initial crux,
 --   saturate the graph and get all the plans for doing so.
 --
 -- XXX This has no idea what to do about non-range-restricted rules.
 planUpdate_ :: BackendPossible fbs                         -- ^ Available steps
             -> (PartialPlan fbs -> Actions fbs -> Cost)    -- ^ Scoring function
-            -> ANFState                                    -- ^ Normal form
-            -> Maybe (EvalCrux DVar, DVar, DVar)           -- ^ Initial eval crux
+            -> S.Set (Crux DVar TBase)                     -- ^ Normal form
+            -> (EvalCrux DVar, DVar, DVar)                 -- ^ Initial eval crux
             -> S.Set DVar
             -> [(Cost, Actions fbs)]                       -- ^ If there's a plan...
-planUpdate_ bp sc anf mic fv = anfPlanner_ (possible bp) sc anf mic S.empty fv
+planUpdate_ bp sc anf mic fv = planner_ (possible bp) sc anf (Just mic) S.empty fv
+-}
 
 planUpdate :: BackendPossible fbs
            -> (PartialPlan fbs -> Actions fbs -> Cost)
-           -> ANFState
-           -> Maybe (EvalCrux DVar, DVar, DVar)
-            -> S.Set DVar
+           -> S.Set (Crux DVar TBase)                     -- ^ Normal form
+           -> (EvalCrux DVar, DVar, DVar)
+           -> S.Set DVar
            -> Maybe (Cost, Actions fbs)
 planUpdate bp sc anf mi fv =
-  bestPlan $ planUpdate_ bp sc anf mi fv
+  bestPlan $ planner_ (possible bp) sc anf (Just mi) S.empty fv
 
 planInitializer :: BackendPossible fbs -> Rule -> Maybe (Cost, Actions fbs)
-planInitializer bp (Rule { r_anf = anf }) =
-  planUpdate bp simpleCost anf Nothing (anfVars anf)
+planInitializer bp (Rule { r_cruxes = cruxes }) =
+  bestPlan $ planner_ (possible bp) simpleCost cruxes Nothing S.empty (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.
+handleDoubles :: (Ord a, Ord b)
+              => (Int -> a -> a -> a) 
+              -> EvalCrux a
+              -> S.Set (EvalCrux a)
+              -> S.Set (UnifCrux a b)
+handleDoubles vc e r = S.fold (go e) S.empty r
+ where
+  go (CEval en _ ei)      (CEval qn _ qi)      s =
+    if en > qn then s else S.insert (CNotEqu ei qi) s
+  go (CCall en eo eis ef) (CEval qn qo qi)     s =
+    if en > qn then s else let cv = vc 0 eo qo
+                            in S.insert (CStruct cv eis ef)
+                             $ S.insert (CNotEqu cv qi) s
+  go (CEval en eo ei)     (CCall qn qo qis qf) s =
+    if en > qn then s else let cv = vc 0 eo qo
+                            in S.insert (CStruct cv qis qf)
+                             $ S.insert (CNotEqu cv ei) s
+  go (CCall en eo eis ef) (CCall qn qo qis qf) s =
+    if en > qn || ef /= qf || length eis /= length qis
+     then s
+     else let ecv = vc 0 eo qo
+              qcv = vc 1 eo qo
+           in S.insert (CStruct ecv eis ef)
+            $ S.insert (CStruct qcv qis qf)
+            $ S.insert (CNotEqu ecv qcv) s
 
 planEachEval :: BackendPossible fbs     -- ^ The backend's primitive support
              -> (DFunctAr -> Bool)      -- ^ Indicator for constant function
              -> Rule
-             -> [(Maybe DFunctAr, Maybe (Cost, DVar, DVar, Actions fbs))]
-planEachEval bp cs r@(Rule { r_anf = anf })  =
-  map (\(mfa,cr) -> (mfa, varify $ planUpdate bp simpleCost anf (Just $ mic cr) (anfVars anf)))
+             -> [(Maybe DFunctAr, Int, Maybe (Cost, DVar, DVar, Actions fbs))]
+-- planEachEval _ _ _ = []
+planEachEval bp cs (Rule { r_cruxes = cruxes })  =
+  map (\(mfa,n,cr) ->
+         let cruxes' = S.union cruxes
+                               (S.map Right $ handleDoubles mkvar cr 
+                                                (S.delete cr $ S.fromList ecs))
+          in (mfa,n, varify $ planUpdate bp simpleCost
+                                       cruxes'
+                                       (mic cr)
+                                       (allCruxVars cruxes')))
     -- Filter out non-constant evaluations
+    --
+    -- XXX This instead should look at the update modes of each evaluation
   $ MA.mapMaybe (\ec -> case ec of
-                  CFCall _ is f | not (cs (f,length is))
-                                -> Just (Just (f,length is), ec)
-                  CFCall _ _  _ -> Nothing
-                  CFEval _ _    -> Just (Nothing,ec))
+                  CCall n _ is f | not (cs (f,length is))
+                                -> Just (Just (f,length is), n, ec)
+                  CCall _ _ _  _ -> Nothing
+                  CEval n _ _    -> Just (Nothing,n,ec))
 
     -- Grab all evaluations
-  $ eval_cruxes anf
+  $ ecs
  where
+  mkvar n v1 v2 = B.concat ["chk",v1,"_",v2,"_",BC.pack $ show n]
+
+  ecs = fst $ E.partitionEithers $ S.toList cruxes
+
     -- XXX I am not terribly happy about these, but it'll do for the moment.
     --
     -- If the mechanism of feeding updates into these plans is to change,
@@ -561,7 +589,7 @@ planBackchains bp (Rule { r_anf = anf, r_head = h })
 -- Update plan combination                                              {{{
 
 type UpdateEvalMap fbs = M.Map (Maybe DFunctAr)
-                               [(Rule, Cost, DVar, DVar, Actions fbs)]
+                               [(Rule, Int, Cost, DVar, DVar, Actions fbs)]
 
 -- | Return all plans for each functor/arity
 --
@@ -571,7 +599,7 @@ type UpdateEvalMap fbs = M.Map (Maybe DFunctAr)
 --
 -- timv: might want to fuse these into one circuit
 --
-combineUpdatePlans :: [(Rule,[( Maybe DFunctAr,
+combineUpdatePlans :: [(Rule,[( Maybe DFunctAr, Int,
                                 Maybe (Cost, DVar, DVar, Actions fbs))])]
                    -> UpdateEvalMap fbs  
 combineUpdatePlans = go (M.empty)
@@ -580,14 +608,14 @@ combineUpdatePlans = go (M.empty)
   go m ((fr,cmca):xs) = go' xs fr cmca m
 
   go' xs _  []           m = go m xs
-  go' xs fr ((fa,mca):ys) m =
+  go' xs fr ((fa,n,mca):ys) m =
     case mca of
       Nothing -> dynacUserErr
                        $ "No update plan for "
                           <+> group (pretty fa)
                           <+> "in rule at"
                           <+> (prettySpanLoc $ r_span fr)
-      Just (c,v1,v2,a) -> go' xs fr ys $ mapInOrApp fa (fr,c,v1,v2,a) m
+      Just (c,v1,v2,a) -> go' xs fr ys $ mapInOrApp fa (fr,n,c,v1,v2,a) m
 
 ------------------------------------------------------------------------}}}
 -- Backward chaining plan combination                                   {{{
@@ -657,7 +685,7 @@ ntMode _ (NTNumeric _) = MBound
 planEachEval_ hi v (Rule { r_anf = anf })  =
   map (\(c,fa) -> (fa, plan_ possible simpleCost anf $ Just (c,hi,v)))
     $ MA.mapMaybe (\c -> case c of
-                           CFCall _ is f | not $ isMath f
+                           CCall _ is f | not $ isMath f
                                          -> Just $ (c,(f,length is))
                            _             -> Nothing )
     $ eval_cruxes anf
diff --git a/src/Dyna/Backend/BackendDefn.hs b/src/Dyna/Backend/BackendDefn.hs
index ccb457b..cefb6d4 100644
--- a/src/Dyna/Backend/BackendDefn.hs
+++ b/src/Dyna/Backend/BackendDefn.hs
@@ -10,12 +10,11 @@ module Dyna.Backend.BackendDefn where
 import qualified Data.Set as S
 import           Dyna.Analysis.Aggregation (AggMap)
 import           Dyna.Analysis.ANF (Rule)
-import           Dyna.Analysis.DOpAMine (BackendRenderDopIter, ModedVar)
-import           Dyna.Analysis.Mode.Det
+import           Dyna.Analysis.DOpAMine (BackendRenderDopIter)
 import           Dyna.Analysis.RuleMode (
                     Actions, BackendPossible, Cost,
                     UpdateEvalMap {-, QueryEvalMap -})
-import           Dyna.Term.TTerm (DFunct, DFunctAr)
+import           Dyna.Term.TTerm (DFunctAr)
 import           System.IO (Handle)
 
 -- XXX The notion of be_constants is not quite right, I think?  It is used
diff --git a/src/Dyna/Backend/Backends.hs b/src/Dyna/Backend/Backends.hs
index 09fd6f8..8d71f9e 100644
--- a/src/Dyna/Backend/Backends.hs
+++ b/src/Dyna/Backend/Backends.hs
@@ -12,7 +12,7 @@ import           Data.Char
 import qualified Data.Map                     as M
 import           Dyna.Backend.BackendDefn
 import           Dyna.Backend.NoBackend
-import           Dyna.Backend.Python
+import           Dyna.Backend.Python.Backend
 import           Dyna.Main.Exception
 import           Text.PrettyPrint.Free        as PP
 
diff --git a/src/Dyna/Backend/Python.hs b/src/Dyna/Backend/Python/Backend.hs
similarity index 93%
rename from src/Dyna/Backend/Python.hs
rename to src/Dyna/Backend/Python/Backend.hs
index a1802cd..c5bdee3 100644
--- a/src/Dyna/Backend/Python.hs
+++ b/src/Dyna/Backend/Python/Backend.hs
@@ -9,7 +9,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE Rank2Types #-}
 
-module Dyna.Backend.Python (pythonBackend) where
+module Dyna.Backend.Python.Backend (pythonBackend) where
 
 import           Control.Applicative ((<*))
 import qualified Control.Arrow              as A
@@ -208,29 +208,21 @@ pdope _d _e =         (indent 4 $ "for _ in [None]:")
                  . go xs
 
 
-printPlanHeader :: Handle -> Rule -> Cost -> IO ()
-printPlanHeader h r c = do
+printPlanHeader :: Handle -> Rule -> Cost -> Maybe Int -> IO ()
+printPlanHeader h r c mn = do
   hPutStrLn h $ "# --"
     -- XXX This "prefixSD" thing is the only real reason we're doing this in
     -- IO; it'd be great if wl-pprint-extras understood how to prefix each
     -- line it was laying out.
   displayIO h $ prefixSD "# " $ renderPretty 1.0 100
                 $ (prettySpanLoc $ r_span r) <> line
+  hPutStrLn h $ "# EvalIx: " ++ (show mn)
   hPutStrLn h $ "# Cost: " ++ (show c)
 
--- XXX This is unforunate and wrong, but our ANF is not quite right to
--- let us do this right.  See also Dyna.Analysis.RuleMode's use of this
--- function.
-findHeadFA (Rule _ h _ _ _ (AS { as_assgn = as })) =
-  case M.lookup h as of
-    Nothing            -> error "No unification for head variable?"
-    Just (Left _)      -> error "NTVar head?"
-    Just (Right (f,a)) -> Just (f, length a)
-
 printInitializer :: Handle -> Rule -> Actions PyDopeBS -> IO ()
-printInitializer fh rule@(Rule _ h _ r _ _) dope = do
+printInitializer fh rule@(Rule _ h _ r _ _ cruxes) dope = do
   displayIO fh $ renderPretty 1.0 100
-                 $ "@initializer" <> parens (uncurry pfa $ MA.fromJust $ findHeadFA rule)
+                 $ "@initializer" <> parens (uncurry pfa $ MA.fromJust $ findHeadFA h cruxes)
                    `above` "def" <+> char '_' <> tupled [] <+> colon
                    `above` pdope dope emit
                    <> line
@@ -239,7 +231,7 @@ printInitializer fh rule@(Rule _ h _ r _ _) dope = do
 
 -- XXX INDIR EVAL
 printUpdate :: Handle -> Rule -> Maybe DFunctAr -> (DVar, DVar) -> Actions PyDopeBS -> IO ()
-printUpdate fh rule@(Rule _ h _ r _ _) (Just (f,a)) (hv,v) dope = do
+printUpdate fh rule@(Rule _ h _ r _ _ _) (Just (f,a)) (hv,v) dope = do
   displayIO fh $ renderPretty 1.0 100
                  $ "@register" <> parens (pfa f a)
                    `above` "def" <+> char '_' <> tupled (map pretty [hv,v]) <+> colon
@@ -267,14 +259,14 @@ driver am um {-qm-} is fh = do
   forM_ (M.toList um) $ \(fa, ps) -> do
      hPutStrLn fh ""
      hPutStrLn fh $ "# " ++ show fa
-     forM_ ps $ \(r,c,vi,vo,act) -> do
-       printPlanHeader fh r c
+     forM_ ps $ \(r,n,c,vi,vo,act) -> do
+       printPlanHeader fh r c (Just n)
        printUpdate fh r fa (vi,vo) act
 
   hPutStrLn fh ""
   hPutStrLn fh $ "# ==Initializers=="
   forM_ is $ \(r,c,a) -> do
-    printPlanHeader  fh r c
+    printPlanHeader  fh r c Nothing
     printInitializer fh r a
 
 {-
diff --git a/src/Dyna/Backend/Python/Selftest.hs b/src/Dyna/Backend/Python/Selftest.hs
index a6cde15..c35eb94 100644
--- a/src/Dyna/Backend/Python/Selftest.hs
+++ b/src/Dyna/Backend/Python/Selftest.hs
@@ -24,7 +24,11 @@ runDynaPy f out = do
 
   (Nothing,Nothing,Nothing,ph) <- createProcess $ CreateProcess
      { cmdspec = RawCommand "/usr/bin/env"
-                            ["python", "bin/interpreter.py", "-o", out, f]
+                            [ "python"
+                            , "src/Dyna/Backend/Python/interpreter.py"
+                            , "-o", out
+                            , f
+                            ]
      , cwd = Nothing
      , env = Nothing
      , std_in = UseHandle devnull
diff --git a/bin/prototype.py b/src/Dyna/Backend/Python/debug.py
similarity index 88%
rename from bin/prototype.py
rename to src/Dyna/Backend/Python/debug.py
index 5fa8a27..b1bd025 100644
--- a/bin/prototype.py
+++ b/src/Dyna/Backend/Python/debug.py
@@ -6,7 +6,7 @@ normalization process.
 
 import re, os
 from collections import defaultdict, namedtuple
-from utils import magenta, red, green, yellow, white, toANF, read_anf
+from utils import magenta, red, green, yellow, white, read_anf
 
 from pygments import highlight
 from pygments.lexers import get_lexer_by_name
@@ -154,17 +154,14 @@ def isvar(x):
 
 def circuit(anf):
 
-    (agg, head, evals, assigns, unifs, result) = anf
+    (agg, head, evals, unifs, result) = anf
 
     g = Hypergraph()
     for var, op, args in evals:
         g.edge(head=var, label=op, body=args)
 
-    for var, op, args in assigns:
-        g.edge(head=var, label='& %s' % op, body=args)
-
     for var, op, val in unifs:
-        g.edge(head=var, label='& ', body=[op])
+        g.edge(head=var, label='& %s' % op, body=val)
 
     g.head = head
     g.result = result
@@ -270,40 +267,46 @@ function selectline(lineno) {
         print >> html, '<div id="circuit-pane" style=""></div>'
         print >> html, '<div id="update-handler-pane" style=""></div>'
 
-        anf = toANF(code)
+        # XXX We do not yet render the dumped dopamine, but it's there...
+        cmd = """dist/build/dyna/dyna -B python \
+--dump-anf="%s"/anf \
+--dump-dopini="%s"/dopini \
+--dump-dopupd="%s"/dopupd \
+-o "%s"/plan "%s" """ % (d,d,d,d,dynafile)
+        if 0 != os.system(cmd):
+            print 'command failed:\n\t' + cmd
+            os.system('gnome-open %s 2>/dev/null >/dev/null' % html.name)
+            return
+
+        with file(d + '/anf') as f:
+            anf = f.read()
 
-        print >> html, '<div style="display:none;">'
+            print >> html, '<div style="display:none;">'
 
-        print >> html, '<h2>ANF</h2>'
-        print >> html, '<pre>\n%s\n</pre>' % anf.strip()
+            print >> html, '<h2>ANF</h2>'
+            print >> html, '<pre>\n%s\n</pre>' % anf.strip()
 
-        print >> html, '<h2>Hyperedge templates</h2>'
+            print >> html, '<h2>Hyperedge templates</h2>'
 
-        linenos = re.findall(';; (.*?):(\d+):\d+-.*?:(\d+):\d+', anf)
+            linenos = re.findall(';; (.*?):(\d+):\d+-.*?:(\d+):\d+', anf)
 
-        rules = [circuit(x) for x in read_anf(anf)]
+            rules = [circuit(x) for x in read_anf(anf)]
 
-        assert len(rules) == len(linenos), 'missing line number in ANF.'
+            assert len(rules) == len(linenos), 'missing line number in ANF.'
 
-        for (i, ((_, lineno, _), g)) in enumerate(zip(linenos, rules)):
-            sty = graph_styles(g)
-            svg = g.render(dynafile + '.d/rule-%s' % i, sty)
-            print >> html, '<div class="circuit-%s">%s</div>' % (lineno, svg)
+            for (i, ((_, lineno, _), g)) in enumerate(zip(linenos, rules)):
+                sty = graph_styles(g)
+                svg = g.render(dynafile + '.d/rule-%s' % i, sty)
+                print >> html, '<div class="circuit-%s">%s</div>' % (lineno, svg)
 
         # find "update plans" -- every term (edge) in a rule must have code to
         # handle an update to it's value.
 
         print >> html, '<h2>Update plans</h2>'
 
-        cmd = """dist/build/dyna/dyna -B python -o "%s".plan "%s" """ % (dynafile,dynafile)
-        if 0 != os.system(cmd):
-            print 'command failed:\n\t' + cmd
-            os.system('gnome-open %s 2>/dev/null >/dev/null' % html.name)
-            return
-
 #        print >> html, '<pre>'
 
-        with file(dynafile + '.plan') as f:
+        with file(d + '/plan') as f:
             code = f.read()
             print >> html, code
 
diff --git a/bin/defn.py b/src/Dyna/Backend/Python/defn.py
similarity index 100%
rename from bin/defn.py
rename to src/Dyna/Backend/Python/defn.py
diff --git a/bin/interpreter.py b/src/Dyna/Backend/Python/interpreter.py
similarity index 100%
rename from bin/interpreter.py
rename to src/Dyna/Backend/Python/interpreter.py
diff --git a/bin/utils.py b/src/Dyna/Backend/Python/utils.py
similarity index 75%
rename from bin/utils.py
rename to src/Dyna/Backend/Python/utils.py
index d8616eb..aa54339 100644
--- a/bin/utils.py
+++ b/src/Dyna/Backend/Python/utils.py
@@ -7,17 +7,6 @@ black, red, green, yellow, blue, magenta, cyan, white = \
     map('\033[3%sm%%s\033[0m'.__mod__, range(8))
 
 
-def toANF(code, f='/tmp/tmp.dyna'):
-    "Convert to ANF using Haskell implemention via system call."
-    with file(f, 'wb') as tmp:
-        tmp.write(code)
-    os.system('rm -f %s.anf' % f)  # clean up any existing ANF output
-    assert 0 == os.system("""dist/build/dyna/dyna --dump-anf="%s".anf --backend=none \"%s\" """ % (f,f)), \
-        'failed to convert file.'
-    with file('%s.anf' % f) as h:
-        return h.read()
-
-
 def parse_sexpr(e):
     """
     Parse a string representing an s-expressions into lists-of-lists.
@@ -62,10 +51,9 @@ def read_anf(e):
     def g(x):
         return list(_g(x))
 
-    for (agg, head, evals, assigns, unifs, [_,result]) in x:
+    for (agg, head, evals, unifs, [_,result]) in x:
         yield (agg,
                head,
                g(evals[1:]),
-               g(assigns[1:]),
                g(unifs[1:]),
                result)
diff --git a/src/Dyna/Main/Driver.hs b/src/Dyna/Main/Driver.hs
index 73a9e85..9847436 100644
--- a/src/Dyna/Main/Driver.hs
+++ b/src/Dyna/Main/Driver.hs
@@ -15,11 +15,13 @@ module Dyna.Main.Driver where
 import           Control.Applicative ((<*))
 import           Control.Exception
 -- import           Control.Monad
+import qualified Data.ByteString.UTF8         as BU
 import qualified Data.Map                     as M
 import qualified Data.Maybe                   as MA
 import qualified Data.Set                     as S
 import           Dyna.Analysis.Aggregation
 import           Dyna.Analysis.ANF
+import           Dyna.Analysis.ANFPretty
 import           Dyna.Analysis.DOpAMine
 import           Dyna.Analysis.RuleMode
 import           Dyna.Backend.BackendDefn
@@ -42,6 +44,7 @@ import qualified Text.Trifecta.Result         as TR
 
 data DumpType = DumpAgg
               | DumpANF
+              | DumpDopIni
               | DumpDopUpd
               | DumpParsed
  deriving (Eq,Ord,Show)
@@ -57,11 +60,11 @@ dump dt doc =
  where
   go h f = hPutDoc f $
     if h
-     then    header `above` doc <> line <> line
-          <> hcat (replicate 4 bar) <> line
+     then    header `above` doc <> line
+          <> hcat (replicate 8 bar) <> line
      else doc
 
-  header = bar <+> fill 18 (text $ show dt) <+> bar
+  header = bar <+> fill 58 (text $ show dt) <+> bar
   bar    = "=========="
 
 anyDumpStderr :: (?dcfg :: DynacConfig) => Bool
@@ -72,7 +75,8 @@ dumpOpts :: Bool -> [OptDescr Opt]
 dumpOpts nos =
      mkDumpOpt "agg"    DumpAgg     "Aggregator summary"
   ++ mkDumpOpt "anf"    DumpANF     "Administrative Normal Form"
-  ++ mkDumpOpt "dopupd" DumpDopUpd  "DOpAMine planning results"
+  ++ mkDumpOpt "dopini" DumpDopIni  "DOpAMine planning results: initializers"
+  ++ mkDumpOpt "dopupd" DumpDopUpd  "DOpAMine planning results: updates"
   ++ mkDumpOpt "parse"  DumpParsed  "Parser output"
  where
   mkDumpOpt arg fl hm =
@@ -191,17 +195,39 @@ procArgs argv = do
 ------------------------------------------------------------------------}}}
 -- Showing DOpAMine                                                     {{{
 
+renderDop :: BackendRenderDopIter bs e -> Actions bs -> Doc e
+renderDop ddi dop = vsep $ map (renderDOpAMine ddi) dop
+
 renderDopUpds :: BackendRenderDopIter bs e -> UpdateEvalMap bs -> Doc e
 renderDopUpds ddi um = vsep $ flip map (M.toList um) $ \(fa,ps) ->
-    pretty fa `above` indent 2 (vsep $ flip map ps $ \(r,c,vi,vo,act) ->
-        planHeader r c (vi,vo) `above` indent 2 (printUpdate act))
+    pretty fa `above` indent 2 (vsep $ flip map ps $ \(r,n,c,vi,vo,act) ->
+        planHeader r n c (vi,vo) `above` indent 2 (renderDop ddi act))
+ where
+  planHeader r n c (vi,vo) =
+        (prettySpanLoc $ r_span r)
+    <+> text "evalix=" <> pretty n
+    <+> text "cost="   <> pretty c
+    <+> text "in="     <> pretty vi
+    <+> text "out="    <> pretty vo
+
+renderDopInis :: BackendRenderDopIter bs e
+              -> [(Rule,Cost,Actions bs)]
+              -> Doc e
+renderDopInis ddi im = vsep $ flip map im $ \(r,c,ps) ->
+  iniHeader r c `above` indent 2 (renderDop ddi ps)
  where
-  planHeader r c (vi,vo) =
-    (prettySpanLoc $ r_span r) <+> text "cost=" <> pretty c <+>
-    text "in=" <> pretty vi <+> text "out=" <> pretty vo
+  iniHeader r c = 
+       ((prettySpanLoc $ r_span r)
+   <+> text "cost=" <> pretty c
+   <+> text "head=" <> pretty (r_head r)
+   <+> text "res=" <> pretty (r_result r))
 
-  printUpdate dop = vsep $ map (renderDOpAMine ddi) dop
+------------------------------------------------------------------------}}}
+-- Warnings                                                             {{{
 
+renderSpannedWarn :: BU.ByteString -> [T.Span] -> Doc e
+renderSpannedWarn w s = "WARNING:" <+> text (BU.toString w) <+> "AT"
+                        `above` indent 2 (vcat (map prettySpanLoc s))
 
 ------------------------------------------------------------------------}}}
 -- Pipeline!                                                            {{{
@@ -212,16 +238,21 @@ processFile fileName = bracket openOut hClose go
   openOut = maybe (return stdout) (flip openFile WriteMode)
             $ dcfg_outFile ?dcfg
 
+  maybeWarnANF [] = Nothing
+  maybeWarnANF xs = Just $ vcat $ map (uncurry renderSpannedWarn) xs
+
   go out = do
     rs <- parse
 
     dump DumpParsed (vcat $ map (text.show) rs)
    
     let urs = map (\(P.LRule x T.:~ _) -> x) rs
-        frs = map normRule urs
+        (frs, anfWarns) = unzip $ map normRule urs
 
     dump DumpANF (vcat $ map printANF frs)
 
+    hPutDoc stderr $ vcat $ MA.mapMaybe maybeWarnANF anfWarns
+
     aggm <- return $! buildAggMap frs
 
     dump DumpAgg (M.foldlWithKey (\d f a -> d `above`
@@ -247,6 +278,7 @@ processFile fileName = bracket openOut hClose go
 -}
 
         in do
+            dump DumpDopIni (renderDopInis be_ddi initializers)
             dump DumpDopUpd (renderDopUpds be_ddi cPlans)
             be_d aggm cPlans {- qPlans -} initializers out
 
@@ -276,9 +308,11 @@ main = catch (getArgs >>= main_) printerr
   pe (UserProgramError d) = do
     hPutStrLn stderr "FATAL: Encountered error in input program:"
     PP.hPutDoc stderr d
+    hPutStrLn stderr ""
   pe (UserProgramANSIError d) = do
     hPutStrLn stderr "FATAL: Encountered error in input program:"
     PPA.hPutDoc stderr d
+    hPutStrLn stderr ""
   pe (InvocationError d) = do
     hPutStrLn stderr "Invocation error:"
     PP.hPutDoc stderr d
@@ -287,10 +321,12 @@ main = catch (getArgs >>= main_) printerr
     hPutStrLn stderr "Terribly sorry, but you've hit an unsupported feature"
     taMsg
     PP.hPutDoc stderr d
+    hPutStrLn stderr ""
   pe (Panic d) = do
     hPutStrLn stderr "Compiler panic!"
     taMsg
     PP.hPutDoc stderr d
+    hPutStrLn stderr ""
 
   taMsg = do
     hPutStrLn stderr $ "This is almost assuredly not your fault!"
diff --git a/src/Dyna/XXX/DataUtils.hs b/src/Dyna/XXX/DataUtils.hs
index 42fdc8b..f8f18e8 100644
--- a/src/Dyna/XXX/DataUtils.hs
+++ b/src/Dyna/XXX/DataUtils.hs
@@ -9,8 +9,8 @@ module Dyna.XXX.DataUtils (
   mapExists, mapForall,
   -- ** Upsertion
   mapUpsert,
-  -- ** Insertion into a map of lists
-  mapInOrApp,
+  -- ** Maps of lists
+  mapInOrApp, mapMinRepView,
   -- ** Unification-style utilities
   mapSemiprune,
   -- ** Backports
@@ -55,7 +55,6 @@ 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.
 
@@ -66,6 +65,18 @@ mapInOrApp k v m = M.alter (\mv -> Just $ v:nel mv) k m
   nel Nothing  = []
   nel (Just x) = x
 
+-- | Remove an element of the minimum key
+--
+-- This lets us use Data.Map as a priority queue,
+-- using 'mapInOrApp' for insertion.
+mapMinRepView :: (Ord k)
+              => M.Map k [v] -> Maybe (v, M.Map k [v])
+mapMinRepView m = do
+  mv <- M.minViewWithKey m
+  case mv of
+    ((_,[]),m')   -> mapMinRepView m'
+    ((k,x:xs),m') -> return (x, M.insert k xs m')
+
 
 -- | For all those times one builds a map which may yield non-productive
 -- steps of variable-to-variable aliasing.  Note that this function may