{-|
Module      : JTMS
Description : Justification-based truth maintenance systems (JTMSes)
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 justification-based truth
maintenance systems (JTMSes) 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 #-}

module Data.TMS.JTMS (
  -- * The JTMST monad
  JTMST, JtmsErr, runJTMST,

  -- * Basic JTMS structures
  JTMS, printJTMS, createJTMS,
  -- ** JTMS accessors
  jtmsTitle,
  -- ** Setting JTMS properties

  -- | === __Lisp origins__
  --
  -- The JTMS property-setting functions are translated from:
  --
  -- > ;; In jtms.lisp:
  -- > (defun change-jtms (jtms &key contradiction-handler node-string
  -- >                            enqueue-procedure debugging
  -- >                               checking-contradictions)
  -- >   (if node-string (setf (jtms-node-string jtms) node-string))
  -- >   (if debugging (setf (jtms-debugging jtms) debugging))
  -- >   (if checking-contradictions
  -- >       (setf (jtms-checking-contradictions jtms)
  -- >          checking-contradictions))
  -- >   (if contradiction-handler
  -- >       (setf (jtms-contradiction-handler jtms) contradiction-handler))
  -- >   (if enqueue-procedure
  -- >       (setf (jtms-enqueue-procedure jtms) enqueue-procedure)))
  setNodeString, nodeStringByDatum, nodeStringByIndex, nodeStringByIndexDatum,
  setDatumString, datumStringByShow,
  setInformantString, informantStringByShow,
  setJustString,
  justStringByIndex, justStringByInformant, justStringByIndexInformant,
  setDebugging, setCheckingContradictions,
  setContradictionHandler, setEnqueueProcedure,

  -- *** Accessors for a `JTMS`'s current state
  getJtmsNodes, getJtmsJusts, getJtmsContradictions, getJtmsAssumptions,
  getJtmsCheckingContradictions, getJtmsNodeString, getJtmsJustString,
  getJtmsDatumString, getJtmsInformantString, getJtmsEnqueueProcedure,
  getJtmsContradictionHandler, getJtmsDebugging,

  -- ** Nodes
  Node, createNode, nodeDatum, printTmsNode, assumeNode, nodeString,

  -- *** Accessors for a `Node`'s current state
  getNodeIsAssumption, getNodeIsContradictory, getNodeBelieved,
  getNodeConsequences, getNodeInRules, getNodeOutRules, getNodeJusts,
  getNodeSupport, isEnabledAssumption, whenSupportedByRule, ifSupportedByRule,

  -- ** Justifications
  justifyNode,
  Justification(ByRule, EnabledAssumption, UserStipulation),
  JustRule(justInformant, justConsequence, justAntecedents),
  printJustRule,

  -- * Reasoning tools
  -- ** Control of assumptions
  enableAssumption, retractAssumption, makeContradiction,
  -- ** Conclusions from current assumption belief
  isInNode, isOutNode, enabledAssumptions, nodeIsPremise, assumptionsOfNode,
  -- ** Output from the current belief state
  whyNodes, whyNode, printContraList,

  -- * Debugging utilities

  -- |Note that these functions are based on `MonadIO`, not just
  -- `Monad`, for printing debugging output.
  debugJTMS, debugNodes, debugNode, debugJusts, debugJust

  ) where

import Control.Monad.State
import Control.Monad.ST.Trans
import Control.Monad.Except
import Control.Monad.Extra
import Data.TMS.Helpers
import Data.TMS.Dbg

-- * The @JTMST@ monad transformer
--
-- Construction and manipulation of a JTMS happens inside this monad
-- wrapper.

-- |Errors which can arise from JTMS operations.
data JtmsErr = CannotEnableNonassumption String Int deriving Int -> JtmsErr -> ShowS
[JtmsErr] -> ShowS
JtmsErr -> String
(Int -> JtmsErr -> ShowS)
-> (JtmsErr -> String) -> ([JtmsErr] -> ShowS) -> Show JtmsErr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [JtmsErr] -> ShowS
$cshowList :: [JtmsErr] -> ShowS
show :: JtmsErr -> String
$cshow :: JtmsErr -> String
showsPrec :: Int -> JtmsErr -> ShowS
$cshowsPrec :: Int -> JtmsErr -> ShowS
Show

-- |The process of building and using a mutable JTMS.
type JTMSTInner s m a = Monad m => ExceptT JtmsErr (STT s m) a

-- |The process of building and using a mutable JTMS.
newtype Monad m => JTMST s m a = JtmsT { JTMST s m a -> Monad m => ExceptT JtmsErr (STT s m) a
unwrap :: JTMSTInner s m a }

-- |Internal unwrapper preserving rank-2 polymorphism of the state
-- thread in the wrapper `STT`.
unwrap2 :: Monad m => (forall s . JTMST s m a) -> (forall s . JTMSTInner s m a)
unwrap2 :: (forall s. JTMST s m a) -> forall s. JTMSTInner s m a
unwrap2 (JtmsT m) = ExceptT JtmsErr (STT s m) a
JTMSTInner s m a
m

instance (Monad m) => Functor (JTMST s m) where
  fmap :: (a -> b) -> JTMST s m a -> JTMST s m b
fmap a -> b
f (JtmsT JTMSTInner s m a
m) = JTMSTInner s m b -> JTMST s m b
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m b -> JTMST s m b)
-> JTMSTInner s m b -> JTMST s m b
forall a b. (a -> b) -> a -> b
$ do
    a
v <- ExceptT JtmsErr (STT s m) a
JTMSTInner s m a
m
    b -> ExceptT JtmsErr (STT s m) b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> ExceptT JtmsErr (STT s m) b)
-> b -> ExceptT JtmsErr (STT s m) b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
v

instance (Monad m, Functor m) => Applicative (JTMST s m) where
  pure :: a -> JTMST s m a
pure a
v = JTMSTInner s m a -> JTMST s m a
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m a -> JTMST s m a)
-> JTMSTInner s m a -> JTMST s m a
forall a b. (a -> b) -> a -> b
$ a -> ExceptT JtmsErr (STT s m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
v
  (JtmsT JTMSTInner s m (a -> b)
m1) <*> :: JTMST s m (a -> b) -> JTMST s m a -> JTMST s m b
<*> (JtmsT JTMSTInner s m a
m2) = JTMSTInner s m b -> JTMST s m b
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m b -> JTMST s m b)
-> JTMSTInner s m b -> JTMST s m b
forall a b. (a -> b) -> a -> b
$ do
    a -> b
f <- ExceptT JtmsErr (STT s m) (a -> b)
JTMSTInner s m (a -> b)
m1
    a
v <- ExceptT JtmsErr (STT s m) a
JTMSTInner s m a
m2
    b -> ExceptT JtmsErr (STT s m) b
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> b
f a
v)

instance (Monad m, Functor m) => Monad (JTMST s m) where
  -- (>>=) :: JTMST s m a -> (a -> JTMST s m b) -> JTMST s m b
  (JtmsT JTMSTInner s m a
m) >>= :: JTMST s m a -> (a -> JTMST s m b) -> JTMST s m b
>>= a -> JTMST s m b
f = JTMSTInner s m b -> JTMST s m b
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m b -> JTMST s m b)
-> JTMSTInner s m b -> JTMST s m b
forall a b. (a -> b) -> a -> b
$ ExceptT JtmsErr (STT s m) a
JTMSTInner s m a
m ExceptT JtmsErr (STT s m) a
-> (a -> ExceptT JtmsErr (STT s m) b)
-> ExceptT JtmsErr (STT s m) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (JTMST s m b -> ExceptT JtmsErr (STT s m) b
forall s (m :: * -> *) a.
Monad m =>
JTMST s m a -> JTMSTInner s m a
unwrap (JTMST s m b -> ExceptT JtmsErr (STT s m) b)
-> (a -> JTMST s m b) -> a -> ExceptT JtmsErr (STT s m) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> JTMST s m b
f)

  -- (>>) :: JTMST s m a -> JTMST s m b -> JTMST s m b
  (JtmsT JTMSTInner s m a
m1) >> :: JTMST s m a -> JTMST s m b -> JTMST s m b
>> (JtmsT JTMSTInner s m b
m2) = JTMSTInner s m b -> JTMST s m b
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m b -> JTMST s m b)
-> JTMSTInner s m b -> JTMST s m b
forall a b. (a -> b) -> a -> b
$ ExceptT JtmsErr (STT s m) a
JTMSTInner s m a
m1 ExceptT JtmsErr (STT s m) a
-> ExceptT JtmsErr (STT s m) b -> ExceptT JtmsErr (STT s m) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ExceptT JtmsErr (STT s m) b
JTMSTInner s m b
m2

  -- return :: a -> JTMST s m a
  return :: a -> JTMST s m a
return a
v = JTMSTInner s m a -> JTMST s m a
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m a -> JTMST s m a)
-> JTMSTInner s m a -> JTMST s m a
forall a b. (a -> b) -> a -> b
$ a -> ExceptT JtmsErr (STT s m) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
v

instance MonadTrans (JTMST s) where
  lift :: m a -> JTMST s m a
lift m a
m = JTMSTInner s m a -> JTMST s m a
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m a -> JTMST s m a)
-> JTMSTInner s m a -> JTMST s m a
forall a b. (a -> b) -> a -> b
$ STT s m a -> ExceptT JtmsErr (STT s m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m a -> ExceptT JtmsErr (STT s m) a)
-> STT s m a -> ExceptT JtmsErr (STT s m) a
forall a b. (a -> b) -> a -> b
$ m a -> STT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
m

instance MonadIO m => MonadIO (JTMST s m) where
  liftIO :: IO a -> JTMST s m a
liftIO = m a -> JTMST s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> JTMST s m a) -> (IO a -> m a) -> IO a -> JTMST s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

-- |Lift `STT` behavior to the `JTMST` level.
jLiftSTT :: Monad m => STT s m r -> JTMST s m r
jLiftSTT :: STT s m r -> JTMST s m r
jLiftSTT STT s m r
md = JTMSTInner s m r -> JTMST s m r
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m r -> JTMST s m r)
-> JTMSTInner s m r -> JTMST s m r
forall a b. (a -> b) -> a -> b
$ STT s m r -> ExceptT JtmsErr (STT s m) r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m r -> ExceptT JtmsErr (STT s m) r)
-> STT s m r -> ExceptT JtmsErr (STT s m) r
forall a b. (a -> b) -> a -> b
$ STT s m r
md

-- |Lift `ExceptT` behavior to the `JTMST` level.
jLiftExcept :: Monad m => ExceptT JtmsErr (STT s m) r -> JTMST s m r
jLiftExcept :: ExceptT JtmsErr (STT s m) r -> JTMST s m r
jLiftExcept ExceptT JtmsErr (STT s m) r
md = JTMSTInner s m r -> JTMST s m r
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m r -> JTMST s m r)
-> JTMSTInner s m r -> JTMST s m r
forall a b. (a -> b) -> a -> b
$ ExceptT JtmsErr (STT s m) r
JTMSTInner s m r
md

-- |Execute a computation in the `JTMST` monad transformer.
runJTMST :: Monad m => (forall s . JTMST s m r) -> m (Either JtmsErr r)
runJTMST :: (forall s. JTMST s m r) -> m (Either JtmsErr r)
runJTMST forall s. JTMST s m r
jtmst = (forall s. STT s m (Either JtmsErr r)) -> m (Either JtmsErr r)
forall (m :: * -> *) a. Monad m => (forall s. STT s m a) -> m a
runSTT ((forall s. STT s m (Either JtmsErr r)) -> m (Either JtmsErr r))
-> (forall s. STT s m (Either JtmsErr r)) -> m (Either JtmsErr r)
forall a b. (a -> b) -> a -> b
$ ExceptT JtmsErr (STT s m) r -> STT s m (Either JtmsErr r)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT JtmsErr (STT s m) r -> STT s m (Either JtmsErr r))
-> ExceptT JtmsErr (STT s m) r -> STT s m (Either JtmsErr r)
forall a b. (a -> b) -> a -> b
$ (forall s. JTMST s m r) -> forall s. JTMSTInner s m r
forall (m :: * -> *) a.
Monad m =>
(forall s. JTMST s m a) -> forall s. JTMSTInner s m a
unwrap2 forall s. JTMST s m r
jtmst

-- * JTMS elements

-- ** The JTMS structure

-- |Standalone implementation of justification-based truth maintenance
-- systems.
--
--  - @d@ is the type of data associated with each `Node` of this JTMS.
--  - @i@ is the type of informants in the external system.
--  - @r@ is the type of rules which may be associated with each `Node`
--    of this JTMS.
--  - @s@ is the (phantom) type of the state thread.
--  - @m@ is the monad in which this computation lives.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defstruct (jtms (:PRINT-FUNCTION print-jtms))
-- >   (title nil)
-- >   (node-counter 0)             ;; unique namer for nodes.
-- >   (just-counter 0)             ;; unique namer for justifications.
-- >   (nodes nil)                  ;; list of all tms nodes.
-- >   (justs nil)                  ;; list of all justifications
-- >   (debugging nil)              ;; debugging flag
-- >   (contradictions nil)         ;; list of contradiction nodes.
-- >   (assumptions nil)            ;; list of assumption nodes.
-- >   (checking-contradictions T)  ;; For external systems
-- >   (node-string nil)
-- >   (contradiction-handler nil)
-- >   (enqueue-procedure nil))
data Monad m => JTMS d i r s m = JTMS {
  -- |Name of this JTMS.
  JTMS d i r s m -> String
jtmsTitle :: String,
  -- |Unique namer for nodes.
  JTMS d i r s m -> STRef s Int
jtmsNodeCounter :: STRef s Int,
  -- |Unique namer for justifications.
  JTMS d i r s m -> STRef s Int
jtmsJustCounter :: STRef s Int,
  -- |List of all TMS nodes.
  JTMS d i r s m -> STRef s [Node d i r s m]
jtmsNodes :: STRef s [Node d i r s m],
  -- |List of all justifications.
  JTMS d i r s m -> STRef s [JustRule d i r s m]
jtmsJusts :: STRef s [JustRule d i r s m],
  -- |List of all contradiction nodes.
  JTMS d i r s m -> STRef s [Node d i r s m]
jtmsContradictions :: STRef s [Node d i r s m],
  -- |List of all assumption nodes.
  JTMS d i r s m -> STRef s [Node d i r s m]
jtmsAssumptions :: STRef s [Node d i r s m],
  -- |For external systems.
  JTMS d i r s m -> STRef s Bool
jtmsCheckingContradictions :: STRef s Bool,
  JTMS d i r s m -> STRef s (Node d i r s m -> String)
jtmsNodeString :: STRef s (Node d i r s m -> String),
  JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
jtmsJustString :: STRef s (JustRule d i r s m -> String),
  JTMS d i r s m -> STRef s (d -> String)
jtmsDatumString :: STRef s (d -> String),
  JTMS d i r s m -> STRef s (i -> String)
jtmsInformantString :: STRef s (i -> String),
  JTMS d i r s m -> STRef s (r -> JTMST s m ())
jtmsEnqueueProcedure :: STRef s (r -> JTMST s m ()),
  JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ())
jtmsContradictionHandler :: STRef s ([Node d i r s m] -> JTMST s m ()),
  JTMS d i r s m -> STRef s Bool
jtmsDebugging :: STRef s Bool
}

-- |TODO For the moment equality on JTMSes in by comparing their names, but
-- this is an ugly and stupid hack.  Need something like: an index for
-- JTMSes generated from JTMST.  Really, this is just for a way to
-- enable nodes from different JTMSes to be seen as unequal.
instance Monad m => Eq (JTMS d i r s m) where
  JTMS d i r s m
j1 == :: JTMS d i r s m -> JTMS d i r s m -> Bool
== JTMS d i r s m
j2 = JTMS d i r s m -> String
forall d i r s (m :: * -> *). Monad m => JTMS d i r s m -> String
jtmsTitle JTMS d i r s m
j1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== JTMS d i r s m -> String
forall d i r s (m :: * -> *). Monad m => JTMS d i r s m -> String
jtmsTitle JTMS d i r s m
j2


