Data.TMS.JTMS

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

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

Note also there are restrictions on the embedded monad m which can be wrapped in the STT transformer; see the Control.Monad.ST.Trans documentation for details.

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

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

The JTMST monad

data Monad m => JTMST s m a

The process of building and using a mutable JTMS.

Instances

MonadTrans (JTMST s)

Defined in Data.TMS.JTMS

Methods

lift :: Monad m => m a -> JTMST s m a

(Monad m, Functor m) => Monad (JTMST s m)

Defined in Data.TMS.JTMS

Methods

(>>=) :: JTMST s m a -> (a -> JTMST s m b) -> JTMST s m b

(>>) :: JTMST s m a -> JTMST s m b -> JTMST s m b

return :: a -> JTMST s m a

Monad m => Functor (JTMST s m)

Defined in Data.TMS.JTMS

Methods

fmap :: (a -> b) -> JTMST s m a -> JTMST s m b

(<$) :: a -> JTMST s m b -> JTMST s m a

(Monad m, Functor m) => Applicative (JTMST s m)

Defined in Data.TMS.JTMS

Methods

pure :: a -> JTMST s m a

(<*>) :: JTMST s m (a -> b) -> JTMST s m a -> JTMST s m b

liftA2 :: (a -> b -> c) -> JTMST s m a -> JTMST s m b -> JTMST s m c

(*>) :: JTMST s m a -> JTMST s m b -> JTMST s m b

(<*) :: JTMST s m a -> JTMST s m b -> JTMST s m a

MonadIO m => MonadIO (JTMST s m)

Defined in Data.TMS.JTMS

Methods

liftIO :: IO a -> JTMST s m a

data JtmsErr

Errors which can arise from JTMS operations.

Instances

Show JtmsErr

Defined in Data.TMS.JTMS

Methods

showsPrec :: Int -> JtmsErr -> ShowS

show :: JtmsErr -> String

showList :: [JtmsErr] -> ShowS

runJTMST :: Monad m => (forall s. JTMST s m r) -> m (Either JtmsErr r)

Execute a computation in the JTMST monad transformer.

Basic JTMS structures

data Monad m => JTMS d i r s m

Standalone implementation of justification-based truth maintenance systems.

• d is the type of data associated with each Node of this JTMS.
• i is the type of informants in the external system.
• r is the type of rules which may be associated with each Node of this JTMS.
• s is the (phantom) type of the state thread.
• m is the monad in which this computation lives.

Lisp origins:

;; In jtms.lisp:
(defstruct (jtms (:PRINT-FUNCTION print-jtms))
  (title nil)
  (node-counter 0)             ;; unique namer for nodes.
  (just-counter 0)             ;; unique namer for justifications.
  (nodes nil)                  ;; list of all tms nodes.
  (justs nil)                  ;; list of all justifications
  (debugging nil)              ;; debugging flag
  (contradictions nil)         ;; list of contradiction nodes.
  (assumptions nil)            ;; list of assumption nodes.
  (checking-contradictions T)  ;; For external systems
  (node-string nil)
  (contradiction-handler nil)
  (enqueue-procedure nil))

Instances

Monad m => Eq (JTMS d i r s m)

TODO For the moment equality on JTMSes in by comparing their names, but this is an ugly and stupid hack. Need something like: an index for JTMSes generated from JTMST. Really, this is just for a way to enable nodes from different JTMSes to be seen as unequal.

Defined in Data.TMS.JTMS

Methods

(==) :: JTMS d i r s m -> JTMS d i r s m -> Bool

(/=) :: JTMS d i r s m -> JTMS d i r s m -> Bool

printJTMS :: forall m1 (m2 :: Type -> Type) d i r s. (MonadIO m1, Monad m2) => JTMS d i r s m2 -> m1 ()

Print a simple tag with the title of this JTMS. Forces the enclosed monad to be MonadIO.

Lisp origins:

;; In jtms.lisp:
(defun print-jtms (jtms stream ignore)
  (declare (ignore ignore))
  (format stream "#<JTMS: ~A>" (jtms-title jtms)))

createJTMS :: Monad m => String -> JTMST s m (JTMS d i r s m)

