From: Nathaniel Wesley Filardo <nwf@cs.jhu.edu>
Date: Tue, 13 Aug 2013 23:43:58 +0000 (-0400)
Subject: New automata library
X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=87aebf0ec453c394ee1a59fac4b96d20f8afaf49;p=dyna2

New automata library

Factor out all the automata logic from Analysis.Mode.Execution.NamedInst to
its own library (Dyna.Analysis.Automata) and port everything over.  I won't
claim it's perfect, but I think it's a good start.

Analysis.Automata.Class is probably the right place to start reading.
---

diff --git a/src/Dyna/Analysis/Automata/Class.hs b/src/Dyna/Analysis/Automata/Class.hs
new file mode 100644
index 0000000..fffb53d
--- /dev/null
+++ b/src/Dyna/Analysis/Automata/Class.hs
@@ -0,0 +1,165 @@
+---------------------------------------------------------------------------
+-- | Self-contained, recursive automata, parametric in ply functor.
+--
+-- Note that particular automata implementations (instances) may have an API
+-- that goes (well) beyond what's available here.  In particular, it is
+-- expected that non-trivial construction is beyond the scope of this common
+-- API.
+
+-- Header material                                                      {{{
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Dyna.Analysis.Automata.Class where
+
+import qualified Data.Traversable                  as T
+
+------------------------------------------------------------------------}}}
+-- Utility type definitions                                             {{{
+
+-- | An alias for universal quantification forcing a non-recursive ply of @f@:
+-- since there is no defined data of fully polymorphic type, any recursive
+-- positions in @f@ must not contain data.
+type NonRec f = forall x . f x
+
+------------------------------------------------------------------------}}}
+-- Basic class definition                                               {{{
+
+class Automata (a :: (* -> *) -> *) where
+  -- Construction
+
+  -- | An inverse (up to isomorphism) to 'autExpose'.
+  --
+  -- Note that this may not be efficient, so it should be used only as a
+  -- last resort.
+  autHide    :: (T.Traversable f) => f (a f) -> a f
+
+  -- | This is most frequently used as a base case in a lopsided
+  -- inductive step, in which one side is known to be acyclic, but the other
+  -- may be cyclic.  When we have reached the leaves of the former,
+  -- 'autShallow' will yield a trivial automata which may then be passed to
+  -- a binary automata function (e.g. 'autCmp') which will deal with cycles.
+  --
+  -- Parametricity ensures that this function has no access to any but the
+  -- top ply of its argument.
+  autShallow :: (T.Traversable f) => f x -> Maybe (a f)
+
+  -- Destruction
+
+  -- | Reveal the topmost ply of this automata.
+  --
+  -- Note that recursive use of this function may well diverge!
+  autExpose :: (Functor f) => a f -> f (a f)
+
+  -- Unary traversals
+
+  -- | Per-state rewriting function.  Callback will be called at most once
+  -- for each state of the automata, and at least once for all reachable
+  -- states, but there may be equivalent states within as well (but see
+  -- 'autMinimize').  The callback has visibility into the states reachable
+  -- from the current position within the automata, but no cycle-breaking is
+  -- performed by the machinery, so careless use of this ability may
+  -- diverge; an 'Ord' instance is asserted for the recursion sites to help
+  -- mitigate this situation.
+  autAtEachState :: forall f .
+                    (forall x . (Ord x) => (x -> f x) -> f x -> f x)
+                 -> a f -> a f
+
+  -- | (Indexed) algebraic reduction of an automaton.  Given a
+  -- cycle-breaking result (as a function of node identity)
+  -- and an algebraic interpretation of a single
+  -- state of the automaton (indexed, again, by node identity),
+  -- produce a result.
+  --
+  -- Note that cycles are only evaluated once: while a given spine is
+  -- active, all observations of that spine will yield the cycle-breaking
+  -- value; once a node is no longer on the active spine, observers will
+  -- observe its result.  Results of this function are only well-defined
+  -- if the callbacks are invariant to node visit order subject to this
+  -- observation constraint.
+  --
+  -- Note that one should not expect to be able to fully reconstruct the
+  -- automata given only the observations made by this function, as the
+  -- states may have meaning internal to automata (e.g. interpreted subject
+  -- to equality constraints or just as regular structure).
+  autReduceIx :: forall f r x .
+                 (T.Traversable f, Enum x, Ord x)
+              => (x -> r)
+              -> (x -> f r -> r)
+              -> a f -> r
+
+  -- | Non-indexed reduction.  See 'autReduceIx'.
+  --
+  -- This could be written in terms of 'autReduceIx', but this may be
+  -- more efficient by not having to map state names.
+  autReduce :: forall f r .
+               (T.Traversable f)
+            => r
+            -> (f r -> r)
+            -> a f -> r
+
+  -- Binary traversals
+  --
+  -- XXX Possibly these want to be split out to an AutBin class, enabling us
+  -- to specify more than just the diagonals in the space of automata?
+
+  -- | Binary reducer; see 'autReduce' for overview.
+  --
+  -- The HOF here is given three callbacks, for both "in-phase" and
+  -- "out-of-phase" work; the former allows simultaneous descent into two
+  -- states, while the others allow the merge to remain at a leaf state in
+  -- one automata while descending the other.
+  autBiReduce :: forall f r .
+                 (Ord (f ()))
+              => r
+              -> (forall x y m .
+                     (Monad m)
+                  => (x        -> NonRec f -> m r)
+                  -> (NonRec f -> y        -> m r)
+                  -> (x        -> y        -> m r)
+                  ->  f x      -> f y      -> m r)
+              -> a f -> a f -> r
+
+  -- | Total synchronous binary merge; @c@ records the type of top-down
+  -- context information needed for what is otherwise a bottom-up operation.
+  -- Since multiple paths may reach pairs of states, @c@ is used internally
+  -- as part of the index -- that is, a given pair of states may be
+  -- given to the callback repeatedly at differing @c@ values.
+  autMerge :: forall c f .
+              (Ord c, Ord (f ()))
+           => (forall x y . f x -> f y -> c)
+           -> (forall x y z m .
+                  (Monad m)
+               => (c -> x        -> NonRec f -> m z)
+               -> (c -> NonRec f -> y        -> m z)
+               -> (c -> x        -> y        -> m z)
+               ->  c -> f x      -> f y      -> m (f z))
+           -> a f -> a f -> a f
+
+
+  -- | Partial synchronous binary merge.
+  --
+  -- Note that the callbacks are total (monadic) functions: failure is
+  -- handled internally to @m@ and may short-circuit.
+  autPMerge :: forall c e f .
+               (Ord c, Ord (f ()))
+            => (forall x y . f x -> f y -> c)
+            -> (forall x y z m .
+                   (Monad m)
+                => (c -> x        -> NonRec f -> m z)
+                -> (c -> NonRec f -> y        -> m z)
+                -> (c -> x        -> y        -> m z)
+                ->  c -> f x      -> f y      -> m (Either e (f z)))
+            -> a f -> a f -> Either e (a f)
+
+------------------------------------------------------------------------}}}
+-- Minimization class definition                                        {{{
+
+class AutMinimize a where
+
+  -- | Automata minimization.
+  autMinimize :: (T.Traversable f, Ord (f Int)) => a f -> a f
+
+------------------------------------------------------------------------}}}
diff --git a/src/Dyna/Analysis/Automata/NamedAut.hs b/src/Dyna/Analysis/Automata/NamedAut.hs
new file mode 100644
index 0000000..f7147e1
--- /dev/null
+++ b/src/Dyna/Analysis/Automata/NamedAut.hs
@@ -0,0 +1,435 @@
+---------------------------------------------------------------------------
+-- | An implementation of our automata using existentially-quantified maps
+
+-- Header material                                                      {{{
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Dyna.Analysis.Automata.NamedAut(NA(NA), naUnfold, naFromMap) where
+
+import           Control.Applicative
+import           Control.Lens
+import           Control.Monad.Identity
+import           Control.Monad.Trans.Either
+import           Control.Monad.State
+import qualified Data.Foldable                     as F
+import qualified Data.Map                          as M
+import qualified Data.Maybe                        as MA
+import qualified Data.Set                          as S
+import qualified Data.Traversable                  as T
+import           Dyna.Analysis.Automata.Class
+import           Dyna.XXX.DataUtils (mapInOrCons)
+import           Dyna.XXX.MonadUtils (incState, tryMapCache, trySetCache)
+
+------------------------------------------------------------------------}}}
+-- Definition                                                           {{{
+
+data NA f = forall a . (Ord a) => NA a (M.Map a (f a))
+
+------------------------------------------------------------------------}}}
+-- Internal utilities                                                   {{{
+
+naImport :: (T.Traversable f, Ord k, Functor m, Monad m)
+         => m a
+         -> (a -> f a -> m ())
+         -> (k -> f k)
+         -> k
+         -> a
+         -> m ()
+naImport nxt ins look r ir = do
+  _ <- flip runStateT M.empty $ go r ir
+  return ()
+ where
+  go k a = T.traverse rec (look k) >>= lift . ins a
+  rec = tryMapCache id (\_ -> lift nxt) go
+
+naPrune :: forall f . (F.Foldable f) => NA f -> NA f
+naPrune (NA a0 m0) = (NA a0 m')
+ where
+  m' = execState (go a0) M.empty
+  go a = tryMapCache id (\_ -> return af) (\_ _ -> F.mapM_ go af) a
+   where af = MA.fromJust $ m0 ^. at a
+
+naRelabel_ :: (Ord a, Enum o)
+           => M.Map a x
+           -> M.Map a o
+naRelabel_ m = flip evalState (toEnum 0) $ T.traverse (\_ -> incState id) m
+
+-- | Convert from whatever internal representation we're using for states
+-- to Int.
+naExposeAll :: (Functor f, Enum o, Ord o) => NA f -> (o, M.Map o (f o))
+naExposeAll (NA a0 m0) = let labels = naRelabel_ m0
+                             relabel a = MA.fromJust $ labels ^. at a
+                         in  ( relabel a0
+                             , fmap (fmap relabel)
+                               $ M.mapKeysWith (error "NA relabel collision")
+                                               relabel m0)
+
+
+-- | Downcast away a forall.
+dc :: NonRec f -> f ()
+dc i = i
+
+------------------------------------------------------------------------}}}
+-- Unfolder                                                             {{{
+
+-- | Build an automata over the functor @f@ by unfolding.  @r@ carries
+-- top-down information flow, while the user-specified 'Monad' @m@ may carry
+-- sideways state (that is, information dependent upon the unfolding order).
+-- @ix@ provides the internal label for the state being unfolded so that it
+-- may be referenced later (/e.g./ by first being stored in @m@ or @r@).
+--
+-- As a convenience, the unfolder is allowed to supply an entire (isolated)
+-- automata in liu of recursively descending.
+naUnfold :: forall f ix m r .
+            (Enum ix, Ord ix, Functor m, Monad m, Traversable f)
+         => (forall t . (MonadTrans t, Monad (t m))
+              => r -> ix -> t m (Either (NA f) (f (Either ix r))))
+         -> r -> m (NA f)
+naUnfold uf = liftM (\(r,(_,m)) -> NA r m)
+            . flip runStateT (toEnum 0,M.empty) . visit
+ where
+  visit r = do
+   i <- nxt
+   f <- uf r i
+   case f of
+     Right f' -> do
+                 f'' <- T.mapM (either return visit) f'
+                 ins i f''
+     Left (NA r' m') -> naImport nxt ins (MA.fromJust . (m' ^.) . at) r' i
+   return i
+
+  nxt = incState _1
+  ins k v = _2 . at k .= Just v
+{-# INLINABLE naUnfold #-}
+
+{-
+-- | Build an automata over the functor @f@ by unfolding.  @t@ carries
+-- top-down information flow while @s@ carries sideways state (that is,
+-- information dependent upon the unfolding order).  @ix@ provides the
+-- internal label for the state being unfolded.
+--
+-- One might use @s@ to carry a (partial) map from @t@ to @ix@ values,
+-- either for tying cyclic knots or to avoid re-unfolding structure.  It may
+-- also be safe to ignore (just pass '()').
+naUnfold :: forall f ix m s t .
+            (Enum ix, Ord ix, Traversable f) =>
+            (t -> ix -> s -> (f (Either ix t), s))  -- ^ Unfolder step
+            -> t                                    -- ^ Initial root
+            -> s                                    -- ^ Initial flow state
+            -> NA f
+naUnfold uf t0 s0 = (\(r,(_,m,_)) -> NA r m)
+                  $ flip runState (toEnum 0, M.empty, s0)
+                  $ visit t0
+ where
+  visit t = do
+    i <- incState _1
+    (f,s') <- uses _3 (uf t i)
+    _3 .= s'
+    f' <- T.mapM (either return visit) f
+    _2 . at i .= Just f'
+    return i
+-}
+
+naFromMap :: forall f oix .
+             (T.Traversable f, Ord oix)
+          => M.Map oix (f oix) -> oix -> NA f
+naFromMap m0 a0 = flip evalState (M.empty :: M.Map oix Int) (naUnfold u a0)
+ where
+  u :: forall t m . (MonadTrans t, Monad (t m), MonadState (M.Map oix Int) m)
+    => oix -> Int -> t m (Either (NA f) (f (Either Int oix)))
+  u oix iix = do
+    lift (at oix .= Just iix)
+    liftM Right $ T.mapM relabel $ MA.fromJust (m0 ^. at oix)
+
+  relabel oix = lift (use (at oix)) >>= return . maybe (Right oix) (Left)
+{-# INLINABLE naFromMap #-}
+
+{-
+naFromAut :: forall a f x .
+             (Automata a, T.Traversable f, Enum x, Ord x)
+          => a f -> (x, M.Map x (f x))
+naFromAut = autReduceIx cyc rec
+ where
+  cyc x = (x,M.empty)
+  rec x fr = (x, M.insert x frx $ M.unions frms)
+   where
+   frx = fmap fst fr
+   frms = F.toList $ fmap snd fr
+{-# INLINABLE naFromAut #-}
+-}
+
+------------------------------------------------------------------------}}}
+-- Internal data types                                                  {{{
+
+data NBinState f c a b = NBS { _nbs_next  :: Int
+                             , _nbs_ctx   :: M.Map Int (f Int)
+                             , _nbs_cache_symm :: M.Map (c,a   ,b   ) Int
+                             , _nbs_cache_lsml :: M.Map (c,a   ,f ()) Int
+                             , _nbs_cache_lsmr :: M.Map (c,f (),b   ) Int
+                             }
+$(makeLenses ''NBinState)
+type NBSC m f c a b = (Monad m, MonadState (NBinState f c a b) m)
+
+iNBS :: forall (f :: * -> *) c a b. NBinState f c a b
+iNBS = NBS 0 M.empty M.empty M.empty M.empty
+
+data MinState a c = MS
+  { _ms_classes :: M.Map c [a]
+  , _ms_clinv   :: M.Map a c
+  }
+ deriving (Show)
+$(makeLenses ''MinState)
+
+data MinSplitState f a c = MSS
+  { _mss_newcl  :: M.Map (f c) [a] }
+ deriving (Show)
+$(makeLenses ''MinSplitState)
+
+------------------------------------------------------------------------}}}
+-- Automata instance                                                    {{{
+
+instance Automata NA where
+  autHide i0 = flip evalState (0::Int, M.empty) $ do
+    i0' <- T.traverse go i0
+    ra  <- nxt
+    ins ra i0'
+    rm  <- use _2
+    return (NA ra rm)
+   where
+    nxt = incState _1
+    ins k v = _2 . at k .= Just v
+
+    go (NA i' m') = do
+      i <- nxt
+      naImport nxt ins (MA.fromJust . (m' ^.) . at) i' i
+      return i
+
+  autShallow f = do
+    f' <- T.mapM (const mzero) f
+    return (NA () (M.fromList [((),f')]))
+  {-# INLINABLE autShallow #-}
+
+  autExpose (NA a0 m) = fmap (\a -> NA a m) $ MA.fromJust $ m ^. at a0
+  {-# INLINABLE autExpose #-}
+
+  autAtEachState q (NA a0 m0) = NA a0 (M.map q' m0)
+   where
+    q' = q (MA.fromJust . (m0 ^.) . at)
+  {-# INLINABLE autAtEachState #-}
+
+  autReduce cyc red (NA a0 m0) = evalState (q a0) M.empty
+   where
+    q a = do
+      _ <- tryMapCache id (\_ -> return cyc) miss a
+      liftM MA.fromJust $ use (at a)
+
+    miss a _ = do
+     fr <- T.mapM q (MA.fromJust $ m0 ^. at a)
+     let r = red fr
+     at a .= Just r
+  {-# INLINABLE autReduce #-}
+
+  autReduceIx cyc red (naExposeAll -> (a0,m0)) = evalState (q a0) M.empty
+   where
+    q a = do
+      _ <- tryMapCache id (return . cyc) miss a
+      liftM MA.fromJust $ use (at a)
+
+    miss a _ = do
+     fr <- T.mapM q (MA.fromJust $ m0 ^. at a)
+     let r = red a fr
+     at a .= Just r
+  {-# INLINABLE autReduceIx #-}
+
+  autBiReduce c q (NA la0 lm) (NA ra0 rm) =
+    evalState (qip la0 ra0) (S.empty, S.empty, S.empty)
+   where
+    qip l r = flip (trySetCache _1 c) (l,r) $ \_ -> do
+               let lf = MA.fromJust $ lm ^. at l
+               let rf = MA.fromJust $ rm ^. at r
+               q qopl qopr qip lf rf
+
+    qopl l r = flip (trySetCache _2 c) (l, dc r) $ \_ -> do
+                let lf = MA.fromJust $ lm ^. at l
+                q qopl qopr qip lf r
+
+    qopr l r = flip (trySetCache _3 c) (dc l, r) $ \_ -> do
+                let rf = MA.fromJust $ rm ^. at r
+                q qopl qopr qip l rf
+  {-# INLINABLE autBiReduce #-}
+
+  -- While unusual, we need this instance type declaration to introduce
+  -- scoped type variables for us to hold on to down below.  Oy!
+  autMerge :: forall c f .
+              (Ord c, Ord (f ()))
+           => (forall x y . f x -> f y -> c)
+           -> (forall x y z m .
+                  (Monad m)
+               => (c -> x        -> NonRec f -> m z)
+               -> (c -> NonRec f -> y        -> m z)
+               -> (c -> x        -> y        -> m z)
+               ->  c -> f x      -> f y      -> m (f z))
+           -> NA f -> NA f -> NA f
+  autMerge ci f (NA (la0 :: la) lm) (NA (ra0 :: ra) rm) = evalState tlq iNBS
+   where
+    f' :: NBSC m f c la ra => c -> f la -> f ra -> m (f Int)
+    f' = f lsml lsmr merge
+
+    tlq = do
+      let lf :: f la = MA.fromJust $ lm ^. at la0
+      let rf :: f ra = MA.fromJust $ rm ^. at ra0
+      let ic = ci lf rf
+      ma <- merge ic la0 ra0
+      mm <- use nbs_ctx
+      return (NA ma mm)
+
+    -- These two are here so that the skolems remain local to this
+    -- defintion.  It's a bit of a shame that the type system is
+    -- not willing to let these exist at higher scope.
+    nxt :: NBSC m f c la ra => m Int
+    nxt = incState nbs_next
+    ins k v = nbs_ctx . at k .= Just v
+
+    merge :: NBSC m f c la ra => c -> la -> ra -> m Int
+    merge c l r =
+      flip (tryMapCache nbs_cache_symm (\_ -> nxt)) (c,l,r) $ \_ a -> do
+        let lf = MA.fromJust $ lm ^. at l
+        let rf = MA.fromJust $ rm ^. at r
+        v <- f' c lf rf
+        ins a v
+
+    lsml :: NBSC m f c la ra => c -> la -> NonRec f -> m Int
+    lsml c l r =
+      flip (tryMapCache nbs_cache_lsml (\_ -> nxt)) (c,l,dc r) $ \_ a -> do
+        let lf = MA.fromJust $ lm ^. at l
+        v <- f' c lf r
+        ins a v
+
+    lsmr :: NBSC m f c la ra => c -> NonRec f -> ra -> m Int
+    lsmr c l r =
+      flip (tryMapCache nbs_cache_lsmr (\_ -> nxt)) (c,dc l,r) $ \_ a -> do
+        let rf = MA.fromJust $ rm ^. at r
+        v <- f' c l rf
+        ins a v
+  {-# INLINABLE autMerge #-}
+
+  autPMerge :: forall c e f .
+               (Ord c, Ord (f ()))
+            => (forall x y . f x -> f y -> c)
+            -> (forall x y z m .
+                   (Monad m)
+                => (c -> x        -> NonRec f -> m z)
+                -> (c -> NonRec f -> y        -> m z)
+                -> (c -> x        -> y        -> m z)
+                ->  c -> f x      -> f y      -> m (Either e (f z)))
+            -> NA f -> NA f -> Either e (NA f)
+  autPMerge ci f (NA (la0 :: la) lm) (NA (ra0 :: ra) rm) =
+    evalState (runEitherT tlq) iNBS
+   where
+    f' :: NBSC m f c la ra
+       => c -> f la -> f ra -> EitherT e m (Either e (f Int))
+    f' = f lsml lsmr merge
+
+    tlq = do
+      let lf :: f la = MA.fromJust $ lm ^. at la0
+      let rf :: f ra = MA.fromJust $ rm ^. at ra0
+      let ic = ci lf rf
+      ma <- merge ic la0 ra0
+      mm <- use nbs_ctx
+      return (NA ma mm)
+
+    -- These two are here so that the skolems remain local to this
+    -- defintion.  It's a bit of a shame that the type system is
+    -- not willing to let these exist at higher scope.
+    nxt :: NBSC m f c la ra => m Int
+    nxt = incState nbs_next
+    ins k v = nbs_ctx . at k .= Just v
+
+    merge :: NBSC m f c la ra => c -> la -> ra -> EitherT e m Int
+    merge c l r =
+      flip (tryMapCache nbs_cache_symm (\_ -> nxt)) (c,l,r) $ \_ a -> do
+        let lf = MA.fromJust $ lm ^. at l
+        let rf = MA.fromJust $ rm ^. at r
+        m <- f' c lf rf
+        v <- hoistEither m
+        ins a v
+
+    lsml :: NBSC m f c la ra => c -> la -> NonRec f -> EitherT e m Int
+    lsml c l r =
+      flip (tryMapCache nbs_cache_lsml (\_ -> nxt)) (c,l,dc r) $ \_ a -> do
+        let lf = MA.fromJust $ lm ^. at l
+        m <- f' c lf r
+        v <- hoistEither m
+        ins a v
+
+    lsmr :: NBSC m f c la ra => c -> NonRec f -> ra -> EitherT e m Int
+    lsmr c l r =
+      flip (tryMapCache nbs_cache_lsmr (\_ -> nxt)) (c,dc l,r) $ \_ a -> do
+        let rf = MA.fromJust $ rm ^. at r
+        m <- f' c l rf
+        v <- hoistEither m
+        ins a v
+  {-# INLINABLE autPMerge #-}
+
+------------------------------------------------------------------------}}}
+-- AutMinimize instance                                                 {{{
+
+instance AutMinimize NA where
+
+  autMinimize (naPrune -> NA a0 m0) =
+    let ms = classifyUntil m0 (MS M.empty M.empty)
+                              (mkClasses [M.keys m0])
+
+        msci = ms ^. ms_clinv
+
+        defn = \(a:_) -> fmap (\a' -> MA.fromJust $ msci ^. at a')
+                            $ MA.fromJust $ m0 ^. at a
+    in NA ((MA.fromJust $ msci ^. at a0) :: Int)
+          (fmap defn $ ms ^. ms_classes)
+
+   where
+
+    -- Attempt to partition a class in the equivalence relationship.  Evaluate
+    -- each contained state to see if they have become distinguished.
+    splitClasses :: forall f a c . (Ord c, Ord a, Traversable f, Ord (f c))
+                 => M.Map a (f a)
+                 -> MinState a c
+                 -> [[a]]
+    splitClasses im ms =
+        concat $ flip map (M.keys $ ms ^. ms_classes)
+      $ \c -> (M.elems . _mss_newcl) $ flip execState (MSS M.empty)
+      $ forM_ (MA.fromJust $ (ms ^. ms_classes) ^. at c)
+      $ \a -> do
+        -- Look up the definition of this state in the original automata
+        -- so that we can sort it into mss_newcl appropriately
+        let ia :: f c
+               = runIdentity
+                 $ traverse (pure . MA.fromJust . ((ms ^. ms_clinv) ^.) . at)
+                 $ (MA.fromJust $ im ^. at a :: f a)
+        mss_newcl %= mapInOrCons ia a
+
+    mkClasses :: (Ord a, Enum c, Ord c) => [[a]] -> MinState a c
+    mkClasses = uncurry MS . go (toEnum 0) M.empty M.empty
+     where
+      go _ mc mi []          = (mc,mi)
+      go c mc mi ([]:xs)     = c `seq` go (succ c) mc mi xs
+      go c mc mi ((a:as):xs) = go c (mapInOrCons c a mc) (M.insert a c mi) (as:xs)
+
+    classifyUntil :: forall a c f . (Ord a, Enum c, Ord c, Traversable f, Ord (f c))
+                  => M.Map a (f a) -> MinState a c -> MinState a c -> MinState a c
+    classifyUntil im p p' =
+      if M.size (p ^. ms_classes) == M.size (p' ^. ms_classes)
+       then p'
+       else classifyUntil im p' (mkClasses $ splitClasses im p')
+
+------------------------------------------------------------------------}}}
diff --git a/src/Dyna/Analysis/Automata/Utilities.hs b/src/Dyna/Analysis/Automata/Utilities.hs
new file mode 100644
index 0000000..28a93b3
--- /dev/null
+++ b/src/Dyna/Analysis/Automata/Utilities.hs
@@ -0,0 +1,41 @@
+---------------------------------------------------------------------------
+-- | Utilities for automata library
+
+-- Header material                                                      {{{
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Dyna.Analysis.Automata.Utilities where
+
+import           Control.Arrow (first)
+import           Control.Lens
+import           Control.Monad.State
+import qualified Data.Foldable                   as F
+import qualified Data.Traversable                as T
+import qualified Data.Map                        as M
+import qualified Data.Maybe                      as MA
+import           Dyna.Analysis.Automata.Class
+import           Dyna.Analysis.Automata.NamedAut
+import           Dyna.XXX.PPrint
+import           Text.PrettyPrint.Free
+
+------------------------------------------------------------------------}}}
+-- Pretty Printing                                                      {{{
+
+autRender :: (T.Traversable f, Automata a)
+          => (f (Doc e) -> Doc e)
+          -> a f -> Doc e
+autRender f a =
+  let (r, defs) = autReduceIx
+                    (\(x :: Int) -> (pan x, M.empty))
+                    (\x fr -> let r  = f $ fmap fst fr
+                                  ms = M.unions $ F.toList $ fmap snd fr
+                              in  (pan x, M.insert x r ms))
+                    a
+  in r <+> "where" <+> valign (map defrow $ M.toList defs)
+ where
+  pan = angles . pretty
+  defrow (k,v) = pan k <+> equals <+> v
+
+------------------------------------------------------------------------}}}
diff --git a/src/Dyna/Analysis/Mode/Execution/Context.hs b/src/Dyna/Analysis/Mode/Execution/Context.hs
index 807d1c8..10f4468 100644
--- a/src/Dyna/Analysis/Mode/Execution/Context.hs
+++ b/src/Dyna/Analysis/Mode/Execution/Context.hs
@@ -104,10 +104,11 @@ data KR f n k =
   | KRKey  k
  deriving (Eq,Ord,Show)
 
-instance (PP.Pretty f, PP.Pretty n, PP.Pretty k)
+instance (Show f, PP.Pretty n, PP.Pretty k)
       => PP.Pretty (KR f n k) where
   pretty (KRName n)   = PP.pretty n
-  pretty (KRStruct e) = IP.compactly PP.pretty (either PP.pretty PP.pretty) e
+  pretty (KRStruct e) = IP.compactly (PP.text . show)
+                                     (either PP.pretty PP.pretty) e
   pretty (KRKey k)    = PP.pretty k
 
 type KRI f n k = InstF f (Either n k)
@@ -131,10 +132,10 @@ data VR f n k =
   | VRKey    k
  deriving (Eq,Ord,Show)
 
-instance (PP.Pretty f, PP.Pretty n, PP.Pretty k)
+instance (Show f, PP.Pretty n, PP.Pretty k)
       => PP.Pretty (VR f n k) where
   pretty (VRName n)   = PP.pretty n
-  pretty (VRStruct y) = IP.compactly PP.pretty PP.pretty y
+  pretty (VRStruct y) = IP.compactly (PP.text . show) PP.pretty y
   pretty (VRKey k)    = PP.pretty k
 
 -- | Widen from a more restrictive to less restrictive recursion type.
@@ -169,7 +170,7 @@ 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
+instance (Show f, Ord f) => PP.Pretty (SIMCtx f) where
   pretty (SIMCtx _ km vm) =
     PP.vcat
     [ PP.text "Unaliased variables:"
diff --git a/src/Dyna/Analysis/Mode/Execution/ContextNoAlias.hs b/src/Dyna/Analysis/Mode/Execution/ContextNoAlias.hs
index 1d1f9cf..25f2473 100644
--- a/src/Dyna/Analysis/Mode/Execution/ContextNoAlias.hs
+++ b/src/Dyna/Analysis/Mode/Execution/ContextNoAlias.hs
@@ -72,9 +72,9 @@ data VR f n =
   | VRStruct (InstF f (VR f n))
  deriving (Eq,Ord,Show)
 
-instance (PP.Pretty f, PP.Pretty n) => PP.Pretty (VR f n) where
+instance (Show 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
+  pretty (VRStruct y) = IP.compactly (PP.text . show) PP.pretty y
 
 {-
 -- This is used during rule analysis to capture the state of the binding
@@ -108,7 +108,7 @@ 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
+instance (Show f, Ord f) => PP.Pretty (SIMCtx f) where
   pretty (SIMCtx vm) = PP.vcat
                      $ flip map (M.toAscList vm)
                      $ \(v,vr) ->        PP.pretty v
diff --git a/src/Dyna/Analysis/Mode/Execution/Functions.hs b/src/Dyna/Analysis/Mode/Execution/Functions.hs
index a1a1f3c..a90177a 100644
--- a/src/Dyna/Analysis/Mode/Execution/Functions.hs
+++ b/src/Dyna/Analysis/Mode/Execution/Functions.hs
@@ -72,17 +72,22 @@ expandV :: (ExpC m f n k, MCVT m DVar ~ VR f n k, MCR m DVar)
 expandV v = clookup v >>= \x ->
             case x of
               VRName n -> return n
-              VRStruct y -> expandY y
+              VRStruct _ -> expandX x
               VRKey k -> clookup k
-                         >>= either return (expandY . q2y)
+                         >>= either return (expandX . VRStruct . q2y)
  where
-  expandY y = nDeep rec y
+  expandX x = nDeep rec x
    where
-    rec (VRName n)    = return (Left n)
-    rec (VRStruct y') = return (Right y')
-    rec (VRKey k)     = do
-      e <- clookup k
-      either (return . Left) (return . Right . q2y) e
+    rec :: (MCR m k, MCVT m k ~ ENKRI f n k, MonadTrans t, Monad (t m))
+        => VR f n k
+        -> Int
+        -> t m (Either n (InstF f (Either a1 (VR f n k))))
+    rec (VRName n)    _ = return (Left n)
+    rec (VRStruct y') _ = return (Right $ fmap Right y')
+    rec (VRKey k)     _ = do
+      e <- lift (clookup k)
+      return $ either Left (Right . fmap Right . q2y) e
+
 
 ------------------------------------------------------------------------}}}
 -- Leq                                                                  {{{
diff --git a/src/Dyna/Analysis/Mode/Execution/FunctionsNoAlias.hs b/src/Dyna/Analysis/Mode/Execution/FunctionsNoAlias.hs
index 30786fd..72f8ee8 100644
--- a/src/Dyna/Analysis/Mode/Execution/FunctionsNoAlias.hs
+++ b/src/Dyna/Analysis/Mode/Execution/FunctionsNoAlias.hs
@@ -75,10 +75,14 @@ expandV :: (ExpC m f n, MCVT m DVar ~ VR f n, MCR m DVar)
         => DVar -> m n
 expandV v = clookup v >>= \x -> case x of
                                   VRName n -> return n
-                                  VRStruct y -> nDeep rec y
+                                  VRStruct _ -> nDeep rec x
  where
-  rec (VRName n)   = return (Left n)
-  rec (VRStruct y) = return (Right y)
+  rec :: (MonadTrans t, Monad (t m))
+      => VR f n
+      -> Int
+      -> t m (Either n (InstF f (Either a1 (VR f n))))
+  rec (VRName n)    _ = return (Left n)
+  rec (VRStruct y') _ = return (Right $ fmap Right y')
 
 ------------------------------------------------------------------------}}}
 -- Leq                                                                  {{{
diff --git a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs
index 694d7a4..189d9d4 100644
--- a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs
+++ b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs
@@ -1,9 +1,6 @@
 ---------------------------------------------------------------------------
--- | Self-contained, mu-recursive inst automata
---
--- XXX This could stand a good bit of refactoring out to being generic, but
--- I am writing it quickly in hopes of checking that it works before
--- investing too much more time.
+-- | Self-contained, mu-recursive inst automata, using the generic Automata
+-- framework.
 
 -- Header material                                                      {{{
 {-# LANGUAGE FlexibleContexts #-}
@@ -18,165 +15,93 @@
 
 module Dyna.Analysis.Mode.Execution.NamedInst (
     -- * Datatype definition
-    NIX(..), NIXM,
+    NIX(..),
     -- * Unary functions
     -- ** Well-formedness predicates
-    nWellFormedUniq, nWellFormedOC,
+    nWellFormedUniq,
     -- ** Inquiries
     nAllNotEmpty, nSomeNotEmpty, nGround,
     -- ** Construction
-    nHide, nShallow, nDeep,
+    nHide, nShallow, nDeep, nFromMap,
     -- ** Destruction
     nExpose, 
-    -- ** Internals
-    nPrune,
     -- ** Rewrites
-    nUpUniq,
+    nUpUniq, nMinimize,
+    -- ** Display
+    renderNIX,
     -- * Binary comparators
-    nCmp, nEq, nLeq, nSub,
+    nEq, nLeq, nSub,
     -- * Total binary functions
-    nTBin, nLeqGLB, nSubGLB,
+    nLeqGLB, nSubGLB,
     -- * Partial binary functions
-    nPBin, nLeqGLBRD, nLeqGLBRL, -- nSubLUB,
+    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.Identity
 import           Control.Monad.State
-import           Control.Monad.Trans.Either
 import qualified Data.Foldable                     as F
-import qualified Data.HashSet                      as H
 import qualified Data.Map                          as M
-import qualified Data.Set                          as S
 import qualified Data.Traversable                  as T
--- import qualified Debug.Trace                       as XT
+import           Dyna.Analysis.Automata.Class
+import           Dyna.Analysis.Automata.NamedAut
+import           Dyna.Analysis.Automata.Utilities
 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.Mem.StableName (makeStableName)
 import           Text.PrettyPrint.Free
 
 ------------------------------------------------------------------------}}}
 -- Datatype definition                                                  {{{
 
--- | Each named position in a NIX automata either references another
--- closed term or an InstF ply which itself recurses as labels in this
--- automata.
---
--- Note that we are contractually obligated to keep NIX automata mutually
--- acyclic (i.e. all cycles must be confied within some NIX automata).
-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,Show f) =>
-  NIX
-  {
-    -- | The top InstF ply in this term.
-    --
-    -- Note that while we could, in theory, have used @:: a@ here,
-    -- this would complicate the out-of-phase branch of comparison
-    -- operators.  Moreover, it's probably a good idea to use a ply
-    -- at the top as it forces NIX to be productive and not just
-    -- immediately alias another NIX via its map.
-    nix_root  :: InstF f a
-  , nix_map   :: NIXM a f
-  }
+newtype NIX f = NIX { unNIX :: NA (InstF 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) ++ "))"
-
 ------------------------------------------------------------------------}}}
--- Utilities                                                            {{{
-
--- | Throw exception if ever a NIX is not well formed
-panicwf :: NIX f -> a
-panicwf n = dynacPanic (text "NIX not well-formed"
-                        `above` indent 2 (renderNIX 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
--- used, for example, in cycle-breaking in backward chaining: we assume the
--- provability of our assumption and continue to look for a
--- counter-argument.  Note that this is rather the opposite of most circular
--- systems!
-tsc :: (Ord e, MonadState s m)
-    => Simple Lens s (S.Set e)
-    -> e
-    -> m Bool
-    -> m Bool
-tsc l e miss = (uses l $ S.member e)
-               `orM`
-               (l %= S.insert e >> miss)
-
--- | Either of Maybe of Lookup.  A common pattern found in implementation.
-eml :: (Ord k)
-    => NIX f -- ^ For debugging
-    -> (a -> c)
-    -> (b -> c)
-    -> M.Map k (Either a b)
-    -> k
-    -> c
-eml n al ar m x = either al ar (ml n m x)
-
--- | Our particular version of 'fromJust' which panics appropriately.
-ml :: (Ord k) => NIX f -> M.Map k b -> k -> b
-ml n m x = maybe (panicwf n) id (M.lookup x m)
+-- Pretty-printing                                                      {{{
 
-------------------------------------------------------------------------}}}
--- Pretty-printing core                                                 {{{
-
-renderNIX_ :: forall f e. (NIX f -> Doc e) -> NIX f -> Doc e
-renderNIX_ p (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 p ri v
-
-   ri = IP.compactly (text . show) rix
-
--- | Print out a NIX just as it is.  Notably, this is used by 'panicwf',
--- rather than the 'Pretty' instance, which, in order to be pretty, calls
--- 'nPrune'.
-renderNIX :: forall f e . NIX f -> Doc e
-renderNIX = fix renderNIX_
+-- | Render a NIX exactly as it stands (the 'Pretty' instance performs
+-- minimization first).
+renderNIX :: forall f e . (Show f) => NIX f -> Doc e
+renderNIX = autRender (IP.compactly (text.show) id) . unNIX
+
+-- | Pretty-printing minimizes automata first
+instance (Show f, Ord f) => Pretty (NIX f) where
+  pretty (nMinimize -> n) = renderNIX n
+
+instance (Show f, Ord f) => Show (NIX f) where
+  show = show . pretty
 
 ------------------------------------------------------------------------}}}
 -- Unary predicates                                                     {{{
 
+-- | Check well-formedness of an inst at a given Uniq.  All uniqueness
+-- annotations within the inst are required to be larger (i.e. less unique,
+-- more restrictive).
+
+-- XXX This formulation does not use iWellFormed_.
+-- XXX I'm not sure that it's correct, either.  It has just enough hacks
+-- that I am uncomfortable.
+nWellFormedUniq :: forall f . Uniq -> NIX f -> Bool
+nWellFormedUniq u0 (NIX n) =
+  case autReduce (Just UClobbered) go n of
+    Nothing -> False
+    Just u  -> u0 <= u
+ where
+  go fmu = let ufu = maybe UClobbered id $ iUniq fmu
+               mfu = T.sequence fmu
+           in mfu >>= \fu -> if ufu <= minimum (UClobbered : F.toList fu)
+                              then Just ufu
+                              else Nothing
+
+{-
 -- | Check well-formedness of an inst at a given Uniq.  All uniqueness
 -- annotations within the inst are required to be larger (i.e. less unique,
 -- more restrictive).
@@ -200,32 +125,8 @@ nWellFormedUniq u0 n0@(NIX i0 m) = evalState (iWellFormed_ q u0 i0)
            eml n0 (return . nWellFormedUniq u)
                   (iWellFormed_ q u)
                   m a
+-}
 
--- | Check that a named inst is acyclic.
---
--- Makes use of the 'StableName' functionality (and 'unsafePerformIO') to
--- ensure that the Haskell heap is acyclic.  This is likely useful for
--- 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 :: (Ord f) => NIX f -> IO ()
-nWellFormedOC n0 = evalStateT (go n0) H.empty
- where
-  mksp x = x `seq` makeStableName x
-
-  visit q i = F.mapM_ (F.mapM_ q) (i ^. inst_rec)
-
-  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 a = tsc id a
-            (eml n0 (lift . go) (visit q) m a >> return True)
 
 -- | Is a named inst ground?
 --
@@ -233,66 +134,42 @@ nWellFormedOC n0 = evalStateT (go n0) H.empty
 -- (see def 3.2.17, p52), which includes everything from UUnique to
 -- UClobbered.  This may not be what you mean.
 nGround :: forall f . NIX f -> Bool
-nGround n0@(NIX i0 m) = evalState (iGround_ q i0) S.empty
+nGround = autReduce True (runIdentity . iGround_ return) . unNIX
+
+nNotEmpty_ :: forall f .
+              ([Bool] -> Bool)
+           -> NIX f
+           -> Bool
+nNotEmpty_ disj = autReduce True (runIdentity . visit) . unNIX
  where
-  q a = tsc id a $ eml n0 (return . nGround) (iGround_ q) m a
+  visit IFree     = return True
+  visit (IUniv _) = return True
+  visit (IAny _)  = return True
+  visit (IBound _ m b) = return (disj (b:fmap and (F.toList m)))
+{-# INLINABLE nNotEmpty_ #-}
 
 -- | Is there some term not ruled out by this inst?
 --
 -- This is mostly useful for the test harness, not actual reasoning, at
 -- the moment, since we are not sufficiently precise (i.e. we will miss some
 -- empty unification results).
+--
+-- Note in particular for InstF, the only non-accepting states are
+-- @IBound _ mempty False@; all the others include some term.
 nSomeNotEmpty :: forall f . NIX f -> Bool
-nSomeNotEmpty = fix (nNotEmpty_core orAny)
- where orAny b bs = b `orM1` (anyM bs)
+nSomeNotEmpty = nNotEmpty_ or
+{-# INLINABLE nSomeNotEmpty #-}
 
--- | Like 'nNotEmpty' but conjunctive across choices -- that is, this
+-- | Like 'nSomeNotEmpty' but conjunctive across choices -- that is, this
 -- requires that all possible branches of an automata are non-empty, rather
--- than 'nNotEmpty', which only checks that there is some reachable state in
--- the automata.
-nAllNotEmpty :: forall f . (Show f) => NIX f -> Bool
-nAllNotEmpty = fix (nNotEmpty_core andAll)
- where andAll b bs = b `andM1` (allM bs)
-
-
-
-nNotEmpty_core :: forall f .
-                  (forall m .
-                     (Monad m)
-                  => Bool
-                  -> [m Bool]
-                  -> m Bool)
-               -> (NIX f -> Bool)
-               -> NIX f -> Bool
-nNotEmpty_core disj self n0@(NIX i0 m0) = evalState (visit i0) S.empty
- where
-  visit IFree     = return True
-  visit (IUniv _) = return True
-  visit (IAny _)  = return True
-  visit (IBound _ m b) = b `disj` (M.foldr (\fas a -> allM (map rec fas) : a) [] m)
-
-  rec idx = tsc id idx (eml n0 (return . self) visit m0 idx)
+-- than 'nSomeNotEmpty', which only checks that there is some input which
+-- is accepted by the automata.
+nAllNotEmpty :: forall f . NIX f -> Bool
+nAllNotEmpty = nNotEmpty_ and
+{-# INLINABLE nAllNotEmpty #-}
 
--- | Increase the nonuniqueness of a particular named inst to at least the
--- given level.
---
--- This would be equivalent to unification with 'IANy' at the given 'Uniq'
--- level, save that it leaves free variables untouched.
 nUpUniq :: forall f . (Ord f) => Uniq -> NIX f -> NIX f
-{-
- - XXX The beginnings of a possibly more efficient implementation
-nUpUniq u0 n0@(NIX i0 m) = uncurry NIX $ runState (T.traverse visit i0) m
- where
-  visit a = eml n0 (return . nUpUniq u0)
-                   (T.traverse visit (over inst_uniq (max u0)))
--}
-nUpUniq u0 n0@(NIX i0 m0) =
-   maybe n0 (\u' -> if u' >= u0 then n0 else NIX i0' m0') (iUniq i0)
- where
-  reuniq = over inst_uniq (max u0)
-
-  m0' = M.map (nUpUniq u0 A.+++ reuniq) m0
-  i0' = reuniq i0
+nUpUniq u0 = NIX . autAtEachState (\_ -> over inst_uniq (max u0)) . unNIX
 {-# INLINABLE nUpUniq #-}
 
 -- | Expose the root ply of a 'NIX' as an Inst which recurses as additional
@@ -300,298 +177,43 @@ nUpUniq u0 n0@(NIX i0 m0) =
 --
 -- 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
+nExpose = fmap NIX . autExpose . unNIX
 {-# INLINABLE nExpose #-}
 
--- | An inefficient \"inverse\" (up to isomorphism) of nExpose.
-nHide :: (Show f) => InstF f (NIX f) -> NIX f
-nHide i = uncurry NIX $ runState (T.mapM next i) M.empty
- where
-  next n = do
-    m <- get
-    let n' = M.size m
-    put (M.insert n' (Left n) m)
-    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
-{-# INLINABLE nShallow #-}
-
-nDeep :: (Show f, Monad m, Functor m)
-      => (r -> m (Either (NIX f) (InstF f r)))
-      -> InstF f r
-      -> m (NIX f)
-nDeep rec root = liftM (\(nr,(_,nm)) -> NIX nr nm) $
-  flip runStateT (0 :: Int, M.empty) $ inst_recps rec' root
- where
-  rec' r = do
-    a  <- _1 <<%= (+(1 :: Int))
-    rhs <- lift (rec r)
-    rhs' <- either (return . Left) (liftM Right . inst_recps rec') rhs
-    _2 %= M.insert a rhs'
-    return a
+nHide :: InstF f (NIX f) -> NIX f
+nHide = NIX . autHide . fmap unNIX
+{-# INLinABLE nHide #-}
 
+nShallow :: (Show f) => InstF f x -> Maybe (NIX f)
+nShallow = fmap NIX . autShallow
+{-# INLINABLE nShallow #-}
 
+nDeep :: (Functor m, Monad m, Enum ix, Ord ix)
+      => (forall t . (MonadTrans t, Monad (t m))
+           => r -> ix -> t m (Either (NIX f) (InstF f (Either ix r))))
+      -> r -> m (NIX f)
+nDeep f r = liftM NIX $ naUnfold (\r' ix' -> liftM (left' unNIX) $ f r' ix') r
+{-# INLINABLE nDeep #-}
+
+nFromMap :: forall f oix.
+            Ord oix
+         => M.Map oix (InstF f oix) -- ^ recursion table
+         -> oix                     -- ^ root
+         -> NIX f
+nFromMap m r = NIX (naFromMap m r)
+{-# INLINABLE nFromMap #-}
 
 ------------------------------------------------------------------------}}}
 -- Binary predicates                                                    {{{
 
-nCmp :: forall f .
-        (Ord f)
-     => (forall a b m .
-            (Monad m)
-         => (a -> (forall i_ . InstF f i_) -> m Bool)
-         -> (a -> b -> m Bool)
-         -> InstF f a -> InstF f b -> m Bool)
-     -> NIX f -> NIX f -> Bool
-nCmp q l0@(NIX li0 lm) r0@(NIX ri0 rm) =
-  evalState (q qop qip li0 ri0) (S.empty, S.empty)
- where
-  -- Q In Phase
-  qip l r  = -- XT.traceShow ("NCMP QIP",l,r) $
-             tsc _1 (l,r) $ do
-               eli <- maybe (panicwf l0) return $ M.lookup l lm
-               eri <- maybe (panicwf r0) return $ M.lookup r rm
-               case (eli,eri) of
-                 (Left  l', Left  r') -> return $ nCmp q l' r'
-                 (Left  l', Right r') -> return $ nCmp q l' (NIX r' rm)
-                 (Right l', Left  r') -> return $ nCmp q (NIX l' lm) r'
-                 (Right l', Right r') -> q qop qip l' r'
-
-  -- Q Out of Phase
-  qop l ri = -- XT.traceShow ("NCMP QOP",l,ri) $
-             tsc _2 (l,downcast ri)
-               $ eml l0 (return . flip (nCmp q) (NIX ri rm))
-                        (flip (q qop qip) ri)
-                        lm l
-
-  downcast :: (forall i_ . InstF f i_) -> InstF f ()
-  downcast i = i
-
 nEq, nLeq, nSub :: (Ord f) => NIX f -> NIX f -> Bool
-nEq  = nCmp (\_ -> iEq_)
-nLeq = nCmp iLeq_
-nSub = nCmp iSub_
+nEq (NIX l) (NIX r) = autBiReduce True (\_ _ -> iEq_) l r
+nLeq (NIX l) (NIX r) = autBiReduce True (\x _ -> iLeq_ x) l r
+nSub (NIX l) (NIX r) = autBiReduce True (\x _ -> iSub_ x) l r
 
 ------------------------------------------------------------------------}}}
 -- Binary functions                                                     {{{
 
-data NBinState a b f u = NBS { _nbs_next  :: Int
-                           , _nbs_ctx   :: NIXM Int f
-                           , _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 u
-iNBS = NBS 0 M.empty M.empty M.empty M.empty
-
-
-nTBin :: forall f . (Ord f, Show f)
-      => (  forall a b c m .
-            (Monad m)
-         => (Uniq -> a -> m c)
-         -> (Uniq -> b -> m c)
-         -> (Uniq -> (forall i_ . InstF f i_) -> a -> m c)
-         -> (Uniq -> (forall i_ . InstF f i_) -> b -> m c)
-         -> (Uniq -> a -> b -> m c)
-         -> Uniq
-         -> InstF f a -> InstF f b -> m (InstF f c))
-      -> NIX f -> NIX f -> NIX f
-nTBin f l0@(NIX li0 lm) r0@(NIX ri0 rm) = evalState (tlq li0 ri0) iNBS
- where
-  tlq l r = do
-    ci <- f' S.empty UUnique l r
-    ctx <- use nbs_ctx
-    return $ nPrune $ NIX ci ctx
-
-  f' sc = f (imp l0 lm) (imp r0 rm) (lsml sc) (lsmr sc) (merge sc)
-
-  -- XXX import needs some caching, too.
-
-  -- Occasionally, we need to "import" a term from one of the two inputs;
-  -- this happens when we unify 'IBound' against 'IAny' or 'IUniv', for
-  -- example.
-  --
-  -- To import the key x from the map m into our context,
-  --   if it is a closed term, just return that
-  --   otherwise, make it a closed term whose root is x and whose map is m
-  imp n m u x = 
-     -- XT.traceShow ("NTB I",u,m,x)
-     eml n return (return . flip NIX m) m x >>= new . Left . nUpUniq u 
-
-  new  x = do
-    k <- nbs_next <<%= (+1)
-    nbs_ctx %= M.insert k x
-    return k
-
-  lsml sc u ir l = -- XT.traceShow ("NTB L",u,ir,l) $
-                   do
-    cached <- uses nbs_cache_lsml $ M.lookup (u,ir,l)
-    maybe merge' return cached
-   where
-    merge' = do
-      k <- nbs_next <<%= (+1)
-      nbs_cache_lsml %= M.insert (u,ir,l) k
-      v <- eml r0
-               (return . luu u . nTBin f (NIX ir rm))
-               (\l' -> Right . over inst_uniq (max u) <$> f' (S.insert k sc) u l' ir)
-               lm l
-      nbs_ctx %= M.insert k v
-      return k
-  
-  lsmr sc u il r = -- XT.traceShow ("NTB R",u,il,r) $
-                   do
-    cached <- uses nbs_cache_lsmr $ M.lookup (u,il,r)
-    maybe merge' return cached
-   where
-    merge' = do
-      k <- nbs_next <<%= (+1)
-      nbs_cache_lsmr %= M.insert (u,il,r) k
-      v <- eml r0
-               (return . luu u . nTBin f (NIX il lm))
-               (\r' -> Right . over inst_uniq (max u) <$> f' (S.insert k sc) u il r')
-               rm r
-      nbs_ctx %= M.insert k v
-      return k
-
-  luu u = Left . nUpUniq u
-
-  merge sc u l r = -- XT.traceShow ("NTB M",u,l,r) $
-                   do
-    cached <- uses nbs_cache_symm $ M.lookup (u,l,r)
-    maybe merge' return cached
-   where
-    merge' = do
-      k <- nbs_next <<%= (+1)
-      nbs_cache_symm %= M.insert (u,l,r) k
-      eli <- maybe (panicwf l0) return $ M.lookup l lm
-      eri <- maybe (panicwf r0) return $ M.lookup r rm
-      v <- case (eli,eri) of
-             (Left  l', Left  r') -> return $ luu u $ nTBin f l' r'
-             (Left  l', Right r') -> return $ luu u $ nTBin f l' (NIX r' rm)
-             (Right l', Left  r') -> return $ luu u $ nTBin f (NIX l' lm) r'
-             (Right l', Right r') -> Right . over inst_uniq (max u)
-                                     <$> f' (S.insert k sc) u l' r'
-      nbs_ctx %= M.insert k v
-      return k
-
--- | Total lattice functions
-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))
-
-nPBin :: forall e f .
-         (Ord f, Show f)
-      => (  forall a b c m .
-            (Monad m, Show a, Show b, Show c)
-         => (Uniq -> a -> m c)
-         -> (Uniq -> b -> m c)
-         -> (Uniq -> (forall i_ . InstF f i_) -> a -> m c)
-         -> (Uniq -> (forall i_ . InstF f i_) -> b -> m c)
-         -> (Uniq -> a -> b -> m c)
-         -> Uniq
-         -> InstF f a -> InstF f b -> m (Either e (InstF f c)))
-      -> NIX f -> NIX f -> Either e (NIX f)
-nPBin f l0@(NIX li0 lm) r0@(NIX ri0 rm) = evalState (runEitherT (tlq li0 ri0)) iNBS
- where
-  tlq l r = do
-    ci <- f' S.empty UUnique l r
-    ci' <- hoistEither ci
-    ctx <- use nbs_ctx
-    return $ nPrune $ NIX ci' ctx
-
-  f' sc = f (imp l0 lm) (imp r0 rm) (lsml sc) (lsmr sc) (merge sc)
-
-  luu u = Left . nUpUniq u
-  mluu u r = luu u <$> hoistEither r
-
-  -- Occasionally, we need to "import" a term from one of the two inputs;
-  -- this happens when we unify 'IBound' against 'IAny' or 'IUniv', for
-  -- example.
-  --
-  -- To import the key x from the map m into our context,
-  --   if it is a closed term, just return that
-  --   otherwise, make it a closed term whose root is x and whose map is m
-  imp n m u x = {- XT.traceShow ("NPB I",m,u,x) $ -}
-    new . luu u =<< eml n return (return . flip NIX m) m x
-
-  new  x = do
-    k <- nbs_next <<%= (+1)
-    nbs_ctx %= M.insert k x
-    return k
-
-  lsml sc u ir l = {- XT.traceShow ("NPB L",u,ir,l) $ -}
-                   do
-    cached <- uses nbs_cache_lsml $ M.lookup (u,ir,l)
-    maybe merge' return cached
-   where
-    merge' = do
-      k <- nbs_next <<%= (+1)
-      nbs_cache_lsml %= M.insert (u,ir,l) k
-      v <- eml r0
-               (mluu u . nPBin f (NIX ir rm))
-               (\l' -> do
-                  l'' <- f' (S.insert k sc) u l' ir
-                  (Right . over inst_uniq (max u)) <$> hoistEither l'')
-               lm l
-      nbs_ctx %= M.insert k v
-      return k
-  
-  lsmr sc u il r = {- XT.traceShow ("NPB R",u,il,r) $ -}
-                   do
-    cached <- uses nbs_cache_lsmr $ M.lookup (u,il,r)
-    maybe merge' return cached
-   where
-    merge' = do
-      k <- nbs_next <<%= (+1)
-      nbs_cache_lsmr %= M.insert (u,il,r) k
-      v <- eml r0
-               (mluu u . nPBin f (NIX il lm))
-               (\r' -> do
-                  r'' <- f' (S.insert k sc) u il r'
-                  (Right . over inst_uniq (max u)) <$> hoistEither r'')
-               rm r
-      nbs_ctx %= M.insert k v
-      return k
-
-
-  merge sc u l r = {- XT.traceShow ("NPB M",u,l,r) $ -}
-                   do
-    cached <- uses nbs_cache_symm $ M.lookup (u,l,r)
-    maybe merge' return cached
-   where
-    merge' = do
-      k <- nbs_next <<%= (+1)
-      nbs_cache_symm %= M.insert (u,l,r) k
-      eli <- maybe (panicwf l0) return $ M.lookup l lm
-      eri <- maybe (panicwf r0) return $ M.lookup r rm
-      v <- case (eli,eri) of
-             (Left  l', Left  r') -> mluu u $ nPBin f l' r'
-             (Left  l', Right r') -> mluu u $ nPBin f l' (NIX r' rm)
-             (Right l', Left  r') -> mluu u $ nPBin f (NIX l' lm) r'
-             (Right l', Right r') -> do
-                                      m' <- f' (S.insert k sc) u l' r'
-                                      (Right . over inst_uniq (max u))
-                                         <$> hoistEither m'
-      nbs_ctx %= M.insert k v
-      return k
-
--- | 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 = nPBin iLeqGLBRD_
-nLeqGLBRL = nPBin iLeqGLBRL_
-
 {-
 
 XXX BITROTTED; NOT YET -- need better understanding of the problem.  The ⊔
@@ -599,11 +221,45 @@ function is particularly interesting and it is not yet clear how to define
 its recursion in a way that is not painfully special-cased.  At this instant
 I have other things that can demand attention.
 
-
 nSubLUB :: forall f . (Ord f, Show f) => NIX f -> NIX f -> Maybe (NIX f)
 nSubLUB = nPBin (\il ir ll lr m -> iSubLUB_ il ir (ll UClobbered) (lr UClobbered) (m UClobbered))
 -}
 
+ctxUniq :: InstF f a -> InstF f' a' -> Uniq
+ctxUniq x y = u x `max` u y
+ where
+  u = maybe UUnique id . iUniq
+
+-- XXX This may suggest that we could eliminate the "import" callbacks on
+-- iLeqGLB_ and friends now that we're not doing anything special with them.
+
+bendImpl :: forall f i i' i'' m r .
+            TyILeqGLB_ f m i i' i'' r
+         -> (Uniq -> i -> NonRec (InstF f)  -> m i'')
+         -> (Uniq -> NonRec (InstF f) -> i' -> m i'')
+         -> (Uniq -> i -> i' -> m i'')
+         -> Uniq -> InstF f i -> InstF f i' -> r
+bendImpl x lsml lsmr merge = x impl impr lsml' lsmr merge
+   where
+    lsml' :: Uniq -> NonRec (InstF f) -> i -> m i''
+    lsml' u r l = lsml u l r
+
+    impl :: Uniq -> i -> m i''
+    impl u l = lsml u l IFree
+
+    impr :: Uniq -> i' -> m i''
+    impr u r = lsmr u IFree r
+
+nLeqGLB, nSubGLB :: forall f . (Ord f) => NIX f -> NIX f -> NIX f
+nLeqGLB (NIX l) (NIX r) = NIX $ autMerge ctxUniq (bendImpl iLeqGLB_) l r
+nSubGLB (NIX l) (NIX r) = NIX $ autMerge (\_ _ -> ()) go l r
+ where
+  go lsml lsmr merge () = iSubGLB_ (flip (lsml ())) (lsmr ()) (merge ())
+
+nLeqGLBRD, nLeqGLBRL :: (Ord f) => NIX f -> NIX f -> Either UnifFail (NIX f)
+nLeqGLBRD (NIX l) (NIX r) = fmap NIX $ autPMerge ctxUniq (bendImpl iLeqGLBRD_) l r
+nLeqGLBRL (NIX l) (NIX r) = fmap NIX $ autPMerge ctxUniq (bendImpl iLeqGLBRL_) l r
+
 ------------------------------------------------------------------------}}}
 -- Mode functions                                                       {{{
 
@@ -624,41 +280,7 @@ mWellFormed (QMode ats vm@(vti,vto) _) =
 ------------------------------------------------------------------------}}}
 -- 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 part 2                                               {{{
-
-instance Pretty (NIX f) where
- pretty (nPrune -> n) = renderNIX_ pretty n
+nMinimize :: (Ord f) => NIX f -> NIX f
+nMinimize = NIX . autMinimize . unNIX
 
 ------------------------------------------------------------------------}}}
diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs
index 52ed1aa..aad7ce4 100644
--- a/src/Dyna/Analysis/Mode/Inst.hs
+++ b/src/Dyna/Analysis/Mode/Inst.hs
@@ -22,6 +22,7 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -Wall #-}
@@ -35,17 +36,16 @@ module Dyna.Analysis.Mode.Inst(
 
 import           Control.Applicative (Applicative)
 import           Control.Lens
--- import           Control.Monad
+import           Control.Monad
 import qualified Data.Foldable            as F
 import qualified Data.Traversable         as T
 import qualified Data.Map                 as M
 import qualified Data.Maybe               as MA
 -- import qualified Data.Set                 as S
+import           Dyna.Analysis.Mode.Uniq
 import           Dyna.XXX.DataUtils       as XDU
 import           Dyna.XXX.MonadUtils
 
-import           Dyna.Analysis.Mode.Uniq
-
 -- import qualified Debug.Trace                       as XT
 
 ------------------------------------------------------------------------}}}
@@ -189,14 +189,11 @@ inIGamma (RA r t) (IBound u ts)  = r == uniqGamma u
 -- | Extract the uniqueness from an inst.
 --
 -- Based on definition 3.2.13, p51 but see prose, p51, \"Note that there is
--- no uniqueness annotation on the free inst\".
+-- no uniqueness annotation on the free inst\".  This is because we assume,
+-- during mode work, that we know where all the free variables are -- that
+-- is, they're either uniquely referenced in some automata or they are
+-- explicitly aliased.
 iUniq :: InstF f i -> Maybe Uniq
-{-
-iUniq IFree          = Nothing
-iUniq (IAny u)       = Just u
-iUniq (IBound u _ _) = Just u
-iUniq (IUniv u)      = Just u
--}
 iUniq = (^? inst_uniq)
 {-# INLINABLE iUniq #-}
 
@@ -366,8 +363,10 @@ type TyILeqGLB_ f m i i' i'' r =
 -- variables).
 
 iLeqGLB_ :: (Monad m, Ord f) => TyILeqGLB_ f m i i' i'' (m (InstF f i''))
-iLeqGLB_ _ r _ _ _ u IFree      x            = T.mapM (r u) x
-iLeqGLB_ l _ _ _ _ u x          IFree        = T.mapM (l u) x
+iLeqGLB_ _ r _ _ _ u IFree      x            = liftM (over inst_uniq (max u))
+                                             $ T.mapM (r u) x
+iLeqGLB_ l _ _ _ _ u x          IFree        = liftM (over inst_uniq (max u))
+                                             $ T.mapM (l u) x
 
 iLeqGLB_ _ _ _ _ _ _ (IAny u)   (IAny u')    = return $ IAny (max u u')
 
diff --git a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs
index f5b273e..bcf7ddf 100644
--- a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs
+++ b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs
@@ -23,6 +23,8 @@ import qualified Data.Map                  as M
 import qualified Data.Maybe                as MA
 import qualified Data.Set                  as S
 import qualified Data.Traversable          as T
+import           Dyna.Analysis.Automata.Class
+import           Dyna.Analysis.Automata.Utilities
 import           Dyna.Analysis.Mode.Execution.NamedInst
 import           Dyna.Analysis.Mode.Inst
 import           Dyna.Analysis.Mode.Selftest.Term
@@ -50,10 +52,11 @@ nWFN' n = nWFU n && nAllNotEmpty n
 prop_arbNIX_is_WFU :: QCP.Property
 prop_arbNIX_is_WFU = QCP.forAll (arbNIX UUnique) nWFU
 
--- | Check 'nPrune' using the separate 'arbNIX' generator, rather than
--- the 'Arbitrary' instance, which calls 'nPrune' internally.
+-- | Check 'nMinimize' using the separate 'arbNIX' generator, rather than
+-- the 'Arbitrary' instance, which calls 'nMinimize' internally.
 prop_nPrune_Eq :: QCP.Property
-prop_nPrune_Eq = QCP.forAll (arbNIX UUnique) (\i -> nWFU i QCP.==> i `nEq` (nPrune i))
+prop_nPrune_Eq = QCP.forAll (arbNIX UUnique)
+                            (\i -> nWFU i QCP.==> i `nEq` (nMinimize i))
 
 -- | Check 'nMinimize'
 -- prop_nMinimize_Eq :: Bool -> QCP.Property
@@ -168,3 +171,5 @@ prop_call_test_sufficient i1 i2 = nWFN' i1 && nWFN' i2 && nSub i1 i2
 
 selftest :: TF.Test
 selftest = moreTries 5000 $(testGroupGenerator)
+
+main = TF.defaultMain [selftest]
diff --git a/src/Dyna/Analysis/Mode/Selftest/Term.hs b/src/Dyna/Analysis/Mode/Selftest/Term.hs
index f315bb7..ac3700f 100644
--- a/src/Dyna/Analysis/Mode/Selftest/Term.hs
+++ b/src/Dyna/Analysis/Mode/Selftest/Term.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 module Dyna.Analysis.Mode.Selftest.Term where
@@ -17,12 +18,15 @@ import qualified Data.List                 as L
 import qualified Data.Map                  as M
 import qualified Data.Maybe                as MA
 import qualified Data.Set                  as S
+import           Dyna.Analysis.Automata.Class
+import           Dyna.Analysis.Automata.Utilities
 import           Dyna.Analysis.Mode.Inst
 import           Dyna.Analysis.Mode.Uniq
 import           Dyna.Analysis.Mode.Execution.NamedInst
 import           Test.QuickCheck
 import           Test.SmallCheck           as SC
 import           Test.SmallCheck.Series    as SCS
+import qualified Text.PrettyPrint.Free     as PP
 
 ------------------------------------------------------------------------}}}
 -- Misc                                                                 {{{
@@ -69,6 +73,8 @@ arbUniq u = oneof $ map return [u..]
 data TestFunct = F | G | H
  deriving (Bounded,Enum,Eq,Ord,Show)
 
+instance PP.Pretty TestFunct where pretty = PP.text . show
+
 genArgs :: (Monad m) => m i -> TestFunct -> m [i]
 genArgs _ F = return []
 genArgs g G = g >>= return . (\x -> [x])
@@ -91,6 +97,7 @@ instance Arbitrary TestFunct where arbitrary = arbitraryBoundedEnum
 instance Arbitrary (S.Set TestFunct) where arbitrary = arbitrarySetBEO
 
 -- | Generate an arbitrary, well-formed NIX at some uniqueness.
+arbNIX :: Uniq -> Gen (NIX TestFunct)
 arbNIX rootU = do
     n <- sized (\s -> choose (1::Int,max 1 s)) -- How many plies?
 
@@ -106,12 +113,12 @@ arbNIX rootU = do
     let igen u = oneof $ map (return.snd) $ filter ((== u) . fst)
                        $ (zip uniqs nl ++ spares)
 
-    plies <- mapM (flip arbNIXME igen) uniqs   -- Generate plies or recurse
+    plies <- mapM (flip arbInstPly igen) uniqs   -- Generate plies or recurse
 
     let m = M.fromList (zip nl plies            -- Make the map
-                        ++ map (\(_,i) -> (i,Right IFree)) spares)
-    root <- arbInstPly rootU igen               -- The root
-    return $ NIX root m
+                        ++ map (\(_,i) -> (i,IFree)) spares)
+    root <- choose (1,n)
+    return $ nFromMap m root
  where
   arbInstPly :: forall i . Uniq -> (Uniq -> Gen i) -> Gen (InstF TestFunct i)
   arbInstPly u n = frequency
@@ -126,21 +133,16 @@ arbNIX rootU = do
                  <*> arbitrary)
     ]
   
-  arbNIXME :: forall f i . (f ~ TestFunct)
-           => Uniq -> (Uniq -> Gen i) -> Gen (Either (NIX f) (InstF f i))
-  arbNIXME u igen = oneof [Left  <$> sized (\s -> resize (s`div`2) (arbNIX u))
-                          ,Right <$> arbInstPly u igen]
-
-
 -- | The not-necessarily-well-formed variant
+arbNIXNWF :: Gen (NIX TestFunct)
 arbNIXNWF = do
     n <- sized (\s -> choose (1::Int,max 1 s)) -- How many plies?
     let nl   = [1..n]
     let igen = choose (1::Int,n)               -- Pick a ply
-    plies <- vectorOf n (arbNIXMENWF igen)     -- Generate plies or recurse
+    plies <- vectorOf n (arbInstPlyNWF igen)   -- Generate plies or recurse
     let m = M.fromList $ zip nl plies          -- Make the map
-    root <- arbInstPlyNWF igen                 -- The root
-    return $ NIX root m
+    root <- choose (1,n)
+    return $ nFromMap m root
  where
   arbInstPlyNWF :: forall i . Gen i -> Gen (InstF TestFunct i)
   arbInstPlyNWF n = frequency
@@ -152,16 +154,11 @@ arbNIXNWF = do
                                  $ genFuncMap arbitrary n)
                 <*> arbitrary)
     ]
-  
-  arbNIXMENWF :: forall f i . (f ~ TestFunct)
-              => Gen i -> Gen (Either (NIX f) (InstF f i))
-  arbNIXMENWF igen = oneof [Left  <$> sized (\s -> resize (s`div`2) arbitrary)
-                        ,Right <$> arbInstPlyNWF igen]
-
 
 instance Arbitrary (NIX TestFunct) where
-  arbitrary = nPrune <$> arbNIX UUnique
+  arbitrary = liftM nMinimize $ arbNIX UUnique
 
+{-
   shrink n@(NIX r m) = (MA.maybeToList noRecN) ++ subautomata
    where
     -- Replace all calls out to other automata with references to the root
@@ -170,7 +167,7 @@ instance Arbitrary (NIX TestFunct) where
 
     -- Pull out all the subautomata
     subautomata = E.lefts (M.elems m)
-
+-}
 
 ------------------------------------------------------------------------}}}
 -- Term: SmallCheck Generators                                          {{{
diff --git a/src/Dyna/Backend/Python/Backend.hs b/src/Dyna/Backend/Python/Backend.hs
index ed0c149..d632605 100644
--- a/src/Dyna/Backend/Python/Backend.hs
+++ b/src/Dyna/Backend/Python/Backend.hs
@@ -265,7 +265,7 @@ pdope_ _ (OPIter v vs _ Det (Just (PDBS c))) = return $ pretty (v^.mv_var)
                                      <+> c v vs
 
 pdope_ _ (OPIter v vs _ DetNon (Just (PDBS c))) = do
-      i <- incState
+      i <- incState id
       return $ "for" <+> "d" <> pretty i
                       <> comma
                       <> piterate vs
@@ -283,7 +283,7 @@ pdope_ _ (OPIter v vs f d   (Just (PDBS c))) = dynacPanic $
 
 -- XXX This works only for the special case at hand (thus the asserts)
 pdope_ bc (OPIter o m f DetSemi Nothing) | (f,length m) `S.member` bc = do
-  dookie <- incState
+  dookie <- incState id
   return $
    assert (iIsFree $ nExpose $ o^.mv_mi) $
    assert (all (not . iIsFree . nExpose . _mv_mi) m) $
@@ -304,7 +304,7 @@ pdope_ bc (OPIter o m f DetSemi Nothing) | (f,length m) `S.member` bc = do
 
 pdope_ bc (OPIter o m f _ Nothing) =
   assert (not $ (f,length m) `S.member` bc) $ do
-      i <- incState
+      i <- incState id
       return $ let mo = m ++ [o] in
           "for" <+> "d" <> pretty i <> "," <> piterate m <> comma <> (ground2underscore o)
                 <+> "in" <+> functorIndirect "chart" f m <> pslice mo <> colon
diff --git a/src/Dyna/XXX/MonadUtils.hs b/src/Dyna/XXX/MonadUtils.hs
index db9aaa4..4cfdb8b 100644
--- a/src/Dyna/XXX/MonadUtils.hs
+++ b/src/Dyna/XXX/MonadUtils.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE Rank2Types #-}
+
 module Dyna.XXX.MonadUtils(
   -- * Data utilities generalizing 'Dyna.XXX.DataUtils'
   mapForallM, mapExistsM, setForallM, setExistsM,
@@ -7,6 +9,8 @@ module Dyna.XXX.MonadUtils(
   andM, andM1, orM, orM1, allM, anyM,
   -- * MonadState utilities
   bracketState, incState, readState,
+  -- * Monad cache utilities
+  trySetCache, tryMapCache,
 ) where
 
 -- import           Control.Applicative
@@ -14,27 +18,34 @@ import           Control.Lens
 import           Control.Monad.Reader
 import           Control.Monad.State
 import qualified Data.Map  as M
+import           Data.Monoid
 import qualified Data.Set  as S
 
 andM :: Monad m => m Bool -> m Bool -> m Bool
 andM x y = x >>= flip andM1 y 
+{-# INLINABLE andM #-}
 
 andM1 :: Monad m => Bool -> m Bool -> m Bool
 andM1 False _ = return False
 andM1 True  x = x
+{-# INLINABLE andM1 #-}
 
 orM :: Monad m => m Bool -> m Bool -> m Bool
 orM x y = x >>= flip orM1 y
+{-# INLINABLE orM #-}
 
 orM1 :: Monad m => Bool -> m Bool -> m Bool
 orM1 True  _ = return True
 orM1 False x = x
+{-# INLINABLE orM1 #-}
 
 allM :: Monad m => [m Bool] -> m Bool
 allM = foldM andM1 True
+{-# INLINABLE allM #-}
 
 anyM :: Monad m => [m Bool] -> m Bool
 anyM = foldM orM1 False
+{-# INLINABLE anyM #-}
 
 timesM :: Monad m => (a -> m a) -> Int -> a -> m a
 timesM f = go
@@ -42,17 +53,22 @@ timesM f = go
   go n _ | n < 0 = error "timesM negative iteration count"
   go 0 a = return a
   go n a = f a >>= go (n-1)
+{-# INLINABLE timesM #-}
 
 mapForallM, mapExistsM :: (Monad m)
                        => (k -> v -> m Bool) -> M.Map k v -> m Bool
 mapForallM p m = M.foldrWithKey (\k v -> (andM $ p k v)) (return True ) m
 mapExistsM p m = M.foldrWithKey (\k v -> (orM  $ p k v)) (return False) m
+{-# INLINABLE mapForallM #-}
+{-# INLINABLE mapExistsM #-}
 
 setForallM, setExistsM :: (Monad m)
                        => (e -> m Bool) -> S.Set e -> m Bool
 setForallM p m = S.foldr (\e -> (andM $ p e)) (return True ) m
 setExistsM p m = S.foldr (\e -> (orM  $ p e)) (return False) m
 
+{-# INLINABLE setForallM #-}
+{-# INLINABLE setExistsM #-}
 
 bracketState :: (MonadState s m) => s -> m t -> m (t, s)
 bracketState bs m = do
@@ -62,10 +78,54 @@ bracketState bs m = do
  s' <- get
  put s
  return (r, s')
+{-# INLINABLE bracketState #-}
 
-incState :: (Num a, MonadState a m) => m a
-incState = id <<%= (+1)
+-- | Increment a state field given its lens.  Often you will just want to
+-- pass "id" or something similarly simple (frequently much shorter than
+-- the type given here!)
+incState :: (Enum a, MonadState s m)
+         => Overloading (->) (->) ((,) a) s s a a
+         -> m a
+incState = (<<%= succ)
+{-# INLINABLE incState #-}
 
 readState :: (MonadState a m) => ReaderT a m b -> m b
 readState x = get >>= runReaderT x
+{-# INLINABLE readState #-}
+
+-- | Often we want to check a set cache for membership, returning 'mempty'
+-- if so, or assume this case and run some action to obtain a result.
+--
+-- This is used, for example, in cycle-breaking in backward chaining, often,
+-- using 'True' for the cycle-break value, we assume the provability of our
+-- assumption and continue to look for a counter-argument.  Note that this
+-- is rather the opposite of most circular systems, where 'False' would be
+-- the cycle-break value.
+trySetCache :: (Ord e, MonadState s m)
+             => Simple Lens s (S.Set e)
+             -> r
+             -> (e -> m r)
+             -> e
+             -> m r
+trySetCache l cyc miss e = do
+  h <- (uses l $ S.member e)
+  if h
+   then return cyc
+   else l %= S.insert e >> miss e
+{-# INLINABLE trySetCache #-}
 
+
+-- | Like 'trySetCache' but a version that actually, well, caches a value.
+-- This depends on us being able to store something into the map before
+-- actually recursing and does not update the map while recursing (the
+-- callbacks may of course do so at their own risk).
+tryMapCache :: (Ord e, MonadState s m)
+            => Simple Lens s (M.Map e a)
+            -> (e -> m a)                   -- On miss, construct @a@
+            -> (e -> a -> m ())             -- Now, given @a@, recurse
+            -> e
+            -> m a
+tryMapCache l mk rec e = use (l . at e) >>= maybe miss return
+ where
+  miss = mk e >>= \k -> (l . at e .= Just k) >> rec e k >> return k
+{-# INLINABLE tryMapCache #-}