-- |Get the next node counter value, incrementing for future accesses.
nextNodeCounter :: Monad m => JTMS d i r s m -> JTMSTInner s m Int
nextNodeCounter :: JTMS d i r s m -> JTMSTInner s m Int
nextNodeCounter JTMS d i r s m
jtms = STT s m Int -> ExceptT JtmsErr (STT s m) Int
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m Int -> ExceptT JtmsErr (STT s m) Int)
-> STT s m Int -> ExceptT JtmsErr (STT s m) Int
forall a b. (a -> b) -> a -> b
$
  let nodeCounter :: STRef s Int
nodeCounter = JTMS d i r s m -> STRef s Int
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Int
jtmsNodeCounter JTMS d i r s m
jtms
  in do
    Int
nodeId <- STRef s Int -> STT s m Int
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s Int
nodeCounter
    STRef s Int -> Int -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef STRef s Int
nodeCounter (Int -> STT s m ()) -> Int -> STT s m ()
forall a b. (a -> b) -> a -> b
$ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nodeId
    Int -> STT s m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
nodeId

-- |Get the next justification rule counter value, incrementing for
-- future accesses.
nextJustCounter :: Monad m => JTMS d i r s m -> JTMSTInner s m Int
nextJustCounter :: JTMS d i r s m -> JTMSTInner s m Int
nextJustCounter JTMS d i r s m
jtms = STT s m Int -> ExceptT JtmsErr (STT s m) Int
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m Int -> ExceptT JtmsErr (STT s m) Int)
-> STT s m Int -> ExceptT JtmsErr (STT s m) Int
forall a b. (a -> b) -> a -> b
$
  let justCounter :: STRef s Int
justCounter = JTMS d i r s m -> STRef s Int
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Int
jtmsJustCounter JTMS d i r s m
jtms
  in do
    Int
justId <- STRef s Int -> STT s m Int
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s Int
justCounter
    STRef s Int -> Int -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef STRef s Int
justCounter (Int -> STT s m ()) -> Int -> STT s m ()
forall a b. (a -> b) -> a -> b
$ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
justId
    Int -> STT s m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
justId

-- | Return the current list of `Node`s of a `JTMS`.
getJtmsNodes :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]
getJtmsNodes :: JTMS d i r s m -> JTMST s m [Node d i r s m]
getJtmsNodes = STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> (JTMS d i r s m -> STT s m [Node d i r s m])
-> JTMS d i r s m
-> JTMST s m [Node d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [Node d i r s m] -> STT s m [Node d i r s m])
-> (JTMS d i r s m -> STRef s [Node d i r s m])
-> JTMS d i r s m
-> STT s m [Node d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsNodes

-- | Return the current `JustRule`s of a `JTMS`.
getJtmsJusts :: Monad m => JTMS d i r s m -> JTMST s m [JustRule d i r s m]
getJtmsJusts :: JTMS d i r s m -> JTMST s m [JustRule d i r s m]
getJtmsJusts = STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m])
-> (JTMS d i r s m -> STT s m [JustRule d i r s m])
-> JTMS d i r s m
-> JTMST s m [JustRule d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m])
-> (JTMS d i r s m -> STRef s [JustRule d i r s m])
-> JTMS d i r s m
-> STT s m [JustRule d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [JustRule d i r s m]
jtmsJusts

-- | Return the current designated contradictory `Node`s of a `JTMS`.
getJtmsContradictions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]
getJtmsContradictions :: JTMS d i r s m -> JTMST s m [Node d i r s m]
getJtmsContradictions = STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> (JTMS d i r s m -> STT s m [Node d i r s m])
-> JTMS d i r s m
-> JTMST s m [Node d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [Node d i r s m] -> STT s m [Node d i r s m])
-> (JTMS d i r s m -> STRef s [Node d i r s m])
-> JTMS d i r s m
-> STT s m [Node d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsContradictions

-- | Return the current possible assumption `Node`s of a `JTMS`.  Note
-- that these nodes will not be used as assumptions unless activated
-- by `enableAssumption`.
getJtmsAssumptions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]
getJtmsAssumptions :: JTMS d i r s m -> JTMST s m [Node d i r s m]
getJtmsAssumptions = STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> (JTMS d i r s m -> STT s m [Node d i r s m])
-> JTMS d i r s m
-> JTMST s m [Node d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [Node d i r s m] -> STT s m [Node d i r s m])
-> (JTMS d i r s m -> STRef s [Node d i r s m])
-> JTMS d i r s m
-> STT s m [Node d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsAssumptions

-- | Return whether a `JTMS` is currently invoking its external
-- handler for deduced contradictions.
getJtmsCheckingContradictions :: Monad m => JTMS d i r s m -> JTMST s m Bool
getJtmsCheckingContradictions :: JTMS d i r s m -> JTMST s m Bool
getJtmsCheckingContradictions = STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool)
-> (JTMS d i r s m -> STT s m Bool)
-> JTMS d i r s m
-> JTMST s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool)
-> (JTMS d i r s m -> STRef s Bool)
-> JTMS d i r s m
-> STT s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Bool
jtmsCheckingContradictions

-- | Return the current `Node` formatter of a `JTMS`.
getJtmsNodeString ::
  Monad m => JTMS d i r s m -> JTMST s m (Node d i r s m -> String)
getJtmsNodeString :: JTMS d i r s m -> JTMST s m (Node d i r s m -> String)
getJtmsNodeString = STT s m (Node d i r s m -> String)
-> JTMST s m (Node d i r s m -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Node d i r s m -> String)
 -> JTMST s m (Node d i r s m -> String))
-> (JTMS d i r s m -> STT s m (Node d i r s m -> String))
-> JTMS d i r s m
-> JTMST s m (Node d i r s m -> String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Node d i r s m -> String)
 -> STT s m (Node d i r s m -> String))
-> (JTMS d i r s m -> STRef s (Node d i r s m -> String))
-> JTMS d i r s m
-> STT s m (Node d i r s m -> String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s (Node d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (Node d i r s m -> String)
jtmsNodeString

-- | Return the current `JustRule` formatter of a `JTMS`.
getJtmsJustString ::
  Monad m => JTMS d i r s m -> JTMST s m (JustRule d i r s m -> String)
getJtmsJustString :: JTMS d i r s m -> JTMST s m (JustRule d i r s m -> String)
getJtmsJustString = STT s m (JustRule d i r s m -> String)
-> JTMST s m (JustRule d i r s m -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (JustRule d i r s m -> String)
 -> JTMST s m (JustRule d i r s m -> String))
-> (JTMS d i r s m -> STT s m (JustRule d i r s m -> String))
-> JTMS d i r s m
-> JTMST s m (JustRule d i r s m -> String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s (JustRule d i r s m -> String)
-> STT s m (JustRule d i r s m -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (JustRule d i r s m -> String)
 -> STT s m (JustRule d i r s m -> String))
-> (JTMS d i r s m -> STRef s (JustRule d i r s m -> String))
-> JTMS d i r s m
-> STT s m (JustRule d i r s m -> String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
jtmsJustString

-- | Return the current @d@ datum formatter of a `JTMS`.
getJtmsDatumString :: Monad m => JTMS d i r s m -> JTMST s m (d -> String)
getJtmsDatumString :: JTMS d i r s m -> JTMST s m (d -> String)
getJtmsDatumString = STT s m (d -> String) -> JTMST s m (d -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (d -> String) -> JTMST s m (d -> String))
-> (JTMS d i r s m -> STT s m (d -> String))
-> JTMS d i r s m
-> JTMST s m (d -> String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s (d -> String) -> STT s m (d -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (d -> String) -> STT s m (d -> String))
-> (JTMS d i r s m -> STRef s (d -> String))
-> JTMS d i r s m
-> STT s m (d -> String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s (d -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (d -> String)
jtmsDatumString

-- | Return the current @i@ informant formatter of a `JTMS`.
getJtmsInformantString :: Monad m => JTMS d i r s m -> JTMST s m (i -> String)
getJtmsInformantString :: JTMS d i r s m -> JTMST s m (i -> String)
getJtmsInformantString = STT s m (i -> String) -> JTMST s m (i -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (i -> String) -> JTMST s m (i -> String))
-> (JTMS d i r s m -> STT s m (i -> String))
-> JTMS d i r s m
-> JTMST s m (i -> String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s (i -> String) -> STT s m (i -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (i -> String) -> STT s m (i -> String))
-> (JTMS d i r s m -> STRef s (i -> String))
-> JTMS d i r s m
-> STT s m (i -> String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s (i -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (i -> String)
jtmsInformantString

-- | Return the current external queuing procedure of a `JTMS`.
getJtmsEnqueueProcedure :: Monad m => JTMS d i r s m -> JTMST s m (r -> JTMST s m ())
getJtmsEnqueueProcedure :: JTMS d i r s m -> JTMST s m (r -> JTMST s m ())
getJtmsEnqueueProcedure = STT s m (r -> JTMST s m ()) -> JTMST s m (r -> JTMST s m ())
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (r -> JTMST s m ()) -> JTMST s m (r -> JTMST s m ()))
-> (JTMS d i r s m -> STT s m (r -> JTMST s m ()))
-> JTMS d i r s m
-> JTMST s m (r -> JTMST s m ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s (r -> JTMST s m ()) -> STT s m (r -> JTMST s m ())
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (r -> JTMST s m ()) -> STT s m (r -> JTMST s m ()))
-> (JTMS d i r s m -> STRef s (r -> JTMST s m ()))
-> JTMS d i r s m
-> STT s m (r -> JTMST s m ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s (r -> JTMST s m ())
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (r -> JTMST s m ())
jtmsEnqueueProcedure

-- | Return the current external handler of a `JTMS` for reacting to a
-- deduced contradiction.
getJtmsContradictionHandler :: Monad m => JTMS d i r s m -> JTMST s m ([Node d i r s m] -> JTMST s m ())
getJtmsContradictionHandler :: JTMS d i r s m -> JTMST s m ([Node d i r s m] -> JTMST s m ())
getJtmsContradictionHandler = STT s m ([Node d i r s m] -> JTMST s m ())
-> JTMST s m ([Node d i r s m] -> JTMST s m ())
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m ([Node d i r s m] -> JTMST s m ())
 -> JTMST s m ([Node d i r s m] -> JTMST s m ()))
-> (JTMS d i r s m -> STT s m ([Node d i r s m] -> JTMST s m ()))
-> JTMS d i r s m
-> JTMST s m ([Node d i r s m] -> JTMST s m ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s ([Node d i r s m] -> JTMST s m ())
-> STT s m ([Node d i r s m] -> JTMST s m ())
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s ([Node d i r s m] -> JTMST s m ())
 -> STT s m ([Node d i r s m] -> JTMST s m ()))
-> (JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ()))
-> JTMS d i r s m
-> STT s m ([Node d i r s m] -> JTMST s m ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ())
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ())
jtmsContradictionHandler

-- | Return the current debugging flag setting of a `JTMS`.
getJtmsDebugging :: Monad m => JTMS d i r s m -> JTMST s m Bool
getJtmsDebugging :: JTMS d i r s m -> JTMST s m Bool
getJtmsDebugging = STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool)
-> (JTMS d i r s m -> STT s m Bool)
-> JTMS d i r s m
-> JTMST s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool)
-> (JTMS d i r s m -> STRef s Bool)
-> JTMS d i r s m
-> STT s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JTMS d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Bool
jtmsDebugging

-- |Print a simple tag with the title of this JTMS.  Forces the
-- enclosed monad to be `MonadIO`.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun print-jtms (jtms stream ignore)
-- >   (declare (ignore ignore))
-- >   (format stream "#<JTMS: ~A>" (jtms-title jtms)))
printJTMS :: JTMS d i r s m -> m ()
printJTMS JTMS d i r s m
jtms = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"#<JTMS: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ JTMS d i r s m -> String
forall d i r s (m :: * -> *). Monad m => JTMS d i r s m -> String
jtmsTitle JTMS d i r s m
jtms String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"

-- ** Individual nodes

-- |Wrapper for one possible belief known to the TMS.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defstruct (tms-node (:PRINT-FUNCTION print-tms-node))
-- >   (index 0)
-- >   (datum nil)           ;; pointer to external problem solver
-- >   (label :OUT)          ;; :IN means believed, :OUT means disbelieved
-- >   (support nil)         ;; Current justification or premise marker
-- >   (justs nil)           ;; Possible justifications
-- >   (consequences nil)    ;; Justifications in which it is an antecedent
-- >   (mark nil)            ;; Marker for sweep algorithms
-- >   (contradictory? nil)  ;; Flag marking it as contradictory
-- >   (assumption? nil)     ;; Flag marking it as an assumption.
-- >   (in-rules nil)     ;; Rules that should be triggered when node goes in
-- >   (out-rules nil)    ;; Rules that should be triggered when node goes out
-- >   (jtms nil))           ;; The JTMS in which this node appears.
data Monad m => Node d i r s m = Node {
  Node d i r s m -> Int
nodeIndex :: Int,
  Node d i r s m -> d
nodeDatum :: d, -- ^Returns the piece of data associated with this node.
  Node d i r s m -> JTMS d i r s m
nodeJTMS :: JTMS d i r s m,
  Node d i r s m -> STRef s Bool
nodeIsAssumption :: STRef s Bool,
  Node d i r s m -> STRef s Bool
nodeIsContradictory :: STRef s Bool,
  Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport :: STRef s (Maybe (Justification d i r s m)),
  Node d i r s m -> STRef s Bool
nodeBelieved :: STRef s Bool,
  Node d i r s m -> STRef s [JustRule d i r s m]
nodeConsequences :: STRef s [JustRule d i r s m],
  Node d i r s m -> STRef s [r]
nodeInRules :: STRef s [r],
  Node d i r s m -> STRef s [r]
nodeOutRules :: STRef s [r],
  Node d i r s m -> STRef s [JustRule d i r s m]
nodeJusts :: STRef s [JustRule d i r s m]
}

-- |Equality on `Node`s is based simply on comparing their JTMS and
-- index number.
instance Monad m => Eq (Node d i r s m) where
  Node d i r s m
n1 == :: Node d i r s m -> Node d i r s m -> Bool
== Node d i r s m
n2 = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
n1 JTMS d i r s m -> JTMS d i r s m -> Bool
forall a. Eq a => a -> a -> Bool
== Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
n2 Bool -> Bool -> Bool
&& Node d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> Int
nodeIndex Node d i r s m
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Node d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> Int
nodeIndex Node d i r s m
n2

-- |Write one node in the standard way for this JTMS.  Forces the
-- wrapped monad to be `MonadIO`.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun print-tms-node (node stream ignore)
-- >   (declare (ignore ignore))
-- >   (format stream "#<Node: ~A>" (node-string node)))
printTmsNode :: MonadIO m => Node d i r s m -> JTMST s m ()
printTmsNode :: Node d i r s m -> JTMST s m ()
printTmsNode Node d i r s m
node = do
  String
s <- Node d i r s m -> JTMST s m String
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m String
nodeString Node d i r s m
node
  IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"#<Node: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"

-- *** Readers of current `Node` state

-- |Return whether a `Node` may currently be used as an assumption.
getNodeIsAssumption :: Monad m => Node d i r s m -> JTMST s m Bool
getNodeIsAssumption :: Node d i r s m -> JTMST s m Bool
getNodeIsAssumption = STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool)
-> (Node d i r s m -> STT s m Bool)
-> Node d i r s m
-> JTMST s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool)
-> (Node d i r s m -> STRef s Bool)
-> Node d i r s m
-> STT s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeIsAssumption

-- |Return whether a `Node` is currently considered a contradiction.
getNodeIsContradictory :: Monad m => Node d i r s m -> JTMST s m Bool
getNodeIsContradictory :: Node d i r s m -> JTMST s m Bool
getNodeIsContradictory = STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool)
-> (Node d i r s m -> STT s m Bool)
-> Node d i r s m
-> JTMST s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool)
-> (Node d i r s m -> STRef s Bool)
-> Node d i r s m
-> STT s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeIsContradictory

-- |Return the current support for believing a `Node`.
getNodeSupport ::
  Monad m => Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))
getNodeSupport :: Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))
getNodeSupport = STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Justification d i r s m))
 -> JTMST s m (Maybe (Justification d i r s m)))
-> (Node d i r s m -> STT s m (Maybe (Justification d i r s m)))
-> Node d i r s m
-> JTMST s m (Maybe (Justification d i r s m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Maybe (Justification d i r s m))
 -> STT s m (Maybe (Justification d i r s m)))
