{-|
Module      : ATMS
Description : Mutable assumption-based truth maintenance systems (ATMSes)
Copyright   : (c) John Maraist, 2022
              Kenneth D. Forbus, Johan de Kleer and Xerox Corporation, 1986-1993
License     : AllRightsReserved
Maintainer  : haskell-tms@maraist.org
Stability   : experimental
Portability : POSIX

Translation of Forbus and de Kleer's assumption-based truth
maintenance systems (ATMSes) from Common Lisp to Haskell.

This is not a very \"Haskelly\" implementation; rather, it is a
translation of the original code with minimal changes.  Most of the
deviations from the original are due to either Haskell's strong
typing, which necessitates some additional tagging, and to the
abomination which is Lisp's @do@ macro.  The translation relies on
mutable data structures using `STT` state thread references.  A more
pure translation, possibly not relying on the
[@ST@ monad]("Control.Monad.ST")/[@STT@ transformer]("Control.Monad.ST.Trans"),
is a significant piece of future work.

Note also there are restrictions on the embedded monad @m@ which can
be wrapped in the `STT` transformer; see [the @Control.Monad.ST.Trans@
documentation]("Control.Monad.ST.Trans") for details.

See the @LICENSE.txt@ and @README-forbus-dekleer.txt@ files
distributed with this work for a paragraph stating scope of permission
and disclaimer of warranty, and for additional information regarding
copyright ownership.  The above copyright notice and that paragraph
must be included in any separate copy of this file.

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
implied, for NON-COMMERCIAL use.  See the License for the specific
language governing permissions and limitations under the License.

-}

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Data.TMS.ATMS.ATMST (
  -- * The ATMST monad
  ATMST,
  AtmsErr(CannotRemoveNodeWIthConsequences, InternalNoEmptyEnv, FromMonadFail),
  runATMST,
  setInitialEnvTableAlloc, setEnvTableIncr,
  getInitialEnvTableAlloc, getEnvTableIncr,

  -- * ATMS data structures

  -- ** Component classes
  NodeDatum, contradictionNodeDatum,

  -- ** Top-level ATMS
  ATMS, createATMS, atmsTitle,

  -- *** ATMS components
  getNodes, getJusts, getContradictions, getAssumptions,
  getContradictionNode, getEmptyEnvironment, getNodeString, getJustString,
  getDatumString, getInformantString, getEnqueueProcedure,

  setDatumStringViaString, setDatumStringViaShow,
  setInformantStringViaString, setInformantStringViaShow,

  -- ** Nodes
  Node, nodeDatum, createNode,
  -- *** Node components
  nodeATMS, nodeString, defaultNodeString, getNodeLabel, getNodeRules,
  getNodeConsequences,
  -- *** Setting node status
  assumeNode, makeContradiction, removeNode,

  -- ** Justifications
  JustRule(JustRule), justInformant, justConsequence, justAntecedents,
  Justification, Explanation, justifyNode,

  -- ** Environments and tables
  Env, EnvTable, envIndex, envAssumptions, getEnvNodes,

  -- * Deduction and search utilities
  interpretations, interpretationsWithDefaults,

  -- ** Related to a node
  isTrueNode, isInNode, isInNodeByEnv, isOutNode, isNodeConsistentWith,
  getNodeIsAssumption, getNodeIsContradictory, {- explainNode, -}

  -- ** Related to environments
  envIsNogood,

  -- * Printing and debugging

  -- | In addition to the functions documented below, many of the
  -- types defined in this module are instances of the classes defined
  -- in `Data.TMS.Formatters`.  Specifically:
  --
  --  - __Defined for `format`, `blurb`, etc:__ `Node`, `Justification`
  --
  --  - __Defined for `pprint`:__ `Node`, `JustRule`, `Justification`,
  --    `Env`, `EnvTable`
  --
  --  - __Defined for `debug`:__ `ATMS`, `Node`, `JustRule`, `Env`
  --
  -- Functions prefixed @format@ build a computation returning a
  -- `String`.  Functions prefixed @debug@ or @print@ build a unit
  -- computation printing the artifact in question to standard output;
  -- those with prefix @debug@ are generally more verbose.
  debugAtmsEnvs,
  printAtmsStatistics,

  -- ** Nodes and node lists
  whyNodes, whyNode,

  -- ** Environments, labels, and tables
  debugEnvTable, formatNodeLabel, debugNodeLabel,
  debugNogoods,
  printNogoods, printEnvs

  ) where

import Control.Monad
import Control.Monad.State
import Control.Monad.ST.Trans
-- import Control.Monad.Except
import Control.Monad.Trans.Except
import Control.Monad.Extra
import Data.List
import Data.Symbol
import Data.TMS.Formatters
import Data.TMS.Helpers
import Data.TMS.MList
import Data.TMS.Dbg


-- * The @ATMST@ monad transformer
--
-- Construction and manipulation of a ATMS happens inside this monad
-- wrapper.

-- |Errors which can arise from ATMS operations.
data AtmsErr = CannotRemoveNodeWIthConsequences String Int
               -- ^ It is not possible to remove a `Node` from an
               -- `ATMS` after a `JustRule` which uses that `Node` is
               -- added to the `ATMS`.
             | InternalNoEmptyEnv
               -- ^ Internal error called when there is no internal
               -- default empty `Env` associated with this `ATMS`.
               -- Should never be signaled for an `ATMS` created with
               -- `createATMS`, since this latter function does set up
               -- the default empty environment before returning the
               -- new `ATMS`.
             | InternalNoContraNode
               -- ^ Internal error called when there is no internal
               -- default contradictory `Node` associated with this
               -- `ATMS`.  Should never be signaled for an `ATMS`
               -- created with `createATMS`, since this latter
               -- function does set up the default contradiction node
               -- before returning the new `ATMS`.
             | UnexpectedNonruleJustification
               -- ^ Indicates that a `Justification` other than
               -- `ByRule` `JustRule` was found, specifically in a
               -- `removeNode` call.
             | FromMonadFail String
               -- ^ Indicates a pattern-matching failure within an
               -- `ATMST` operation.
  deriving Show

{- ===== Internal state of an ATMST. =================================== -}

-- |Internal state of an ATMST process
data AtmstState = AtmstState {
  initialEnvTableAlloc :: Int,
  envTableIncr :: Int
  }

-- |Initial state of an ATMST process.
initialAtmstState :: AtmstState
initialAtmstState = AtmstState 50 75

-- |Update the initial table size of an ATMST state.
withInitialEnvTableAlloc :: AtmstState -> Int -> AtmstState
withInitialEnvTableAlloc (AtmstState _ ei) ia = AtmstState ia ei

-- |Update the table increment size of an ATMST state.
withEnvTableIncr :: AtmstState -> Int -> AtmstState
withEnvTableIncr (AtmstState ia _) ei = AtmstState ia ei

{- ===== ATMST definition. ============================================= -}

-- |The process of building and using a mutable ATMS.
type ATMSTInner s m a =
  Monad m => ExceptT AtmsErr (StateT AtmstState (STT s m)) a

-- |The process of building and using a mutable ATMS.
newtype Monad m => ATMST s m a = AtmsT { unwrap :: ATMSTInner s m a }

-- |Internal unwrapper preserving rank-2 polymorphism of the state
-- thread in the wrapper `STT`.
unwrap2 :: Monad m => (forall s . ATMST s m a) -> (forall s . ATMSTInner s m a)
unwrap2 (AtmsT m) = m

instance (Monad m) => Functor (ATMST s m) where
  fmap f (AtmsT m) = AtmsT $ do
    v <- m
    return $ f v

instance (Monad m, Functor m) => Applicative (ATMST s m) where
  pure v = AtmsT $ pure v
  (AtmsT m1) <*> (AtmsT m2) = AtmsT $ do
    f <- m1
    v <- m2
    return (f v)

instance (Monad m, Functor m) => Monad (ATMST s m) where
  -- (>>=) :: ATMST s m a -> (a -> ATMST s m b) -> ATMST s m b
  (AtmsT m) >>= f = AtmsT $ m >>= (unwrap . f)

  -- (>>) :: ATMST s m a -> ATMST s m b -> ATMST s m b
  (AtmsT m1) >> (AtmsT m2) = AtmsT $ m1 >> m2

  -- return :: a -> ATMST s m a
  return v = AtmsT $ return v

instance MonadTrans (ATMST s) where
  lift m = AtmsT $ lift $ lift $ lift m

instance MonadIO m => MonadIO (ATMST s m) where
  liftIO = lift . liftIO

-- |Lift `STT` behavior to the `ATMST` level.
sttLayer :: Monad m => STT s m r -> ATMST s m r
sttLayer md = AtmsT $ lift $ lift $ md

-- |Lift `ExceptT` behavior to the `ATMST` level.
exceptLayer ::
  Monad m => ExceptT AtmsErr (StateT AtmstState (STT s m)) r -> ATMST s m r
exceptLayer = AtmsT

-- |Lift `StateT` behavior to the `ATMST` level.
stateLayer ::
  Monad m => StateT AtmstState (STT s m) r -> ATMST s m r
stateLayer = AtmsT . lift

instance Monad m => MonadFail (ATMST s m) where
  fail s = exceptLayer $ throwE $ FromMonadFail s

-- |Retrieve the current initial `Env` table size setting.
getInitialEnvTableAlloc :: Monad m => ATMST s m Int
getInitialEnvTableAlloc = stateLayer $ fmap initialEnvTableAlloc get

-- |Retrieve the current initial `Env` table size setting.
setInitialEnvTableAlloc :: Monad m => Int -> ATMST s m ()
setInitialEnvTableAlloc ia = stateLayer $ modify (`withInitialEnvTableAlloc` ia)

-- |Retrieve the current initial `Env` table size setting.
getEnvTableIncr :: Monad m => ATMST s m Int
getEnvTableIncr = stateLayer $ fmap envTableIncr get

-- |Retrieve the current initial `Env` table size setting.
setEnvTableIncr :: Monad m => Int -> ATMST s m ()
setEnvTableIncr ia = stateLayer $ modify (`withEnvTableIncr` ia)

-- |Execute a computation in the `ATMST` monad transformer.
runATMST :: Monad m => (forall s . ATMST s m r) -> m (Either AtmsErr r)
runATMST atmst = do
  let core = unwrap2 atmst
      afterExcept = runExceptT core
      afterState = do
        (result, endState) <- runStateT afterExcept initialAtmstState
        return result
  runSTT afterState

{- ----------------------------------------------------------------- -}

-- |Class of type which can be used as the datum underlying `Node`s in
-- an `ATMS`.
class NodeDatum d where
  -- |The datum associated with the contradiction node in a
  -- newly-initialized `ATMS` with `Node` data of this type.
  contradictionNodeDatum :: d

instance NodeDatum String where
  contradictionNodeDatum = "The contradiction"
instance NodeDatum Symbol where
  contradictionNodeDatum = intern "The contradiction"

-- |Top-level representation of an assumption-based truth maintenance
-- system.
data (Monad m, NodeDatum d) => ATMS d i r s m = ATMS {
  -- |Name of this ATMS.
  atmsTitle :: String,
  -- |Unique namer for nodes.
  atmsNodeCounter :: STRef s Int,
  -- |Unique namer for justifications.
  atmsJustCounter :: STRef s Int,
  -- |Unique namer for environments.
  atmsEnvCounter :: STRef s Int,
  -- |Current size of environment table.
  atmsEnvTableAlloc :: STRef s Int,
  -- |List of all TMS nodes.
  atmsNodes :: STRef s [Node d i r s m],
  -- |List of all justifications.
  atmsJusts :: STRef s [JustRule d i r s m],
  -- |List of all contradiction nodes.
  atmsContradictions :: STRef s [Node d i r s m],
  -- |List of all assumption nodes.
  atmsAssumptions :: STRef s [Node d i r s m],
  -- |The environment table.
  atmsEnvTable :: STRef s (EnvTable d i r s m),
  -- |The table of nogood environments.
  atmsNogoodTable :: STRef s (EnvTable d i r s m),
  -- |Canonical empty Env for this ATMS.  This value is not set more
  -- than once, but it created (by `createATMS`) after the ATMS is
  -- allocated, so we use a reference to be able to set it up later.
  atmsEmptyEnv :: STRef s (Maybe (Env d i r s m)),
  -- |Canonical contradiction `Node` for this ATMS.  This value is not
  -- set more than once, but it written (by `createATMS`) after the
  -- ATMS is allocated, so we use a reference to be able to set it up
  -- later.
  atmsContraNode :: STRef s (Maybe (Node d i r s m)),
  -- |Function for formatting a `Node` of this ATMS.
  atmsNodeString :: STRef s (Node d i r s m -> String),
  -- |Function for representing a justification rule.
  atmsJustString :: STRef s (JustRule d i r s m -> String),
  -- |Function for representing the data associated with `Node`s.
  atmsDatumString :: STRef s (d -> String),
  -- |Function for representing the informants of justifications.
  atmsInformantString :: STRef s (i -> String),
  -- |List of external procedures to be executed for this ATMS.
  atmsEnqueueProcedure :: STRef s (r -> ATMST s m ()),
  -- |Set to `True` when we wish to debug this ATMS.
  adebugging :: STRef s Bool
}

-- |Print the internal title signifying an ATMS.
--
-- Translated from @print-atms@ in @atms.lisp@.
instance NodeDatum d => Printed (ATMS d i r) ATMST where
  pprint atms = liftIO $ putStrLn $ "#<ATMS: " ++ atmsTitle atms ++ ">"

-- |Give a verbose printout of an `ATMS`.
instance NodeDatum d => Debugged (ATMS d i r) ATMST where
  debug atms = do
    liftIO $ putStrLn $ "=============== " ++ atmsTitle atms
    debugNodes atms
    debugJusts atms
    debugAtmsEnvs atms
    debugNogoods atms
    liftIO $ putStrLn "=============== "

