;;; PLT Scheme Inference Collection
;;; inference-control.ss
;;; Copyright (c) 2006 M. Douglas Williams
;;;
;;; This library is free software; you can redistribute it and/or
;;; modify it under the terms of the GNU Lesser General Public
;;; License as published by the Free Software Foundation; either
;;; version 2.1 of the License, or (at your option) any later version.
;;;
;;; This library is distributed in the hope that it will be useful,
;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
;;; Lesser General Public License for more details.
;;;
;;; You should have received a copy of the GNU Lesser General Public
;;; License along with this library; if not, write to the Free
;;; Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
;;; 02111-1307 USA.
;;;
;;; Version Date     Comments
;;; 1.0.1   07/16/06 Modified assert, retract, and modify to maintain
;;;                  the assertion index.  Eventually need to revisit
;;;                  the code for efficiency.
;;; 1.0.2   07/19/06 Added stop-simulation, succeed, and fail.  Fixed
;;;                  notall and all existential processing.  Fixed
;;;                  check to return the correct assertion.

(module inference-control mzscheme
  
  (provide (all-defined))
    
  (require "inference-environments.ss")
  (require "bindings.ss")
  (require "patterns.ss")
  (require "facts.ss")
  (require "rulesets.ss")
  (require "matches.ss")
  (require "assertions.ss")
  (require (lib "list.ss" "srfi" "1"))

  ;; assert: list x any -> assertion
  ;; assert: list -> assertion
  ;; Assert a fact.  This function returns a new assertion from the given
  ;; fact.  It does not check to see if the fact has already been asserted.
  ;; The assertion is passed into the rule network for inferencing.
  (define assert
    (case-lambda
      ((fact reason)
       (when (current-inference-trace)
         (printf "assert: ~a~n" fact))
       (let ((assertion (make-assertion fact reason)))
         ;; Add the assertion to the assertion index.
         (hash-table-put! (current-inference-assertion-index)
                          (fact-first fact)
                          (cons assertion
                                (hash-table-get
                                 (current-inference-assertion-index)
                                 (fact-first fact) (lambda () '()))))
         ;; Match and propagate assertion through rule network.
         (for-each
          (lambda (match-node)
            (match-node-assert match-node assertion))
          (hash-table-get (current-inference-data-index)
                          (fact-first fact) (lambda () '())))
         assertion))
      ((fact)
       (assert fact #t))))
  
  ;; retract: assertion -> void
  ;; Retract an assertion.  The retraction is passed into the rule network
  ;; for inferencing
  (define (retract assertion)
    (when (current-inference-trace)
      (printf "retract: ~a~n" (assertion-fact assertion)))
    ;; Remove the fact from the assertion index.
    (hash-table-put! (current-inference-assertion-index)
                     (fact-first (assertion-fact assertion))
                     (delete! assertion
                              (hash-table-get
                               (current-inference-assertion-index)
                               (fact-first (assertion-fact assertion)))))
    ;; Match and unpropagate through the rule network.
    (for-each 
     (lambda (match-node)
       (match-node-retract match-node assertion))
     (hash-table-get (current-inference-data-index)
                     (fact-first (assertion-fact assertion)))))
  
  ;; modify: assertion x list x any -> assertion
  ;; modify: assertion x list -> assertion
  ;; Modify an assertion.  In essence, retract the assertion and then
  ;; re-assert it using the given fact.
  (define modify
    (case-lambda
      ((assertion fact reason)
       ;; Retract the assertion.
       (retract assertion)
       ;; Re-assert with the new fact and reason.
       ;(set-assertion-fact! assertion fact)
       ;(set-assertion-reason! assertion reason)
       ;(for-each
       ; (lambda (match-node)
       ;   (match-node-assert match-node assertion))
       ; (hash-table-get (current-inference-data-index)
       ;                 (fact-first fact) (lambda () '())))
       ;assertion)
       (assert fact reason))
      ((assertion fact)
       (modify assertion fact #t))))
  
  ;; check: fact? -> match?
  ;; Check a fact using backtracking.  Can be called directly for a
  ;; pure backward chaining strategy.  Also called to initiate backward
  ;; chaining for match nodes.
  (define (check fact)
    (when (current-inference-trace)
      (printf "check: ~a~n" fact))
    (let/ec return
      (let ((assertion (make-assertion fact #f)))
        (for-each
         (lambda (match-node)
           (let ((match (match-node-check match-node assertion return)))
             (when (not (null? match))
               (return match))))
         (hash-table-get (current-inference-goal-index)
                         (fact-first fact) (lambda () '())))
        '())))
  
  ;; query: pattern? -> list
  ;; Return a list of assertions matching a pattern.  Not currently
  ;; used internally.  May be useful for dynamic bindings within a
  ;; rule.
  (define (query pattern)
    (let ((matches '()))
      (for-each
       (lambda (assertion)
         (let* ((fact (assertion-fact assertion))
                (bindings (pattern-unify fact pattern '())))
           (if bindings
               (set! matches
                     (cons (cons assertion bindings)
                           matches)))))
       (hash-table-get (current-inference-assertion-index)
                       (pattern-first pattern) (lambda () '())))
      matches))
  
  ;; Inference Control
  
  ;; node structure
  ;;   successors           - list of successor nodes
  ;;   matches              - list of matches for the node
  ;;                        -   #f for goal nodes
  ;; match-node structure
  ;;   assertion-variable   - assertion variable or #f
  ;;   pattern              - pattern to be matched
  ;;   match-constraint-predicate
  ;;                        - match constraint predicate
  ;; join-node structure
  ;;   left                 - left node (#f or another join node)
  ;;   right                - right node (match node)
  ;;   join-constraint-predicate
  ;;                        - constraint predicate function
  ;;   existential?         - existential nature of the associated
  ;;                          match node (right)
  ;;                            #f         - not an existential match
  ;;                            no, notany - no assertions match
  ;;                            any        - at least one match
  ;;                            notall     - at least one doesn't match
  ;;                            all        - all assertions match
  ;;   match-counts         - alist of count for joined matches
  ;; rule-node predicate
  ;;   rule                 - rule structure
  ;;   join                 - join node (predecessor)
  ;;   action               - procedure to execute (or #f)
  (define-struct node
    (successors matches)
    (make-inspector))
  (define-struct (match-node node)
    (assertion-variable pattern match-constraint-predicate)
    (make-inspector))
  (define-struct (join-node node)
    (left right join-constraint-predicate existential? match-counts)
    (make-inspector))
  (define-struct (rule-node node)
    (rule join action)
    (make-inspector))
  
  ;; link-nodes: node x node -> void
  ;; Link nodes in a predecessor -> successor relationship.
  (define (link-nodes predecessor successor)
    (set-node-successors!
     predecessor
     (cons successor (node-successors predecessor))))
  
  ;; add-match-to-node-matches: list x node -> void
  ;; Add a match to the list of matches for a node.
  (define (add-match-to-node-matches match node)
    (when (node-matches node)
      (set-node-matches!
       node (cons match (node-matches node)))))
  
  ;; remove-match-from-node-matches: list x node -> void
  ;; Remove a match from the lisy of matches for a node.  For now,
  ;; assume we have the actual match and can use eq?.
  (define (remove-match-from-node-matches match node)
    (let/cc exit
      (let loop ((previous #f)
                 (matches (node-matches node)))
        (when (not (null? matches))
          (when (eq? match (car matches))
            (if previous
                (set-cdr! previous (cdr matches))
                (set-node-matches! node (cdr matches)))
            (exit))
          (loop matches (cdr matches))))))
  
  ;; get-node-matches: node? x bindings? -> matches?
  ;; Returns the matches for a node.  If the node is a backward
  ;; chaining match node, initiate backward chaining.
  (define (get-node-matches node bindings)
    (let ((matches (node-matches node)))
      (if matches
          matches
          (if (match-node? node)
              (check (pattern-substitute
                      (match-node-pattern node) bindings))
              #f))))
    
  ;; Ruleset Activation
  
  ;; activate: rule-set -> void
  ;; Activate a ruleset.  Builds the rule network for a ruleset by
  ;; activating all of the rules
  (define (activate ruleset)
    ;; The initial join nodes is used for all data nodes.
    (let ((initial-join-node
           (make-join-node
            '()                            ; successors
            '((()))                        ; matches
            #f                             ; left
            #f                             ; right
            #f                             ; constraint-predicate
            #f                             ; existential?
            '())))                         ; match-counts
      (for-each
       (lambda (rule)
         (if (null? (rule-goals rule))
             (activate-data-rule rule initial-join-node)
             (activate-goal-rule rule)))
       (ruleset-rules ruleset)))
    (fix-goal-matches))
  
  ;; activate-data-rule: rule -> void
  ;; Activate a data rule.  Build the rule network for a rule by creating
  ;; and linking nodes.  There is one match node and one join node per
  ;; precondition clause and one rule node per rule.
  (define (activate-data-rule rule initial-join-node)
    (let ((match-node #f)
          (join-node #f)
          (rule-node #f)
          (previous-join-node initial-join-node)
          (previous-variable-list '()))
      ;; Process precondition clauses
      (for-each
       (lambda (clause)
         (let ((existential? #f)
               (assertion-variable #f)
               (pattern #f)
               (variable-list '()))
           ;; Parse clause
           (cond ((and (pair? clause)
                       (variable? (car clause)))
                  (set! assertion-variable (car clause))
                  (set! pattern (caddr clause)))
                 ((and (pair? clause)
                       (memq (car clause) '(no notany any notall all)))
                  (set! existential? (car clause))
                  (set! pattern (cadr clause)))
                 (else
                  (set! pattern clause)))
           ;; Add pattern variables to the variable list
           (set! variable-list
                 (merge-variable-lists
                  previous-variable-list
                  (if assertion-variable
                      (cons assertion-variable (pattern-variables pattern))
                      (pattern-variables pattern))))
           ;; Get match constraints
           (let ((match-constraints
                  (pattern-match-constraints
                   pattern (pattern-variables pattern))))
             ;; Make match node and add to index
             (set! match-node
                   (make-match-node
                    '()                      ; successors
                    '()                      ; matches
                    assertion-variable       ; assertion-variable
                    (pattern-base-pattern pattern)   ; pattern
                    (if (null? match-constraints) ; constraint-predicate
                        #f
                        (eval `(lambda ,(pattern-variables pattern)
                                 (and ,@match-constraints))))))
             (hash-table-put! (current-inference-data-index)
                              (pattern-first pattern)
                              (cons match-node
                                    (hash-table-get (current-inference-data-index)
                                                    (pattern-first pattern)
                                                    (lambda () '())))))
           ;; Make join node and link from match-node
           (let ((join-constraints
                  (pattern-join-constraints
                   pattern (pattern-variables pattern))))
             (set! join-node
                   (make-join-node
                    '()                    ; successors
                    (if (or (memq existential? '(no notany)) ; matches
                            (eq? existential? 'all))
                        (node-matches previous-join-node)
                        '())
                    previous-join-node     ; left
                    match-node             ; right
                    (if (null? join-constraints); constraint-predicate
                        #f
                        (eval `(lambda ,variable-list
                                 (and ,@join-constraints))))
                    existential?          ; existential?
                    '())))                ; match-counts
           (link-nodes match-node join-node)
           ;; Link from previous join-node, if any
           (link-nodes previous-join-node join-node)
           (set! previous-join-node join-node)
           ;; Update previous-variable-list for non existentials
           (if (not existential?)
               (set! previous-variable-list variable-list))))
       (rule-preconditions rule))
      ;; Create rule node, link to it from the last join node, and add it
      (set! rule-node
            (make-rule-node
             '()                           ; successors
             (node-matches previous-join-node) ; matches
             rule                          ; rule
             join-node                     ; join
             (if (not (rule-actions rule))
                 #f
                 (eval #`(lambda #,previous-variable-list
                           (and #,@(rule-actions rule)))))))
                                           ; action
      (link-nodes join-node rule-node)
      (current-inference-rule-nodes
       (append! (current-inference-rule-nodes)
                (list rule-node))))
    (void))
  
  (define (activate-goal-rule rule)
    (let ((match-node #f)
          (join-node #f)
          (rule-node #f)
          (previous-node #f)
          (previous-variable-list #f))
      ;; Create goal match node
      (let ((goal-pattern (car (rule-goals rule))))
        (set! previous-node
              (make-match-node
               '()                       ; successors
               #f                        ; matches
               #f                        ; assertion-variable
               goal-pattern              ; goal pattern
               #f))                      ; match-constraint-predicate
        (hash-table-put! (current-inference-goal-index)
                         (car goal-pattern)
                         (cons previous-node
                               (hash-table-get (current-inference-goal-index)
                                               (car goal-pattern)
                                               (lambda () '()))))
        (set! previous-variable-list
              (pattern-variables goal-pattern)))
      ;; Process precondition clauses
      (for-each
       (lambda (clause)
         (let ((existential? #f)
               (assertion-variable #f)
               (pattern #f)
               (variable-list '()))
           ;; Parse clause
           (cond ((variable? (car clause))
                  (set! assertion-variable (car clause))
                  (set! pattern (caddr clause)))
                 ((memq (car clause) '(no notany any notall all))
                  (set! existential? (car clause))
                  (set! pattern (cadr clause)))
                 (else
                  (set! pattern clause)))
           ;; Add pattern variables to the variable list
           (set! variable-list
                 (merge-variable-lists
                  previous-variable-list
                  (if assertion-variable
                      (cons assertion-variable (pattern-variables pattern))
                      (pattern-variables pattern))))
           ;; Get match constraints
           (let ((match-constraints
                  (pattern-match-constraints
                   pattern (pattern-variables pattern))))
             ;; Make match node and add to index
             (set! match-node
                   (make-match-node
                    '()                  ; successors
                    '()                  ; matches
                    assertion-variable   ; assertion-variable
                    (pattern-base-pattern pattern)
                                         ; pattern
                    (if (null? match-constraints)
                        #f
                        (eval `(lambda ,(pattern-variables pattern)
                                 (and ,@match-constraints))))))
             (hash-table-put! (current-inference-data-index)
                              (car pattern)
                              (cons match-node
                                    (hash-table-get (current-inference-data-index)
                                                    (car pattern)
                                                    (lambda () '())))))
           ;; Make join node and link from match-node
           (let ((join-constraints
                  (pattern-join-constraints
                   pattern (pattern-variables pattern))))
             (set! join-node
                   (make-join-node
                    '()                  ; successors
                    #f                   ; matches
                    previous-node        ; left
                    match-node           ; right
                    (if (null? join-constraints)
                        #f
                        (eval `(lambda ,variable-list
                                 ,@join-constraints)))
                                         ; join-constraint-predicate
                    existential?         ; existential?
                    '())))               ; match-counts
           (link-nodes match-node join-node)
           ;; Link from previous node
           (link-nodes previous-node join-node)
           (set! previous-node join-node)
           ;; Update previous-variable-list for non existentials
           (if (not existential?)
               (set! previous-variable-list variable-list))))
       (rule-preconditions rule))
      ;; Create the rule node
      (set! rule-node
            (make-rule-node
             '()                         ; successors
             #f                          ; matches
             rule                        ; rule
             previous-node
             (if (not (rule-actions rule))
                 #f
                 (eval #`(lambda #,previous-variable-list
                           (and #,@(rule-actions rule)))))))
                                           ; action
      (link-nodes previous-node rule-node)
      (current-inference-rule-nodes
       (append! (current-inference-rule-nodes)
                (list rule-node))))
    (void))
  
  ;;
  (define (fix-goal-matches)
    (hash-table-for-each (current-inference-data-index)
     (lambda (key value)
       (when (hash-table-get (current-inference-goal-index) key
                             (lambda () #f))
         (for-each
          (lambda (match-node)
            (set-node-matches! match-node #f))
          value)
         (hash-table-remove! (current-inference-data-index) key)))))
  
  ;; merge-variable-lists: list x list -> list
  ;; Merge two list of variables maintaining the order.
  (define (merge-variable-lists list1 list2)
    (cond ((null? list2)
           list1)
          ((memq (car list2) list1)
           (merge-variable-lists list1 (cdr list2)))
          (else
           (merge-variable-lists
            (append list1 (list (car list2))) (cdr list2)))))
  
  ;; Match Node Processing
  
  ;; match-node-assert: match-node x assertion -> void
  ;; Match an assertion against the pattern in a match node.  If there
  ;; is a match, update the matches for the node and propagate the
  ;; match to the join node(s).
  (define (match-node-assert match-node assertion)
    (let ((bindings (pattern-unify
                     (assertion-fact assertion)
                     (match-node-pattern match-node) '())))
      (when (current-inference-trace)
        (printf "match-node-assert: fact = ~a; pattern = ~a; bindings = ~a~n"
                (assertion-fact assertion) (match-node-pattern match-node) bindings))
      (when bindings
        ;; Add assertion variable, if any.
        (when (match-node-assertion-variable match-node)
          (set! bindings
                (cons
                 (cons (match-node-assertion-variable match-node)
                       assertion)
                 bindings)))
        ;; Check match constraints
        (when (and (match-node-match-constraint-predicate match-node)
                   (not (apply (match-node-match-constraint-predicate match-node)
                               (bindings-data bindings))))
          (set! bindings #f)))
      (if bindings
          ;; Build and propagate match to successors
          (let ((match (cons (list assertion) bindings)))
            (when (current-inference-trace)
              (printf "match-node-assert: match = ~a~n" match))
            (add-match-to-node-matches match match-node)
            (for-each
             (lambda (successor)
               (propagate-match-from-match-node match successor))
             (node-successors match-node)))
          (for-each
           (lambda (successor)
             (propagate-nonmatch-from-match-node successor))
           (node-successors match-node)))))
  
  ;; match-node-retract: match-node x assertion -> void
  ;; Retract an assertion from a match node and propagate the
  ;; retraction through the rule network.
  (define (match-node-retract match-node assertion)
    (when (current-inference-trace)
      (printf "match-node-retract: fact = ~a~n"
              (assertion-fact assertion)))
    (let/cc exit
      (let loop ((previous #f)
                 (matches (node-matches match-node)))
        (when (not (null? matches))
          (let ((match (car matches)))
            (when (eq? assertion (caar match))
              ;; Remove the match
              (if previous
                  (set-cdr! previous (cdr matches))
                  (set-node-matches! match-node (cdr matches)))
              (for-each
               (lambda (successor)
                 (unpropagate-match-from-match-node match successor))
               (node-successors match-node))
              (exit)))
          (loop matches (cdr matches))))
      ;; Match not found
      (for-each
       (lambda (successor)
         (unpropagate-nonmatch-from-match-node successor))
       (node-successors match-node))))
  
  ;; match-node-check
  ;; Perform backward chaining from a match node.
  (define (match-node-check match-node assertion continuation)
    (let/ec exit
      (let ((bindings (pattern-unify
                       (assertion-fact assertion)
                       (match-node-pattern match-node) '())))
        (when (current-inference-trace)
          (printf "match-node-check: fact = ~a; pattern = ~a; bindings = ~a~n"
                  (assertion-fact assertion) (match-node-pattern match-node) bindings))
        (when bindings
          ;; Add assertion variable, if any.
          (if (match-node-assertion-variable match-node)
              (set! bindings
                    (cons
                     (cons (match-node-assertion-variable match-node)
                           assertion)
                     bindings)))
          ;; Check match constraints
          (when (and (match-node-match-constraint-predicate match-node)
                     (not (apply (match-node-match-constraint-predicate match-node)
                                 (bindings-data bindings))))
            (exit #f))
          ;; Build and propagate match to successors
          (let ((match (cons (list assertion) bindings)))
            (when (current-inference-trace)
              (printf "match-node-check: match = ~a~n" match))
            (add-match-to-node-matches match match-node)
            (for-each
             (lambda (successor)
               (propagate-match-from-join-node match successor continuation))
             (node-successors match-node)))))
      '()))
  
  ;; Match Propagation and Unpropagation
  
  ;; Propagate Match
  
  ;; propagate-match-from-match-node: list x join-node -> void
  ;; Propagate a match from a match node.  This is called when a match
  ;; node proopagates a match in response to an assertion.
  (define (propagate-match-from-match-node match join-node)
    (when (node-matches join-node)
      (for-each
       (lambda (left-match)
         (let ((joined-match (join left-match match join-node)))
           (if (join-node-existential? join-node)
               ;; Existential join node
               (let* ((count-association
                       (assq left-match (join-node-match-counts join-node)))
                      (count (if count-association
                                 (cdr count-association)
                                 0)))
                 ;; Update the count (either stay the same or go up by 1)
                 (when joined-match
                   (set! count (+ count 1))
                   (if count-association
                       (set-cdr! count-association count)
                       (set-join-node-match-counts!
                        join-node (cons (cons left-match count)
                                        (join-node-match-counts join-node)))))
                 (case (join-node-existential? join-node)
                   ((no notany)
                    (when (and joined-match
                               (= count 1)) ; count went from 0 to 1
                      (unpropagate-match-to-successors left-match join-node)))
                   ((any)
                    (when (and joined-match
                               (= count 1)) ; count went from 0 to 1
                      (propagate-match-to-successors left-match join-node #f)))
                   ((notall)
                    (let ((n (length (hash-table-get
                                      (current-inference-assertion-index)
                                      (pattern-first
                                       (match-node-pattern
                                        (join-node-right join-node)))))))
                      (when (and (not joined-match)
                                 (= count (- n 1)))
                        ; count went from n to n-1
                        (propagate-match-to-successors left-match join-node #f))))
                   ((all)
                    (let ((n (length (hash-table-get
                                      (current-inference-assertion-index)
                                      (pattern-first
                                       (match-node-pattern
                                        (join-node-right join-node)))))))
                      (when (and (not joined-match)
                                 (= count (- n 1)))
                        ; count went from n to n-1
                        (unpropagate-match-to-successors left-match join-node #f))))))
               ;; Binding join node
               (when joined-match
                 (propagate-match-to-successors joined-match join-node #f)))))
       (get-node-matches (join-node-left join-node) (car match)))))
  
  ;; propagate-nonmatch-from-match-node: join-node?
  ;; Propagate a nonmatch from a match node.  This is used to update
  ;; notall and all existential matches.
  (define (propagate-nonmatch-from-match-node join-node)
    (when (node-matches join-node)
      (for-each
       (lambda (left-match)
         (when (join-node-existential? join-node)
           (let* ((count-association
                   (assq left-match (join-node-match-counts join-node)))
                  (count (if count-association
                             (cdr count-association)
                             0)))
             (case (join-node-existential? join-node)
               ((notall)
                (let ((n (length (hash-table-get
                                  (current-inference-assertion-index)
                                  (pattern-first
                                   (match-node-pattern
                                    (join-node-right join-node)))))))
                  (when (= count (- n 1))
                    (propagate-match-to-successors left-match join-node #f))))
               ((all)
                (let ((n (length (hash-table-get
                                  (current-inference-assertion-index)
                                  (pattern-first
                                   (match-node-pattern
                                    (join-node-right join-node)))))))
                  (when (= count (- n 1))
                    (unpropagate-match-to-successors left-match join-node))))))))
       (get-node-matches (join-node-left join-node) '()))))
  
  ;; propagate-match-from-join-node: list x join-node -> void
  ;; Propagate a match from one join node to a successor join node.
  (define (propagate-match-from-join-node match join-node continuation)
    (when (current-inference-trace)
      (printf "propagate-match-from-join-node: ~a~n" match))
    (if (join-node-existential? join-node)
        ;; Existential join node
        (let ((count 0))
          (for-each
           (lambda (right-match)
             (let ((joined-match (join match right-match join-node)))
               (when joined-match
                 (set! count (+ count 1)))))
           (node-matches (join-node-right join-node)))
          ;; Add match to match counts
          (set-join-node-match-counts!
           join-node (cons (cons match count)
                           (join-node-match-counts join-node)))
          ;; Propagate match based on existential type
          (case (join-node-existential? join-node)
            ((no notany)
             (when (= count 0)
               (propagate-match-to-successors match join-node continuation)))
            ((any)
             (when (> count 1)
               (propagate-match-to-successors match join-node continuation)))
            ((notall)
             (let ((n (length (hash-table-get
                               (current-inference-assertion-index)
                               (pattern-first
                                (match-node-pattern
                                 (join-node-right join-node)))))))
               (when (< count n)
                 (propagate-match-to-successors match join-node continuation))))
            ((all)
             (let ((n (length (hash-table-get
                               (current-inference-assertion-index)
                               (pattern-first
                                (match-node-pattern
                                 (join-node-right join-node)))))))
               (when (= count n)
                 (propagate-match-to-successors match join-node continuation))))))
        ;; Binding join node
        (for-each
         (lambda (right-match)
           (let ((joined-match (join match right-match join-node)))
             (when joined-match
               (propagate-match-to-successors joined-match join-node continuation))))
         (get-node-matches (join-node-right join-node) (cdr match)))))
  
  ;; propagate-match-to-successors: list x join-node -> void
  ;; Propagate a match from a join node to its successor nodes.
  (define (propagate-match-to-successors match join-node continuation)
    ;; Add match to node matches
    (add-match-to-node-matches match join-node)
    ;; Propagate match to successor nodes
    (for-each
     (lambda (successor)
       (if (join-node? successor)
           (propagate-match-from-join-node match successor continuation)
           (propagate-match-to-rule match successor continuation)))
     (node-successors join-node)))
  
  ;; propagate-match-to-rule: list x rule-node -> void
  ;; Propagate a match from a join node to a successor rule node.
  (define (propagate-match-to-rule match rule-node continuation)
    (when (current-inference-trace)
      (printf "Match propagated to rule instance ~a with bindings ~a~n"
              (rule-name (rule-node-rule rule-node)) (cdr match)))
    (add-match-to-node-matches match rule-node)
    (when (not (node-matches rule-node))
      (when (current-inference-trace)
        (printf "Executing rule instance ~a with bindings ~a.~n"
                (rule-name (rule-node-rule rule-node))
                (cdr match)))
      (when (rule-node-action rule-node)
        (apply (rule-node-action rule-node)
               (bindings-data match)))
      (continuation (list (cons (list (caar match)) (cdr match))))))
  
  ;; Unpropagate Matches
  
  ;; unpropagate-match-from-match-node: list x join-node -> void
  ;; Unpropagate a match from a match node.  This is called when a match
  ;; node unpropagates a match in response to a retraction.
  (define (unpropagate-match-from-match-node match join-node)
    (if (join-node-existential? join-node)
        ;; Existential node
        (for-each
         (lambda (left-match)
           (let* ((count-association
                   (assq left-match (join-node-match-counts join-node)))
                  (count (cdr count-association))
                  (joined-match (join left-match match join-node)))
             (when joined-match
               (set! count (- count 1))
               (set-cdr! count-association count))
             (case (join-node-existential? join-node)
               ((no notany)
                (when (and joined-match
                           (= count 0))   ; count went from 1 to 0
                  (propagate-match-to-successors left-match join-node #f)))
               ((any)
                (when (and join-node
                           (= count 0))   ; count went from 1 to 0
                  (unpropagate-match-to-successors left-match join-node)))
               ((notall)
                (let ((n (length (hash-table-get
                                  (current-inference-assertion-index)
                                  (pattern-first
                                   (match-node-pattern
                                    (join-node-right join-node)))))))
                  (when (and (not joined-match)
                             (= count n))
                  ;  count went from n-1 to n
                  (unpropagate-match-to-successors left-match join-node))))
               ((all)
                (let ((n (length (hash-table-get
                                  (current-inference-assertion-index)
                                  (pattern-first
                                   (match-node-pattern
                                    (join-node-right join-node)))))))
                  (when (and (not joined-match)
                             (= count n))
                    ;  count went from n-1 to n
                    (propagate-match-to-successors left-match join-node #f)))))))
         (node-matches (join-node-left join-node)))
        ;; Binding join node
        (let ((assertion (caar match)))
          (for-each
           (lambda (match)
             (when (eq? assertion
                        (last (car match)))
               (unpropagate-match-to-successors match join-node)))
           (node-matches join-node)))))
  
  ;; unpropagate-nonmatch-from-match-node: join-node?
  ;; Unpropagate a nonmatch (from a retraction).  This is needed to
  ;; update notall and all existential matches.
  (define (unpropagate-nonmatch-from-match-node join-node)
    (when (join-node-existential? join-node)
      (for-each
       (lambda (left-match)
         (let* ((count-association
                 (assq left-match (join-node-match-counts join-node)))
                (count (if count-association
                           (cdr count-association)
                           0)))
           (case (join-node-existential? join-node)
             ((notall)
              (let ((n (length (hash-table-get
                                (current-inference-assertion-index)
                                (pattern-first
                                 (match-node-pattern
                                  (join-node-right join-node)))))))
                (when (= count n)
                  (unpropagate-match-to-successors left-match join-node))))
             ((all)
              (let ((n (length (hash-table-get
                                (current-inference-assertion-index)
                                (pattern-first
                                 (match-node-pattern
                                  (join-node-right join-node)))))))
                (when (= count n)
                  (propagate-match-to-successors left-match join-node #f)))))))
       (node-matches (join-node-left join-node)))))
  
  ;; unpropagate-match-from-join-node: list x join-node -> void
  ;; Unpropagate a match from a join node.
  ;; For each of the matches for the node:
  ;;   When the given match is a subset of the node match:
  ;;     Remove the node match and unpropagate it to its successors.
  (define (unpropagate-match-from-join-node match join-node)
    ;; Remove the count
    (let/ec exit
      (let loop ((previous #f)
                 (alist (join-node-match-counts join-node)))
        (when (not (null? alist))
          (let ((association (car alist)))
            (when (eq? match (car association))
              (if previous
                  (set-cdr! previous (cdr alist))
                  (set-join-node-match-counts! join-node (cdr alist)))
              (exit)))
          (loop alist (cdr alist)))))
    ;; Unpropagate match to successors
    (for-each 
     (lambda (node-match)
       (when (match-subset? match node-match)
         (unpropagate-match-to-successors node-match join-node)))
     (node-matches join-node)))
  
  ;; unpropagate-match-to-successors: list x join-node -> void
  ;; Unpropagate a match from a join node to its successors.
  (define (unpropagate-match-to-successors match join-node)
    ;; Remove the match from the node matches.
    (remove-match-from-node-matches match join-node)
    ;; Unpropagate match to successor nodes.
    (for-each
     (lambda (successor)
       (if (join-node? successor)
           (unpropagate-match-from-join-node match successor)
           (unpropagate-match-to-rule match successor)))
     (node-successors join-node)))
  
  ;; unpropagate-match-to-rule: list x rule-node -> void
  ;; Unpropagate a match from a join node to a successor rule node.
  (define (unpropagate-match-to-rule match rule-node)
    (when (current-inference-trace)
      (printf "Match unpropagated to rule instance ~a with bindings ~a~n"
              (rule-name (rule-node-rule rule-node)) (cdr match)))
    (remove-match-from-node-matches match rule-node))
  
  ;; join: list x list x join-node -> #f or list
  ;; Join two (left and right) matches.  If the bindings are consistant
  ;; and the constraints are met, join the matches and propagate the
  ;; joined match to any successor (join or rule) nodes.
  (define (join left-match right-match join-node)
    (let ((left-assertions (car left-match))
          (left-bindings (cdr left-match))
          (right-assertions (car right-match))
          (right-bindings (cdr right-match)))
      (let/cc return
        ;; Check that bindings match
        (for-each
         (lambda (right-binding)
           (if (assq (car right-binding) left-bindings)
               (if (not (equal? (cdr right-binding)
                                (cdr (assq (car right-binding) left-bindings))))
                   (return #f))))
         right-bindings)
        ;; Add new bindings
        (let ((bindings left-bindings))
          (for-each
           (lambda (right-binding)
             (if (not (assq (car right-binding) left-bindings))
                 (set! bindings (append bindings (list right-binding)))))
           right-bindings)
          ;; Check constraints
          (if (and (join-node-join-constraint-predicate join-node)
                   (not (apply (join-node-join-constraint-predicate join-node)
                               (bindings-data bindings))))
              (return #f))
          ;; Return match
          (cons (append left-assertions right-assertions) bindings)))))
  
  ;; start-inference -> void
  ;; The inference engine main loop.
  (define (start-inference)
    (assert '(start))
    (let/cc exit
      ;; Set the global exit continuation.
      (current-inference-exit exit)
      ;; Simple selection - find the first rule instance
      (let loop ()
        (let/cc break
          (for-each
           (lambda (rule-node)
             (if (not (null? (node-matches rule-node)))
                 (let* ((rule (rule-node-rule rule-node))
                        (match (car (node-matches rule-node)))
                        (arguments (bindings-data (cdr match))))
                   (when (current-inference-trace)
                     (printf "Executing rule instance ~a with bindings ~a~n"
                             (rule-name rule) (cdr match)))
                   ;; Remove the match
                   (set-node-matches!
                    rule-node (cdr (node-matches rule-node)))
                   ;; Apply the rule
                   (apply (rule-node-action rule-node) arguments)
                   (loop))))
           (current-inference-rule-nodes))
          (exit)))))
  
  ;; stop-inference: any
  ;; stop-inference:
  ;; Stop the current inferencing and optionally return a value.
  (define stop-inference
    (case-lambda
      ((return-value)
       ((current-inference-exit) return-value))
      (()
       ((current-inference-exit)))))
  
  ;; succeed:
  ;; Stop the current inferencing and return #t indicating success.
  (define (succeed)
    (stop-inference #t))
  
  ;; fail:
  ;; Stop the current inferencing and return #f indicating failure.
  (define (fail)
    (stop-inference #f))
  
  ;; print-rule-network
  ;; For debugging.
  (define (print-rule-network)
    (for-each
     (lambda (rule-node)
       (printf "----------~n")
       (printf "Rule: ~a~n~n" (rule-name (rule-node-rule rule-node)))
       (print-join-node (rule-node-join rule-node)))
     (current-inference-rule-nodes)))
  
  (define (print-join-node join-node)
    (when (join-node-left join-node)
      (if (join-node? (join-node-left join-node))
          (print-join-node (join-node-left join-node))
          (print-match-node (join-node-left join-node))))
    (when (join-node-right join-node)
      (print-match-node (join-node-right join-node)))
    (printf "join node: existential? = ~a~n" (join-node-existential? join-node))
    (printf "join-node: match-counts = ~a~n" (join-node-match-counts join-node))
    (printf "join node: matches = ~a~n~n" (node-matches join-node)))
  
  (define (print-match-node match-node)
    (printf "match-node: pattern = ~a~n" (match-node-pattern match-node))
    (printf "match-node: matches = ~a~n~n" (node-matches match-node)))

  )