-> (Node d i r s m -> STRef s (Maybe (Justification d i r s m)))
-> Node d i r s m
-> STT s m (Maybe (Justification d i r s m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport

-- |Return where a `Node` is supported by a particular `JustRule`.
getIsNodeSupportedBy ::
  Monad m => Node d i r s m -> JustRule d i r s m -> JTMST s m Bool
getIsNodeSupportedBy :: Node d i r s m -> JustRule d i r s m -> JTMST s m Bool
getIsNodeSupportedBy Node d i r s m
node JustRule d i r s m
jrule = do
  Maybe (Justification d i r s m)
support <- Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))
getNodeSupport Node d i r s m
node
  case Maybe (Justification d i r s m)
support of
    Just (ByRule JustRule d i r s m
j) | JustRule d i r s m
j JustRule d i r s m -> JustRule d i r s m -> Bool
forall a. Eq a => a -> a -> Bool
== JustRule d i r s m
jrule -> Bool -> JTMST s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Maybe (Justification d i r s m)
_ -> Bool -> JTMST s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- |Return whether a `Node` is currently believed.
getNodeBelieved :: Monad m => Node d i r s m -> JTMST s m Bool
getNodeBelieved :: Node d i r s m -> JTMST s m Bool
getNodeBelieved = STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool)
-> (Node d i r s m -> STT s m Bool)
-> Node d i r s m
-> JTMST s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool)
-> (Node d i r s m -> STRef s Bool)
-> Node d i r s m
-> STT s m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeBelieved

-- |Return the `JustRule`s which use a `Node` as an antecedent.
getNodeConsequences ::
  Monad m => Node d i r s m -> JTMST s m [JustRule d i r s m]
getNodeConsequences :: Node d i r s m -> JTMST s m [JustRule d i r s m]
getNodeConsequences = STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m])
-> (Node d i r s m -> STT s m [JustRule d i r s m])
-> Node d i r s m
-> JTMST s m [JustRule d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m])
-> (Node d i r s m -> STRef s [JustRule d i r s m])
-> Node d i r s m
-> STT s m [JustRule d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [JustRule d i r s m]
nodeConsequences

-- |Return the current in-rules of a `Node`.
getNodeInRules :: Monad m => Node d i r s m -> JTMST s m [r]
getNodeInRules :: Node d i r s m -> JTMST s m [r]
getNodeInRules = STT s m [r] -> JTMST s m [r]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [r] -> JTMST s m [r])
-> (Node d i r s m -> STT s m [r])
-> Node d i r s m
-> JTMST s m [r]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s [r] -> STT s m [r]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [r] -> STT s m [r])
-> (Node d i r s m -> STRef s [r]) -> Node d i r s m -> STT s m [r]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> STRef s [r]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [r]
nodeInRules

-- |Return the current out-rules of a `Node`.
getNodeOutRules :: Monad m => Node d i r s m -> JTMST s m [r]
getNodeOutRules :: Node d i r s m -> JTMST s m [r]
getNodeOutRules = STT s m [r] -> JTMST s m [r]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [r] -> JTMST s m [r])
-> (Node d i r s m -> STT s m [r])
-> Node d i r s m
-> JTMST s m [r]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s [r] -> STT s m [r]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [r] -> STT s m [r])
-> (Node d i r s m -> STRef s [r]) -> Node d i r s m -> STT s m [r]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> STRef s [r]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [r]
nodeOutRules

-- |Return the `JustRule`s which currently give a `Node` as their
-- conclusion.
getNodeJusts :: Monad m => Node d i r s m -> JTMST s m [JustRule d i r s m]
getNodeJusts :: Node d i r s m -> JTMST s m [JustRule d i r s m]
getNodeJusts = STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m])
-> (Node d i r s m -> STT s m [JustRule d i r s m])
-> Node d i r s m
-> JTMST s m [JustRule d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m])
-> (Node d i r s m -> STRef s [JustRule d i r s m])
-> Node d i r s m
-> STT s m [JustRule d i r s m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [JustRule d i r s m]
nodeJusts


-- ** Justifications

-- |Wrapper for one justification relationship between many antecedent
-- nodes and one consequent node.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defstruct (just (:PRINT-FUNCTION print-just))
-- >   (index 0)
-- >   informant
-- >   consequence
-- >   antecedents)
data Monad m => JustRule d i r s m = JustRule {
  JustRule d i r s m -> Int
justIndex :: Int,
  JustRule d i r s m -> i
justInformant :: i,
  JustRule d i r s m -> Node d i r s m
justConsequence :: Node d i r s m,
  JustRule d i r s m -> [Node d i r s m]
justAntecedents :: [Node d i r s m]
}

-- |Equality on `JustRule`s is based simply on comparing their index
-- number.
instance Monad m => Eq (JustRule d i r s m) where
  JustRule d i r s m
n1 == :: JustRule d i r s m -> JustRule d i r s m -> Bool
== JustRule d i r s m
n2 = JustRule d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> Int
justIndex JustRule d i r s m
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== JustRule d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> Int
justIndex JustRule d i r s m
n2

-- |Print the tag of a JTMS justification.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun print-just (just stream ignore)
-- >   (declare (ignore ignore))
-- >   (format stream "#<Just ~D>" (just-index just)))
printJustRule :: MonadIO m => JustRule d i r s m -> JTMST s m ()
printJustRule :: JustRule d i r s m -> JTMST s m ()
printJustRule JustRule d i r s m
just =
  IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"#<Just " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> Int
justIndex JustRule d i r s m
just) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"

-- |Forms of data which might signal support for a node.  The original
-- Lisp does not need this declaration since it is untyped; the latter
-- two cases are simply symbols.
data Monad m => Justification d i r s m =
  ByRule (JustRule d i r s m) | EnabledAssumption | UserStipulation

-- |Returns @True@ when the node is supported by a `JustRule` with no
-- antecedents.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun tms-node-premise? (node &aux support)
-- >   (and (setq support (tms-node-support node))
-- >        (not (eq support :ENABLED-ASSUMPTION))
-- >        (null (just-antecedents support))))
nodeIsPremise :: Monad m => Node d i r s m -> JTMST s m Bool
nodeIsPremise :: Node d i r s m -> JTMST s m Bool
nodeIsPremise Node d i r s m
node = JTMSTInner s m Bool -> JTMST s m Bool
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m Bool -> JTMST s m Bool)
-> JTMSTInner s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STT s m Bool -> ExceptT JtmsErr (STT s m) Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m Bool -> ExceptT JtmsErr (STT s m) Bool)
-> STT s m Bool -> ExceptT JtmsErr (STT s m) Bool
forall a b. (a -> b) -> a -> b
$ do
  Maybe (Justification d i r s m)
support <- STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Maybe (Justification d i r s m))
 -> STT s m (Maybe (Justification d i r s m)))
-> STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node
  case Maybe (Justification d i r s m)
support of
    Just (ByRule (JustRule Int
_ i
_ Node d i r s m
_ [Node d i r s m]
antecedents)) -> Bool -> STT s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> STT s m Bool) -> Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Node d i r s m]
antecedents
    Maybe (Justification d i r s m)
_ -> Bool -> STT s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- * Simple utilities

-- |Produce a representation of the node in the default manner for its
-- JTMS.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun node-string (node)
-- >   (funcall (jtms-node-string (tms-node-jtms node)) node))
nodeString :: Monad m => Node d i r s m -> JTMST s m String
nodeString :: Node d i r s m -> JTMST s m String
nodeString Node d i r s m
node = JTMSTInner s m String -> JTMST s m String
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m String -> JTMST s m String)
-> JTMSTInner s m String -> JTMST s m String
forall a b. (a -> b) -> a -> b
$ STT s m String -> ExceptT JtmsErr (STT s m) String
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m String -> ExceptT JtmsErr (STT s m) String)
-> STT s m String -> ExceptT JtmsErr (STT s m) String
forall a b. (a -> b) -> a -> b
$ do
  Node d i r s m -> String
ns <- STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Node d i r s m -> String)
 -> STT s m (Node d i r s m -> String))
-> STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (Node d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (Node d i r s m -> String)
jtmsNodeString (JTMS d i r s m -> STRef s (Node d i r s m -> String))
-> JTMS d i r s m -> STRef s (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
  String -> STT s m String
forall (m :: * -> *) a. Monad m => a -> m a
return (Node d i r s m -> String
ns Node d i r s m
node)

-- Debugging is turned off for now.

-- -- Overloading the debugging operators to allow printing when the
-- -- underlying monad is `MonadIO`.
-- class Monad m => JTMSDebugger m where
--   debuggingJtms :: String -> m ()
--   debuggingJtms _ = return ()
--
-- instance MonadIO m => JTMSDebugger (JTMST s m) where
--   debuggingJtms s = liftIO $ print s
--
-- -- ===== __Lisp origins:__
-- --
-- -- > ;; In jtms.lisp:
-- -- > (defmacro debugging-jtms (jtms msg &optional node &rest args)
-- -- >   `(when (jtms-debugging ,jtms)
-- -- >      (format *trace-output*
-- -- >        ,msg (if ,node (node-string ,node)) ,@args)))

-- |Raise a JTMS-related error.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun tms-error (string node) (error string (node-string node)))
tmsError :: Monad m => JtmsErr -> JTMST s m ()
tmsError :: JtmsErr -> JTMST s m ()
tmsError JtmsErr
e = JTMSTInner s m () -> JTMST s m ()
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m () -> JTMST s m ())
-> JTMSTInner s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ JtmsErr -> ExceptT JtmsErr (STT s m) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError JtmsErr
e

-- |The default representation of a node is by @show@ing its datum.
-- Requires that @d@ is in class `Show`.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun default-node-string (n) (format nil "~A" (tms-node-datum n)))
defaultNodeString :: (Show d, Monad m) => Node d i r s m -> String
defaultNodeString :: Node d i r s m -> String
defaultNodeString Node d i r s m
node = d -> String
forall a. Show a => a -> String
show (d -> String) -> d -> String
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> d
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> d
nodeDatum Node d i r s m
node

-- |Create and return a new JTMS.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun create-jtms (title &key (node-string 'default-node-string)
-- >                                debugging
-- >                                (checking-contradictions t)
-- >                                (contradiction-handler 'ask-user-handler)
-- >                                enqueue-procedure)
-- >   (make-jtms :TITLE title
-- >              :NODE-STRING node-string
-- >              :DEBUGGING debugging
-- >              :CHECKING-CONTRADICTIONS checking-contradictions
-- >              :CONTRADICTION-HANDLER contradiction-handler
-- >              :ENQUEUE-PROCEDURE enqueue-procedure))
createJTMS :: Monad m => String -> JTMST s m (JTMS d i r s m)
createJTMS :: String -> JTMST s m (JTMS d i r s m)
createJTMS String
title = JTMSTInner s m (JTMS d i r s m) -> JTMST s m (JTMS d i r s m)
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m (JTMS d i r s m) -> JTMST s m (JTMS d i r s m))
-> JTMSTInner s m (JTMS d i r s m) -> JTMST s m (JTMS d i r s m)
forall a b. (a -> b) -> a -> b
$ STT s m (JTMS d i r s m)
-> ExceptT JtmsErr (STT s m) (JTMS d i r s m)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m (JTMS d i r s m)
 -> ExceptT JtmsErr (STT s m) (JTMS d i r s m))
-> STT s m (JTMS d i r s m)
-> ExceptT JtmsErr (STT s m) (JTMS d i r s m)
forall a b. (a -> b) -> a -> b
$ do
  STRef s Int
nc <- Int -> STT s m (STRef s Int)
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef Int
0
  STRef s Int
jc <- Int -> STT s m (STRef s Int)
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef Int
0
  STRef s [Node d i r s m]
nodes <- [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef ([] :: [Node d i r s m])
  STRef s [JustRule d i r s m]
justs <- [JustRule d i r s m] -> STT s m (STRef s [JustRule d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef ([] :: [JustRule d i r s m])
  STRef s [Node d i r s m]
contradictions <- [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef ([] :: [Node d i r s m])
  STRef s [Node d i r s m]
assumptions <- [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef ([] :: [Node d i r s m])
  STRef s Bool
checkingContradictions <- Bool -> STT s m (STRef s Bool)
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef Bool
True
  STRef s (Node d i r s m -> String)
nodeString <- (Node d i r s m -> String)
-> STT s m (STRef s (Node d i r s m -> String))
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef (Int -> String
forall a. Show a => a -> String
show (Int -> String)
-> (Node d i r s m -> Int) -> Node d i r s m -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> Int
nodeIndex)
  STRef s (JustRule d i r s m -> String)
justString <- (JustRule d i r s m -> String)
-> STT s m (STRef s (JustRule d i r s m -> String))
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef (Int -> String
forall a. Show a => a -> String
show (Int -> String)
-> (JustRule d i r s m -> Int) -> JustRule d i r s m -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JustRule d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> Int
justIndex)
  STRef s (d -> String)
datumString <- (d -> String) -> STT s m (STRef s (d -> String))
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef (\ d
datum -> String
"?")
  STRef s (i -> String)
informantString <- (i -> String) -> STT s m (STRef s (i -> String))
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef (\ i
inf -> String
"?")
  STRef s (r -> JTMST s m ())
enqueueProcedure <- (r -> JTMST s m ()) -> STT s m (STRef s (r -> JTMST s m ()))
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef (\ r
_ -> () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  STRef s ([Node d i r s m] -> JTMST s m ())
contradictionHandler <- ([Node d i r s m] -> JTMST s m ())
-> STT s m (STRef s ([Node d i r s m] -> JTMST s m ()))
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef (\ [Node d i r s m]
_ -> () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  STRef s Bool
debugging <- Bool -> STT s m (STRef s Bool)
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef Bool
False
  JTMS d i r s m -> STT s m (JTMS d i r s m)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
-> STRef s Int
-> STRef s Int
-> STRef s [Node d i r s m]
-> STRef s [JustRule d i r s m]
-> STRef s [Node d i r s m]
-> STRef s [Node d i r s m]
-> STRef s Bool
-> STRef s (Node d i r s m -> String)
-> STRef s (JustRule d i r s m -> String)
-> STRef s (d -> String)
-> STRef s (i -> String)
-> STRef s (r -> JTMST s m ())
-> STRef s ([Node d i r s m] -> JTMST s m ())
-> STRef s Bool
-> JTMS d i r s m
forall d i r s (m :: * -> *).
String
-> STRef s Int
-> STRef s Int
-> STRef s [Node d i r s m]
-> STRef s [JustRule d i r s m]
-> STRef s [Node d i r s m]
-> STRef s [Node d i r s m]
-> STRef s Bool
-> STRef s (Node d i r s m -> String)
-> STRef s (JustRule d i r s m -> String)
-> STRef s (d -> String)
-> STRef s (i -> String)
-> STRef s (r -> JTMST s m ())
-> STRef s ([Node d i r s m] -> JTMST s m ())
-> STRef s Bool
-> JTMS d i r s m
JTMS String
title STRef s Int
nc STRef s Int
jc STRef s [Node d i r s m]
nodes STRef s [JustRule d i r s m]
justs STRef s [Node d i r s m]
contradictions STRef s [Node d i r s m]
assumptions
               STRef s Bool
checkingContradictions
               STRef s (Node d i r s m -> String)
nodeString STRef s (JustRule d i r s m -> String)
justString STRef s (d -> String)
datumString STRef s (i -> String)
informantString
               STRef s (r -> JTMST s m ())
enqueueProcedure STRef s ([Node d i r s m] -> JTMST s m ())
contradictionHandler STRef s Bool
debugging)

-- |Helper function for writing setter command for `JTMS` components.
--
-- Not part of the original Lisp.
jtmsSetter :: Monad m =>
  (JTMS d i r s m -> STRef s v) -> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter :: (JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s v
field JTMS d i r s m
jtms = ExceptT JtmsErr (STT s m) () -> JTMST s m ()
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (ExceptT JtmsErr (STT s m) () -> JTMST s m ())
-> (v -> ExceptT JtmsErr (STT s m) ()) -> v -> JTMST s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STT s m () -> ExceptT JtmsErr (STT s m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m () -> ExceptT JtmsErr (STT s m) ())
-> (v -> STT s m ()) -> v -> ExceptT JtmsErr (STT s m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s v -> v -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (JTMS d i r s m -> STRef s v
field JTMS d i r s m
jtms)

-- |Set the display function for `Node`s in a `JTMS`.
--
-- After @change-jtms@ in @jtms.lisp@.
setNodeString ::
  Monad m => JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
setNodeString :: JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
setNodeString = (JTMS d i r s m -> STRef s (Node d i r s m -> String))
-> JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s v.
Monad m =>
(JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s (Node d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (Node d i r s m -> String)
jtmsNodeString

-- |When the node type @d@ implements `Show`, use this display method
-- as the standard for printing the node.
nodeStringByDatum :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()
nodeStringByDatum :: JTMS d i r s m -> JTMST s m ()
nodeStringByDatum JTMS d i r s m
jtms = JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
setNodeString JTMS d i r s m
jtms ((Node d i r s m -> String) -> JTMST s m ())
-> (Node d i r s m -> String) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ d -> String
forall a. Show a => a -> String
show (d -> String) -> (Node d i r s m -> d) -> Node d i r s m -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> d
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> d
nodeDatum

-- |Use the node index for its display.
nodeStringByIndex :: (Monad m) => JTMS d i r s m -> JTMST s m ()
nodeStringByIndex :: JTMS d i r s m -> JTMST s m ()
nodeStringByIndex JTMS d i r s m
jtms = JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
setNodeString JTMS d i r s m
jtms ((Node d i r s m -> String) -> JTMST s m ())
-> (Node d i r s m -> String) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show (Int -> String)
-> (Node d i r s m -> Int) -> Node d i r s m -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> Int
nodeIndex

-- |When the node type @d@ implements `Show`, use both the node index
-- and this display method as the standard for printing the node.
nodeStringByIndexDatum :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()
nodeStringByIndexDatum :: JTMS d i r s m -> JTMST s m ()
nodeStringByIndexDatum JTMS d i r s m
jtms = JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()
setNodeString JTMS d i r s m
jtms ((Node d i r s m -> String) -> JTMST s m ())
-> (Node d i r s m -> String) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ Node d i r s m
n ->
  (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> Int
nodeIndex Node d i r s m
n) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (d -> String
forall a. Show a => a -> String
show (d -> String) -> d -> String
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> d
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> d
nodeDatum Node d i r s m
n)

-- |Set the display function for the datum associated with each `Node`
-- in a `JTMS`.
setDatumString ::
  Monad m => JTMS d i r s m -> (d -> String) -> JTMST s m ()
setDatumString :: JTMS d i r s m -> (d -> String) -> JTMST s m ()
setDatumString = (JTMS d i r s m -> STRef s (d -> String))
-> JTMS d i r s m -> (d -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s v.
Monad m =>
(JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s (d -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (d -> String)
jtmsDatumString

-- |When the datum type @d@ implements `Show`, use this display method
-- as the standard for printing the datum.
datumStringByShow :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()
datumStringByShow :: JTMS d i r s m -> JTMST s m ()
datumStringByShow JTMS d i r s m
jtms = JTMS d i r s m -> (d -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> (d -> String) -> JTMST s m ()
setDatumString JTMS d i r s m
jtms d -> String
forall a. Show a => a -> String
show

-- |Set the display function for informants in a `JTMS`.
setInformantString ::
  Monad m => JTMS d i r s m -> (i -> String) -> JTMST s m ()
setInformantString :: JTMS d i r s m -> (i -> String) -> JTMST s m ()
setInformantString = (JTMS d i r s m -> STRef s (i -> String))
-> JTMS d i r s m -> (i -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s v.
Monad m =>
(JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s (i -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (i -> String)
jtmsInformantString

-- |When the informant type @i@ implements `Show`, use this display method
-- as the standard for printing the informant.
informantStringByShow :: (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()
informantStringByShow :: JTMS d i r s m -> JTMST s m ()
informantStringByShow JTMS d i r s m
jtms = JTMS d i r s m -> (i -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> (i -> String) -> JTMST s m ()
setInformantString JTMS d i r s m
jtms i -> String
forall a. Show a => a -> String
show

-- |Set the display function for `JustRule`s in a `JTMS`.
--
-- After @change-jtms@ in @jtms.lisp@.
setJustString ::
  Monad m => JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
setJustString :: JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
setJustString = (JTMS d i r s m -> STRef s (JustRule d i r s m -> String))
-> JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s v.
Monad m =>
(JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
jtmsJustString

-- |Use the `JustRule` index when printing the just.
justStringByIndex :: (Monad m) => JTMS d i r s m -> JTMST s m ()
justStringByIndex :: JTMS d i r s m -> JTMST s m ()
justStringByIndex JTMS d i r s m
jtms = JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
setJustString JTMS d i r s m
jtms ((JustRule d i r s m -> String) -> JTMST s m ())
-> (JustRule d i r s m -> String) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show (Int -> String)
-> (JustRule d i r s m -> Int) -> JustRule d i r s m -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JustRule d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> Int
justIndex

-- |When the informant type @i@ implements `Show`, use the `JustRule` index when printing the just.
justStringByInformant :: (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()
justStringByInformant :: JTMS d i r s m -> JTMST s m ()
justStringByInformant JTMS d i r s m
jtms = JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
setJustString JTMS d i r s m
jtms ((JustRule d i r s m -> String) -> JTMST s m ())
-> (JustRule d i r s m -> String) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ i -> String
forall a. Show a => a -> String
show (i -> String)
-> (JustRule d i r s m -> i) -> JustRule d i r s m -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JustRule d i r s m -> i
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> i
justInformant

-- |When the informant type @i@ implements `Show`, use the `JustRule` index when printing the just.
justStringByIndexInformant ::
  (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()
justStringByIndexInformant :: JTMS d i r s m -> JTMST s m ()
justStringByIndexInformant JTMS d i r s m
jtms = JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()
setJustString JTMS d i r s m
jtms ((JustRule d i r s m -> String) -> JTMST s m ())
-> (JustRule d i r s m -> String) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \JustRule d i r s m
j ->
  Int -> String
forall a. Show a => a -> String
show (JustRule d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> Int
justIndex JustRule d i r s m
j) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ i -> String
forall a. Show a => a -> String
show (JustRule d i r s m -> i
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> i
justInformant JustRule d i r s m
j)

-- |Turn on or turn off debugging in a JTMS.  This setting currently
-- has no effect.
--
-- After @change-jtms@ in @jtms.lisp@.
setDebugging :: Monad m => JTMS d i r s m -> Bool -> JTMST s m ()
setDebugging :: JTMS d i r s m -> Bool -> JTMST s m ()
setDebugging = (JTMS d i r s m -> STRef s Bool)
-> JTMS d i r s m -> Bool -> JTMST s m ()
forall (m :: * -> *) d i r s v.
Monad m =>
(JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Bool
jtmsDebugging

-- |Set whether the `JTMS` should issue external notifications of
-- contradictions.
--
-- After @change-jtms@ in @jtms.lisp@.
setCheckingContradictions :: Monad m => JTMS d i r s m -> Bool -> JTMST s m ()
setCheckingContradictions :: JTMS d i r s m -> Bool -> JTMST s m ()
setCheckingContradictions = (JTMS d i r s m -> STRef s Bool)
-> JTMS d i r s m -> Bool -> JTMST s m ()
forall (m :: * -> *) d i r s v.
Monad m =>
(JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Bool
jtmsCheckingContradictions

-- |Set the contradiction handler.  The `JTMS` default is to do
-- nothing; the intention is to allow a callback to the external
-- system using the `JTMS`.
--
-- After @change-jtms@ in @jtms.lisp@.
setContradictionHandler :: Monad m =>
  JTMS d i r s m -> ([Node d i r s m] -> JTMST s m ()) -> JTMST s m ()
setContradictionHandler :: JTMS d i r s m
-> ([Node d i r s m] -> JTMST s m ()) -> JTMST s m ()
setContradictionHandler = (JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ()))
-> JTMS d i r s m
-> ([Node d i r s m] -> JTMST s m ())
-> JTMST s m ()
forall (m :: * -> *) d i r s v.
Monad m =>
(JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ())
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ())
jtmsContradictionHandler

-- |Set the queuing behavior needed for the external system.
--
-- After @change-jtms@ in @jtms.lisp@.
setEnqueueProcedure :: Monad m =>
  JTMS d i r s m -> (r -> JTMST s m ()) -> JTMST s m ()
setEnqueueProcedure :: JTMS d i r s m -> (r -> JTMST s m ()) -> JTMST s m ()
setEnqueueProcedure = (JTMS d i r s m -> STRef s (r -> JTMST s m ()))
-> JTMS d i r s m -> (r -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) d i r s v.
Monad m =>
(JTMS d i r s m -> STRef s v)
-> JTMS d i r s m -> v -> JTMST s m ()
jtmsSetter JTMS d i r s m -> STRef s (r -> JTMST s m ())
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (r -> JTMST s m ())
jtmsEnqueueProcedure

-- * Basic inference-engine interface

-- |Returns @True@ if the current believed assumptions justify the
-- fact represented by the given node.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun in-node? (node) (eq (tms-node-label node) :IN))
isInNode :: Monad m => Node d i r s m -> JTMST s m Bool
isInNode :: Node d i r s m -> JTMST s m Bool
isInNode Node d i r s m
node = JTMSTInner s m Bool -> JTMST s m Bool
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m Bool -> JTMST s m Bool)
-> JTMSTInner s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ do
  Bool
believed <- STT s m Bool -> ExceptT JtmsErr (STT s m) Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m Bool -> ExceptT JtmsErr (STT s m) Bool)
-> STT s m Bool -> ExceptT JtmsErr (STT s m) Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeBelieved Node d i r s m
node)
  Bool -> ExceptT JtmsErr (STT s m) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
believed

-- |Returns @True@ if the current believed assumptions do not justify
-- the fact represented by the given node.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun out-node? (node) (eq (tms-node-label node) :OUT))
isOutNode :: Monad m => Node d i r s m -> JTMST s m Bool
isOutNode :: Node d i r s m -> JTMST s m Bool
isOutNode Node d i r s m
node = do
  Bool
believed <- Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isInNode Node d i r s m
node
  Bool -> JTMST s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> JTMST s m Bool) -> Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
believed

-- |Add a node to a JTMS.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun tms-create-node (jtms datum &key assumptionp contradictoryp)
-- >   (let ((node (make-tms-node :INDEX (incf (jtms-node-counter jtms))
-- >                              :DATUM datum
-- >                              :ASSUMPTION? assumptionp
-- >                              :CONTRADICTORY? contradictoryp
-- >                              :JTMS jtms)))
-- >     (if assumptionp (push node (jtms-assumptions jtms)))
-- >     (if contradictoryp (push node (jtms-contradictions jtms)))
-- >     (push node (jtms-nodes jtms))
-- >     node))
createNode :: Monad m => JTMS d i r s m -> d -> Bool -> Bool ->
                           JTMST s m (Node d i r s m)
createNode :: JTMS d i r s m -> d -> Bool -> Bool -> JTMST s m (Node d i r s m)
createNode JTMS d i r s m
jtms d
datum Bool
isAssumption Bool
isContradictory = JTMSTInner s m (Node d i r s m) -> JTMST s m (Node d i r s m)
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m (Node d i r s m) -> JTMST s m (Node d i r s m))
-> JTMSTInner s m (Node d i r s m) -> JTMST s m (Node d i r s m)
forall a b. (a -> b) -> a -> b
$ do
  Int
nodeIdx <- JTMS d i r s m -> JTMSTInner s m Int
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> JTMSTInner s m Int
nextNodeCounter JTMS d i r s m
jtms
  STT s m (Node d i r s m)
-> ExceptT JtmsErr (STT s m) (Node d i r s m)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m (Node d i r s m)
 -> ExceptT JtmsErr (STT s m) (Node d i r s m))
-> STT s m (Node d i r s m)
-> ExceptT JtmsErr (STT s m) (Node d i r s m)
forall a b. (a -> b) -> a -> b
$ do
    STRef s Bool
assumptionRef <- Bool -> STT s m (STRef s Bool)
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef Bool
isAssumption
    STRef s Bool
contraRef <- Bool -> STT s m (STRef s Bool)
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef Bool
isContradictory
    STRef s (Maybe (Justification d i r s m))
supportRef <- Maybe (Justification d i r s m)
-> STT s m (STRef s (Maybe (Justification d i r s m)))
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef Maybe (Justification d i r s m)
forall a. Maybe a
Nothing
    STRef s Bool
believedRef <- Bool -> STT s m (STRef s Bool)
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef Bool
False
    STRef s [JustRule d i r s m]
conseqRef <- [JustRule d i r s m] -> STT s m (STRef s [JustRule d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
    STRef s [r]
inRulesRef <- [r] -> STT s m (STRef s [r])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
    STRef s [r]
outRulesRef <- [r] -> STT s m (STRef s [r])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
    STRef s [JustRule d i r s m]
justsRef <- [JustRule d i r s m] -> STT s m (STRef s [JustRule d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
    let node :: Node d i r s m
node = Int
-> d
-> JTMS d i r s m
-> STRef s Bool
-> STRef s Bool
-> STRef s (Maybe (Justification d i r s m))
-> STRef s Bool
-> STRef s [JustRule d i r s m]
-> STRef s [r]
-> STRef s [r]
-> STRef s [JustRule d i r s m]
-> Node d i r s m
forall d i r s (m :: * -> *).
Int
-> d
-> JTMS d i r s m
-> STRef s Bool
-> STRef s Bool
-> STRef s (Maybe (Justification d i r s m))
-> STRef s Bool
-> STRef s [JustRule d i r s m]
-> STRef s [r]
-> STRef s [r]
-> STRef s [JustRule d i r s m]
-> Node d i r s m
Node Int
nodeIdx d
datum JTMS d i r s m
jtms STRef s Bool
assumptionRef STRef s Bool
contraRef
                    STRef s (Maybe (Justification d i r s m))
supportRef STRef s Bool
believedRef STRef s [JustRule d i r s m]
conseqRef
                    STRef s [r]
inRulesRef STRef s [r]
outRulesRef STRef s [JustRule d i r s m]
justsRef
        nodeListRef :: STRef s [Node d i r s m]
nodeListRef = JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsNodes JTMS d i r s m
jtms
      in do
        if Bool
isAssumption
          then Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
node (STRef s [Node d i r s m] -> STT s m ())
-> STRef s [Node d i r s m] -> STT s m ()
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsAssumptions JTMS d i r s m
jtms
          else () -> STT s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

        if Bool
isContradictory
          then Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
node (STRef s [Node d i r s m] -> STT s m ())
-> STRef s [Node d i r s m] -> STT s m ()
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsContradictions JTMS d i r s m
jtms
          else () -> STT s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

        Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
node STRef s [Node d i r s m]
nodeListRef

        Node d i r s m -> STT s m (Node d i r s m)
forall (m :: * -> *) a. Monad m => a -> m a
return Node d i r s m
node

-- |Internal method used to flag this node as an assumption, and to
-- enable belief in this assumption.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > ;;; Converts a regular node to an assumption and enables it.
-- > (defun assume-node (node &aux (jtms (tms-node-jtms node)))
-- >   (unless (or (tms-node-assumption? node) (tms-node-premise? node))
-- >     (debugging-jtms jtms "~%Converting ~A into an assumption" node)
-- >     (setf (tms-node-assumption? node) t)
-- >     (push node (jtms-assumptions jtms)))
-- >   (enable-assumption node))
assumeNode :: Monad m => Node d i r s m -> JTMST s m ()
assumeNode :: Node d i r s m -> JTMST s m ()
assumeNode Node d i r s m
node =
  let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
      isAssumptionRef :: STRef s Bool
isAssumptionRef = Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeIsAssumption Node d i r s m
node
  in do
    JTMST s m Bool -> JTMST s m () -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((JTMST s m Bool -> JTMST s m Bool
forall (m :: * -> *). Functor m => m Bool -> m Bool
notM (JTMST s m Bool -> JTMST s m Bool)
-> JTMST s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s Bool
isAssumptionRef)
          JTMST s m Bool -> JTMST s m Bool -> JTMST s m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
&&^ (JTMST s m Bool -> JTMST s m Bool
forall (m :: * -> *). Functor m => m Bool -> m Bool
notM (JTMST s m Bool -> JTMST s m Bool)
-> JTMST s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
nodeIsPremise Node d i r s m
node))
      (do STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> Bool -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef STRef s Bool
isAssumptionRef Bool
True
          STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
node (STRef s [Node d i r s m] -> STT s m ())
-> STRef s [Node d i r s m] -> STT s m ()
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsAssumptions JTMS d i r s m
jtms)
      (() -> JTMST s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    Node d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m ()
enableAssumption Node d i r s m
node

-- |API command used when the external system categorizes this node as
-- representing a contradiction.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun make-contradiction (node &aux (jtms (tms-node-jtms node)))
-- >   (unless (tms-node-contradictory? node)
-- >     (setf (tms-node-contradictory? node) t)
-- >     (push node (jtms-contradictions jtms))
-- >     (check-for-contradictions jtms)))
makeContradiction :: Monad m => Node d i r s m -> JTMST s m ()
makeContradiction :: Node d i r s m -> JTMST s m ()
makeContradiction Node d i r s m
node =
  let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
      isContraRef :: STRef s Bool
isContraRef = Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeIsContradictory Node d i r s m
node
  in do
    JTMST s m Bool -> JTMST s m () -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (JTMST s m Bool -> JTMST s m Bool
forall (m :: * -> *). Functor m => m Bool -> m Bool
notM (JTMST s m Bool -> JTMST s m Bool)
-> JTMST s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s Bool
isContraRef)
      (do STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> Bool -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef STRef s Bool
isContraRef Bool
False
          STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
node (STRef s [Node d i r s m] -> STT s m ())
-> STRef s [Node d i r s m] -> STT s m ()
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsContradictions JTMS d i r s m
jtms
          JTMS d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> JTMST s m ()
checkForContradictions JTMS d i r s m
jtms)
      (() -> JTMST s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())

-- |Add a rule for concluding belief in the @consequence@.  The rule
-- is triggered when the @antecedents@ are all believed, and is
-- associated with (perhaps named as) the @informant@.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun justify-node (informant consequence antecedents &aux just jtms)
-- >   (setq jtms (tms-node-jtms consequence)
-- >      just (make-just :INDEX (incf (jtms-just-counter jtms))
-- >                      :INFORMANT informant
-- >                      :CONSEQUENCE consequence
-- >                      :ANTECEDENTS antecedents))
-- >   (push just (tms-node-justs consequence))
-- >   (dolist (node antecedents) (push just (tms-node-consequences node)))
-- >   (push just (jtms-justs jtms))
-- >   (debugging-jtms jtms
-- >                "~%Justifying ~A by ~A using ~A."
-- >                consequence
-- >                informant
-- >                (mapcar #'node-string antecedents))
-- >   (if (or antecedents (out-node? consequence))
-- >       (if (check-justification just) (install-support consequence just))
-- >       (setf (tms-node-support consequence) just))
-- >   (check-for-contradictions jtms))
justifyNode :: Monad m =>
                 i -> Node d i r s m -> [Node d i r s m] -> JTMST s m ()
justifyNode :: i -> Node d i r s m -> [Node d i r s m] -> JTMST s m ()
justifyNode i
informant Node d i r s m
consequence [Node d i r s m]
antecedents =
  let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
consequence
  in do
    Int
justIdx <- JTMSTInner s m Int -> JTMST s m Int
forall s (m :: * -> *) a. JTMSTInner s m a -> JTMST s m a
JtmsT (JTMSTInner s m Int -> JTMST s m Int)
-> JTMSTInner s m Int -> JTMST s m Int
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> JTMSTInner s m Int
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> JTMSTInner s m Int
nextJustCounter JTMS d i r s m
jtms
    let just :: JustRule d i r s m
just = Int
-> i -> Node d i r s m -> [Node d i r s m] -> JustRule d i r s m
forall d i r s (m :: * -> *).
Int
-> i -> Node d i r s m -> [Node d i r s m] -> JustRule d i r s m
JustRule Int
justIdx i
informant Node d i r s m
consequence [Node d i r s m]
antecedents

    -- Add this new JustRule as a possible justification of the
    -- consequent.
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> STRef s [JustRule d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push JustRule d i r s m
just (STRef s [JustRule d i r s m] -> STT s m ())
-> STRef s [JustRule d i r s m] -> STT s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [JustRule d i r s m]
nodeJusts Node d i r s m
consequence

    -- For each antecedent, add the new rule as a possible consequence
    -- of that antecedent node.
    [Node d i r s m]
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Node d i r s m]
antecedents ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ Node d i r s m
node -> do
      STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> STRef s [JustRule d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push JustRule d i r s m
just (STRef s [JustRule d i r s m] -> STT s m ())
-> STRef s [JustRule d i r s m] -> STT s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [JustRule d i r s m]
nodeConsequences Node d i r s m
node

    -- Add the new rule to the JTMS's list of justification rules.
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> STRef s [JustRule d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push JustRule d i r s m
just (STRef s [JustRule d i r s m] -> STT s m ())
-> STRef s [JustRule d i r s m] -> STT s m ()
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [JustRule d i r s m]
jtmsJusts JTMS d i r s m
jtms

    -- We attempt to use this new rule right now if either the
    -- consequence is currently OUT, or if there actually are
    -- antecedents.
    JTMST s m Bool -> JTMST s m () -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Bool -> JTMST s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> JTMST s m Bool) -> Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Node d i r s m]
antecedents)
          JTMST s m Bool -> JTMST s m Bool -> JTMST s m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
||^ (STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STT s m Bool -> STT s m Bool
forall (m :: * -> *). Functor m => m Bool -> m Bool
notM (STT s m Bool -> STT s m Bool) -> STT s m Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool) -> STRef s Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeBelieved Node d i r s m
consequence))
      -- To use the rule now, if the antecedents are satisfied, add it
      -- as a support for the consequence.
      (JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (JustRule d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
JustRule d i r s m -> JTMST s m Bool
checkJustification JustRule d i r s m
just) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$
       Node d i r s m -> Justification d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> Justification d i r s m -> JTMST s m ()
installSupport Node d i r s m
consequence (Justification d i r s m -> JTMST s m ())
-> Justification d i r s m -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> Justification d i r s m
forall d i r s (m :: * -> *).
JustRule d i r s m -> Justification d i r s m
ByRule JustRule d i r s m
just)
      -- Otherwise we can install as a support straightaway.
      (STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> Maybe (Justification d i r s m) -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
consequence) (Maybe (Justification d i r s m) -> STT s m ())
-> Maybe (Justification d i r s m) -> STT s m ()
forall a b. (a -> b) -> a -> b
$ Justification d i r s m -> Maybe (Justification d i r s m)
forall a. a -> Maybe a
Just (Justification d i r s m -> Maybe (Justification d i r s m))
-> Justification d i r s m -> Maybe (Justification d i r s m)
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> Justification d i r s m
forall d i r s (m :: * -> *).
JustRule d i r s m -> Justification d i r s m
ByRule JustRule d i r s m
just)

    -- Check for new contradictions introduced with this rule.
    JTMS d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> JTMST s m ()
checkForContradictions JTMS d i r s m
jtms

-- * Support for adding justifications

-- |Detect the case when justification @just@ is satisfied, but the
-- `JTMS` does not believe its consequence.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun check-justification (just)
-- >   (and (out-node? (just-consequence just))
-- >        (justification-satisfied? just)))
checkJustification :: Monad m => JustRule d i r s m -> JTMST s m Bool
checkJustification :: JustRule d i r s m -> JTMST s m Bool
checkJustification JustRule d i r s m
just =
  (Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isOutNode (Node d i r s m -> JTMST s m Bool)
-> Node d i r s m -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> Node d i r s m
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> Node d i r s m
justConsequence JustRule d i r s m
just) JTMST s m Bool -> JTMST s m Bool -> JTMST s m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
&&^ JustRule d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
JustRule d i r s m -> JTMST s m Bool
isJustificationSatisfied JustRule d i r s m
just

-- |Returns @True@ when all of the antecedents of justification @j@
-- are believed by the `JTMS`.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun justification-satisfied? (just)
-- >   (every #'in-node? (just-antecedents just)))
isJustificationSatisfied :: Monad m => JustRule d i r s m -> JTMST s m Bool
isJustificationSatisfied :: JustRule d i r s m -> JTMST s m Bool
isJustificationSatisfied JustRule d i r s m
j = (Node d i r s m -> JTMST s m Bool)
-> [Node d i r s m] -> JTMST s m Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
allM Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isInNode ([Node d i r s m] -> JTMST s m Bool)
-> [Node d i r s m] -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> [Node d i r s m]
justAntecedents JustRule d i r s m
j

-- |Add a reason for this @conseq@ node to be believed.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun install-support (conseq just)
-- >   (make-node-in conseq just)
-- >   (propagate-inness conseq))
installSupport ::
  Monad m => Node d i r s m -> Justification d i r s m -> JTMST s m ()
installSupport :: Node d i r s m -> Justification d i r s m -> JTMST s m ()
installSupport Node d i r s m
node Justification d i r s m
just = do
  Node d i r s m -> Justification d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> Justification d i r s m -> JTMST s m ()
makeNodeIn Node d i r s m
node Justification d i r s m
just
  Node d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m ()
propagateInness Node d i r s m
node

-- |Trigger justifications which rely (directly or indirectly) on the
-- @node@ as an antecedent when @node@ becomes believed.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun propagate-inness (node &aux (jtms (tms-node-jtms node))
-- >                                    (q (list node)))
-- >   (do () ((null (setq node (pop q))))
-- >     (debugging-jtms jtms "~%   Propagating belief in ~A." node)
-- >     (dolist (justification (tms-node-consequences node))
-- >       (when (check-justification justification)
-- >         (make-node-in (just-consequence justification) justification)
-- >         (push (just-consequence justification) q)))))
propagateInness :: Monad m => Node d i r s m -> JTMST s m ()
propagateInness :: Node d i r s m -> JTMST s m ()
propagateInness Node d i r s m
fromNode =
  let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
fromNode
  in do
    STRef s [Node d i r s m]
queue <- STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STRef s [Node d i r s m])
 -> JTMST s m (STRef s [Node d i r s m]))
-> STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef [Node d i r s m
fromNode]
    JTMST s m (Maybe (Node d i r s m))
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whileReturnJust (STT s m (Maybe (Node d i r s m))
-> JTMST s m (Maybe (Node d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Node d i r s m))
 -> JTMST s m (Maybe (Node d i r s m)))
-> STT s m (Maybe (Node d i r s m))
-> JTMST s m (Maybe (Node d i r s m))
forall a b. (a -> b) -> a -> b
$ STRef s [Node d i r s m] -> STT s m (Maybe (Node d i r s m))
forall (m :: * -> *) s a.
Monad m =>
STRef s [a] -> STT s m (Maybe a)
pop STRef s [Node d i r s m]
queue) ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ Node d i r s m
node -> do
      [JustRule d i r s m]
justs <- STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m])
-> STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m])
-> STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [JustRule d i r s m]
nodeConsequences Node d i r s m
node
      [JustRule d i r s m]
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [JustRule d i r s m]
justs ((JustRule d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ JustRule d i r s m
j ->
        JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (JustRule d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
JustRule d i r s m -> JTMST s m Bool
checkJustification JustRule d i r s m
j) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$
          let conseq :: Node d i r s m
conseq = JustRule d i r s m -> Node d i r s m
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> Node d i r s m
justConsequence JustRule d i r s m
j
          in do
            Node d i r s m -> Justification d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> Justification d i r s m -> JTMST s m ()
makeNodeIn Node d i r s m
conseq (Justification d i r s m -> JTMST s m ())
-> Justification d i r s m -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> Justification d i r s m
forall d i r s (m :: * -> *).
JustRule d i r s m -> Justification d i r s m
ByRule JustRule d i r s m
j
            STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
conseq STRef s [Node d i r s m]
queue

-- |Called when the given @reason@ causes the JTMS to believe @node@.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun make-node-in (conseq reason &aux jtms enqueuef)
-- >   (setq jtms (tms-node-jtms conseq)
-- >      enqueuef (jtms-enqueue-procedure jtms))
-- >   (debugging-jtms jtms "~%     Making ~A in via ~A."
-- >           conseq
-- >           (if (symbolp reason)
-- >               reason
-- >               (cons (just-informant reason)
-- >                     (mapcar (jtms-node-string jtms)
-- >                             (just-antecedents reason)))))
-- >   (setf (tms-node-label conseq) :IN)
-- >   (setf (tms-node-support conseq) reason)
-- >   (when enqueuef
-- >     (dolist (in-rule (tms-node-in-rules conseq))
-- >       (funcall enqueuef in-rule))
-- >     (setf (tms-node-in-rules conseq) nil)))
makeNodeIn ::
  Monad m => Node d i r s m -> Justification d i r s m -> JTMST s m ()
makeNodeIn :: Node d i r s m -> Justification d i r s m -> JTMST s m ()
makeNodeIn Node d i r s m
conseq Justification d i r s m
reason =
  let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
conseq
  in do
    r -> JTMST s m ()
enqueuef <- STT s m (r -> JTMST s m ()) -> JTMST s m (r -> JTMST s m ())
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (r -> JTMST s m ()) -> JTMST s m (r -> JTMST s m ()))
-> STT s m (r -> JTMST s m ()) -> JTMST s m (r -> JTMST s m ())
forall a b. (a -> b) -> a -> b
$ STRef s (r -> JTMST s m ()) -> STT s m (r -> JTMST s m ())
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (r -> JTMST s m ()) -> STT s m (r -> JTMST s m ()))
-> STRef s (r -> JTMST s m ()) -> STT s m (r -> JTMST s m ())
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (r -> JTMST s m ())
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (r -> JTMST s m ())
jtmsEnqueueProcedure JTMS d i r s m
jtms
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> Bool -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeBelieved Node d i r s m
conseq) Bool
True
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> Maybe (Justification d i r s m) -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
conseq) (Maybe (Justification d i r s m) -> STT s m ())
-> Maybe (Justification d i r s m) -> STT s m ()
forall a b. (a -> b) -> a -> b
$ Justification d i r s m -> Maybe (Justification d i r s m)
forall a. a -> Maybe a
Just Justification d i r s m
reason
    JTMST s m [r] -> (r -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (STT s m [r] -> JTMST s m [r]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [r] -> JTMST s m [r]) -> STT s m [r] -> JTMST s m [r]
forall a b. (a -> b) -> a -> b
$ STRef s [r] -> STT s m [r]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [r] -> STT s m [r]) -> STRef s [r] -> STT s m [r]
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [r]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [r]
nodeInRules Node d i r s m
conseq) r -> JTMST s m ()
enqueuef
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s [r] -> [r] -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (Node d i r s m -> STRef s [r]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [r]
nodeInRules Node d i r s m
conseq) []

-- > * Assumption Manipulation

-- |This command is called when the external system chooses to
-- disbelieve the assumption represented by @node@.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun retract-assumption (node &aux jtms)
-- >   (when (eq (tms-node-support node) :ENABLED-ASSUMPTION)
-- >     (setq jtms (tms-node-jtms node))
-- >     (debugging-jtms jtms "~%  Retracting assumption ~A." node)
-- >     (make-node-out node)
-- >     (find-alternative-support jtms
-- >                               (cons node (propagate-outness node jtms)))))
retractAssumption :: Monad m => Node d i r s m -> JTMST s m ()
retractAssumption :: Node d i r s m -> JTMST s m ()
retractAssumption Node d i r s m
node = do
  Maybe (Justification d i r s m)
support <- STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Justification d i r s m))
 -> JTMST s m (Maybe (Justification d i r s m)))
-> STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node)
  case Maybe (Justification d i r s m)
support of
    Just Justification d i r s m
EnabledAssumption ->
      let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
      in do
        Node d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m ()
makeNodeOut Node d i r s m
node
        [Node d i r s m]
propagated <- Node d i r s m -> JTMS d i r s m -> JTMST s m [Node d i r s m]
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMS d i r s m -> JTMST s m [Node d i r s m]
propagateOutness Node d i r s m
node JTMS d i r s m
jtms
        JTMS d i r s m -> [Node d i r s m] -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> [Node d i r s m] -> JTMST s m ()
findAlternativeSupport JTMS d i r s m
jtms ([Node d i r s m] -> JTMST s m ())
-> [Node d i r s m] -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m
node Node d i r s m -> [Node d i r s m] -> [Node d i r s m]
forall a. a -> [a] -> [a]
: [Node d i r s m]
propagated
    Maybe (Justification d i r s m)
_ -> () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- |Return whether the given node is an enabled assumption.
isEnabledAssumption :: Monad m => Node d i r s m -> JTMST s m Bool
isEnabledAssumption :: Node d i r s m -> JTMST s m Bool
isEnabledAssumption Node d i r s m
node = do
  Maybe (Justification d i r s m)
support <- STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Justification d i r s m))
 -> JTMST s m (Maybe (Justification d i r s m)))
-> STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Maybe (Justification d i r s m))
 -> STT s m (Maybe (Justification d i r s m)))
-> STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node
  case Maybe (Justification d i r s m)
support of
    Just Justification d i r s m
EnabledAssumption -> Bool -> JTMST s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Maybe (Justification d i r s m)
_ -> Bool -> JTMST s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- |Check whether the given node is supported by a `JustRule`.  If it
-- is, run the given computation with that `JustRule`.
whenSupportedByRule :: Monad m =>
  Node d i r s m -> (JustRule d i r s m -> JTMST s m a) -> JTMST s m (Maybe a)
whenSupportedByRule :: Node d i r s m
-> (JustRule d i r s m -> JTMST s m a) -> JTMST s m (Maybe a)
whenSupportedByRule Node d i r s m
node JustRule d i r s m -> JTMST s m a
body = do
  Maybe (Justification d i r s m)
support <- STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Justification d i r s m))
 -> JTMST s m (Maybe (Justification d i r s m)))
-> STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Maybe (Justification d i r s m))
 -> STT s m (Maybe (Justification d i r s m)))
-> STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node
  case Maybe (Justification d i r s m)
support of
    Just (ByRule JustRule d i r s m
just) -> do
      a
result <- JustRule d i r s m -> JTMST s m a
body JustRule d i r s m
just
      Maybe a -> JTMST s m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> JTMST s m (Maybe a)) -> Maybe a -> JTMST s m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
result
    Maybe (Justification d i r s m)
_ -> Maybe a -> JTMST s m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing

-- |Check whether the given node is supported by a `JustRule`.  If it
-- is, run the @thenM@ computation with that `JustRule`; if not, run
-- the @elseM@ computation.
ifSupportedByRule :: Monad m =>
  Node d i r s m -> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
    -> JTMST s m ()
ifSupportedByRule :: Node d i r s m
-> (JustRule d i r s m -> JTMST s m ())
-> JTMST s m ()
-> JTMST s m ()
ifSupportedByRule Node d i r s m
node JustRule d i r s m -> JTMST s m ()
thenM JTMST s m ()
elseM = do
  Maybe (Justification d i r s m)
support <- STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Justification d i r s m))
 -> JTMST s m (Maybe (Justification d i r s m)))
-> STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Maybe (Justification d i r s m))
 -> STT s m (Maybe (Justification d i r s m)))
-> STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node
  case Maybe (Justification d i r s m)
support of
    Just (ByRule JustRule d i r s m
just) -> JustRule d i r s m -> JTMST s m ()
thenM JustRule d i r s m
just
    Maybe (Justification d i r s m)
_ -> JTMST s m ()
elseM

supportAntecedents :: Monad m => Node d i r s m -> JTMST s m [Node d i r s m]
supportAntecedents :: Node d i r s m -> JTMST s m [Node d i r s m]
supportAntecedents Node d i r s m
node = do
  Maybe (Justification d i r s m)
support <- STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Justification d i r s m))
 -> JTMST s m (Maybe (Justification d i r s m)))
-> STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Maybe (Justification d i r s m))
 -> STT s m (Maybe (Justification d i r s m)))
-> STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node
  case Maybe (Justification d i r s m)
support of
    Just (ByRule JustRule d i r s m
j) -> [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Node d i r s m] -> JTMST s m [Node d i r s m])
-> [Node d i r s m] -> JTMST s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> [Node d i r s m]
justAntecedents JustRule d i r s m
j
    Maybe (Justification d i r s m)
_ -> [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) a. Monad m => a -> m a
return []

emptySupportAntecedents :: Monad m => Node d i r s m -> JTMST s m Bool
emptySupportAntecedents :: Node d i r s m -> JTMST s m Bool
emptySupportAntecedents Node d i r s m
node = do
  [Node d i r s m]
ants <- Node d i r s m -> JTMST s m [Node d i r s m]
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m [Node d i r s m]
supportAntecedents Node d i r s m
node
  Bool -> JTMST s m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> JTMST s m Bool) -> Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Node d i r s m]
ants

-- |Called when the external system chooses to believe the assumption
-- represented by @node@.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun enable-assumption (node &aux (jtms (tms-node-jtms node)))
-- >   (unless (tms-node-assumption? node)
-- >     (tms-error "Can't enable the non-assumption ~A" node))
-- >   (debugging-jtms jtms "~%  Enabling assumption ~A." node)
-- >   (cond
-- >      ((out-node? node)
-- >       (make-node-in node :ENABLED-ASSUMPTION)
-- >       (propagate-inness node))
-- >      ((or (eq (tms-node-support node) :ENABLED-ASSUMPTION)
-- >           (null (just-antecedents (tms-node-support node)))))
-- >      (t (setf (tms-node-support node) :ENABLED-ASSUMPTION)))
-- >   (check-for-contradictions jtms))
enableAssumption :: Monad m => Node d i r s m -> JTMST s m ()
enableAssumption :: Node d i r s m -> JTMST s m ()
enableAssumption Node d i r s m
node =
  let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
  in do
    JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (JTMST s m Bool -> JTMST s m Bool
forall (m :: * -> *). Functor m => m Bool -> m Bool
notM (JTMST s m Bool -> JTMST s m Bool)
-> JTMST s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool) -> STRef s Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeIsAssumption Node d i r s m
node) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$
      ExceptT JtmsErr (STT s m) () -> JTMST s m ()
forall (m :: * -> *) s r.
Monad m =>
ExceptT JtmsErr (STT s m) r -> JTMST s m r
jLiftExcept (ExceptT JtmsErr (STT s m) () -> JTMST s m ())
-> ExceptT JtmsErr (STT s m) () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ JtmsErr -> ExceptT JtmsErr (STT s m) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (JtmsErr -> ExceptT JtmsErr (STT s m) ())
-> JtmsErr -> ExceptT JtmsErr (STT s m) ()
forall a b. (a -> b) -> a -> b
$
        String -> Int -> JtmsErr
CannotEnableNonassumption (JTMS d i r s m -> String
forall d i r s (m :: * -> *). Monad m => JTMS d i r s m -> String
jtmsTitle JTMS d i r s m
jtms) (Node d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> Int
nodeIndex Node d i r s m
node)
    JTMST s m Bool -> JTMST s m () -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isOutNode Node d i r s m
node)
      (do Node d i r s m -> Justification d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> Justification d i r s m -> JTMST s m ()
makeNodeIn Node d i r s m
node Justification d i r s m
forall d i r s (m :: * -> *). Justification d i r s m
EnabledAssumption
          Node d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m ()
propagateInness Node d i r s m
node)
      (JTMST s m Bool -> JTMST s m () -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isEnabledAssumption Node d i r s m
node JTMST s m Bool -> JTMST s m Bool -> JTMST s m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
||^ Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
emptySupportAntecedents Node d i r s m
node)
        (() -> JTMST s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
        (STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> Maybe (Justification d i r s m) -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node) (Maybe (Justification d i r s m) -> STT s m ())
-> Maybe (Justification d i r s m) -> STT s m ()
forall a b. (a -> b) -> a -> b
$ Justification d i r s m -> Maybe (Justification d i r s m)
forall a. a -> Maybe a
Just Justification d i r s m
forall d i r s (m :: * -> *). Justification d i r s m
EnabledAssumption))
    JTMS d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> JTMST s m ()
checkForContradictions JTMS d i r s m
jtms

-- |Called when the JTMS disbelieves @node@.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun make-node-out (node &aux jtms enqueuef)
-- >   (setq jtms (tms-node-jtms node)
-- >      enqueuef (jtms-enqueue-procedure jtms))
-- >   (debugging-jtms jtms "~%     retracting belief in ~a." node)
-- >   (setf (tms-node-support node) nil)
-- >   (setf (tms-node-label node) :OUT)
-- >   (if enqueuef (dolist (out-rule (tms-node-out-rules node))
-- >               (funcall enqueuef out-rule)))
-- >   (setf (tms-node-out-rules node) nil))
makeNodeOut :: Monad m => Node d i r s m -> JTMST s m ()
makeNodeOut :: Node d i r s m -> JTMST s m ()
makeNodeOut Node d i r s m
node =
  let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
  in do
    r -> JTMST s m ()
enqueuef <- STT s m (r -> JTMST s m ()) -> JTMST s m (r -> JTMST s m ())
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (r -> JTMST s m ()) -> JTMST s m (r -> JTMST s m ()))
-> STT s m (r -> JTMST s m ()) -> JTMST s m (r -> JTMST s m ())
forall a b. (a -> b) -> a -> b
$ STRef s (r -> JTMST s m ()) -> STT s m (r -> JTMST s m ())
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (r -> JTMST s m ()) -> STT s m (r -> JTMST s m ()))
-> STRef s (r -> JTMST s m ()) -> STT s m (r -> JTMST s m ())
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (r -> JTMST s m ())
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (r -> JTMST s m ())
jtmsEnqueueProcedure JTMS d i r s m
jtms
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> Maybe (Justification d i r s m) -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node) Maybe (Justification d i r s m)
forall a. Maybe a
Nothing
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> Bool -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeBelieved Node d i r s m
node) Bool
False
    JTMST s m [r] -> (r -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (STT s m [r] -> JTMST s m [r]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [r] -> JTMST s m [r]) -> STT s m [r] -> JTMST s m [r]
forall a b. (a -> b) -> a -> b
$ STRef s [r] -> STT s m [r]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (Node d i r s m -> STRef s [r]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [r]
nodeOutRules Node d i r s m
node)) ((r -> JTMST s m ()) -> JTMST s m ())
-> (r -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ r
outRule ->
      r -> JTMST s m ()
enqueuef r
outRule
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s [r] -> [r] -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (Node d i r s m -> STRef s [r]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [r]
nodeOutRules Node d i r s m
node) []

-- |Propagate the retraction of an assumption by finding all other
-- nodes which used that assumption in their justification.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun propagate-outness (node jtms &aux out-queue)
-- >   (debugging-jtms jtms "~%   Propagating disbelief in ~A." node)
-- >   (do ((js (tms-node-consequences node) (append (cdr js) new))
-- >        (new nil nil)
-- >        (conseq nil))
-- >       ((null js) out-queue)
-- >     ;; For each justification using the node, check to see if
-- >     ;; it supports some other node.  If so, forget that node,
-- >     ;; queue up the node to look for other support, and recurse
-- >     (setq conseq (just-consequence (car js)))
-- >     (when (eq (tms-node-support conseq) (car js))
-- >       (make-node-out conseq)
-- >       (push conseq out-queue)
-- >       (setq new (tms-node-consequences conseq)))))
propagateOutness ::
  Monad m => Node d i r s m -> JTMS d i r s m -> JTMST s m [Node d i r s m]
propagateOutness :: Node d i r s m -> JTMS d i r s m -> JTMST s m [Node d i r s m]
propagateOutness Node d i r s m
node JTMS d i r s m
jtms = do
  STRef s [Node d i r s m]
result <- STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STRef s [Node d i r s m])
 -> JTMST s m (STRef s [Node d i r s m]))
-> STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
  STRef s [JustRule d i r s m]
queue <- STT s m (STRef s [JustRule d i r s m])
-> JTMST s m (STRef s [JustRule d i r s m])
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STRef s [JustRule d i r s m])
 -> JTMST s m (STRef s [JustRule d i r s m]))
-> STT s m (STRef s [JustRule d i r s m])
-> JTMST s m (STRef s [JustRule d i r s m])
forall a b. (a -> b) -> a -> b
$ [JustRule d i r s m] -> STT s m (STRef s [JustRule d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
  JTMST s m [JustRule d i r s m]
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (Node d i r s m -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m [JustRule d i r s m]
getNodeConsequences Node d i r s m
node) ((JustRule d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \JustRule d i r s m
j -> STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> STRef s [JustRule d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push JustRule d i r s m
j STRef s [JustRule d i r s m]
queue
  (forall r. STT s m r -> JTMST s m r)
-> STRef s [JustRule d i r s m]
-> (JustRule d i r s m -> JTMST s m ())
-> JTMST s m ()
forall (m0 :: * -> *) (m :: * -> *) s a.
(Monad m0, Monad m) =>
(forall r. STT s m0 r -> m r) -> STRef s [a] -> (a -> m ()) -> m ()
whileListM_ forall r. STT s m r -> JTMST s m r
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT STRef s [JustRule d i r s m]
queue ((JustRule d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \JustRule d i r s m
j ->
    let conseq :: Node d i r s m
conseq = JustRule d i r s m -> Node d i r s m
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> Node d i r s m
justConsequence JustRule d i r s m
j
    in JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Node d i r s m -> JustRule d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JustRule d i r s m -> JTMST s m Bool
getIsNodeSupportedBy Node d i r s m
conseq JustRule d i r s m
j) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ do
      Node d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m ()
makeNodeOut Node d i r s m
conseq
      STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
conseq STRef s [Node d i r s m]
result
      [JustRule d i r s m]
further <- Node d i r s m -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m [JustRule d i r s m]
getNodeConsequences Node d i r s m
conseq
      STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ [JustRule d i r s m] -> STRef s [JustRule d i r s m] -> STT s m ()
forall (m :: * -> *) (t :: * -> *) a s.
(Monad m, Traversable t) =>
t a -> STRef s [a] -> STT s m ()
pushAll [JustRule d i r s m]
further STRef s [JustRule d i r s m]
queue
  STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s [Node d i r s m]
result

-- |Search for support for nodes @outs@ which were disbelieved after an
-- assumption retraction.
--
-- The original Lisp code returns the justification when
-- short-circuiting from the inner loop.  But this return value is
-- never used; moreover there is no return value used from callers of
-- this function.  So this type-checked translation returns the unit
-- value.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun find-alternative-support (jtms out-queue)
-- >   (debugging-jtms jtms "~%   Looking for alternative supports.")
-- >   (dolist (node out-queue)
-- >     (unless (in-node? node)
-- >       (dolist (just (tms-node-justs node))
-- >         (when (check-justification just)
-- >           (install-support (just-consequence just) just)
-- >           (return just))))))
findAlternativeSupport ::
  Monad m => JTMS d i r s m -> [Node d i r s m] -> JTMST s m ()
findAlternativeSupport :: JTMS d i r s m -> [Node d i r s m] -> JTMST s m ()
findAlternativeSupport JTMS d i r s m
jtms [Node d i r s m]
outs = do
  STRef s [Node d i r s m]
stack <- STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STRef s [Node d i r s m])
 -> JTMST s m (STRef s [Node d i r s m]))
-> STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef [Node d i r s m]
outs
  (forall r. STT s m r -> JTMST s m r)
-> STRef s [Node d i r s m]
-> (Node d i r s m -> JTMST s m ())
-> JTMST s m ()
forall (m0 :: * -> *) (m :: * -> *) s a.
(Monad m0, Monad m) =>
(forall r. STT s m0 r -> m r) -> STRef s [a] -> (a -> m ()) -> m ()
whileListM_ forall r. STT s m r -> JTMST s m r
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT STRef s [Node d i r s m]
stack ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ Node d i r s m
node ->
    JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessMM (Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isInNode Node d i r s m
node) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$
      JTMST s m [JustRule d i r s m]
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m])
-> STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m])
-> STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [JustRule d i r s m]
nodeJusts Node d i r s m
node) ((JustRule d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ JustRule d i r s m
just ->
        JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (JustRule d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
JustRule d i r s m -> JTMST s m Bool
checkJustification JustRule d i r s m
just) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ do
          Node d i r s m -> Justification d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> Justification d i r s m -> JTMST s m ()
installSupport (JustRule d i r s m -> Node d i r s m
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> Node d i r s m
justConsequence JustRule d i r s m
just) (JustRule d i r s m -> Justification d i r s m
forall d i r s (m :: * -> *).
JustRule d i r s m -> Justification d i r s m
ByRule JustRule d i r s m
just)
          Node d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m ()
propagateInness Node d i r s m
node

-- > * Contradiction handling interface

-- |Pass all believed contradiction nodes to the
-- @contradictionHandler@.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun check-for-contradictions (jtms &aux contradictions)
-- >   (when (jtms-checking-contradictions jtms)
-- >     (dolist (cnode (jtms-contradictions jtms))
-- >       (if (in-node? cnode) (push cnode contradictions)))
-- >     (if contradictions
-- >       (funcall (jtms-contradiction-handler jtms) jtms contradictions))))
checkForContradictions :: Monad m => JTMS d i r s m -> JTMST s m ()
checkForContradictions :: JTMS d i r s m -> JTMST s m ()
checkForContradictions JTMS d i r s m
jtms = do
  STRef s [Node d i r s m]
localContras <- STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STRef s [Node d i r s m])
 -> JTMST s m (STRef s [Node d i r s m]))
-> STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
  JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool) -> STRef s Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Bool
jtmsCheckingContradictions JTMS d i r s m
jtms) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ do
    JTMST s m [Node d i r s m]
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [Node d i r s m] -> STT s m [Node d i r s m])
-> STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsContradictions JTMS d i r s m
jtms) ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ Node d i r s m
cnode ->
      JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isInNode Node d i r s m
cnode) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ (STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
cnode STRef s [Node d i r s m]
localContras)
    (forall r. STT s m r -> JTMST s m r)
-> STRef s [Node d i r s m]
-> ([Node d i r s m] -> JTMST s m ())
-> JTMST s m ()
forall (m0 :: * -> *) (m :: * -> *) s a.
(Monad m0, Monad m) =>
(forall r. STT s m0 r -> m r)
-> STRef s [a] -> ([a] -> m ()) -> m ()
whenNonnullR forall r. STT s m r -> JTMST s m r
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT STRef s [Node d i r s m]
localContras (([Node d i r s m] -> JTMST s m ()) -> JTMST s m ())
-> ([Node d i r s m] -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ [Node d i r s m]
contras -> do
      [Node d i r s m] -> JTMST s m ()
handler <- STT s m ([Node d i r s m] -> JTMST s m ())
-> JTMST s m ([Node d i r s m] -> JTMST s m ())
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m ([Node d i r s m] -> JTMST s m ())
 -> JTMST s m ([Node d i r s m] -> JTMST s m ()))
-> STT s m ([Node d i r s m] -> JTMST s m ())
-> JTMST s m ([Node d i r s m] -> JTMST s m ())
forall a b. (a -> b) -> a -> b
$ STRef s ([Node d i r s m] -> JTMST s m ())
-> STT s m ([Node d i r s m] -> JTMST s m ())
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s ([Node d i r s m] -> JTMST s m ())
 -> STT s m ([Node d i r s m] -> JTMST s m ()))
-> STRef s ([Node d i r s m] -> JTMST s m ())
-> STT s m ([Node d i r s m] -> JTMST s m ())
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ())
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s ([Node d i r s m] -> JTMST s m ())
jtmsContradictionHandler JTMS d i r s m
jtms
      [Node d i r s m] -> JTMST s m ()
handler [Node d i r s m]
contras

-- |
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defmacro without-contradiction-check (jtms &body body)
-- >   (contradiction-check jtms nil body))
withoutContradictionCheck ::
  Monad m => JTMS d i r s m -> JTMST s m () -> JTMST s m ()
withoutContradictionCheck :: JTMS d i r s m -> JTMST s m () -> JTMST s m ()
withoutContradictionCheck JTMS d i r s m
jtms = JTMS d i r s m -> Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> Bool -> JTMST s m () -> JTMST s m ()
contradictionCheck JTMS d i r s m
jtms Bool
False

-- |
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defmacro with-contradiction-check (jtms &body body)
-- >   (contradiction-check jtms t body))
withContradictionCheck ::
  Monad m => JTMS d i r s m -> JTMST s m () -> JTMST s m ()
withContradictionCheck :: JTMS d i r s m -> JTMST s m () -> JTMST s m ()
withContradictionCheck JTMS d i r s m
jtms = JTMS d i r s m -> Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> Bool -> JTMST s m () -> JTMST s m ()
contradictionCheck JTMS d i r s m
jtms Bool
True

-- |
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun contradiction-check (jtms flag body)
-- >   (let ((jtmsv (gensym)) (old-value (gensym)))
-- >     `(let* ((,jtmsv ,jtms)
-- >          (,old-value (jtms-checking-contradictions ,jtmsv)))
-- >        (unwind-protect
-- >         (progn (setf (jtms-checking-contradictions ,jtmsv) ,flag) ,@body)
-- >       (setf (jtms-checking-contradictions ,jtmsv) ,old-value)))))
contradictionCheck ::
  Monad m => JTMS d i r s m -> Bool -> JTMST s m () -> JTMST s m ()
contradictionCheck :: JTMS d i r s m -> Bool -> JTMST s m () -> JTMST s m ()
contradictionCheck JTMS d i r s m
jtms Bool
flag JTMST s m ()
body = do
  Bool
oldFlag <- STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool) -> STRef s Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Bool
jtmsCheckingContradictions JTMS d i r s m
jtms
  STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> Bool -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (JTMS d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Bool
jtmsCheckingContradictions JTMS d i r s m
jtms) Bool
flag
  JTMST s m ()