-- |Shortcut maker for reading from an `ATMS` reference.
getATMSMutable ::
  (Monad m, NodeDatum d) =>
    (ATMS d i r s m -> STRef s a) -> ATMS d i r s m  -> ATMST s m a
{-# INLINE getATMSMutable #-}
getATMSMutable refGetter atms = sttLayer $ readSTRef (refGetter atms)
-- |Shortcut to write to an ATMS reference.
setATMSMutable ::
  (Monad m, NodeDatum d) =>
    (ATMS d i r s m -> STRef s a) -> ATMS d i r s m -> a -> ATMST s m ()
{-# INLINE setATMSMutable #-}
setATMSMutable refGetter atms envs =
  sttLayer $ writeSTRef (refGetter atms) envs

-- |Return the `ATMS`'s current `Node` list.
getNodes ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]
{-# INLINE getNodes #-}
getNodes = getATMSMutable atmsNodes

-- |Return the `ATMS`'s current `EnvTable`.
getEnvTable ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (EnvTable d i r s m)
{-# INLINE getEnvTable #-}
getEnvTable = getATMSMutable atmsEnvTable

-- |Return the `ATMS`'s current `EnvTable` for nogood `Env`s.
getNogoodTable ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (EnvTable d i r s m)
{-# INLINE getNogoodTable #-}
getNogoodTable = getATMSMutable atmsNogoodTable

-- |Return the `ATMS`'s current `JustRule` list.
getJusts ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [JustRule d i r s m]
{-# INLINE getJusts #-}
getJusts = getATMSMutable atmsJusts

-- |Return the `ATMS`'s current contradictions list.
getContradictions ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]
{-# INLINE getContradictions #-}
getContradictions = getATMSMutable atmsContradictions

-- |Return the `ATMS`'s current assumptions list.
getAssumptions ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]
{-# INLINE getAssumptions #-}
getAssumptions = getATMSMutable atmsAssumptions

-- |Return the `ATMS`'s built-in empty environment.
getEmptyEnvironment ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (Env d i r s m)
{-# INLINE getEmptyEnvironment #-}
getEmptyEnvironment atms = do
  maybeEnv <- getATMSMutable atmsEmptyEnv atms
  case maybeEnv of
    Just env -> return env
    Nothing -> exceptLayer $ throwE InternalNoEmptyEnv

-- |Return the `ATMS`'s built-in contradiction node.
getContradictionNode ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (Node d i r s m)
{-# INLINE getContradictionNode #-}
getContradictionNode atms = do
  maybeNode <- getATMSMutable atmsContraNode atms
  case maybeNode of
    Just node -> return node
    Nothing -> exceptLayer $ throwE InternalNoContraNode

-- |Return the `ATMS`'s current `Node` formatter.
getNodeString ::
  (Monad m, NodeDatum d) =>
    ATMS d i r s m -> ATMST s m (Node d i r s m -> String)
{-# INLINE getNodeString #-}
getNodeString = getATMSMutable atmsNodeString
-- |Shortcut to write to the reference to a ATMS's `Node` formatter.
setNodeString ::
  (Monad m, NodeDatum d) =>
    ATMS d i r s m -> (Node d i r s m -> String) -> ATMST s m ()
{-# INLINE setNodeString #-}
setNodeString = setATMSMutable atmsNodeString

-- |Return the `ATMS`'s current `JustRule` formatter.
getJustString ::
  (Monad m, NodeDatum d) =>
    ATMS d i r s m -> ATMST s m (JustRule d i r s m -> String)
{-# INLINE getJustString #-}
getJustString = getATMSMutable atmsJustString
-- |Shortcut to write to the reference to a ATMS's `JustRule` formatter.
setJustString ::
  (Monad m, NodeDatum d) =>
    ATMS d i r s m -> (JustRule d i r s m -> String) -> ATMST s m ()
{-# INLINE setJustString #-}
setJustString = setATMSMutable atmsJustString

-- |Return the `ATMS`'s current datum formatter.
getDatumString ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (d -> String)
{-# INLINE getDatumString #-}
getDatumString = getATMSMutable atmsDatumString
-- |Shortcut to write to the reference to a ATMS's datum formatter.
setDatumString ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> (d -> String) -> ATMST s m ()
{-# INLINE setDatumString #-}
setDatumString = setATMSMutable atmsDatumString

-- |When the data associated with `Node`s are all `String`s, we can
-- direct the `ATMS` to display each datum as itself.
setDatumStringViaString :: Monad m => ATMS String i r s m -> ATMST s m ()
setDatumStringViaString atms = setDatumString atms id

-- |When the data associated with `Node`s are of a type of class
-- `Show`, we can direct the `ATMS` to display each datum using the
-- `show` instance.
setDatumStringViaShow ::
  (NodeDatum d, Show d, Monad m) => ATMS d i r s m -> ATMST s m ()
setDatumStringViaShow atms = setDatumString atms show

-- |Return the `ATMS`'s current informant formatter.
getInformantString ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (i -> String)
{-# INLINE getInformantString #-}
getInformantString = getATMSMutable atmsInformantString
-- |Shortcut to write to the reference to a ATMS's informant formatter.
setInformantString ::
  (Monad m, NodeDatum d) => ATMS d i r s m -> (i -> String) -> ATMST s m ()
{-# INLINE setInformantString #-}
setInformantString = setATMSMutable atmsInformantString

-- |When the informants associated with `JustRule`s are all
-- `String`s, we can direct the `ATMS` to display each informant as
-- itself.
setInformantStringViaString ::
  (Monad m, NodeDatum d) => ATMS d String r s m -> ATMST s m ()
setInformantStringViaString atms = setInformantString atms id

-- |When the informants associated with `JustRule`s are of a type of
-- class `Show`, we can direct the `ATMS` to display each datum using
-- the `show` instance.
setInformantStringViaShow ::
  (Show i, Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
setInformantStringViaShow atms = setInformantString atms show

-- |Return the `ATMS`'s current rule-queueing procedure.
getEnqueueProcedure ::
  (Monad m, NodeDatum d) =>
    ATMS d i r s m -> ATMST s m (r -> ATMST s m ())
{-# INLINE getEnqueueProcedure #-}
getEnqueueProcedure = getATMSMutable atmsEnqueueProcedure
-- |Shortcut to write to the reference to a ATMS's rule-queueing procedure.
setEnqueueProcedure ::
  (Monad m, NodeDatum d) =>
    ATMS d i r s m -> (r -> ATMST s m ()) -> ATMST s m ()
{-# INLINE setEnqueueProcedure #-}
setEnqueueProcedure = setATMSMutable atmsEnqueueProcedure

-- |Get the next node counter value, incrementing for future accesses.
nextNodeCounter :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m Int
nextNodeCounter jtms = sttLayer $ do
  let nodeCounter = atmsNodeCounter jtms
  nodeId <- readSTRef nodeCounter
  writeSTRef nodeCounter $ 1 + nodeId
  return nodeId

-- |Get the next justification rule counter value, incrementing for
-- future accesses.
nextJustCounter :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m Int
nextJustCounter atms = sttLayer $ do
  let justCounter = atmsJustCounter atms
  justId <- readSTRef justCounter
  writeSTRef justCounter $ 1 + justId
  return justId

-- |Get the next environment rule counter value, incrementing for
-- future accesses.
nextEnvCounter :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m Int
nextEnvCounter atms = sttLayer $ do
  let envCounter = atmsEnvCounter atms
  envId <- readSTRef envCounter
  writeSTRef envCounter $ 1 + envId
  return envId

{- ----------------------------------------------------------------- -}

-- |Wrapper for the datum associated with a node of the `ATMS`.
--
-- Translated from @(tms-node@ in @atms.lisp@.
data (Monad m, NodeDatum d) => Node d i r s m = Node {
  nodeIndex :: Int,
  -- |Retrieve the datum associated with a `Node`.
  nodeDatum :: d,
  nodeLabel :: STRef s [Env d i r s m],
  nodeJusts :: STRef s [Justification d i r s m],
  nodeConsequences :: STRef s [JustRule d i r s m],
  nodeIsContradictory :: STRef s Bool,
  nodeIsAssumption :: STRef s Bool,
  nodeRules :: STRef s [r],
  -- |Retrieve the `ATMS` associated with a `Node`.
  nodeATMS :: ATMS d i r s m
}

instance (Monad m, NodeDatum d) => Eq (Node d i r s m) where
  n1 == n2 = nodeIndex n1 == nodeIndex n2

instance (Monad m, NodeDatum d) => Ord (Node d i r s m) where
  n1 < n2 = nodeIndex n1 < nodeIndex n2
  n1 `compare` n2 = nodeIndex n1 `compare` nodeIndex n2

instance (Monad m, NodeDatum d) => Show (Node d i r s m) where
  show n = "<Node " ++ show (nodeIndex n) ++ ">"

-- |`format`, `blurb`, etc. may be applied to `Node`s in an
-- `ATMST`.
instance NodeDatum d => Formatted (Node d i r) ATMST where
  format node = do
    datumFmt <- getDatumString $ nodeATMS node
    return $ datumFmt (nodeDatum node)

-- |Print a `Node` of an `ATMS` with its tag.
--
-- Translated from @print-tms-node@ in @atms.lisp@.
instance NodeDatum d => Printed (Node d i r) ATMST where
  pprint node = do
    str <- nodeString node
    liftIO $ putStr $ "<NODE: " ++ str ++ ">"

-- |Give a verbose printout of a `Node` of an `ATMS`.
instance NodeDatum d => Debugged (Node d i r) ATMST where
  debug node = do
    let atms = nodeATMS node
    datumFmt <- getDatumString atms
    informantFmt <- getInformantString atms
    liftIO $ putStrLn $ "- " ++ datumFmt (nodeDatum node)

    label <- getNodeLabel node
    case label of
      [] -> liftIO $ putStrLn "  Empty label"
      [env] -> do
        liftIO $ putStr "  Single environment label: "
        debug env
      _ -> forM_ label $ \env -> do
        liftIO $ putStrLn "  - "
        debug env

    conseqs <- getNodeConsequences node
    case conseqs of
      [] -> liftIO $ putStrLn "  Antecedent to no justifications"
      _ -> do
        liftIO $ putStr "  Antecedent to:"
        forM_ conseqs $ \ conseq -> do
          liftIO $ putStr $ " " ++ informantFmt (justInformant conseq)
        liftIO $ putStrLn ""

-- |Shortcut maker for reading from a `Node` reference.
getNodeMutable ::
  (Monad m, NodeDatum d) =>
    (Node d i r s m -> STRef s a) -> Node d i r s m  -> ATMST s m a
{-# INLINE getNodeMutable #-}
getNodeMutable refGetter node = sttLayer $ readSTRef (refGetter node)
-- |Shortcut to write to the reference to a node's label.
setNodeMutable ::
  (Monad m, NodeDatum d) =>
    (Node d i r s m -> STRef s a) -> Node d i r s m -> a -> ATMST s m ()
{-# INLINE setNodeMutable #-}
setNodeMutable refGetter node val = sttLayer $ writeSTRef (refGetter node) val

-- |Return the `Node`'s label.
getNodeLabel ::
  (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [Env d i r s m]
{-# INLINE getNodeLabel #-}
getNodeLabel = getNodeMutable nodeLabel
-- |Shortcut to write to the reference to a node's label.
setNodeLabel ::
  (Monad m, NodeDatum d) => Node d i r s m -> [Env d i r s m] -> ATMST s m ()
{-# INLINE setNodeLabel #-}
setNodeLabel = setNodeMutable nodeLabel

-- |Return the `Node`'s rules.
getNodeRules :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [r]
{-# INLINE getNodeRules #-}
getNodeRules = getNodeMutable nodeRules
-- |Shortcut to write to the reference to a node's rules.
setNodeRules :: (Monad m, NodeDatum d) => Node d i r s m -> [r] -> ATMST s m ()
{-# INLINE setNodeRules #-}
setNodeRules = setNodeMutable nodeRules

-- |Return the `JustRule`s concluding a `Node`.
getNodeJusts ::
  (Monad m, NodeDatum d) =>
    Node d i r s m -> ATMST s m [Justification d i r s m]
{-# INLINE getNodeJusts #-}
getNodeJusts = getNodeMutable nodeJusts

-- |Return the `Node`'s consequences.
getNodeConsequences ::
  (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [JustRule d i r s m]
{-# INLINE getNodeConsequences #-}
getNodeConsequences = getNodeMutable nodeConsequences
-- |Shortcut to write to the reference to a node's consequences.
setNodeConsequences ::
  (Monad m, NodeDatum d) =>
    Node d i r s m -> [JustRule d i r s m] -> ATMST s m ()
{-# INLINE setNodeConsequences #-}
setNodeConsequences = setNodeMutable nodeConsequences

-- |Return whether the `Node`'s is currently contradictory.
getNodeIsContradictory ::
  (Monad m, NodeDatum d) => Node d i r s m  -> ATMST s m Bool
getNodeIsContradictory node = sttLayer $ readSTRef (nodeIsContradictory node)

-- |Set whether a `Node`'s is currently contradictory.
setNodeIsContradictory ::
  (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()
setNodeIsContradictory node =
  sttLayer $ writeSTRef (nodeIsContradictory node) True

-- |Return whether the `Node`'s is currently markable as an assumption.
getNodeIsAssumption ::
  (Monad m, NodeDatum d) => Node d i r s m  -> ATMST s m Bool
getNodeIsAssumption node = sttLayer $ readSTRef (nodeIsAssumption node)

-- |The justification of one `ATMS` `Node` by zero or more others.
data (Monad m, NodeDatum d) => JustRule d i r s m = JustRule {
  justIndex :: Int,
  -- |The informant associated with applying this inference rule.
  justInformant :: i,
  -- |The conclusion of this inference rule.
  justConsequence :: Node d i r s m,
  -- |The antecedents of this inference rule.
  justAntecedents :: [Node d i r s m]
}

instance (Monad m, NodeDatum d) => Eq (JustRule d i r s m) where
  e1 == e2 = (justIndex e1) == (justIndex e2)

-- |Print a more verbose description of a `Just`ification rule of an
-- `ATMS`.
--
-- Translated from @print-just@ in @atms.lisp@.
instance NodeDatum d => Printed (JustRule d i r) ATMST where
  pprint rule = do
    infStr <- formatJustInformant rule
    liftIO $ putStr $ "<" ++ infStr ++ " " ++ show (justIndex rule) ++ ">"

instance NodeDatum d => Debugged (JustRule d i r) ATMST where
  debug (JustRule idx inf conseq ants) = do
    let atms = nodeATMS conseq
    informantFmt <- getInformantString atms
    datumFmt <- getDatumString atms
    liftIO $ putStrLn $ "  "
      ++ "[" ++ informantFmt inf ++ "." ++ show idx ++ "] "
      ++ datumFmt (nodeDatum conseq) ++ " <= "
      ++ intercalate ", " (map (datumFmt . nodeDatum) ants)

-- |Description of why a `Node` may be believed by the `ATMS`.
data Justification d i r s m =
  ByRule (JustRule d i r s m) | ByAssumption (Node d i r s m) | ByContradiction

-- |`format`, `blurb`, etc. may be applied to `Node`s in an
-- `ATMST`.
instance NodeDatum d => Formatted (Justification d i r) ATMST where
  format (ByRule j) = return $ "By rule " ++ show (justIndex j)
  format (ByAssumption n) = do
    nodeFmt <- getNodeString (nodeATMS n)
    return $ "By assumption " ++ nodeFmt n
  format ByContradiction = return "By contradiction"

-- |`format`, `blurb`, etc. may be applied to `Justification`s
-- in an `ATMST`.
instance NodeDatum d => Printed (Justification d i r) ATMST where
  pprint j = case j of
    ByRule rule -> pprint rule
    ByAssumption node -> do
      liftIO $ putStr $ "Assumed node "
      pprint node
    ByContradiction -> liftIO $ putStrLn $ "By contradiction"

-- |Explanation of why a `Node` may be believed by the `ATMS` for
-- output to a query.
data Explanation d i r s m =
  IsRule (JustRule d i r s m) | IsAssumption (Node d i r s m)

-- |Explanation of why a `Node` may be classified as no-good by the
-- `ATMS`.
data WhyNogood d i r s m =
  Good | ByJustification (Justification d i r s m) | ByEnv (Env d i r s m)

-- |Translation of the explanation of why a `Node` may be classified
-- (or not) as no-good to a boolean value.
isNogood :: WhyNogood d i r s m -> Bool
isNogood Good = False
isNogood _ = True

{- ----------------------------------------------------------------- -}

-- |An environment of `Node`s which may be used as the basis of
-- reasoning in an `ATMS`.
data (Monad m, NodeDatum d) => Env d i r s m = Env {
  -- |The unique nomber of this `Env` within its `ATMS`.
  envIndex :: Int,
  -- |The number of assumptions contained within this `Env`.
  envCount :: Int,
  -- |The assumptions contained within this `Env`.
  envAssumptions :: [Node d i r s m],
  envNodes :: STRef s [Node d i r s m],
  envWhyNogood :: STRef s (WhyNogood d i r s m),
  envRules :: STRef s [r]
}

instance (Monad m, NodeDatum d) => Eq (Env d i r s m) where
  e1 == e2 = (envIndex e1) == (envIndex e2)

instance (Monad m, NodeDatum d) => Show (Env d i r s m) where
  show n = "<Env " ++ show (envIndex n) ++ ">"

-- |`format` etc. for `Env`, translated from @print-env@ in @atms.lisp@.
instance NodeDatum d => Formatted (Env d i r) ATMST where
  format env = do
    let assumptions = envAssumptions env
    case (null assumptions) of
      True -> return "<empty env>"
      False -> do
        printer <- getNodeString $ nodeATMS $ head assumptions
        strs <- mapM format assumptions
        return $ "<env:" ++ intercalate "," strs ++ ">"

-- |`pprint` for `Env`, translated from @print-env@ in @atms.lisp@.
instance NodeDatum d => Printed (Env d i r) ATMST where
  pprint env = do
    whenM (envIsNogood env) $ liftIO $ putStr "* "
    -- liftIO $ putStr "ZZZZZ "
    envString env
    liftIO $ putStrLn ""

-- |Give a verbose printout of one `Env`ironment of an `ATMS`.
instance NodeDatum d => Debugged (Env d i r) ATMST where
  debug env = do
    isNogood <- envIsNogood env
    case envAssumptions env of
      [] -> liftIO $ putStrLn "<empty env>"
      nodes @ (n : _) -> do
        let atms = nodeATMS n
        datumFmt <- getDatumString atms
        when isNogood $ liftIO $ putStr "[X] "
        liftIO $ putStrLn $
          (intercalate ", " $ map (datumFmt . nodeDatum) nodes)
          ++ " (count " ++ show (length nodes) ++ ")"

-- |Shortcut maker for reading from a `Env` reference.
getEnvMutable ::
  (Monad m, NodeDatum d) =>
    (Env d i r s m -> STRef s a) -> Env d i r s m  -> ATMST s m a
{-# INLINE getEnvMutable #-}
getEnvMutable refGetter env = sttLayer $ readSTRef (refGetter env)
-- |Shortcut to write to the reference to a env's label.
setEnvMutable ::
  (Monad m, NodeDatum d) =>
    (Env d i r s m -> STRef s a) -> Env d i r s m -> a -> ATMST s m ()
{-# INLINE setEnvMutable #-}
setEnvMutable refGetter env envs = sttLayer $ writeSTRef (refGetter env) envs

-- |Shortcut for reading the `Node`s of an `Env`.
getEnvNodes ::
  (Monad m, NodeDatum d) => Env d i r s m  -> ATMST s m [Node d i r s m]
getEnvNodes = getEnvMutable envNodes
-- |Shortcut for writing the `Node`s of an `Env`.
setEnvNodes ::
  (Monad m, NodeDatum d) => Env d i r s m  -> [Node d i r s m] -> ATMST s m ()
setEnvNodes = setEnvMutable envNodes

-- |Shortcut for reading the rules of an `Env`.
getEnvRules :: (Monad m, NodeDatum d) => Env d i r s m  -> ATMST s m [r]
getEnvRules = getEnvMutable envRules
-- |Shortcut for writing the rules of an `Env`.
setEnvRules :: (Monad m, NodeDatum d) => Env d i r s m  -> [r] -> ATMST s m ()
setEnvRules = setEnvMutable envRules

-- |Shortcut for testing whether an `Env` is nogood.
envIsNogood :: (Monad m, NodeDatum d) => Env d i r s m -> ATMST s m Bool
envIsNogood env = do
  fmap isNogood $ sttLayer $ readSTRef $ envWhyNogood env

-- |Type alias for the array storage of a table of `Env`s arranged by
-- length.
newtype EnvTable d i r s m = EnvTable (STArray s Int [Env d i r s m])

-- |Print the `Env`ironments contained in the given `EnvTable`.
--
-- Translated from @print-env-table@ in @atms.lisp@.
instance NodeDatum d => Printed (EnvTable d i r) ATMST where
  pprint (EnvTable arr) = do
    let (lo, hi) = boundsSTArray arr
    forM_ [lo..hi] $ \i ->
      forMM_ (sttLayer $ readSTArray arr i) pprint

findInEnvTable ::
  (Monad m, NodeDatum d) =>
    (Env d i r s m -> Bool) -> EnvTable d i r s m ->
      ATMST s m (Maybe (Env d i r s m))
findInEnvTable pred (EnvTable arr) =
  let (lo, hi) = boundsSTArray arr
  in findInEnvTableEntries pred  [lo..hi] arr
  where findInEnvTableEntries ::
          Monad m =>
            (Env d i r s m -> Bool) -> [Int] -> STArray s Int [Env d i r s m] ->
              ATMST s m (Maybe (Env d i r s m))
        findInEnvTableEntries pred [] arr = return Nothing
        findInEnvTableEntries pred (i : idxs) arr = do
          entries <- sttLayer $ readSTArray arr i
          case find pred entries of
            Nothing -> findInEnvTableEntries pred idxs arr
            res -> return res

        findInEnvTableEntry ::
          Monad m =>
            (Env d i r s m -> Bool) -> [Env d i r s m] -> Maybe (Env d i r s m)
        findInEnvTableEntry pred envs = find pred envs

-- |Shortcut for retrieving the `Node` formatter from an `ATMS`, and
-- applying it to the given `Node`.
--
-- Translated from @node-string@ in @atms.lisp@.
nodeString :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String
nodeString node = do
  nodeFmt <- getNodeString $ nodeATMS node
  return $ nodeFmt node

-- |Default formatter for the `Node`s of an `ATMS`.
--
-- Translated from @default-node-string@ in @atms.lisp@.
defaultNodeString ::
  (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String
defaultNodeString node = do
  datumFormatter <- getDatumString $ nodeATMS node
  return $ datumFormatter $ nodeDatum node

-- |Insert an element into a sorted list.
--
-- Translated from @ordered-insert@ in @atms.lisp@.
orderedInsert :: Eq a => a -> [a] -> (a -> a -> Bool) -> [a]
orderedInsert item [] _ = [item]
orderedInsert item list@(i : _) test | test item i  = item : list
orderedInsert item list@(i : _) _    | item == i    = list
orderedInsert item (i : is) test = i : orderedInsert item is test

{- Does not seem to be used
-- Translated from @ordered-push@ in @atms.lisp@.
--
-- > ;; In atms.lisp
-- > (defmacro ordered-push (item list test)
-- >   `(setq ,list (ordered-insert ,item ,list ,test)))
orderedPush :: a -> [a] -> (a -> a -> Bool) -> [a]
orderedPush = error "< unimplemented orderedPush >"
-}

-- |We order assumptions in `Env` lists by their index.
--
-- Translated from @assumption-order@ in @atms.lisp@.
assumptionOrder ::
  (Monad m, NodeDatum d) => Node d i r s m -> Node d i r s m -> Bool
assumptionOrder n1 n2 = nodeIndex n1 < nodeIndex n2

-- Ordering predicate for two `Env`s; uses their internal index.
--
-- Translated from @env-order@ in @atms.lisp@.
envOrder :: (Monad m, NodeDatum d) => Env d i r s m -> Env d i r s m -> Bool
envOrder e1 e2 = envIndex e1 < envIndex e2

{- ----------------------------------------------------------------- -}

-- * Basic inference engine interface.

-- |Create a new, empty ATMS.
--
-- Translated from @create-atms@ in @atms.lisp@.
createATMS ::
  (Debuggable m, NodeDatum d) => String -> ATMST s m (ATMS d i r s m)
createATMS title = do
  ecInitialAlloc <- getInitialEnvTableAlloc
  emptyEnvRef <- sttLayer $ newSTRef Nothing
  contraNodeRef <- sttLayer $ newSTRef Nothing
  result <- sttLayer $ do
    nc <- newSTRef 0
    jc <- newSTRef 0
    ec <- newSTRef 0
    etAlloc <- newSTRef ecInitialAlloc
    nodes <- newSTRef ([] :: [Node d i r s m])
    justs <- newSTRef ([] :: [JustRule d i r s m])
    contradictions <- newSTRef ([] :: [Node d i r s m])
    assumptions <- newSTRef ([] :: [Node d i r s m])
    etable <- newSTArray (0, ecInitialAlloc) []
    etableRef <- newSTRef (EnvTable etable)
    ngtable <- newSTArray (0, ecInitialAlloc) []
    ngtableRef <- newSTRef (EnvTable ngtable)
    nodeString <- newSTRef (show . nodeIndex)
    justString <- newSTRef (show . justIndex)
    datumString <- newSTRef (\ datum -> "?")
    informantString <- newSTRef (\ inf -> "?")
    enqueueProcedure <- newSTRef (\ _ -> return ())
    debugging <- newSTRef False
    return $ ATMS title nc jc ec etAlloc
                  nodes justs contradictions assumptions
                  etableRef ngtableRef emptyEnvRef contraNodeRef
                  nodeString justString datumString informantString
                  enqueueProcedure debugging
  emptyEnv <- createEnv result []
  sttLayer $ writeSTRef emptyEnvRef (Just emptyEnv)
  contra <- createNode result contradictionNodeDatum False True
  sttLayer $ writeSTRef contraNodeRef (Just contra)
  return result

{- ----------------------------------------------------------------- -}

-- |Returns `True` if the given `Node` is axiomatic, following from
-- the assumption of zero other nodes.
--
-- Translated from @true-node?@ in @atms.lisp@.
isTrueNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m Bool
isTrueNode node = do
  envs <- getNodeLabel node
  return $ case envs of
    [] -> False
    e : _ -> null $ envAssumptions e

-- |Returns `True` if the given `Node` is justified by some labelling
-- `Env`ironment of `Node`s in the `ATMS`.
--
-- Translated from @in-node?@ in @atms.lisp@.
isInNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m Bool
isInNode node = fmap (not . null) (getNodeLabel node)

-- |Returns `True` if the given `Node` is justified by some subset of
-- the given environment in the `ATMS`.
--
-- Translated from @in-node?@ in @atms.lisp@.
isInNodeByEnv ::
  (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool
isInNodeByEnv node env = do
  labelEnvs <- getNodeLabel node
  return $ any (\ le -> isSubsetEnv le env) labelEnvs

-- |Returns `True` if the given `Node` is justified by no labelling
-- `Env`ironment of `Node`s in the `ATMS`.
--
-- Translated from @out-node?@ in @atms.lisp@.
isOutNode ::
  (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool
isOutNode node env = fmap not $ isInNodeByEnv node env

-- |Returns `True` if some environment justifying the given `Node` is
-- consistent with the given environment, where two environments are
-- consistent when their union is not no-good.
--
-- Translated from @node-consistent-with?@ in @atms.lisp@.
isNodeConsistentWith ::
  (Debuggable m, NodeDatum d) =>
    Node d i r s m -> Env d i r s m -> ATMST s m Bool
isNodeConsistentWith node env = do
  labelEnvs <- getNodeLabel node
  anyByM (\ le -> do
             union <- unionEnv le env
             fmap not $ envIsNogood union)
    labelEnvs

-- |Create a new `Node` in an `ATMS`.
--
-- Translated from @create-node@ in @atms.lisp@.
createNode :: (Debuggable m, NodeDatum d) =>
  ATMS d i r s m -> d -> Bool -> Bool -> ATMST s m (Node d i r s m)
createNode atms datum isAssumption isContradictory = do
  idx <- nextNodeCounter atms
  label <- sttLayer $ newSTRef []
  justs <- sttLayer $ newSTRef []
  conseq <- sttLayer $ newSTRef []
  assumptionFlag <- sttLayer $ newSTRef isAssumption
  contraFlag <- sttLayer $ newSTRef isContradictory
  rules <- sttLayer $ newSTRef []
  let node = Node idx datum label justs conseq
                  contraFlag assumptionFlag rules atms
  sttLayer $ do
    push node $ atmsNodes atms
    when isContradictory $ push node $ atmsContradictions atms
  when isAssumption $ do
    selfEnv <- createEnv atms [node]
    sttLayer $ do
      push node $ atmsAssumptions atms
      push selfEnv $ nodeLabel node
  return node

-- |Mark the given `Node` as to be believed as an assumption by its
-- `ATMS`.
--
-- Translated from @assume-node@ in @atms.lisp@.
assumeNode :: (Debuggable m, NodeDatum d) => Node d i r s m -> ATMST s m ()
assumeNode node =
  unlessM (getNodeIsAssumption node) $ do
    let atms = nodeATMS node
    sttLayer $ push node (atmsAssumptions atms)
    selfEnv <- findOrMakeEnv [node] atms
    nodes <- sttLayer $ toMList [Just selfEnv]
    update nodes node (ByAssumption node)

-- |Mark the given `Node` as an additional contradiction node of the
-- `ATMS`.
--
-- Translated from @make-contradiction@ in @atms.lisp@.
makeContradiction :: (Debuggable m, NodeDatum d) => Node d i r s m -> ATMST s m ()
makeContradiction node = do
  let atms = nodeATMS node
  unlessM (getNodeIsContradictory node) $ do
    setNodeIsContradictory node
    sttLayer $ push node $ atmsContradictions atms
    whileDoWith (getNodeLabel node) (not . null) $ \ (env : _) ->
      newNogood atms env ByContradiction

-- |Direct the `ATMS` to believe a particular `Node` when all of the
-- given list of `Node`s are also believed.  The first argument is the
-- informant associated with this inference.
--
-- Translated from @justify-node@ in @atms.lisp@.
justifyNode ::
  (Debuggable m, NodeDatum d) =>
    i -> Node d i r s m -> [Node d i r s m] -> ATMST s m ()
justifyNode informant consequence antecedents = do
  -- Retrieve the ATMS in which we are working
  let atms = nodeATMS consequence

  -- Number and create a new justification record.
  idx <- nextJustCounter atms
  let just = JustRule idx informant consequence antecedents

  -- Register the new justification with the node it can imply.
  sttLayer $ push (ByRule just) (nodeJusts consequence)

  -- Register the new justification with the nodes that can trigger
  -- it.
  sttLayer $ forM_ antecedents $ \node ->
    {-# SCC "justifyNode.push" #-} push just $ nodeConsequences node

  -- Register the new justification with the ATMS itself.
  sttLayer $ push just $ atmsJusts atms

  -- Introduce the new justification
  emptyEnv <- getEmptyEnvironment atms
  envListRef <- sttLayer $ fromListMap Just [emptyEnv]
  propagate just Nothing envListRef

-- |Direct the `ATMS` to find the combination of all of the given
-- `Node`s to be a contradiction associated with the given informant.
--
-- Translated from @nogood-nodes@ in @atms.lisp@.
nogoodNodes :: (Debuggable m, NodeDatum d) => i -> [Node d i r s m] -> ATMST s m ()
nogoodNodes informant nodes = do
  contra <- getContradictionNode (nodeATMS (head nodes))
  justifyNode informant contra nodes

-- * Label updating

-- Translated from @propagate@ in @atms.lisp@.
propagate ::
  (Debuggable m, NodeDatum d) =>
    JustRule d i r s m ->
      Maybe (Node d i r s m) ->
        MList s (Maybe (Env d i r s m)) ->
          ATMST s m ()
propagate just antecedent envs = do
  $(dbg [| debugPropagateArgs just antecedent envs |])
  newEnvs <- weave antecedent envs (justAntecedents just)
  when (not (mnull newEnvs)) $ do
    update newEnvs (justConsequence just) (ByRule just)

debugPropagateArgs ::
  (MonadIO m, NodeDatum d) =>
    JustRule d i r s m ->
      Maybe (Node d i r s m) ->
        MList s (Maybe (Env d i r s m)) ->
          ATMST s m ()
debugPropagateArgs justRule antecedent envs = do
  liftIO $ putStrLn "Calling propagate with"
  let atms = nodeATMS $ justConsequence justRule
  liftIO $ putStr ". Just: "
  debug justRule

  case antecedent of
    Just n -> debug n
    Nothing -> liftIO $ putStrLn ". No antecedent"

  envLen <- sttLayer $ mlength envs
  case envLen of
    0 -> liftIO $ putStrLn ". No envs"
    1 -> do
      liftIO $ putStrLn ". Env: "
      envm <- sttLayer $ mcar envs
      case envm of
        Nothing -> liftIO $ putStrLn "<nulled out>"
        Just env -> debug env
    _ -> do
      liftIO $ putStrLn ". Envs:"
      mlistFor_ sttLayer envs $ \em -> do
        liftIO $ putStr "  . "
        case em of
          Just e -> debug e
          Nothing -> liftIO $ putStrLn "<nulled out>"

-- Translated from @update@ in @atms.lisp@.
update ::
  (Debuggable m, NodeDatum d) =>
    MList s (Maybe (Env d i r s m)) ->
      Node d i r s m ->
        Justification d i r s m ->
          ATMST s m ()
update newEnvs consequence just = do
  $(dbg [| debugUpdateArgs newEnvs consequence just |])
  let atms = nodeATMS consequence

  -- If the consequence node is a contradiction, then all we need to
  -- do is mark all of the environments implying it as contradictory
  -- as well.
  ifM (getNodeIsContradictory consequence)
    (mlistFor_ sttLayer newEnvs $ \ envmaybe ->
        case envmaybe of
          Nothing -> return ()
          Just env -> newNogood atms env just) $

    -- Otherwise we propagate further.  If this step prunes out all
    -- `Env`s from the `newEnvs`, then we have nothing further to do.
    do revNewEnvs <- updateLabel consequence newEnvs
       newEnvsRef <- sttLayer $ newSTRef $ revNewEnvs
       ifM (sttLayer $ getMnull newEnvsRef) (return ()) $ do

         -- Process rules queued in the consequence.
         enqueuef <- getEnqueueProcedure atms
         forMM_ (getNodeRules consequence) $ enqueuef

         -- Propagate to the justification rules which might depend on
         -- this node.  If ever the new Env list we are accumulating is
         -- paired down to the empty list, then we can exit these loops.
         forMMwhile_ (getNodeConsequences consequence)
           (sttLayer $ notM $ getMnull newEnvsRef) $ \ supportedJust -> do
             currentNewEnvs <- sttLayer $ readSTRef newEnvsRef
             propagate supportedJust (Just consequence) newEnvs
             mlistForCons_ sttLayer newEnvs $ \ mcons -> do
               thisEnvMaybe <- sttLayer $ mcar mcons
               case thisEnvMaybe of
                 Just thisEnv -> do
                   label <- getNodeLabel consequence
                   unless (elem thisEnv label) $
                     sttLayer $ rplaca mcons Nothing
                 Nothing -> return ()
               cleanedNewEnvs <- sttLayer $ getMlistStripNothing newEnvsRef
               sttLayer $ writeSTRef newEnvsRef cleanedNewEnvs

debugUpdateArgs ::
  (MonadIO m, NodeDatum d) =>
    MList s (Maybe (Env d i r s m)) ->
      Node d i r s m ->
        Justification d i r s m ->
          ATMST s m ()
debugUpdateArgs envs consequence justification = do
  liftIO $ putStrLn "Calling update with"
  envLen <- sttLayer $ mlength envs
  case envLen of
    0 -> liftIO $ putStrLn ". No envs"
    1 -> do
      liftIO $ putStr ". Env: "
      envm <- sttLayer $ mcar envs
      case envm of
        Nothing -> liftIO $ putStrLn "<nulled out>"
        Just env -> debug env
    _ -> do
      liftIO $ putStrLn ". Envs:"
      mlistFor_ sttLayer envs $ \em -> do
        liftIO $ putStr "  . "
        case em of
          Just e -> debug e
          Nothing -> liftIO $ putStrLn "<nulled out>"

  liftIO $ putStr ". Consequence: "
  blurb consequence
  liftIO $ putStrLn ""

  liftIO $ putStr ". Just: "
  case justification of
    ByRule justRule -> debug justRule
    ByAssumption node -> do
      liftIO $ putStr "by assumption "
      pprint node
    ByContradiction -> liftIO $ putStrLn "by contradiction"

-- |Internal method to update the label of this node to include the
-- given environments.  The inclusion is not simply list extension;
-- new environments subsumed by an existing label environment will be
-- omitted, and existing label environments subsumed by a new
-- environment will be removed.
--
-- Translated from @update-label@ in @atms.lisp@.
updateLabel ::
  (Debuggable m, NodeDatum d) =>
    Node d i r s m -> MList s (Maybe (Env d i r s m)) ->
      ATMST s m (MList s (Maybe (Env d i r s m)))
updateLabel node newEnvs = do
  $(dbg [| debugUpdateLabelArgs node newEnvs |])

  -- We will edit the label of this node, so we extract it as a
  -- mutable list, and replace it at the end of this function.
  envsR <- do labels <- getNodeLabel node
              envs <- sttLayer $ fromListMap Just labels
              sttLayer $ newSTRef envs

  -- These two loops traverse respectively the given newEnvs, and the
  -- node label environments, to find pairs of environments where one
  -- of the pair is a subset of the other.
  mlistForCons_ sttLayer newEnvs $ \ newEnvCons -> do
    newEnvCarMaybe <- sttLayer $ mcar newEnvCons
    case newEnvCarMaybe of
      Nothing -> return ()
      Just newEnvCar -> do

        thisEnvs <- sttLayer $ readSTRef envsR
        mlistForCons_ sttLayer thisEnvs $ \ nenvCons -> do
          nenvCarMaybe <- sttLayer $ mcar nenvCons
          case nenvCarMaybe of
            Nothing -> return ()
            Just nenvCar -> do
               case compareEnv newEnvCar nenvCar of
                EQenv -> sttLayer $ rplaca newEnvCons Nothing
                S21env -> sttLayer $ rplaca newEnvCons Nothing
                S12env -> do
                  nodeList <- getEnvNodes nenvCar
                  setEnvNodes nenvCar $ delete node nodeList
                  sttLayer $ rplaca nenvCons Nothing
                DisjEnv -> return ()

        $(dbg [| do liftIO $ putStr " >> pushing onto envs: "
                    blurbMaybeEnv newEnvCarMaybe
                    liftIO $ putStrLn "" |])
        sttLayer $ mlistRefPush newEnvCarMaybe envsR
        $(dbg [| do liftIO $ putStr " >> envs: "
                    blurbMaybeEnvMListRef envsR
                    liftIO $ putStrLn "" |])
        return ()

  -- Strip all `Nothing`s from the `newEnvs`, and add the `node` to
  -- each environment's node list.
  finalNewEnvs <- sttLayer $ mlistStripNothing newEnvs
  mlistFor_ sttLayer finalNewEnvs $ \ newEnvMaybe ->
    case newEnvMaybe of
      Just newEnv -> sttLayer $ push node $ envNodes newEnv  -- [B]
      _ -> return ()

  -- Un-lift the working version of the node label list, and write the
  -- update back to the node label list.
  $(dbg [| do liftIO $ putStr " >> envs: "
              blurbMaybeEnvMListRef envsR
              liftIO $ putStrLn "" |])
  envs <- sttLayer $ readSTRef envsR
  updatedLabel <- sttLayer $ toUnmaybeList envs
  $(dbg [| do liftIO $ putStr " >> updatedLabel: "
              blurbEnvList 10000 "" updatedLabel
              liftIO $ putStrLn "" |])

  -- debugNodeLabel node
  -- sttLayer $ writeSTRef (nodeLabel node) updatedLabel
  setNodeLabel node updatedLabel
  -- debugNodeLabel node

  -- Return the Nothing-stripped version of the newEnvs parameter.
  $(dbg [| debugUpdateLabelFinal node updatedLabel finalNewEnvs |])
  return finalNewEnvs

debugUpdateLabelArgs ::
  (MonadIO m, NodeDatum d) =>
    Node d i r s m -> MList s (Maybe (Env d i r s m)) -> ATMST s m ()
debugUpdateLabelArgs node newEnvs = do
  let atms = nodeATMS node

  liftIO $ putStr "Calling updateLabel with node "
  blurb node
  liftIO $ putStrLn ""

  envLen <- sttLayer $ mlength newEnvs
  case envLen of
    0 -> liftIO $ putStrLn ". No envs"
    1 -> do
      liftIO $ putStr ". Env: "
      envm <- sttLayer $ mcar newEnvs
      case envm of
        Nothing -> liftIO $ putStrLn "<nulled out>"
        Just env -> debug env
    _ -> do
      liftIO $ putStrLn ". Envs:"
      mlistFor_ sttLayer newEnvs $ \em -> do
        liftIO $ putStr "  . "
        case em of
          Just e -> debug e
          Nothing -> liftIO $ putStrLn "<nulled out>"

debugUpdateLabelFinal ::
  (MonadIO m, NodeDatum d) =>
    Node d i r s m -> [Env d i r s m] -> MList s (Maybe (Env d i r s m)) ->
      ATMST s m ()
debugUpdateLabelFinal node labelEnvs newEnvs = do

  case labelEnvs of
    [] -> liftIO $ putStrLn ". No label envs"
    [env] -> do
      liftIO $ putStr ". Single label env: "
      debug env
    _ -> do
      liftIO $ putStrLn ". Final envs:"
      forM_ labelEnvs $ \e -> do
        liftIO $ putStr "  . "
        debug e

  envLen <- sttLayer $ mlength newEnvs
  case envLen of
    0 -> liftIO $ putStrLn ". No final envs"
    1 -> do
      liftIO $ putStr ". Single final env: "
      envm <- sttLayer $ mcar newEnvs
      case envm of
        Nothing -> liftIO $ putStrLn "<nulled out>"
        Just env -> debug env
    _ -> do
      liftIO $ putStrLn ". Final envs:"
      mlistFor_ sttLayer newEnvs $ \em -> do
        liftIO $ putStr "  . "
        case em of
          Just e -> debug e
          Nothing -> liftIO $ putStrLn "<nulled out>"

  debug node

-- |Update the label of node @antecedent@ to include the given @envs@
-- environments, pruning environments which are a superset of another
-- included enviroment.
--
-- Implements Algorithm 12.3 of /Building Problem Solvers/.
--
-- Translated from @weave@ in @atms.lisp@.
weave :: (Debuggable m, NodeDatum d) =>
  Maybe (Node d i r s m) ->
    (MList s (Maybe (Env d i r s m))) ->
      [Node d i r s m] ->
        ATMST s m (MList s (Maybe (Env d i r s m)))
weave antecedent givenEnvs antecedents = {-# SCC "weave.top" #-} do
  $(dbg [| debugWeaveArgs antecedent givenEnvs antecedents |])

  envsRef <- sttLayer $ newSTRef givenEnvs

  forM_ antecedents $ \node ->
    {-# SCC "weave.outer-ants" #-}
    unless (maybe False (node ==) antecedent) $ do
      $(dbg [| debugWeaveNodeAntecedent node |])

      -- From loop to loop we update what's stored under envsRef, so
      -- we start this outer loop by reading what we start off with
      -- there.
      envs <- sttLayer $ readSTRef envsRef

      -- We will update envs with the list built in newEnvs.
      newEnvs <- sttLayer $ newSTRef MNil

      -- We look at all pairs of
      --  - An Env from the passed-in ENVS, plus
      --  - An Env from the NODE's label.
      -- The union of these two is NEW-ENV, and the body of the loop
      -- considers how we should incorporate NEW-ENV into NEW-ENVS.
      {-# SCC "weave.forEnvLoop" #-} mlistFor_ sttLayer envs $ \envmaybe ->
        case envmaybe of
          Nothing -> return ()
          Just env -> do
            {-# SCC "weave.forEnv" #-} forMM_ (sttLayer $ readSTRef $ nodeLabel node) $ \nodeEnv -> do
              $(dbg [| debugWeavePairIntro env nodeEnv |])

              newEnv <- unionEnv env nodeEnv
              $(dbg [| debugWeavePairUnion newEnv |])

              -- We are not interested in nogood environments, so we
              -- skip filing the union if it is nogood.
              unlessM (envIsNogood newEnv) $ do

                -- If NEW-ENV is a superset of (or is equal to)
                -- anything already in NEW-ENVS, then NEW-ENV is
                -- redundant, and we abort the body of the inner
                -- match-searching loop without adding NEW-ENV to
                -- NEW-ENVS.
                --
                -- Otherwise if anything already in NEW-ENVS is a
                -- superset of NEW-ENV, then (1) NEW-ENV makes that
                -- element redundant, and we strip it out of NEW-ENVS;
                -- and (2) we add NEW-ENV to NEW-ENVS.

                addEnv <- sttLayer $ newSTRef True

                oldMCons <- sttLayer $ readSTRef newEnvs
                mlistForConsWhile_ sttLayer oldMCons
                                   (sttLayer $ readSTRef addEnv) $ \ cons ->
                  case cons of
                    MNil -> return () -- Should not be possible
                    mc@(MCons carRef cdrRef) -> do
                      maybeCar <- sttLayer $ readSTRef carRef
                      case maybeCar of
                        Nothing -> return ()
                        Just car ->
                          case compareEnv newEnv car of
                            EQenv  -> sttLayer $ writeSTRef addEnv False
                            S12env -> do
                              $(dbg [| debugWeaveLoopRemovingEnv car |])
                              sttLayer $ rplaca cons Nothing
                            S21env -> sttLayer $ writeSTRef addEnv False
                            DisjEnv -> return ()

                -- If we haven't found newEnv to be redundant, then
                -- add it to newEnvs.
                sttLayer $ whenM (readSTRef addEnv) $ do
                  newMCons <- mlistPush (Just newEnv) oldMCons
                  writeSTRef newEnvs newMCons
                $(dbg [| debugWeaveLoopPairEnd addEnv newEnvs |])

      -- So we have nearly produced the refinement of ENVS for this
      -- NODE in the ANTECEDENTS.  It might have spurious NILs, so we
      -- strip those out and update envsRef.
      preFinalNewEnvs <- sttLayer $ readSTRef newEnvs
      filteredNewEnvs <- sttLayer $ mlistStripNothing preFinalNewEnvs
      sttLayer $ writeSTRef envsRef filteredNewEnvs

  -- Finally, return the last refinement of ENVS.
  result <- sttLayer $ readSTRef envsRef
  $(dbg [| debugWeaveResult result |])
  return result

debugWeaveArgs :: (MonadIO m, NodeDatum d) =>
  Maybe (Node d i r s m) ->
    (MList s (Maybe (Env d i r s m))) ->
      [Node d i r s m] ->
        ATMST s m ()
debugWeaveArgs antecedent givenEnvs antecedents = do
  liftIO $ putStrLn "Calling weave with"
  case antecedent of
    Just n -> debug n
    Nothing -> liftIO $ putStrLn ". No antecedent"
  let atms = case antecedent of
               Just a  -> Just $ nodeATMS a
               Nothing -> case antecedents of
                            a : _ -> Just $ nodeATMS a
                            _ -> Nothing
  case atms of
    Just a -> do
      liftIO $ putStrLn ". Envs:"
      mlistFor_ sttLayer givenEnvs $ \em -> do
        liftIO $ putStr "  . "
        case em of
          Just e -> debug e
          Nothing -> liftIO $ putStrLn "<nulled out>"
        return ()
    _ -> return ()

  liftIO $ putStr ". Antecedents:"
  forM_ antecedents $ \a -> do
    let atms = nodeATMS a
    datumFmt <- getDatumString atms
    liftIO $ putStr $ " " ++ datumFmt (nodeDatum a)
  liftIO $ putStrLn " "

debugWeaveNodeAntecedent antecedent = do
  datumFmt <- getDatumString (nodeATMS antecedent)
  liftIO $ putStrLn $
    " - For node antecedent " ++ datumFmt (nodeDatum antecedent)

debugWeavePairIntro ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> Env d i r s m -> ATMST s m ()
debugWeavePairIntro srcEnv nodeEnv = do
  liftIO $ putStr $ "    - For "
  blurbEnv srcEnv
  liftIO $ putStr $ " from env, "
  blurbEnv nodeEnv
  liftIO $ putStrLn $ " from node label"

debugWeavePairUnion ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
debugWeavePairUnion union = do
  liftIO $ putStr "      Union is "
  blurbEnv union
  liftIO $ putStrLn ""

debugWeaveResult ::
  (MonadIO m, NodeDatum d) => MList s (Maybe (Env d i r s m)) -> ATMST s m ()
debugWeaveResult result = do
  liftIO $ putStr " --> result of weave is "
  blurbMaybeEnvMList result
  liftIO $ putStrLn ""

debugWeaveLoopRemovingEnv ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
debugWeaveLoopRemovingEnv env = do
  liftIO $ putStr "       - Removing from result: env "
  blurbEnv env
  liftIO $ putStrLn ""

debugWeaveLoopPairEnd ::
  (MonadIO m, NodeDatum d) =>
    STRef s Bool -> (STRef s (MList s (Maybe (Env d i r s m)))) -> ATMST s m ()
debugWeaveLoopPairEnd addR envmsR = do
  add <- sttLayer $ readSTRef addR
  liftIO $ putStrLn $ "      Adding union: " ++ (if add then "yes" else "no")
  mlist <- sttLayer $ readSTRef envmsR
  liftIO $ putStr $ "      Updated result to: "
  blurbMaybeEnvMList mlist
  liftIO $ putStrLn ""

-- Translated from @in-antecedent?@ in @atms.lisp@.
isInAntecedent :: (Debuggable m, NodeDatum d) => [Node d i r s m] -> ATMST s m Bool
isInAntecedent [] = return True
isInAntecedent nodes = do
  empty <- getEmptyEnvironment (nodeATMS (head nodes))
  isWeave empty nodes

-- |Check whether any union of antecedent environments is consistent.
--
-- Translated from @weave?@ in @atms.lisp@.
isWeave ::
  (Debuggable m, NodeDatum d) => Env d i r s m -> [Node d i r s m] -> ATMST s m Bool
isWeave _ [] = return True
isWeave env (n : ns) =
  anyMM (\e -> do
            newEnv <- unionEnv e env
            ifM (envIsNogood e) (return False) (isWeave newEnv ns))
        (getNodeLabel n)

-- |Returns `True` if the `Env`ironment argument supports all of the
-- given `Node`s.
--
-- Translated from @supporting-antecedent?@ in @atms.lisp@.
isSupportingAntecedent ::
  (Monad m, NodeDatum d) =>
    [Node d i r s m] -> Env d i r s m -> ATMST s m Bool
isSupportingAntecedent nodes env = allByM (\n -> isInNodeByEnv n env) nodes

-- |Remove a `Node` from the `ATMS`.
--
-- Translated from @remove-node@ in @atms.lisp@.
removeNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()
removeNode node = do
  let atms = nodeATMS node
  whenM (fmap (not . null) $ getNodeConsequences node) $ do
    nodeStr <- getNodeString atms
    exceptLayer $ throwE $
      CannotRemoveNodeWIthConsequences (nodeStr node) (nodeIndex node)

  let nodeRef = atmsNodes atms
   in sttLayer $ readSTRef nodeRef >>= writeSTRef nodeRef . delete node

  forRM_ sttLayer (nodeJusts node) $ \ justification ->
    case justification of
      ByRule justRule -> forM_ (justAntecedents justRule) $ \ ant -> do
        let conseqRef = nodeConsequences ant
          in sttLayer $
               readSTRef conseqRef >>= writeSTRef conseqRef . delete justRule
      _ -> exceptLayer $ throwE $ UnexpectedNonruleJustification

  forRM_ sttLayer (nodeLabel node) $ \ env -> do
    let nodesRef = envNodes env
      in sttLayer $ readSTRef nodesRef >>= writeSTRef nodesRef . delete node

-- * Creating and extending environments.

-- |Create and return a new `Env` for the given assumptions.  Note
-- that this function does not sort or otherwise organize
-- @assumptions@, and it only called with an empty or singleton list.
-- Instead, it is `consEnv` which inserts nodes in order when one
-- environement is defined in terms of another.
--
-- Translated from @create-env@ in @atms.lisp@.
createEnv ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> [Node d i r s m] -> ATMST s m (Env d i r s m)
createEnv atms assumptions = do
  $(dbg [| debugCreateEnvStart assumptions |])
  index <- nextEnvCounter atms
  whyNogood <- sttLayer $ newSTRef Good
  nodes <- sttLayer $ newSTRef []
  rules <- sttLayer $ newSTRef []
  let env = Env index (length assumptions) assumptions nodes whyNogood rules
  $(dbg [| debugCreateEnvEnv env |])
  insertInTable atms (atmsEnvTable atms) env
  $(dbg [| debugCreateEnvEnv env |])
  setEnvContradictory atms env
  $(dbg [| debugCreateEnvEnv env |])
  return env

debugCreateEnvStart ::
  (MonadIO m, NodeDatum d) => [Node d i r s m] -> ATMST s m ()
debugCreateEnvStart nodes = do
  liftIO $ putStrLn $ "             - Running createEnv"
  astr <- formats "<none>" "," nodes
  liftIO $ putStrLn $ "               assumptions " ++ astr

debugCreateEnvEnv ::
  (MonadIO m, NodeDatum d) => (Env d i r s m) -> ATMST s m ()
debugCreateEnvEnv env = do
  liftIO $ putStr $ "               env "
  blurbEnv env
  liftIO $ putStrLn ""

-- Translated from @union-env@ in @atms.lisp@.
unionEnv ::
  (Debuggable m, NodeDatum d) =>
    Env d i r s m -> Env d i r s m -> ATMST s m (Env d i r s m)
unionEnv e1 e2 =
  if envCount e1 > envCount e2 then unionEnv' e2 e1 else unionEnv' e1 e2
  where unionEnv' e1 e2 = do
          $(dbg [| debugUnionEnvStart e1 e2 |])
          acc <- sttLayer $ newSTRef e2
          forMwhile_ (envAssumptions e1)
                     (do thisE2 <- sttLayer $ readSTRef acc
                         notM $ envIsNogood thisE2) $ \assume -> do
            oldE2 <- sttLayer $ readSTRef acc
            $(dbg [| debugUnionEnvLoopStart assume oldE2 |])
            newE2 <- consEnv assume oldE2
            $(dbg [| debugUnionEnvLoopCons newE2 |])
            sttLayer $ writeSTRef acc newE2
          result <- sttLayer $ readSTRef acc
          $(dbg [| debugUnionEnvResult result |])
          return result

debugUnionEnvStart ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> Env d i r s m -> ATMST s m ()
debugUnionEnvStart e1 e2 = do
  liftIO $ putStr "       - Starting unionEnv' with "
  blurbEnv e1
  liftIO $ putStr "; "
  blurbEnv e2
  liftIO $ putStrLn ""

debugUnionEnvLoopStart ::
  (MonadIO m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m ()
debugUnionEnvLoopStart node e2 = do
  datumFmt <- getDatumString $ nodeATMS node
  liftIO $ putStrLn $ "         - Running loop with"
  liftIO $ putStrLn $ "           node " ++ datumFmt (nodeDatum node)
  liftIO $ putStr "           env "
  blurbEnv e2
  liftIO $ putStrLn ""

debugUnionEnvLoopCons ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
debugUnionEnvLoopCons e = do
  liftIO $ putStr "           consEnv returns "
  blurbEnv e
  liftIO $ putStrLn ""

debugUnionEnvResult ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
debugUnionEnvResult result = do
  liftIO $ putStr "         unionEnv returns "
  blurbEnv result
  liftIO $ putStrLn ""


-- |Derive an environment from the addition of one additional
-- assumption to a previous `Env`'s assumption list.
--
-- Translated from @cons-env@ in @atms.lisp@.
consEnv ::
  (Debuggable m, NodeDatum d) =>
    Node d i r s m -> Env d i r s m -> ATMST s m (Env d i r s m)
consEnv assumption env = do
  $(dbg [| debugConsEnvStart assumption env |])

  let nassumes = orderedInsert assumption (envAssumptions env) assumptionOrder
  $(dbg [| debugConsEnvInserted nassumes |])

  envByLookup <- lookupEnv nassumes
  $(dbg [| debugConsEnvLookup envByLookup |])
  maybe (createEnv (nodeATMS assumption) nassumes) (return . id) envByLookup

debugConsEnvStart ::
  (MonadIO m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m ()
debugConsEnvStart node e2 = do
  datumFmt <- getDatumString $ nodeATMS node
  liftIO $ putStrLn $ "         - Running consEnv"
  liftIO $ putStrLn $ "           inserting node " ++ datumFmt (nodeDatum node)
  liftIO $ putStr "           into env "
  blurbEnv e2
  liftIO $ putStrLn ""

debugConsEnvInserted ::
  (MonadIO m, NodeDatum d) => [Node d i r s m] -> ATMST s m ()
debugConsEnvInserted nodes =
  case nodes of
    [] -> liftIO $ putStrLn "           list after insertion: empty list"
    (n : _) -> do
      datumFmt <- getDatumString $ nodeATMS n
      liftIO $ putStrLn $
        "           list after insertion: ["
        ++ intercalate ", " (map (datumFmt . nodeDatum) nodes)
        ++ "]"

debugConsEnvLookup ::
  (MonadIO m, NodeDatum d) => Maybe (Env d i r s m) -> ATMST s m ()
debugConsEnvLookup Nothing =
  liftIO $ putStrLn $ "           lookup gives Nothing"
debugConsEnvLookup (Just env) = do
  liftIO $ putStr $ "           lookup gives "
  blurbEnv env
  liftIO $ putStrLn ""

-- |Return the `Env`ironment containing the given list of `Node`s,
-- creating one if necessary.
--
-- Translated from @find-or-make-env@ in @atms.lisp@.
findOrMakeEnv ::
  (Debuggable m, NodeDatum d) =>
    [Node d i r s m] -> ATMS d i r s m -> ATMST s m (Env d i r s m)
findOrMakeEnv [] atms = getEmptyEnvironment atms
findOrMakeEnv assumptions atms = do
  check <- lookupEnv assumptions
  case check of
    Nothing -> createEnv atms assumptions
    Just env -> return env

-- * Env tables.

-- Translated from @insert-in-table@ in @atms.lisp@.
insertInTable ::
  (Monad m, NodeDatum d) =>
    ATMS d i r s m -> STRef s (EnvTable d i r s m) -> Env d i r s m ->
      ATMST s m ()
insertInTable atms tableRef env = do
  let count = envCount env
  EnvTable currentTable <- sttLayer $ readSTRef tableRef
  let (_, alloc) = boundsSTArray currentTable

  -- Re-allocate the array if it needs to grow, and update the
  -- reference.
  when (alloc < count) $ do
    incr <- getEnvTableIncr
    let newAlloc = count + incr
    sttLayer $ do
      newArray <- newSTArray (0, newAlloc) []
      forM_ [1..alloc] $ \i -> do
        envs <- readSTArray currentTable i
        writeSTArray newArray i envs
      writeSTRef tableRef $ EnvTable newArray

  -- Add the env to its slot in the table.
  sttLayer $ do
    EnvTable array <- readSTRef tableRef
    oldEnvs <- readSTArray array count
    writeSTArray array count $ env : oldEnvs

-- Translated from @lookup-env@ in @atms.lisp@.
lookupEnv ::
  (Monad m, NodeDatum d) =>
    [Node d i r s m] -> ATMST s m (Maybe (Env d i r s m))
lookupEnv [] = return Nothing
lookupEnv assumptions@(a : _) = do
  let atms = nodeATMS a
      ns = sortOn nodeIndex assumptions
  EnvTable envTable <- sttLayer $ readSTRef $ atmsEnvTable atms
  entries <- sttLayer $ readSTArray envTable $ length ns
  case filter (\x -> {-# SCC "lookupEnv.pred" #-} envAssumptions x == ns) entries of
    [] -> return Nothing
    (x : _) -> return $ Just x

-- Translated from @subset-env?@ in @atms.lisp@.
isSubsetEnv :: (Monad m, NodeDatum d) => Env d i r s m -> Env d i r s m -> Bool
isSubsetEnv e1 e2 =
  if e1 == e2 then True
  else if envCount e1 > envCount e2 then False
  else ordSubsetp (envAssumptions e1) (envAssumptions e2)

-- |The possible results of comparing two `Env`s.
data EnvCompare =
  EQenv     -- ^ Two `Env`s are the same
  | S12env  -- ^ The first `Env` is a subset of the second.
  | S21env  -- ^ The second `Env` is a subset of the first.
  | DisjEnv -- ^ Two `Env`s are disjoint.

-- Translated from @compare-env@ in @atms.lisp@.
compareEnv ::
  (Monad m, NodeDatum d) => Env d i r s m -> Env d i r s m -> EnvCompare
compareEnv e1 e2 =
  if e1 == e2
  then EQenv
  else if envCount e1 < envCount e2
       then if nodeListIsSubsetEq (envAssumptions e1) (envAssumptions e2)
            then S12env
            else DisjEnv
       else if nodeListIsSubsetEq (envAssumptions e2) (envAssumptions e1)
            then S21env
            else DisjEnv

-- |Return true if the first sorted (by `Env` index) node list is a
-- subset of the second.
nodeListIsSubsetEq ::
  (Monad m, NodeDatum d) => [Node d i r s m] -> [Node d i r s m] -> Bool
nodeListIsSubsetEq [] _ = True
nodeListIsSubsetEq _ [] = False
nodeListIsSubsetEq l1@(x : xs) (y : ys) =
  case nodeIndex x `compare` nodeIndex y of
    LT -> False
    EQ -> nodeListIsSubsetEq xs ys
    GT -> nodeListIsSubsetEq l1 ys
-- * Processing nogoods

-- Translated from @new-nogood@ in @atms.lisp@.
newNogood ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> Env d i r s m -> Justification d i r s m -> ATMST s m ()
newNogood atms cenv why = do
  $(dbg [| debugNewNogoodStart cenv why |])

  -- Record in `cenv` the reason why `cenv` is nogood.
  sttLayer $ writeSTRef (envWhyNogood cenv) (ByJustification why)

  -- `cenv` can no longer be used in node labels, so remove it from
  -- any node labels in which it appears, and propagate out any
  -- changes.
  removeEnvFromLabels cenv atms

  -- Add `cenv` to the ATMS table of nogoods.
  insertInTable atms (atmsNogoodTable atms) cenv

  -- Remove any nogood table entries made redundant by `cenv`.
  let cenvCount = envCount cenv
  EnvTable nogoodTable <- getNogoodTable atms
  forM_ [1 .. cenvCount - 1] $ \ i -> do
    entry <- sttLayer $ readSTArray nogoodTable i
    sttLayer $ writeSTArray nogoodTable i $
      filter (not . isSubsetEnv cenv) entry

  -- Find currently-non-nogood environments which are supersets of the
  -- nogood, and process them as nogoods.
  EnvTable envTable <- getEnvTable atms
  let (_, maxCount) = boundsSTArray envTable
  forM_ [cenvCount + 1, maxCount] $ \ i -> do
    entry <- sttLayer $ readSTArray envTable i
    forM_ entry $ \ old -> do
      isNogood <- envIsNogood old
      when (isNogood && isSubsetEnv cenv old) $ do
        sttLayer $ writeSTRef (envWhyNogood old) (ByEnv cenv)
        removeEnvFromLabels old atms

debugNewNogoodStart ::
  (MonadIO m, NodeDatum d) =>
    Env d i r s m -> Justification d i r s m -> ATMST s m ()
debugNewNogoodStart cenv why = do
  liftIO $ putStr "Starting newNogood with "
  debug cenv
  format why >>= (liftIO . putStrLn)


-- Translated from @set-env-contradictory@ in @atms.lisp@.
setEnvContradictory ::
  (Debuggable m, NodeDatum d) => ATMS d i r s m -> Env d i r s m -> ATMST s m ()
setEnvContradictory atms env = do
  $(dbg [| setEnvContradictoryStart env |])
  ifM (envIsNogood env)
    (do $(dbg [| liftIO $ putStr "                 Already nogood \n" |])
        return ()) $ do
    let count = envCount env
    EnvTable nogoodTableArray <- sttLayer $ readSTRef $ atmsNogoodTable atms
    forM_ [1..count] $ \i -> do
      continueLoop <- sttLayer $ newSTRef True
      $(dbg [| setEnvContradictoryStartOuter i |])
      forMMwhile_ (sttLayer $ readSTArray nogoodTableArray i)
                  (sttLayer $ readSTRef continueLoop) $ \cenv -> do
        $(dbg [| setEnvContradictoryStartInner cenv |])
        when (isSubsetEnv cenv env) $ do
          $(dbg [| setEnvContradictoryStartInnerWhen cenv env |])
          sttLayer $ do
            writeSTRef (envWhyNogood env) $ ByEnv cenv
            writeSTRef continueLoop False

setEnvContradictoryStart ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
setEnvContradictoryStart e = do
  liftIO $ putStr "               - Running setEnvContradictory with "
  blurbEnv e
  liftIO $ putStrLn ""

setEnvContradictoryStartOuter ::
  (MonadIO m) => Int -> ATMST s m ()
setEnvContradictoryStartOuter i = do
  liftIO $ putStrLn $ ("                 Starting outer loop for "
                       ++ show i
                       ++ "-length envs")

setEnvContradictoryStartInner ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
setEnvContradictoryStartInner cenv = do
  liftIO $ putStr "                   Starting inner loop with nogood env "
  blurbEnv cenv
  liftIO $ putStrLn ""

setEnvContradictoryStartInnerWhen ::
  (MonadIO m, NodeDatum d) => Env d i r s m -> Env d i r s m -> ATMST s m ()
setEnvContradictoryStartInnerWhen cenv env = do
  liftIO $ putStr "                   Nogood "
  blurbEnv cenv
  liftIO $ putStr " is subset of "
  blurbEnv env
  liftIO $ putStrLn ", marking latter nogood"

-- Translated from @remove-env-from-labels@ in @atms.lisp@.
removeEnvFromLabels ::
  (Monad m, NodeDatum d) => Env d i r s m -> ATMS d i r s m -> ATMST s m ()
removeEnvFromLabels env atms = do
  -- Run all rules associated with `env`, and clear the list of
  -- associated rules.
  enqueuef <- getEnqueueProcedure atms
  forMM_ (getEnvRules env) $ \ rule -> do
    enqueuef rule
  setEnvRules env []

  -- Remove `env` from the label of the nodes currently including it.
  forMM_ (getEnvNodes env) $ \ node -> do
    oldLabel <- getNodeLabel node
    setNodeLabel node $ delete env oldLabel

-- * Interpretation construction

-- |Return the minimum environments which give the `ATMS` belief in
-- the given choice sets.  The choice sets are essentially
-- conjunctive-normal form expressions; in the list of sublists of
-- nodes, under each environment in the result at least one node of
-- each sublist will be believed.
--
-- This function is for the case where no nodes are taken as defaults;
-- here we simply call `interpretationsWithDefaults` with an empty
-- list of defaults.
interpretations ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> [[Node d i r s m]] -> ATMST s m [Env d i r s m]
interpretations atms choiceSets = do
  $(dbg [| do formatss' choiceSets >>=
                liftIO . putStrLn . (++) "Called interpretations with "
         |])
  interpretationsWithDefaults atms choiceSets []

-- |Initial setup for @interpretations@: convert the @choiceSets@ over
-- `Node`s into structures over the nodes' labelling `Env`ironments,
-- and set up the outermost loop.
--
-- Translated from these @interpretations@ in @atms.lisp@.
--
-- > (defun interpretations (atms choice-sets &optional defaults
-- >                    &aux solutions)
-- >   (let ( ;; ...
-- >         (choice-sets (mapcar ;; Call to altSetToEnvList
-- >                              choice-sets)))
-- >     ;; First call interpsStartPrep for this loop
-- >     (dolist (choice (car choice-sets))
-- >       ;; ...
-- >       )
-- >     ;; Then continuation is afterDepthSolutions for
-- >     ;; cleanup and extend-via-defaults.
interpretationsWithDefaults ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> [[Node d i r s m]] -> [Node d i r s m] ->
      ATMST s m [Env d i r s m]
interpretationsWithDefaults atms choiceSets defaults = do
  $(dbg [| do str <- formatss' choiceSets
              liftIO $ putStr $ "- Refining choice sets " ++ str ++ "\n" |])
  choiceSetEnvLists <- mapM (altSetToEnvList atms) choiceSets
  $(dbg [| do liftIO $ putStrLn $ "  Refined choice sets to environment lists:"
              formatss' choiceSetEnvLists >>=
                (liftIO . putStrLn . (++) "    ") |])

  let cntn = afterDepthSolutions atms choiceSetEnvLists defaults return
  case choiceSetEnvLists of
    [] -> cntn []
    (cse:choiceSetEnvLists) ->
      interpsForOneAlternative atms cse choiceSetEnvLists cntn []

-- |Convert a `Node` passed in a choice-set of `interpretations` into
-- the list of `Env`ironments in the label of that node.
--
-- Translated from the lambda expression of the @MAPCAR@ in this
-- portion of @interpretations@ in @atms.lisp@:
--
-- >   (let ( ;; ...
-- >         (choice-sets
-- >           (mapcar #'(lambda (alt-set)
-- >                       (format *trace-output*
-- >                           "~%  - ~a --> ???" alt-set)
-- >                       (let ((result
-- >                              (mapcan #'(lambda (alt)
-- >                                          (format *trace-output*
-- >                                              "~%    - ~a --> ~a"
-- >                                              alt (tms-node-label alt))
-- >                                          (copy-list (tms-node-label alt)))
-- >                                      alt-set)))
-- >                         (format *trace-output*
-- >                             "~%    ~a --> ~a" alt-set result)
-- >                         result))
-- >                   choice-sets)))
altSetToEnvList ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> [Node d i r s m] -> ATMST s m [Env d i r s m]
altSetToEnvList atms nodes = do
  mapped <- mapM getNodeLabel nodes
  $(dbg [| do s1 <- formats' nodes
              s2 <- formatss' mapped
              liftIO $ putStrLn $ "  - " ++ s1 ++ " --> " ++ s2 |])
  return $ foldl (++) [] mapped

-- |The body of @interpretations@ is translated from the Lisp in a
-- continuation-passing style; this type is a shorthand for the common
-- last two argument and result types of the continuation-processing
-- functions.
type ChoiceSetCntn d i r s m =
  ([Env d i r s m] -> ATMST s m [Env d i r s m]) ->
    [Env d i r s m] ->
      ATMST s m [Env d i r s m]

-- Control, and one pass through the body, of the loop in
-- @interpretations@ (in file @atms.lisp@) in the context:
--
-- > (defun interpretations (atms choice-sets &optional defaults
-- >                              &aux solutions)
-- >   ...
-- >   (let ((*solutions* nil)
-- >         (choice-sets ...))
-- >     (dolist (choice (car choice-sets)) ;; This loop
--
-- Aside from debugging tracing, the body of the loop just calls
-- @getDepthSolutions@ for the first element of the list of choice
-- sets.  The continuation of the @getDepthSolutions@ call is a
-- recursive call to this function on the remainder of the choice sets
-- list.
interpsForOneAlternative ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> [Env d i r s m] -> [[Env d i r s m]] ->
      ChoiceSetCntn d i r s m
interpsForOneAlternative atms [] choiceSetEnvLists k solutions = do
  $(dbg [| liftIO $ putStrLn "- Completed calls to getDepthSolutions" |])
  k solutions
interpsForOneAlternative atms (env : envs) choiceSetEnvLists k solutions = do
  getDepthSolutions atms env choiceSetEnvLists
                    (interpsForOneAlternative atms envs choiceSetEnvLists k)
                    solutions

-- |Translation of @get-depth-solutions1@.  This function operates a
-- depth-first traversal over possible solutions.  Each choice set in
-- the @choice-sets@ argument could contribute @N@ different possible
-- next-steps to building a solution; the original Lisp function
-- contains multiple self-recursive calls, one for each of these
-- possible steps.  At the end of a sequence of recursive calls, one
-- construction step per choice set, the base case received a
-- constructed candidate solution.  The base case considers adding a
-- to a global list of found solutions, possibly removing previous
-- solution elements made redundant by the new solution.
--
-- The translation, like the rest of the translation of
-- @interpretations@, is in continuation-passing style.  Rather than a
-- global variable of solutions, the continuation receives the
-- solutions-to-date-list as its final argument.  Rather than multiple
-- recursive calls which might mutate a global list, there are
-- extensions of the continuation which might manipulate the solutions
-- list they are eventually passed.  The test of a constructed
-- candidate still occurs when the search reaches a leaf at a fully
-- constructed candidate, and calls its continuation with its
-- transformation of the solutions list.
--
-- > ;; In atms.lisp
-- > (defun get-depth-solutions1 (solution choice-sets &aux new-solution)
-- >   (cond
-- >     ((null choice-sets)
-- >      (unless (do ((old-solutions *solutions* (cdr old-solutions)))
-- >                  ((null old-solutions))
-- >                (when (car old-solutions)
-- >                  (case (compare-env (car old-solutions) solution)
-- >                    ((:EQ :S12) (return t))
-- >                    (:S21 (rplaca old-solutions nil)))))
-- >        (push solution *solutions*)))
-- >     ((env-nogood? solution)) ;something died.
-- >     (t (dolist (choice (car choice-sets))
-- >          (setq new-solution (union-env solution choice))
-- >          (unless (env-nogood? new-solution)
-- >            (get-depth-solutions1 new-solution (cdr choice-sets)))))))
getDepthSolutions ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> Env d i r s m -> [[Env d i r s m]] ->
      ChoiceSetCntn d i r s m
getDepthSolutions atms cand [] k solns = do
  $(dbg [| formats' solns >>=
             liftIO . putStrLn . (++) "    getDepthSolutions => "
         |])
  let filtered = filterWithNewSoln cand solns
  $(dbg [| formats' filtered >>= liftIO . putStrLn . (++) "    filtered "
         |])
  k filtered
getDepthSolutions atms partial (cs : css) k solns = do
  $(dbg [| do format partial >>= liftIO . putStrLn .
                (++) "- Calling getDepthSolutions with partial solution "
              formats' cs >>= liftIO . putStrLn . (++) "    choice sets "
              formats' solns >>= liftIO . putStrLn . (++) "    initial solns "
         |])
  getDepthSolutionsFor atms partial cs css k solns

-- |One pass through the body of the @getDepthSolutions$ loop.
getDepthSolutionsFor ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> Env d i r s m -> [Env d i r s m] -> [[Env d i r s m]] ->
      ChoiceSetCntn d i r s m
getDepthSolutionsFor atms    _    []      _  k solns = do
  $(dbg [| formats' solns >>=
             liftIO . putStrLn . (++) "    getDepthSolutionsFor => " |])
  k solns
getDepthSolutionsFor atms partial (c:cs) css k solns = do
  $(dbg [| do format c >>= liftIO . putStrLn .
                (++) "- Calling getDepthSolutionsFor with first choice "
              formats' cs >>= liftIO . putStrLn . (++) "    other choices "
              formatss' css >>=
                liftIO . putStrLn . (++) "    other choice sets "
              formats' solns >>= liftIO . putStrLn . (++) "    initial solns "
         |])
  let k' = getDepthSolutionsFor atms partial cs css k
           -- To try the next alternative of this choice set
  newPartial <- unionEnv partial c
  ifM (envIsNogood newPartial)
      (do ($(dbg [| do format newPartial >>= liftIO . putStrLn .
                         (++) "    nogood from unionEnv "
                  |]))
          k' solns)
      (do ($(dbg [| do format partial >>= liftIO . putStrLn .
                         (++) "    continuing with "
                  |]))
          (getDepthSolutions atms newPartial css k' solns))

-- |Implementation of the list manipulation achieved in the DO-loop at:
--
-- > ;; In atms.lisp
-- > (defun get-depth-solutions1 (solution choice-sets &aux new-solution)
-- >   (cond
-- >     ((null choice-sets)
-- >      (unless (do ((old-solutions *solutions* (cdr old-solutions)))
-- >                  ((null old-solutions))
--
-- The purpose is to add a new solution to a list of solutions.  But
-- first the solution must be tested against existing solution to find
-- cases where the new one is nondisjoint from some old one(s).  If
-- the new solution is smaller than an old, then the old is redundant
-- and should be pruned.  If the old solution is a subset of the new
-- solution, then the new one is redundant and need not be added to
-- the solutions list at all.
filterWithNewSoln ::
  (Monad m, NodeDatum d) => Env d i r s m -> [Env d i r s m] -> [Env d i r s m]
filterWithNewSoln env envs =
  let (redundant, _, envs') = filterWithNewSoln' env envs
  in if redundant then envs' else env : envs'

filterWithNewSoln' ::
  (Monad m, NodeDatum d) => Env d i r s m -> [Env d i r s m] ->
    (Bool, Bool, [Env d i r s m])
filterWithNewSoln' _ [] = (False, False, [])
filterWithNewSoln' e solns@(s:ss) =
  case compareEnv s e of
    EQenv -> (True, False, solns)
    S12env -> (True, False, solns)
    S21env -> let (r, c, ss') = filterWithNewSoln' e ss
              in (r, True, ss')
    DisjEnv -> let (r, c, ss') = filterWithNewSoln' e ss
               in if c
                  then (r, c, s:ss')
                  else (r, c, solns)

-- TO BE TRANSLATED from @interpretations@ in @atms.lisp@.
--
-- > ;; In atms.lisp
-- > (proclaim '(special *solutions*))
-- > (defun interpretations (atms choice-sets &optional defaults
-- >                    &aux solutions)
-- >   (if (atms-debugging atms)
-- >    (format *trace-output*
-- >       "~%Constructing interpretations depth-first for ~a:" choice-sets))
-- >   (format *trace-output* "~%- Refining choice sets")
-- >   (let ((*solutions* nil)
-- >    (choice-sets
-- >      (mapcar #'(lambda (alt-set)
-- >                  (format *trace-output*
-- >                      "~%  - ~a --> ???" alt-set)
-- >                  (let ((result
-- >                         (mapcan #'(lambda (alt)
-- >                                     (format *trace-output*
-- >                                         "~%    - ~a --> ~a"
-- >                                         alt (tms-node-label alt))
-- >                                     (copy-list (tms-node-label alt)))
-- >                                 alt-set)))
-- >                    (format *trace-output*
-- >                        "~%    ~a --> ~a" alt-set result)
-- >                    result))
-- >              choice-sets)))
-- >     (format *trace-output* "~%  Refined choice sets to ~a" choice-sets)
-- >     (dolist (choice (car choice-sets))
-- >       (format *trace-output*
-- >      "~%- Calling depth-solutions with choice ~a" choice)
-- >       (format *trace-output*
-- >      "~%                               choice sets ~a" (car choice-sets))
-- >       (get-depth-solutions1 choice (cdr choice-sets))
-- >       (format *trace-output*
-- >      "~%      => solutions ~a" *solutions*))
-- >     (setq *solutions* (delete nil *solutions* :TEST #'eq))
-- >     (unless *solutions*
-- >       (if choice-sets (return-from interpretations nil)
-- >                  (setq *solutions* (list (atms-empty-env atms)))))
-- >     (when defaults
-- >       (setq solutions *solutions* *solutions* nil)
-- >       (dolist (solution solutions)
-- >    (extend-via-defaults solution defaults defaults)))
-- >     (delete nil *solutions* :TEST #'eq)))

afterDepthSolutions ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> [[Env d i r s m]] -> [Node d i r s m] ->
      ChoiceSetCntn d i r s m
afterDepthSolutions atms choiceSets defaults k solutions =
  if (null solutions)
  then if (null choiceSets)
       then do
         empty <- getEmptyEnvironment atms
         extendSolutionsIfDefaults atms defaults k [empty]
       else return []
  else extendSolutionsIfDefaults atms defaults k solutions

extendSolutionsIfDefaults ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> [Node d i r s m] -> ChoiceSetCntn d i r s m
extendSolutionsIfDefaults atms [] k solns = k solns
extendSolutionsIfDefaults atms defaults k solns =
  extendSolutionsViaDefaults atms solns defaults k []

extendSolutionsViaDefaults ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> [Env d i r s m] -> [Node d i r s m] ->
      ChoiceSetCntn d i r s m
extendSolutionsViaDefaults atms [] defaults k = k
extendSolutionsViaDefaults atms (s:ss) defaults k =
  extendViaDefaults atms s defaults defaults
                    (extendSolutionsViaDefaults atms ss defaults k)

-- |TO BE TRANSLATED from @extend-via-defaults@ in @atms.lisp@.
--
-- > ;; In atms.lisp
-- > (defun extend-via-defaults (solution remaining original)
-- >   (do ((new-solution)
-- >        (defaults remaining (cdr defaults)))
-- >       ((null defaults)
-- >        (or (member solution *solutions* :TEST #'eq)
-- >       (dolist (default original)
-- >         (or (member default (env-assumptions solution)
-- >                     :TEST #'eq)
-- >             (env-nogood? (cons-env default solution))
-- >             (return t)))
-- >       (push solution *solutions*)))
-- >     (setq new-solution (cons-env (car defaults) solution))
-- >     (unless (env-nogood? new-solution)
-- >       (extend-via-defaults new-solution (cdr defaults) original))))
extendViaDefaults ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> Env d i r s m -> [Node d i r s m] -> [Node d i r s m] ->
      ChoiceSetCntn d i r s m
extendViaDefaults atms baseSoln remaining original k solutions =
  extendViaDefaultsLoop atms baseSoln remaining original k solutions

extendViaDefaultsLoop ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> Env d i r s m -> [Node d i r s m] -> [Node d i r s m] ->
      ChoiceSetCntn d i r s m
extendViaDefaultsLoop atms candSoln [] original k solutions = do

  --  TODO Check (member solution *solutions* :TEST #'eq)
  --

  checkExtendedSoln atms candSoln original k solutions
extendViaDefaultsLoop atms baseSoln (d:ds) original k solutions = do
  newSoln <- consEnv d baseSoln
  let nextLoop = extendViaDefaultsLoop atms baseSoln ds original k
  ifM (envIsNogood newSoln)
    (nextLoop solutions)
    (extendViaDefaultsLoop atms newSoln ds original nextLoop solutions)

checkExtendedSoln ::
  (Debuggable m, NodeDatum d) =>
    ATMS d i r s m -> Env d i r s m -> [Node d i r s m] ->
      ChoiceSetCntn d i r s m
checkExtendedSoln atms candSoln [] k solutions = k $ candSoln : solutions
checkExtendedSoln atms candSoln (orig:origs) k solutions =
  if (elem orig (envAssumptions candSoln))
  then k solutions
  else do
    allEnv <- consEnv orig candSoln
    ifM (envIsNogood allEnv)
        (k solutions)
        (checkExtendedSoln atms candSoln origs k solutions)


-- * Generating explanations

-- |This function returns a list of justifications which form a
-- directed acyclic graph (DAG) for the derivation. This is quite
-- complicated because this is really a simple consequent JTMS.
--
-- Translated from @explain-node@ in @atms.lisp@.
explainNode ::
  (Monad m, NodeDatum d) =>
    Node d i r s m -> Env d i r s m -> ATMST s m [Explanation d i r s m]
explainNode node env = explainNode1 env node [] []

-- Translated from @explain-node-1@ in @atms.lisp@.
--
-- > ;; In atms.lisp
-- > (defun explain-node-1 (env node queued-nodes explanation)
-- >   (cond ((member node queued-nodes) nil)
-- >    ((and (tms-node-assumption? node)
-- >          (member node (env-assumptions env)))
-- >     (cons (cons 'ASSUME node) explanation))
-- >    ((dolist (just explanation)
-- >       (if (if (listp just)
-- >               (eq (cdr just) node) (eq (just-consequence just) node))
-- >           (return explanation))))
-- >    (t (setq queued-nodes (cons node queued-nodes))
-- >       (dolist (just (tms-node-justs node))
-- >         (unless (dolist (a (just-antecedents just))
-- >                   (unless (in-node? a env) (return t)))
-- >          (let ((new-explanation explanation))
-- >            (dolist (a (just-antecedents just)
-- >                       (return-from explain-node-1
-- >                         (cons just new-explanation)))
-- >              (setq new-explanation
-- >                    (explain-node-1 env a queued-nodes new-explanation))
-- >              (unless new-explanation (return nil)))))))))
explainNode1 ::
  (Monad m, NodeDatum d) =>
    Env d i r s m -> Node d i r s m -> [Node d i r s m] ->
      [Justification d i r s m] ->
        ATMST s m [Explanation d i r s m]
explainNode1 = error "< TODO unimplemented explainNode1 >"

-- |Print the justifying `Env`ironments which label a `Node`.
--
-- Translated from @why-node@ in @atms.lisp@.
whyNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
whyNode node = do
  let atms = nodeATMS node
  datumStr <- getDatumString atms
  liftIO $ putStr $ "<" ++ datumStr (nodeDatum node)
  forMM_ (getNodeLabel node) envString
  liftIO $ putStrLn ">"

-- |Print the justifying `Env`ironments which label each `Node` of an
-- `ATMS`.
--
-- Translated from @why-nodes@ in @atms.lisp@.
whyNodes :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
whyNodes atms = do
  nodes <- getNodes atms
  forM_ nodes whyNode

-- |Print a `Node`'s justifications.
--
-- TO BE TRANSLATED from @node-justifications@ in @atms.lisp@.
--
-- > ;; In atms.lisp
-- > (defun node-justifications (node &optional (stream t))
-- >   (format t "~% For ~A:" (node-string node))
-- >   (dolist (j (tms-node-justs node))
-- >     (print-justification j stream)))
nodeJustifications ::
  (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
nodeJustifications node = do
  nodeStr <- nodeString node
  liftIO $ putStr $ " For " ++ nodeStr ++ ":"
  justs <- getNodeJusts node
  forM_ justs pprint

-- |Retrieve an `ATMS`'s `Env`ironment with the given index number.
--
-- Translated from @e@ in @atms.lisp@.
--
-- > ;; In atms.lisp
-- > (defun e (atms n)
-- >   (dolist (bucket (atms-env-table atms))
-- >     (dolist (env (cdr bucket))
-- >     (if (= (env-index env) n) (return-from e env)))))
e :: (Monad m, NodeDatum d) =>
  ATMS d i r s m -> Int -> ATMST s m (Maybe (Env d i r s m))
e atms i = do
  table <- getEnvTable atms
  findInEnvTable (\env -> envIndex env == i) table

-- |Convert an `Env`ironment into a string listing the nodes of the
-- environment.
--
-- Translated from @env-string@ in @atms.lisp@.
envString :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
envString env = do
  let assumptions = envAssumptions env
  unless (null assumptions) $ do
    printer <- getNodeString (nodeATMS (head assumptions))
    liftIO $ putStr $ intercalate ", " (map printer assumptions)

-- * Printing global data

-- |List the nogood `Env`ironments of an `ATMS`.
--
-- Translated from @print-nogoods@ in @atms.lisp@.
printNogoods :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
printNogoods atms = getNogoodTable atms >>= \table -> pprint table

-- |Print the `Env`ironments of an `ATMS`.
--
-- Translated from @print-envs@ in @atms.lisp@.
printEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
printEnvs atms = getEnvTable atms >>= \table -> pprint table

-- |Print statistics about an `ATMS`.
--
-- Translated from @print-atms-statistics@ in @atms.lisp@.
printAtmsStatistics ::
  (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
printAtmsStatistics atms = do
  liftIO $ putStrLn $ "Env table: "
  printEnvs atms
  liftIO $ putStrLn $ "Nogood table: "
  printNogoods atms

-- |Give a verbose printout of the `Node`s of an `ATMS`.
debugNodes :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
debugNodes atms = do
  nodes <- getNodes atms
  liftIO $ putStrLn $ show (length nodes) ++ " nodes:"
  forM_ (reverse nodes) debug

-- |Computation returning a one-line summary of the label of a `Node`
-- of an `ATMS`.
formatNodeLabel :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String
formatNodeLabel node = do
  label <- getNodeLabel node
  case label of
    [] -> return "empty"
    _ -> formatss "<none>" "; " "<none>" "," $ map envAssumptions label

-- |Give a verbose printout of the `Just`ification rules of an
-- `ATMS`.
debugJusts :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
debugJusts atms = do
  justs <- getJusts atms
  let len = length justs
  liftIO $ putStrLn $ show len ++ " justification structure"
    ++ (if len == 1 then "" else "s") ++ ":"
  forM_ (sortOn justIndex justs) $ debug

-- |Computation returning a one-line summary of the informant of a
-- `Just`ification rule of an `ATMS`.
formatJustInformant ::
  (Monad m, NodeDatum d) => JustRule d i r s m -> ATMST s m String
formatJustInformant rule = do
  informantFmt <- getInformantString $ nodeATMS $ justConsequence rule
  return $ informantFmt $ justInformant rule

-- |Give a verbose printout of the `Env`ironments of an `ATMS`.
debugAtmsEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
debugAtmsEnvs atms = do
  liftIO $ putStrLn "Environments:"
  envTable <- getEnvTable atms
  debugEnvTable atms envTable

-- |Print a short summary of a mutable list of nullable (via `Maybe`)
-- `Env`ironments from an `ATMS`.
blurbMaybeEnvMList ::
  (MonadIO m, NodeDatum d) => MList s (Maybe (Env d i r s m)) -> ATMST s m ()
blurbMaybeEnvMList mlist = do
  sep <- sttLayer $ newSTRef ""
  liftIO $ putStr "m["
  mlistFor_ sttLayer mlist $ \envm -> do
    thisSep <- sttLayer $ readSTRef sep
    liftIO $ putStr thisSep
    case envm of
      Just env -> blurbEnv env
      Nothing -> liftIO $ putStr "<nothing>"
    sttLayer $ writeSTRef sep ", "
  liftIO $ putStr "]"

-- |Print a short summary of a reference to a mutable list of
-- nullable (via `Maybe`) `Env`ironments from an `ATMS`.
blurbMaybeEnvMListRef ::
  (MonadIO m, NodeDatum d) =>
    STRef s (MList s (Maybe (Env d i r s m))) -> ATMST s m ()
blurbMaybeEnvMListRef mlistRef = do
  mlist <- sttLayer $ readSTRef mlistRef
  blurbMaybeEnvMList mlist

-- |Print a short summary of a nullable (via `Maybe`) reference to an
-- `Env`ironment of an `ATMS`.
blurbMaybeEnv ::
  (MonadIO m, NodeDatum d) => Maybe (Env d i r s m) -> ATMST s m ()
blurbMaybeEnv envm = case envm of
                       Just env -> blurbEnv env
                       Nothing -> liftIO $ putStr "<nothing>"

-- |Print a short summary of one `Env`ironment of an `ATMS`.
blurbEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
blurbEnv env = do
  wng <- sttLayer $ readSTRef $ envWhyNogood env
  isNogood <- envIsNogood env
  case envAssumptions env of
    [] -> do
      liftIO $ putStr "<empty>"
    nodes @ (first : _) -> do
      datumFmt <- getDatumString (nodeATMS first)
      when isNogood $ liftIO $ putStr "[X] "
      liftIO $ putStr $
        "{" ++ (intercalate ", " $ map (datumFmt . nodeDatum) nodes) ++ "}"

-- |Give a verbose printout of the no-good `Env`ironments of an
-- `ATMS`.
debugNogoods :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
debugNogoods atms = do
  liftIO $ putStrLn "No-good environments:"
  nogoodTable <- getNogoodTable atms
  debugEnvTable atms nogoodTable

-- |Give a verbose printout of the `Env`ironments of an `EnvTable` of
-- an `ATMS`.
debugEnvTable ::
  (MonadIO m, NodeDatum d) =>
    ATMS d i r s m -> EnvTable d i r s m -> ATMST s m ()
debugEnvTable atms (EnvTable array) = do
  let (lo, hi) = boundsSTArray array
  forM_ [lo..hi] $ \ i -> do
    envs <- sttLayer $ readSTArray array i
    forM_ (reverse envs) $ \ env -> do
      liftIO $ putStr "- "
      debug env

{-
-- |Print a short summary of the label of a `Node` of an `ATMS`.
blurbNodeLabel ::
  (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m String
blurbNodeLabel node = do
  -- lbl <- getNodeLabel node
  lbl <- sttLayer $ readSTRef (nodeLabel node)
  blurb node
  liftIO $ putStr " label: "
  blurbEnvList 10000 "\n" lbl
  liftIO $ putStrLn ""
-}

-- |Give a verbose printout of the label of a `Node` of an `ATMS`.
debugNodeLabel ::
  (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
debugNodeLabel node = do
  -- lbl <- getNodeLabel node
  lbl <- sttLayer $ readSTRef (nodeLabel node)
  blurb node
  liftIO $ putStr " label: "
  blurbEnvList 10000 "\n" lbl
  liftIO $ putStrLn ""

-- |Print a short summary of a list of `Env`ironments of an `ATMS`.
blurbEnvList ::
  (MonadIO m, NodeDatum d) => Int -> String -> [Env d i r s m] -> ATMST s m ()
blurbEnvList multiLineIf lineLead envs =
  case length envs of
    0 -> liftIO $ putStr "empty env list"
    n | n < multiLineIf -> do
          liftIO $ putStr $ show n ++" envs: "
          sepR <- sttLayer $ newSTRef ""
          forM_ envs $ \env -> do
            sep <- sttLayer $ readSTRef sepR
            liftIO $ putStr sep
            blurbEnv env
            sttLayer $ writeSTRef sepR ", "
    n -> do
      liftIO $ putStrLn $ show n ++" envs:"
      forM_ envs $ \env -> do
        liftIO $ putStr lineLead
        blurbEnv env
        liftIO $ putStrLn ""

instance MonadIO m => MonadIO (STT s m) where liftIO = lift . liftIO