Create and return a new JTMS.

Lisp origins:

;; In jtms.lisp:
(defun create-jtms (title &key (node-string 'default-node-string)
                               debugging
                               (checking-contradictions t)
                               (contradiction-handler 'ask-user-handler)
                               enqueue-procedure)
  (make-jtms :TITLE title
             :NODE-STRING node-string
             :DEBUGGING debugging
             :CHECKING-CONTRADICTIONS checking-contradictions
             :CONTRADICTION-HANDLER contradiction-handler
             :ENQUEUE-PROCEDURE enqueue-procedure))

JTMS accessors

jtmsTitle :: JTMS d i r s m -> String

Name of this JTMS.

Setting JTMS properties

Lisp origins

The JTMS property-setting functions are translated from:

;; In jtms.lisp:
(defun change-jtms (jtms &key contradiction-handler node-string
                           enqueue-procedure debugging
                              checking-contradictions)
  (if node-string (setf (jtms-node-string jtms) node-string))
  (if debugging (setf (jtms-debugging jtms) debugging))
  (if checking-contradictions
      (setf (jtms-checking-contradictions jtms)
         checking-contradictions))
  (if contradiction-handler
      (setf (jtms-contradiction-handler jtms) contradiction-handler))
  (if enqueue-procedure
      (setf (jtms-enqueue-procedure jtms) enqueue-procedure)))

setNodeString :: Monad m => JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()

Set the display function for Nodes in a JTMS.

After change-jtms in jtms.lisp.

nodeStringByDatum :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()

When the node type d implements Show, use this display method as the standard for printing the node.

nodeStringByIndex :: Monad m => JTMS d i r s m -> JTMST s m ()

Use the node index for its display.

nodeStringByIndexDatum :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()

When the node type d implements Show, use both the node index and this display method as the standard for printing the node.

setDatumString :: Monad m => JTMS d i r s m -> (d -> String) -> JTMST s m ()

Set the display function for the datum associated with each Node in a JTMS.

datumStringByShow :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()

When the datum type d implements Show, use this display method as the standard for printing the datum.

setInformantString :: Monad m => JTMS d i r s m -> (i -> String) -> JTMST s m ()

Set the display function for informants in a JTMS.

informantStringByShow :: (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()

When the informant type i implements Show, use this display method as the standard for printing the informant.

setJustString :: Monad m => JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()

Set the display function for JustRules in a JTMS.

After change-jtms in jtms.lisp.

justStringByIndex :: Monad m => JTMS d i r s m -> JTMST s m ()

Use the JustRule index when printing the just.

justStringByInformant :: (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()

When the informant type i implements Show, use the JustRule index when printing the just.

justStringByIndexInformant :: (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()

When the informant type i implements Show, use the JustRule index when printing the just.

setDebugging :: Monad m => JTMS d i r s m -> Bool -> JTMST s m ()

Turn on or turn off debugging in a JTMS. This setting currently has no effect.

After change-jtms in jtms.lisp.

setCheckingContradictions :: Monad m => JTMS d i r s m -> Bool -> JTMST s m ()

Set whether the JTMS should issue external notifications of contradictions.

After change-jtms in jtms.lisp.

setContradictionHandler :: Monad m => JTMS d i r s m -> ([Node d i r s m] -> JTMST s m ()) -> JTMST s m ()

Set the contradiction handler. The JTMS default is to do nothing; the intention is to allow a callback to the external system using the JTMS.

After change-jtms in jtms.lisp.

setEnqueueProcedure :: Monad m => JTMS d i r s m -> (r -> JTMST s m ()) -> JTMST s m ()

Set the queuing behavior needed for the external system.

After change-jtms in jtms.lisp.

Accessors for a JTMS's current state

getJtmsNodes :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]

Return the current list of Nodes of a JTMS.

getJtmsJusts :: Monad m => JTMS d i r s m -> JTMST s m [JustRule d i r s m]

Return the current JustRules of a JTMS.

getJtmsContradictions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]

Return the current designated contradictory Nodes of a JTMS.

getJtmsAssumptions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]

Return the current possible assumption Nodes of a JTMS. Note that these nodes will not be used as assumptions unless activated by enableAssumption.

getJtmsCheckingContradictions :: Monad m => JTMS d i r s m -> JTMST s m Bool

Return whether a JTMS is currently invoking its external handler for deduced contradictions.

getJtmsNodeString :: Monad m => JTMS d i r s m -> JTMST s m (Node d i r s m -> String)

Return the current Node formatter of a JTMS.

getJtmsJustString :: Monad m => JTMS d i r s m -> JTMST s m (JustRule d i r s m -> String)

Return the current JustRule formatter of a JTMS.

getJtmsDatumString :: Monad m => JTMS d i r s m -> JTMST s m (d -> String)

Return the current d datum formatter of a JTMS.

getJtmsInformantString :: Monad m => JTMS d i r s m -> JTMST s m (i -> String)

Return the current i informant formatter of a JTMS.

getJtmsEnqueueProcedure :: Monad m => JTMS d i r s m -> JTMST s m (r -> JTMST s m ())

Return the current external queuing procedure of a JTMS.

getJtmsContradictionHandler :: Monad m => JTMS d i r s m -> JTMST s m ([Node d i r s m] -> JTMST s m ())

Return the current external handler of a JTMS for reacting to a deduced contradiction.

getJtmsDebugging :: Monad m => JTMS d i r s m -> JTMST s m Bool

Return the current debugging flag setting of a JTMS.

Nodes

data Monad m => Node d i r s m

Wrapper for one possible belief known to the TMS.

Lisp origins:

;; In jtms.lisp:
(defstruct (tms-node (:PRINT-FUNCTION print-tms-node))
  (index 0)
  (datum nil)           ;; pointer to external problem solver
  (label :OUT)          ;; :IN means believed, :OUT means disbelieved
  (support nil)         ;; Current justification or premise marker
  (justs nil)           ;; Possible justifications
  (consequences nil)    ;; Justifications in which it is an antecedent
  (mark nil)            ;; Marker for sweep algorithms
  (contradictory? nil)  ;; Flag marking it as contradictory
  (assumption? nil)     ;; Flag marking it as an assumption.
  (in-rules nil)     ;; Rules that should be triggered when node goes in
  (out-rules nil)    ;; Rules that should be triggered when node goes out
  (jtms nil))           ;; The JTMS in which this node appears.

Instances

Monad m => Eq (Node d i r s m)

Equality on Nodes is based simply on comparing their JTMS and index number.

Defined in Data.TMS.JTMS

Methods

(==) :: Node d i r s m -> Node d i r s m -> Bool

(/=) :: Node d i r s m -> Node d i r s m -> Bool

createNode :: Monad m => JTMS d i r s m -> d -> Bool -> Bool -> JTMST s m (Node d i r s m)

Add a node to a JTMS.

Lisp origins:

;; In jtms.lisp:
(defun tms-create-node (jtms datum &key assumptionp contradictoryp)
  (let ((node (make-tms-node :INDEX (incf (jtms-node-counter jtms))
                             :DATUM datum
                             :ASSUMPTION? assumptionp
                             :CONTRADICTORY? contradictoryp
                             :JTMS jtms)))
    (if assumptionp (push node (jtms-assumptions jtms)))
    (if contradictoryp (push node (jtms-contradictions jtms)))
    (push node (jtms-nodes jtms))
    node))

nodeDatum :: Node d i r s m -> d

Returns the piece of data associated with this node.

printTmsNode :: MonadIO m => Node d i r s m -> JTMST s m ()

Write one node in the standard way for this JTMS. Forces the wrapped monad to be MonadIO.

Lisp origins:

;; In jtms.lisp:
(defun print-tms-node (node stream ignore)
  (declare (ignore ignore))
  (format stream "#<Node: ~A>" (node-string node)))

assumeNode :: Monad m => Node d i r s m -> JTMST s m ()

Internal method used to flag this node as an assumption, and to enable belief in this assumption.

Lisp origins:

;; In jtms.lisp:
;;; Converts a regular node to an assumption and enables it.
(defun assume-node (node &aux (jtms (tms-node-jtms node)))
  (unless (or (tms-node-assumption? node) (tms-node-premise? node))
    (debugging-jtms jtms "~%Converting ~A into an assumption" node)
    (setf (tms-node-assumption? node) t)
    (push node (jtms-assumptions jtms)))
  (enable-assumption node))

nodeString :: Monad m => Node d i r s m -> JTMST s m String

Produce a representation of the node in the default manner for its JTMS.

Lisp origins:

;; In jtms.lisp:
(defun node-string (node)
  (funcall (jtms-node-string (tms-node-jtms node)) node))

Accessors for a Node's current state

getNodeIsAssumption :: Monad m => Node d i r s m -> JTMST s m Bool

Return whether a Node may currently be used as an assumption.

getNodeIsContradictory :: Monad m => Node d i r s m -> JTMST s m Bool

Return whether a Node is currently considered a contradiction.

getNodeBelieved :: Monad m => Node d i r s m -> JTMST s m Bool

Return whether a Node is currently believed.

getNodeConsequences :: Monad m => Node d i r s m -> JTMST s m [JustRule d i r s m]

Return the JustRules which use a Node as an antecedent.

getNodeInRules :: Monad m => Node d i r s m -> JTMST s m [r]

Return the current in-rules of a Node.

getNodeOutRules :: Monad m => Node d i r s m -> JTMST s m [r]

Return the current out-rules of a Node.

getNodeJusts :: Monad m => Node d i r s m -> JTMST s m [JustRule d i r s m]

Return the JustRules which currently give a Node as their conclusion.

getNodeSupport :: Monad m => Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))

