{-# LANGUAGE RankNTypes #-}
module Data.TMS.JTMS (
JTMST, JtmsErr, runJTMST,
JTMS, printJTMS, createJTMS,
jtmsTitle,
setNodeString, nodeStringByDatum, nodeStringByIndex, nodeStringByIndexDatum,
setDatumString, datumStringByShow,
setInformantString, informantStringByShow,
setJustString,
justStringByIndex, justStringByInformant, justStringByIndexInformant,
setDebugging, setCheckingContradictions,
setContradictionHandler, setEnqueueProcedure,
getJtmsNodes, getJtmsJusts, getJtmsContradictions, getJtmsAssumptions,
getJtmsCheckingContradictions, getJtmsNodeString, getJtmsJustString,
getJtmsDatumString, getJtmsInformantString, getJtmsEnqueueProcedure,
getJtmsContradictionHandler, getJtmsDebugging,
Node, createNode, nodeDatum, printTmsNode, assumeNode, nodeString,
getNodeIsAssumption, getNodeIsContradictory, getNodeBelieved,
getNodeConsequences, getNodeInRules, getNodeOutRules, getNodeJusts,
getNodeSupport, isEnabledAssumption, whenSupportedByRule, ifSupportedByRule,
justifyNode,
Justification(ByRule, EnabledAssumption, UserStipulation),
JustRule(justInformant, justConsequence, justAntecedents),
printJustRule,
enableAssumption, retractAssumption, makeContradiction,
isInNode, isOutNode, enabledAssumptions, nodeIsPremise, assumptionsOfNode,
whyNodes, whyNode, printContraList,
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
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
type JTMSTInner s m a = Monad m => ExceptT JtmsErr (STT s m) a
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 }
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 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 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
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
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
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
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
data Monad m => JTMS d i r s m = JTMS {
JTMS d i r s m -> String
jtmsTitle :: String,
JTMS d i r s m -> STRef s Int
jtmsNodeCounter :: STRef s Int,
JTMS d i r s m -> STRef s Int
jtmsJustCounter :: STRef s Int,
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsNodes :: STRef s [Node d i r s m],
JTMS d i r s m -> STRef s [JustRule d i r s m]
jtmsJusts :: STRef s [JustRule d i r s m],
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsContradictions :: STRef s [Node d i r s m],
JTMS d i r s m -> STRef s [Node d i r s m]
jtmsAssumptions :: STRef s [Node d i r s m],
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
}
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
">"
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,
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]
}
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
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
">"
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
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
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
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
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
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
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
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
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
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]
}
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
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
">"
data Monad m => Justification d i r s m =
ByRule (JustRule d i r s m) | EnabledAssumption | UserStipulation
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
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)
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
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
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)
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)
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
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
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
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)
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
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
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
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
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
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
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
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)
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
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
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
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
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
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
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
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
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 ())
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
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
[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
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
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))
(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)
(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)
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
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
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
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
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
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) []
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 ()
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
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
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
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
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) []
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
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
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
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
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
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
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
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
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
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 []
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
(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
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
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)
(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
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
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
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"))
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
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
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
"-----"
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
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
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
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)