body
  STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> Bool -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef (JTMS d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s Bool
jtmsCheckingContradictions JTMS d i r s m
jtms) Bool
oldFlag

--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defmacro with-contradiction-handler (jtms handler &body body)
-- >   (let ((jtmsv (gensym)) (old-handler (gensym)))
-- >     `(let* ((,jtmsv ,jtms)
-- >          (,old-handler (jtms-contradiction-handler ,jtmsv)))
-- >      (unwind-protect
-- >       (progn (setf (jtms-contradiction-handler ,jtmsv) ,handler) ,@body)
-- >        (setf (jtms-contradiction-handler ,jtmsv) ,old-handler)))))

--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun default-assumptions (jtms)
-- >   (with-contradiction-check jtms
-- >     (with-contradiction-handler jtms #'(lambda (&rest ignore)
-- >                                          (declare (ignore ignore))
-- >                                          (throw 'CONTRADICTION t))
-- >       (dolist (assumption (jtms-assumptions jtms))
-- >         (cond ((eq (tms-node-support assumption) :ENABLED-ASSUMPTION)
-- >                ;; No-op
-- >               )
-- >               ((not (eq :DEFAULT (tms-node-assumption? assumption)))
-- >                ;; No-op
-- >               )
-- >               ((catch 'CONTRADICTION (enable-assumption assumption))
-- >                (retract-assumption assumption)))))))
-- defaultAssumptions :: Monad m => JTMS d i r s m -> JTMST s m ()
-- defaultAssumptions jtms = error "<TODO unimplemented>"

-- > * Well-founded support inqueries

--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun supporting-justification-for-node (node) (tms-node-support node))
supportingJustificationForNode ::
  Monad m => Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))
supportingJustificationForNode :: Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))
supportingJustificationForNode Node d i r s m
node = STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Justification d i r s m))
 -> JTMST s m (Maybe (Justification d i r s m)))
-> STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Maybe (Justification d i r s m))
 -> STT s m (Maybe (Justification d i r s m)))
-> STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node

-- |API command returning the believed assumption nodes used to
-- justify belief in this node.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun assumptions-of-node (node &aux assumptions (marker (list :MARK)))
-- >   (do ((nodes (list node) (append (cdr nodes) new))
-- >        (new nil nil))
-- >       ((null nodes) assumptions)
-- >     (let ((node (car nodes)))
-- >       (cond
-- >         ((eq (tms-node-mark node) marker))
-- >         ((eq (tms-node-support node) :ENABLED-ASSUMPTION)
-- >          (push node assumptions))
-- >         ((in-node? node)
-- >          (setq new (just-antecedents (tms-node-support node)))))
-- >       (setf (tms-node-mark node) marker))))
assumptionsOfNode :: Monad m => Node d i r s m -> JTMST s m [Node d i r s m]
assumptionsOfNode :: Node d i r s m -> JTMST s m [Node d i r s m]
assumptionsOfNode Node d i r s m
node =
  let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
  in do
    [Node d i r s m]
nodes <- STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [Node d i r s m] -> STT s m [Node d i r s m])
-> STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsNodes JTMS d i r s m
jtms

    -- We look at each node at most once.
    STArray s Int Bool
marking <- STT s m (STArray s Int Bool) -> JTMST s m (STArray s Int Bool)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STArray s Int Bool) -> JTMST s m (STArray s Int Bool))
-> STT s m (STArray s Int Bool) -> JTMST s m (STArray s Int Bool)
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Bool -> STT s m (STArray s Int Bool)
forall i (m :: * -> *) e s.
(Ix i, Applicative m) =>
(i, i) -> e -> STT s m (STArray s i e)
newSTArray (Int
0, [Node d i r s m] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Node d i r s m]
nodes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Bool
False

    -- Set up a list for results.
    STRef s [Node d i r s m]
assumptions <- STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STRef s [Node d i r s m])
 -> JTMST s m (STRef s [Node d i r s m]))
-> STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []

    -- Set up the stack of nodes to consider.
    STRef s [Node d i r s m]
queue <- STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STRef s [Node d i r s m])
 -> JTMST s m (STRef s [Node d i r s m]))
-> STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
node STRef s [Node d i r s m]
queue

    -- Loop while the stack is not empty.
    (forall r. STT s m r -> JTMST s m r)
-> STRef s [Node d i r s m]
-> (Node d i r s m -> JTMST s m ())
-> JTMST s m ()
forall (m0 :: * -> *) (m :: * -> *) s a.
(Monad m0, Monad m) =>
(forall r. STT s m0 r -> m r) -> STRef s [a] -> (a -> m ()) -> m ()
whileListM_ forall r. STT s m r -> JTMST s m r
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT STRef s [Node d i r s m]
queue ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \Node d i r s m
node ->
      let idx :: Int
idx = Node d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> Int
nodeIndex Node d i r s m
node
      in do
        -- Make sure we do not process a node more than once.
        JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessMM (STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STArray s Int Bool -> Int -> STT s m Bool
forall i (m :: * -> *) s e.
(Ix i, Applicative m) =>
STArray s i e -> i -> STT s m e
readSTArray STArray s Int Bool
marking Int
idx) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ do
          -- The case when the node is an enabled assumption
          JTMST s m Bool -> JTMST s m () -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isEnabledAssumption Node d i r s m
node)
            (STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
node STRef s [Node d i r s m]
assumptions)

            -- The alternative case where the node is believed
            (JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool) -> STRef s Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeBelieved Node d i r s m
node) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ do
                Maybe (Justification d i r s m)
support <- Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))
getNodeSupport Node d i r s m
node
                case Maybe (Justification d i r s m)
support of
                  Just (ByRule JustRule d i r s m
j) ->
                    STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) (t :: * -> *) a s.
(Monad m, Traversable t) =>
t a -> STRef s [a] -> STT s m ()
pushAll (JustRule d i r s m -> [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> [Node d i r s m]
justAntecedents JustRule d i r s m
j) STRef s [Node d i r s m]
queue
                  Maybe (Justification d i r s m)
_ -> () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())

          STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ STArray s Int Bool -> Int -> Bool -> STT s m ()
forall i (m :: * -> *) s e.
(Ix i, Applicative m) =>
STArray s i e -> i -> e -> STT s m ()
writeSTArray STArray s Int Bool
marking Int
idx Bool
True

    -- The result is assumptions we've accumulated.
    STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s [Node d i r s m]
assumptions

    
-- |Returns the list of currently enabled assumptions.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun enabled-assumptions (jtms &aux result)
-- >   (dolist (assumption (jtms-assumptions jtms) result)
-- >     (if (eq (tms-node-support assumption) :ENABLED-ASSUMPTION)
-- >      (push assumption result))))
enabledAssumptions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]
enabledAssumptions :: JTMS d i r s m -> JTMST s m [Node d i r s m]
enabledAssumptions JTMS d i r s m
jtms = do
  STRef s [Node d i r s m]
result <- STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (STRef s [Node d i r s m])
 -> JTMST s m (STRef s [Node d i r s m]))
-> STT s m (STRef s [Node d i r s m])
-> JTMST s m (STRef s [Node d i r s m])
forall a b. (a -> b) -> a -> b
$ [Node d i r s m] -> STT s m (STRef s [Node d i r s m])
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef []
  JTMST s m [Node d i r s m]
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (JTMS d i r s m -> JTMST s m [Node d i r s m]
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> JTMST s m [Node d i r s m]
getJtmsAssumptions JTMS d i r s m
jtms) ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \Node d i r s m
node -> do
    JTMST s m Bool -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isEnabledAssumption Node d i r s m
node) (JTMST s m () -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$
      STT s m () -> JTMST s m ()
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m () -> JTMST s m ()) -> STT s m () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [Node d i r s m] -> STT s m ()
forall (m :: * -> *) a s. Monad m => a -> STRef s [a] -> STT s m ()
push Node d i r s m
node STRef s [Node d i r s m]
result
  STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s [Node d i r s m]
result

-- > * Inference engine stub to allow this JTMS to be used standalone

-- |Print the belief state and any justification of this node.
-- Requires that the underlying monad @m@ be `MonadIO`.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun why-node (node &aux justification)
-- >   (setq justification (tms-node-support node))
-- >   (cond
-- >     ((eq justification :ENABLED-ASSUMPTION)
-- >      (format t "~%~A is an enabled assumption" (node-string node)))
-- >     (justification (format t "~%~A is IN via ~A on"
-- >                      (node-string node)
-- >                      (just-informant justification))
-- >                    (dolist (anode (just-antecedents justification))
-- >                      (format t "~%  ~A" (node-string anode))))
-- >     (T (format t "~%~A is OUT." (node-string node))))
-- >   node)
whyNode :: MonadIO m => Node d i r s m -> JTMST s m ()
whyNode :: Node d i r s m -> JTMST s m ()
whyNode Node d i r s m
node = do
  String
str <- Node d i r s m -> JTMST s m String
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m String
nodeString Node d i r s m
node
  JTMST s m Bool -> JTMST s m () -> JTMST s m () -> JTMST s m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Node d i r s m -> JTMST s m Bool
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m Bool
isEnabledAssumption Node d i r s m
node)
    (IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is an enabled assumption")
    (Node d i r s m
-> (JustRule d i r s m -> JTMST s m ())
-> JTMST s m ()
-> JTMST s m ()
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m
-> (JustRule d i r s m -> JTMST s m ())
-> JTMST s m ()
-> JTMST s m ()
ifSupportedByRule Node d i r s m
node
     (\JustRule d i r s m
just -> do
         i -> String
fmtInf <- JTMS d i r s m -> JTMST s m (i -> String)
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> JTMST s m (i -> String)
getJtmsInformantString (JTMS d i r s m -> JTMST s m (i -> String))
-> JTMS d i r s m -> JTMST s m (i -> String)
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
         IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
           String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is IN via " String -> ShowS
forall a. [a] -> [a] -> [a]
++ i -> String
fmtInf (JustRule d i r s m -> i
forall d i r s (m :: * -> *). Monad m => JustRule d i r s m -> i
justInformant JustRule d i r s m
just) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" on"
         [Node d i r s m]
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (JustRule d i r s m -> [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> [Node d i r s m]
justAntecedents JustRule d i r s m
just) ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ Node d i r s m
ant -> do
           String
antStr <- Node d i r s m -> JTMST s m String
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m String
nodeString Node d i r s m
ant
           IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
antStr
         IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"")
     (IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is out"))

-- |Prints the justifications of all current nodes.  Requires that the
-- underlying monad @m@ be `MonadIO`.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun why-nodes (jtms)
-- >   (dolist (node (jtms-nodes jtms)) (why-node node)))
whyNodes :: MonadIO m => JTMS d i r s m -> JTMST s m ()
whyNodes :: JTMS d i r s m -> JTMST s m ()
whyNodes JTMS d i r s m
jtms =
  JTMST s m [Node d i r s m]
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (JTMS d i r s m -> JTMST s m [Node d i r s m]
forall (m :: * -> *) d i r s.
Monad m =>
JTMS d i r s m -> JTMST s m [Node d i r s m]
getJtmsAssumptions JTMS d i r s m
jtms) Node d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
MonadIO m =>
Node d i r s m -> JTMST s m ()
whyNode


-- |
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (proclaim '(special *contra-assumptions*))
-- >
-- > (defun ask-user-handler (jtms contradictions)
-- >   (handle-one-contradiction (car contradictions))
-- >   (check-for-contradictions jtms))
-- askUserHandler ::
--   MonadIO m => JTMS d i r s m -> [Node d i r s m] -> JTMST s m ()
-- askUserHandler jtms contradictions = error "<TODO unimplemented>"

-- |
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun handle-one-contradiction (contra-node
-- >                               &aux the-answer *contra-assumptions*)
-- >   (setq *contra-assumptions* (assumptions-of-node contra-node))
-- >   (unless *contra-assumptions*
-- >     (tms-error "~%There is a flaw in the universe...~A" contra-node))
-- >   (format t "~%Contradiction found: ~A" (node-string contra-node))
-- >   (print-contra-list *contra-assumptions*)
-- >   (format t "~%Call (TMS-ANSWER <number>) to retract assumption.")
-- >   (setq the-answer
-- >      (catch 'tms-contradiction-handler
-- >        (break "JTMS contradiction break")))
-- >   (if (and (integerp the-answer)
-- >         (> the-answer 0)
-- >         (not (> the-answer (length *contra-assumptions*))))
-- >       (retract-assumption (nth (1- the-answer)
-- >                             *contra-assumptions*))))
-- handleOneContradiction :: Monad m => JTMS d i r s m -> JTMST s m ()
-- handleOneContradiction node = error "<TODO unimplemented>"

-- |Print a verbose debugging output list of the contradictions in the
-- JTMS.  Requires that the underlying monad @m@ be `MonadIO`.
--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun print-contra-list (nodes)
-- >   (do ((counter 1 (1+ counter))
-- >        (nn nodes (cdr nn)))
-- >       ((null nn))
-- >     (format t "~%~A ~A" counter
-- >          (node-string (car nn)))))
printContraList :: MonadIO m => [Node d i r s m] -> JTMST s m ()
printContraList :: [Node d i r s m] -> JTMST s m ()
printContraList [Node d i r s m]
nodes = [Node d i r s m]
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Node d i r s m]
nodes ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ \ Node d i r s m
node -> do
  String
nodeStr <- Node d i r s m -> JTMST s m String
forall (m :: * -> *) d i r s.
Monad m =>
Node d i r s m -> JTMST s m String
nodeString Node d i r s m
node
  IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$  String
"- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nodeStr

-- |
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- > (defun tms-answer (num)
-- >   (if (integerp num)
-- >       (if (> num 0)
-- >        (if (not (> num (length *contra-assumptions*)))
-- >            (throw 'tms-contradiction-handler num)
-- >            (format t "~%Ignoring answer, too big."))
-- >        (format t "~%Ignoring answer, too small"))
-- >       (format t "~%Ignoring answer, must be an integer.")))
-- tmsAnswer :: MonadIO m => Int -> JTMST s m ()
-- tmsAnswer = error "<TODO unimplemented>"

-- |Print debugging information about a `JTMS`.
debugJTMS :: MonadIO m => String -> JTMS d i r s m -> JTMST s m ()
debugJTMS :: String -> JTMS d i r s m -> JTMST s m ()
debugJTMS String
desc JTMS d i r s m
jtms = do
  IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"----- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
desc
  JTMS d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
MonadIO m =>
JTMS d i r s m -> JTMST s m ()
debugJusts JTMS d i r s m
jtms
  JTMS d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
MonadIO m =>
JTMS d i r s m -> JTMST s m ()
debugNodes JTMS d i r s m
jtms
  IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"-----"

-- |Print debugging information about the `Node`s of a `JTMS`.
debugNodes :: MonadIO m => JTMS d i r s m -> JTMST s m ()
debugNodes :: JTMS d i r s m -> JTMST s m ()
debugNodes JTMS d i r s m
jtms = JTMST s m [Node d i r s m]
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [Node d i r s m] -> JTMST s m [Node d i r s m])
-> STT s m [Node d i r s m] -> JTMST s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [Node d i r s m] -> STT s m [Node d i r s m])
-> STRef s [Node d i r s m] -> STT s m [Node d i r s m]
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsNodes JTMS d i r s m
jtms) ((Node d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (Node d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$
  \ Node d i r s m
node -> Node d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
MonadIO m =>
Node d i r s m -> JTMST s m ()
debugNode Node d i r s m
node

-- |Print debugging information about a `Node`.
debugNode :: MonadIO m => Node d i r s m -> JTMST s m ()
debugNode :: Node d i r s m -> JTMST s m ()
debugNode Node d i r s m
node = let jtms :: JTMS d i r s m
jtms = Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
  in do
    Node d i r s m -> String
nodeFmt <- STT s m (Node d i r s m -> String)
-> JTMST s m (Node d i r s m -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Node d i r s m -> String)
 -> JTMST s m (Node d i r s m -> String))
-> STT s m (Node d i r s m -> String)
-> JTMST s m (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Node d i r s m -> String)
 -> STT s m (Node d i r s m -> String))
-> STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (Node d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (Node d i r s m -> String)
jtmsNodeString (JTMS d i r s m -> STRef s (Node d i r s m -> String))
-> JTMS d i r s m -> STRef s (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m
jtms
    JustRule d i r s m -> String
justFmt <- STT s m (JustRule d i r s m -> String)
-> JTMST s m (JustRule d i r s m -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (JustRule d i r s m -> String)
 -> JTMST s m (JustRule d i r s m -> String))
-> STT s m (JustRule d i r s m -> String)
-> JTMST s m (JustRule d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ STRef s (JustRule d i r s m -> String)
-> STT s m (JustRule d i r s m -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (JustRule d i r s m -> String)
 -> STT s m (JustRule d i r s m -> String))
-> STRef s (JustRule d i r s m -> String)
-> STT s m (JustRule d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
jtmsJustString (JTMS d i r s m -> STRef s (JustRule d i r s m -> String))
-> JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m
jtms
    d -> String
datumFmt <- STT s m (d -> String) -> JTMST s m (d -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (d -> String) -> JTMST s m (d -> String))
-> STT s m (d -> String) -> JTMST s m (d -> String)
forall a b. (a -> b) -> a -> b
$ STRef s (d -> String) -> STT s m (d -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (d -> String) -> STT s m (d -> String))
-> STRef s (d -> String) -> STT s m (d -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (d -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (d -> String)
jtmsDatumString (JTMS d i r s m -> STRef s (d -> String))
-> JTMS d i r s m -> STRef s (d -> String)
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
    i -> String
informantFmt <- STT s m (i -> String) -> JTMST s m (i -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (i -> String) -> JTMST s m (i -> String))
-> STT s m (i -> String) -> JTMST s m (i -> String)
forall a b. (a -> b) -> a -> b
$ STRef s (i -> String) -> STT s m (i -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (i -> String) -> STT s m (i -> String))
-> STRef s (i -> String) -> STT s m (i -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (i -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (i -> String)
jtmsInformantString (JTMS d i r s m -> STRef s (i -> String))
-> JTMS d i r s m -> STRef s (i -> String)
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> JTMS d i r s m
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> JTMS d i r s m
nodeJTMS Node d i r s m
node
    Bool
isAssumption <- STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool) -> STRef s Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeIsAssumption Node d i r s m
node
    Bool
isContradictory <- STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool) -> STRef s Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeIsContradictory Node d i r s m
node
    Maybe (Justification d i r s m)
support <- STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Maybe (Justification d i r s m))
 -> JTMST s m (Maybe (Justification d i r s m)))
-> STT s m (Maybe (Justification d i r s m))
-> JTMST s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Maybe (Justification d i r s m))
 -> STT s m (Maybe (Justification d i r s m)))
-> STRef s (Maybe (Justification d i r s m))
-> STT s m (Maybe (Justification d i r s m))
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s (Maybe (Justification d i r s m))
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s (Maybe (Justification d i r s m))
nodeSupport Node d i r s m
node
    Bool
believed <- STT s m Bool -> JTMST s m Bool
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m Bool -> JTMST s m Bool) -> STT s m Bool -> JTMST s m Bool
forall a b. (a -> b) -> a -> b
$ STRef s Bool -> STT s m Bool
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s Bool -> STT s m Bool) -> STRef s Bool -> STT s m Bool
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s Bool
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s Bool
nodeBelieved Node d i r s m
node
    [JustRule d i r s m]
justs <- STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m])
-> STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m])
-> STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [JustRule d i r s m]
nodeJusts Node d i r s m
node
    [JustRule d i r s m]
consequences <- STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m])
-> STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m])
-> STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
Node d i r s m -> STRef s [JustRule d i r s m]
nodeConsequences Node d i r s m
node

    IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Node " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Node d i r s m -> Int
forall d i r s (m :: * -> *). Monad m => Node d i r s m -> Int
nodeIndex Node d i r s m
node)
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Node d i r s m -> String
nodeFmt Node d i r s m
node) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(isAssumption " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
isAssumption
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", isContradictory " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
isContradictory String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
believed then String
"" else String
"not ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"believed)"

      case Maybe (Justification d i r s m)
support of
        Just Justification d i r s m
EnabledAssumption -> String -> IO ()
putStrLn String
"- Supported: enabled assumption"
        Just Justification d i r s m
UserStipulation   -> String -> IO ()
putStrLn String
"- Supported: user stipulation"
        Just (ByRule JustRule d i r s m
j) ->
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"- IN via {j.informant} (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (JustRule d i r s m -> String
justFmt JustRule d i r s m
j) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        Maybe (Justification d i r s m)
Nothing -> String -> IO ()
putStrLn String
"- OUT"

      if [JustRule d i r s m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [JustRule d i r s m]
justs
        then String -> IO ()
putStrLn String
"- Concluded by no justification rules"
        else do
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"- Concluded by " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [JustRule d i r s m] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [JustRule d i r s m]
justs)
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" justification rule" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if [JustRule d i r s m] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [JustRule d i r s m]
justs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then String
"" else String
"s")
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((String -> ShowS) -> [String] -> String
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (\ String
x String
y -> String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
y) ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (JustRule d i r s m -> String) -> [JustRule d i r s m] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map JustRule d i r s m -> String
justFmt [JustRule d i r s m]
justs)

      if [JustRule d i r s m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [JustRule d i r s m]
consequences
        then String -> IO ()
putStrLn String
"- Antecedent to no rules"
        else do
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"- Antecedent to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [JustRule d i r s m] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [JustRule d i r s m]
consequences)
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" justification rule"
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if [JustRule d i r s m] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [JustRule d i r s m]
consequences Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then String
"" else String
"s")
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (JustRule d i r s m -> String) -> [JustRule d i r s m] -> String
forall a. (a -> String) -> [a] -> String
commaList JustRule d i r s m -> String
justFmt [JustRule d i r s m]
consequences

-- |Print debugging information about the `JustRule`s of a `JTMS`.
debugJusts :: MonadIO m => JTMS d i r s m -> JTMST s m ()
debugJusts :: JTMS d i r s m -> JTMST s m ()
debugJusts JTMS d i r s m
jtms = JTMST s m [JustRule d i r s m]
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Foldable t) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m])
-> STT s m [JustRule d i r s m] -> JTMST s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m])
-> STRef s [JustRule d i r s m] -> STT s m [JustRule d i r s m]
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s [JustRule d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s [JustRule d i r s m]
jtmsJusts JTMS d i r s m
jtms) ((JustRule d i r s m -> JTMST s m ()) -> JTMST s m ())
-> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$
  \ JustRule d i r s m
just -> JTMS d i r s m -> JustRule d i r s m -> JTMST s m ()
forall (m :: * -> *) d i r s.
MonadIO m =>
JTMS d i r s m -> JustRule d i r s m -> JTMST s m ()
debugJust JTMS d i r s m
jtms JustRule d i r s m
just

-- |Print debugging information about a `JustRule`.
debugJust :: MonadIO m => JTMS d i r s m -> JustRule d i r s m -> JTMST s m ()
debugJust :: JTMS d i r s m -> JustRule d i r s m -> JTMST s m ()
debugJust JTMS d i r s m
jtms JustRule d i r s m
just = do
  Node d i r s m -> String
nodeFmt <- STT s m (Node d i r s m -> String)
-> JTMST s m (Node d i r s m -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Node d i r s m -> String)
 -> JTMST s m (Node d i r s m -> String))
-> STT s m (Node d i r s m -> String)
-> JTMST s m (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Node d i r s m -> String)
 -> STT s m (Node d i r s m -> String))
-> STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (Node d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (Node d i r s m -> String)
jtmsNodeString JTMS d i r s m
jtms
  JustRule d i r s m -> String
justFmt <- STT s m (JustRule d i r s m -> String)
-> JTMST s m (JustRule d i r s m -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (JustRule d i r s m -> String)
 -> JTMST s m (JustRule d i r s m -> String))
-> STT s m (JustRule d i r s m -> String)
-> JTMST s m (JustRule d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ STRef s (JustRule d i r s m -> String)
-> STT s m (JustRule d i r s m -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (JustRule d i r s m -> String)
 -> STT s m (JustRule d i r s m -> String))
-> STRef s (JustRule d i r s m -> String)
-> STT s m (JustRule d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (JustRule d i r s m -> String)
jtmsJustString JTMS d i r s m
jtms
  Node d i r s m -> String
nodeFmt <- STT s m (Node d i r s m -> String)
-> JTMST s m (Node d i r s m -> String)
forall (m :: * -> *) s r. Monad m => STT s m r -> JTMST s m r
jLiftSTT (STT s m (Node d i r s m -> String)
 -> JTMST s m (Node d i r s m -> String))
-> STT s m (Node d i r s m -> String)
-> JTMST s m (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef (STRef s (Node d i r s m -> String)
 -> STT s m (Node d i r s m -> String))
-> STRef s (Node d i r s m -> String)
-> STT s m (Node d i r s m -> String)
forall a b. (a -> b) -> a -> b
$ JTMS d i r s m -> STRef s (Node d i r s m -> String)
forall d i r s (m :: * -> *).
Monad m =>
JTMS d i r s m -> STRef s (Node d i r s m -> String)
jtmsNodeString JTMS d i r s m
jtms
  IO () -> JTMST s m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> JTMST s m ()) -> IO () -> JTMST s m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
    String
"JustRule (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (JustRule d i r s m -> String
justFmt JustRule d i r s m
just) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Node d i r s m -> String
nodeFmt (Node d i r s m -> String) -> Node d i r s m -> String
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> Node d i r s m
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> Node d i r s m
justConsequence JustRule d i r s m
just) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((Node d i r s m -> String) -> [Node d i r s m] -> String
forall a. (a -> String) -> [a] -> String
commaList Node d i r s m -> String
nodeFmt ([Node d i r s m] -> String) -> [Node d i r s m] -> String
forall a b. (a -> b) -> a -> b
$ JustRule d i r s m -> [Node d i r s m]
forall d i r s (m :: * -> *).
Monad m =>
JustRule d i r s m -> [Node d i r s m]
justAntecedents JustRule d i r s m
just)

--
-- ===== __Lisp origins:__
--
-- > ;; In jtms.lisp:
-- >
-- > (defun explore-network (node)
-- >   (unless (in-node? node)
-- >        (format t "~% Sorry, ~A not believed." (node-string node))
-- >        (return-from explore-network node))
-- >   (do ((stack nil)
-- >        (current node)
-- >        (options nil)
-- >        (olen 0)
-- >        (done? nil))
-- >       (done? current)
-- >       (why-node current)
-- >       (setq options (if (typep (tms-node-support current) 'just)
-- >                      (just-antecedents (tms-node-support current))))
-- >       (setq olen (length options))
-- >       (do ((good? nil)
-- >         (choice 0))
-- >        (good? (case good?
-- >                     (q (return-from explore-network current))
-- >                     (0 (if stack
-- >                            (setq current (pop stack))
-- >                            (return-from explore-network current)))
-- >                     (t (push current stack)
-- >                        (setq current (nth (1- good?) options)))))
-- >        (format t "~%>>>")
-- >        (setq choice (read))
-- >        (cond ((or (eq choice 'q)
-- >                   (and (integerp choice)
-- >                        (not (> choice olen))
-- >                        (not (< choice 0))))
-- >               (setq good? choice))
-- >              (t (format t
-- >                  "~% Must be q or an integer from 0 to ~D."
-- >                  olen))))))

-- * Other helpers