Return the current support for believing a Node.

isEnabledAssumption :: Monad m => Node d i r s m -> JTMST s m Bool

Return whether the given node is an enabled assumption.

whenSupportedByRule :: Monad m => Node d i r s m -> (JustRule d i r s m -> JTMST s m a) -> JTMST s m (Maybe a)

Check whether the given node is supported by a JustRule. If it is, run the given computation with that JustRule.

ifSupportedByRule :: Monad m => Node d i r s m -> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m () -> JTMST s m ()

Check whether the given node is supported by a JustRule. If it is, run the thenM computation with that JustRule; if not, run the elseM computation.

Justifications

justifyNode :: Monad m => i -> Node d i r s m -> [Node d i r s m] -> JTMST s m ()

Add a rule for concluding belief in the consequence. The rule is triggered when the antecedents are all believed, and is associated with (perhaps named as) the informant.

Lisp origins:

;; In jtms.lisp:
(defun justify-node (informant consequence antecedents &aux just jtms)
  (setq jtms (tms-node-jtms consequence)
     just (make-just :INDEX (incf (jtms-just-counter jtms))
                     :INFORMANT informant
                     :CONSEQUENCE consequence
                     :ANTECEDENTS antecedents))
  (push just (tms-node-justs consequence))
  (dolist (node antecedents) (push just (tms-node-consequences node)))
  (push just (jtms-justs jtms))
  (debugging-jtms jtms
               "~%Justifying ~A by ~A using ~A."
               consequence
               informant
               (mapcar #'node-string antecedents))
  (if (or antecedents (out-node? consequence))
      (if (check-justification just) (install-support consequence just))
      (setf (tms-node-support consequence) just))
  (check-for-contradictions jtms))

data Monad m => Justification d i r s m

Forms of data which might signal support for a node. The original Lisp does not need this declaration since it is untyped; the latter two cases are simply symbols.

Constructors

ByRule (JustRule d i r s m)

EnabledAssumption

UserStipulation

data Monad m => JustRule d i r s m

Wrapper for one justification relationship between many antecedent nodes and one consequent node.

Lisp origins:

;; In jtms.lisp:
(defstruct (just (:PRINT-FUNCTION print-just))
  (index 0)
  informant
  consequence
  antecedents)

Instances

Monad m => Eq (JustRule d i r s m)

Equality on JustRules is based simply on comparing their index number.

Defined in Data.TMS.JTMS

Methods

(==) :: JustRule d i r s m -> JustRule d i r s m -> Bool

(/=) :: JustRule d i r s m -> JustRule d i r s m -> Bool

printJustRule :: MonadIO m => JustRule d i r s m -> JTMST s m ()

Print the tag of a JTMS justification.

Lisp origins:

;; In jtms.lisp:
(defun print-just (just stream ignore)
  (declare (ignore ignore))
  (format stream "#<Just ~D>" (just-index just)))

Reasoning tools

Control of assumptions

enableAssumption :: Monad m => Node d i r s m -> JTMST s m ()

Called when the external system chooses to believe the assumption represented by node.

Lisp origins:

;; In jtms.lisp:
(defun enable-assumption (node &aux (jtms (tms-node-jtms node)))
  (unless (tms-node-assumption? node)
    (tms-error "Can't enable the non-assumption ~A" node))
  (debugging-jtms jtms "~%  Enabling assumption ~A." node)
  (cond
     ((out-node? node)
      (make-node-in node :ENABLED-ASSUMPTION)
      (propagate-inness node))
     ((or (eq (tms-node-support node) :ENABLED-ASSUMPTION)
          (null (just-antecedents (tms-node-support node)))))
     (t (setf (tms-node-support node) :ENABLED-ASSUMPTION)))
  (check-for-contradictions jtms))

retractAssumption :: Monad m => Node d i r s m -> JTMST s m ()

This command is called when the external system chooses to disbelieve the assumption represented by node.

Lisp origins:

;; In jtms.lisp:
(defun retract-assumption (node &aux jtms)
  (when (eq (tms-node-support node) :ENABLED-ASSUMPTION)
    (setq jtms (tms-node-jtms node))
    (debugging-jtms jtms "~%  Retracting assumption ~A." node)
    (make-node-out node)
    (find-alternative-support jtms
                              (cons node (propagate-outness node jtms)))))

makeContradiction :: Monad m => Node d i r s m -> JTMST s m ()

API command used when the external system categorizes this node as representing a contradiction.

Lisp origins:

;; In jtms.lisp:
(defun make-contradiction (node &aux (jtms (tms-node-jtms node)))
  (unless (tms-node-contradictory? node)
    (setf (tms-node-contradictory? node) t)
    (push node (jtms-contradictions jtms))
    (check-for-contradictions jtms)))

Conclusions from current assumption belief

isInNode :: Monad m => Node d i r s m -> JTMST s m Bool

Returns True if the current believed assumptions justify the fact represented by the given node.

Lisp origins:

;; In jtms.lisp:
(defun in-node? (node) (eq (tms-node-label node) :IN))

isOutNode :: Monad m => Node d i r s m -> JTMST s m Bool

Returns True if the current believed assumptions do not justify the fact represented by the given node.

Lisp origins:

;; In jtms.lisp:
(defun out-node? (node) (eq (tms-node-label node) :OUT))

enabledAssumptions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]

Returns the list of currently enabled assumptions.

Lisp origins:

;; In jtms.lisp:
(defun enabled-assumptions (jtms &aux result)
  (dolist (assumption (jtms-assumptions jtms) result)
    (if (eq (tms-node-support assumption) :ENABLED-ASSUMPTION)
     (push assumption result))))

nodeIsPremise :: Monad m => Node d i r s m -> JTMST s m Bool

Returns True when the node is supported by a JustRule with no antecedents.

Lisp origins:

;; In jtms.lisp:
(defun tms-node-premise? (node &aux support)
  (and (setq support (tms-node-support node))
       (not (eq support :ENABLED-ASSUMPTION))
       (null (just-antecedents support))))

assumptionsOfNode :: Monad m => Node d i r s m -> JTMST s m [Node d i r s m]

API command returning the believed assumption nodes used to justify belief in this node.

Lisp origins:

;; In jtms.lisp:
(defun assumptions-of-node (node &aux assumptions (marker (list :MARK)))
  (do ((nodes (list node) (append (cdr nodes) new))
       (new nil nil))
      ((null nodes) assumptions)
    (let ((node (car nodes)))
      (cond
        ((eq (tms-node-mark node) marker))
        ((eq (tms-node-support node) :ENABLED-ASSUMPTION)
         (push node assumptions))
        ((in-node? node)
         (setq new (just-antecedents (tms-node-support node)))))
      (setf (tms-node-mark node) marker))))

Output from the current belief state

whyNodes :: MonadIO m => JTMS d i r s m -> JTMST s m ()

Prints the justifications of all current nodes. Requires that the underlying monad m be MonadIO.

Lisp origins:

;; In jtms.lisp:
(defun why-nodes (jtms)
  (dolist (node (jtms-nodes jtms)) (why-node node)))

whyNode :: MonadIO m => Node d i r s m -> JTMST s m ()

Print the belief state and any justification of this node. Requires that the underlying monad m be MonadIO.

Lisp origins:

;; In jtms.lisp:
(defun why-node (node &aux justification)
  (setq justification (tms-node-support node))
  (cond
    ((eq justification :ENABLED-ASSUMPTION)
     (format t "~%~A is an enabled assumption" (node-string node)))
    (justification (format t "~%~A is IN via ~A on"
                     (node-string node)
                     (just-informant justification))
                   (dolist (anode (just-antecedents justification))
                     (format t "~%  ~A" (node-string anode))))
    (T (format t "~%~A is OUT." (node-string node))))
  node)

printContraList :: MonadIO m => [Node d i r s m] -> JTMST s m ()

Lisp origins:

;; In jtms.lisp:
(proclaim '(special *contra-assumptions*))

(defun ask-user-handler (jtms contradictions)
  (handle-one-contradiction (car contradictions))
  (check-for-contradictions jtms))

askUserHandler :: MonadIO m => JTMS d i r s m -> [Node d i r s m] -> JTMST s m () askUserHandler jtms contradictions = error "unimplemented"

Lisp origins:

;; In jtms.lisp:
(defun handle-one-contradiction (contra-node
                              &aux the-answer *contra-assumptions*)
  (setq *contra-assumptions* (assumptions-of-node contra-node))
  (unless *contra-assumptions*
    (tms-error "~%There is a flaw in the universe...~A" contra-node))
  (format t "~%Contradiction found: ~A" (node-string contra-node))
  (print-contra-list *contra-assumptions*)
  (format t "~%Call (TMS-ANSWER <number>) to retract assumption.")
  (setq the-answer
     (catch 'tms-contradiction-handler
       (break "JTMS contradiction break")))
  (if (and (integerp the-answer)
        (> the-answer 0)
        (not (> the-answer (length *contra-assumptions*))))
      (retract-assumption (nth (1- the-answer)
                            *contra-assumptions*))))

handleOneContradiction :: Monad m => JTMS d i r s m -> JTMST s m () handleOneContradiction node = error "unimplemented"

Print a verbose debugging output list of the contradictions in the JTMS. Requires that the underlying monad m be MonadIO.

Lisp origins:

;; In jtms.lisp:
(defun print-contra-list (nodes)
  (do ((counter 1 (1+ counter))
       (nn nodes (cdr nn)))
      ((null nn))
    (format t "~%~A ~A" counter
         (node-string (car nn)))))

Debugging utilities

Note that these functions are based on MonadIO, not just Monad, for printing debugging output.

debugJTMS :: MonadIO m => String -> JTMS d i r s m -> JTMST s m ()

Lisp origins:

;; In jtms.lisp:
(defun tms-answer (num)
  (if (integerp num)
      (if (> num 0)
       (if (not (> num (length *contra-assumptions*)))
           (throw 'tms-contradiction-handler num)
           (format t "~%Ignoring answer, too big."))
       (format t "~%Ignoring answer, too small"))
      (format t "~%Ignoring answer, must be an integer.")))

tmsAnswer :: MonadIO m => Int -> JTMST s m () tmsAnswer = error "unimplemented"

Print debugging information about a JTMS.

debugNodes :: MonadIO m => JTMS d i r s m -> JTMST s m ()

Print debugging information about the Nodes of a JTMS.

debugNode :: MonadIO m => Node d i r s m -> JTMST s m ()

Print debugging information about a Node.

debugJusts :: MonadIO m => JTMS d i r s m -> JTMST s m ()

Print debugging information about the JustRules of a JTMS.

debugJust :: MonadIO m => JTMS d i r s m -> JustRule d i r s m -> JTMST s m ()

Print debugging information about a JustRule.