;;; 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.
;;; 1.0.3   07/22/06 Cleaned up the code (e.g. merged code to activate
;;;                  data and goal rules).  Made trace more readable.
;;;                  (Doug Williams)
;;; 1.0.4   07/24/06 Added import and export.  (Doug Williams)
;;; 1.0.5   07/30/06 Added initial support for shared nodes in the rule
;;;                  network.  (Doug Williams)
;;; 1.0.6   08/18/06 Store the value of n for each match node rather than
;;;                  recomputing it.  (Doug Williams)
;;; 1.0.7   08/18/06 Made agenda use depth first insertion within other
;;;                  strategies.  (Doug Williams)
;;; 1.0.8   08/25/06 Added assumption processing.  (Doug Williams)
;;; 1.0.9   09/23/06 Changed (original) modify to replace and added
;;;                  reuse of the assertion object.  (Doug Williams)

(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.
  ;; Note that this code is reused in replace.  Any changes here need to
  ;; be made there too.
  (define assert
    (case-lambda
      ((fact reason)
       (let ((assertion (make-assertion fact reason)))
         (when (current-inference-trace)
           (printf ">>> ~a~n" assertion))
         ;; 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 (current-inference-rule))
       )))
  
  ;; retract: assertion -> void
  ;; Retract an assertion.  The retraction is passed into the rule network
  ;; for inferencing
  (define (retract assertion)
    (when (current-inference-trace)
      (printf "<<< ~a~n" 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)))))
  
  ;; replace: assertion x list x any -> assertion
  ;; replace: assertion x list -> assertion
  ;; Replace an assertion.  In essence, retract the assertion and then
  ;; re-assert it using the given fact.
  (define replace
    (case-lambda
      ((assertion fact reason)
       ;; Retract the assertion.
       (retract assertion)
       ;; Re-assert with the new fact and reason.
       ;; Copies from assert
       ;(assert fact reason)
       (set-assertion-fact! assertion fact)
       (set-assertion-reason! assertion reason)
       (when (current-inference-trace)
         (printf ">>> ~a~n" assertion))
       ;; 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)
      ((assertion fact)
       (replace assertion fact (current-inference-rule))
       )))
  
  ;; 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)
    (let/ec return
      (let ((assertion (make-assertion fact (current-inference-rule))))
        (when (current-inference-trace)
          (printf "??? ~a~n" assertion))
        (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))
  
  ;; assume: fact? -> any
  (define (assume fact)
    (let ((saved (copy-inference-environment (current-inference-environment))))
      (assert fact)
      (let ((result (start-inference)))
        (if result
            (current-inference-exit (inference-environment-exit saved))
            (current-inference-environment saved))
        result)))
  
  ;; 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
  ;;   n                    - number of assertions for initial symbol
  ;; 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-variables
     match-constraints
     match-constraint-predicate
     n)
    (make-inspector))
  (define-struct (join-node node)
    (left
     right
     join-constraint-variables
     join-constraints
     join-constraint-predicate
     existential?
     match-counts)
    (make-inspector))
  (define-struct (rule-node node)
    (rule
     join
     action)
    (make-inspector))
  
  ;; get-match-node: (same arguments as make-match-node)
  (define (get-match-node successors
                          matches
                          assertion-variable
                          pattern
                          match-constraint-variables
                          match-constraints
                          match-constraint-predicate
                          n)
    (let/ec return
      (for-each
       (lambda (match-node)
         (when (and (eq? assertion-variable
                         (match-node-assertion-variable match-node))
                    (equal? pattern
                            (match-node-pattern match-node))
                    (equal? match-constraint-variables
                            (match-node-match-constraint-variables match-node))
                    (equal? match-constraints
                            (match-node-match-constraints match-node)))
           (return match-node)))
       (hash-table-get (current-inference-data-index)
                       (pattern-first pattern)
                       (lambda () '())))
      (let ((match-node
             (make-match-node
              successors                        ; successors
              matches                           ; matches
              assertion-variable                ; assertion-variable
              pattern                           ; pattern
              match-constraint-variables        ; match-constraint-variables
              match-constraints                 ; match-contraints
              match-constraint-predicate        ; match-constraint-predicate
              n)))                              ; n
        (hash-table-put! (current-inference-data-index)
                         (pattern-first pattern)
                         (cons match-node
                               (hash-table-get (current-inference-data-index)
                                               (pattern-first pattern)
                                               (lambda () '()))))
        match-node)))


  ;; get-join-node: (same arguments as make-join-node)
  (define (get-join-node successors
                         matches
                         left
                         right
                         join-constraint-variables
                         join-constraints
                         join-constraint-predicate
                         existential?
                         match-counts)
    (let/ec return
      (for-each
       (lambda (join-node)
         (when (and (eq? left
                         (join-node-left join-node))
                    (eq? right
                         (join-node-right join-node))
                    (equal? join-constraint-variables
                            (join-node-join-constraint-variables join-node))
                    (equal? join-constraints
                            (join-node-join-constraints join-node))
                    (eq? existential?
                         (join-node-existential? join-node)))
           (return join-node)))
       (node-successors left))
      (make-join-node
       successors
       matches
       left
       right
       join-constraint-variables
       join-constraints
       join-constraint-predicate
       existential?
       match-counts)))
  
  ;; link-nodes: node x node -> void
  ;; Link nodes in a predecessor -> successor relationship.
  (define (link-nodes predecessor successor)
    (when (not (memq successor (node-successors predecessor)))
      (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
            '()                          ; join-constraint-variables
            '()                          ; join-constraints
            #f                           ; join-constraint-predicate
            #f                           ; existential?
            '())))                       ; match-counts
      (for-each
       (lambda (rule)
         (activate-rule rule initial-join-node))
       (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-rule rule initial-node)
    (let ((match-node #f)
          (join-node #f)
          (rule-node #f)
          (previous-node initial-node)
          (previous-variable-list '()))
      ;; Create goal match node (goal nodes only)
      (when (not (null? (rule-goals rule)))
        (let ((goal-pattern (car (rule-goals rule))))
          (set! previous-node
                (make-match-node
                 '()                     ; successors
                 #f                      ; matches
                 #f                      ; assertion-variable
                 goal-pattern            ; pattern
                 '()                     ; match-constraint-variables
                 '()                     ; match-constraints
                 #f                      ; match-constraint-predicate
                 0                       ; n
                 ))
          (hash-table-put!
           (current-inference-goal-index)
           (pattern-first goal-pattern)
           (cons previous-node
                 (hash-table-get
                  (current-inference-goal-index)
                  (pattern-first 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 ((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
                   (get-match-node
                    '()                      ; successors
                    '()                      ; matches
                    assertion-variable       ; assertion-variable
                    (pattern-base-pattern pattern) ; pattern
                    (if assertion-variable   ; match-constraint-variables
                        (cons assertion-variable (pattern-variables pattern))
                        (pattern-variables pattern))
                    match-constraints        ; match-contraints
                    (if (null? match-constraints) ; match-constraint-predicate
                        #f
                        (eval
                         `(lambda ,(if assertion-variable
                                       (cons assertion-variable
                                             (pattern-variables pattern))
                                       (pattern-variables pattern))
                            (and ,@match-constraints))))
                    0)))                      ; n
           ;; Make join node and link from match-node
           (let ((join-constraints
                  (pattern-join-constraints
                   pattern (pattern-variables pattern))))
             (set! join-node
                   (get-join-node
                    '()                    ; successors
                    (if (null? (rule-goals rule))
                        (if (or (memq existential? '(no notany))
                                (eq? existential? 'all))
                            (node-matches previous-node)
                            '())       
                        #f)                ; matches
                    previous-node          ; left
                    match-node             ; right
                    variable-list          ; join-constraint-variables
                    join-constraints       ; join-constraints
                    (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-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 rule node, link to it from the last join node, and add it
      (set! rule-node
            (make-rule-node
             '()                           ; successors
             (if (null? (rule-goals rule))
                 (node-matches previous-node)
                 #f)                       ; matches
             rule                          ; rule
             previous-node                 ; join
             (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))
  
  ;; fix-goal-matches:
  ;; Locate goal match nodes (i.e. any match node where the first symbol
  ;; of its pattern matches a goal-directed rule) and mark them as such
  ;; by setting their matches field to #f.
  (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)
    (set-match-node-n! match-node (+ (match-node-n match-node) 1))
    (let ((bindings (pattern-unify
                     (assertion-fact assertion)
                     (match-node-pattern match-node) '())))
      (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)))
            (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)
    (set-match-node-n! match-node (- (match-node-n match-node) 1))
    (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 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)))
            (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 (match-node-n (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 (match-node-n (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 (match-node-n (join-node-right join-node))))
                  (when (= count (- n 1))
                    (propagate-match-to-successors left-match join-node #f))))
               ((all)
                (let ((n (match-node-n (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)
    (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 (match-node-n (join-node-right join-node))))
               (when (< count n)
                 (propagate-match-to-successors match join-node continuation))))
            ((all)
             (let ((n (match-node-n (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)
    ;(add-match-to-node-matches match rule-node)
    (if (node-matches rule-node)
        (let ((rule-instance
               (make-rule-instance rule-node match 0)))
          (agenda-add! rule-instance))
        (begin
          (when (current-inference-trace)
            (printf "<== ~a: ~a~n"
                    (rule-node-rule rule-node)
                    (cdr match)))
          (when (rule-node-action rule-node)
            (current-inference-rule (rule-node-rule))
            (apply (rule-node-action rule-node)
                   (bindings-data match))
            (current-inference-rule #f)
            (current-inference-rules-fired
             (+ (current-inference-rules-fired) 1))
            )
          (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 (match-node-n (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 (match-node-n (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 (match-node-n (join-node-right join-node))))
                (when (= count n)
                  (unpropagate-match-to-successors left-match join-node))))
             ((all)
              (let ((n (match-node-n (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)
    (agenda-remove! rule-node match))
    
  ;; 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)))))
  
  ;; Rule instances
  
  (define-struct rule-instance (rule-node match random))
  
  ;; rule-instance-apply: rule-instance?
  (define (rule-instance-apply rule-instance)
    (let* ((rule-node (rule-instance-rule-node rule-instance))
           (rule (rule-node-rule rule-node))
           (match (rule-instance-match rule-instance))
           (arguments (bindings-data (cdr match))))
      (when (current-inference-trace)
        (printf "==> ~a: ~a~n"
                rule (cdr match)))
      ;; Apply the rule
      (current-inference-rule rule)
      (apply (rule-node-action rule-node) arguments)
      (current-inference-rule #f)
      (current-inference-rules-fired
       (+ (current-inference-rules-fired) 1))
      ))
  
  ;; agenda-add!: rule-instance?
  ;; Add a rule instance to the agenda in accordance with the current
  ;; conflict resolution strategy.
  (define (agenda-add! rule-instance)
    (let* ((rule-node (rule-instance-rule-node rule-instance))
           (rule (rule-node-rule rule-node))
           (priority (rule-priority rule)))
      (when (eq? (current-inference-strategy) 'random)
        (set-rule-instance-random! rule-instance (random)))
      (let ((agenda-tail (current-inference-agenda))
            (previous #f))
        (let loop ()
          (when (not (null? agenda-tail))
            (let* ((item (car agenda-tail))
                   (item-rule-node (rule-instance-rule-node item))
                   (item-rule (rule-node-rule item-rule-node))
                   (item-priority (rule-priority item-rule)))
              (cond ((> item-priority priority)
                     (set! previous agenda-tail)
                     (set! agenda-tail (cdr agenda-tail))
                     (loop))
                    ((and (= item-priority priority)
                          (or (eq? (current-inference-strategy) 'breadth)
                              (and (eq? (current-inference-strategy) 'order)
                                   (< (rule-order item-rule)
                                       (rule-order rule)))
                              (and (eq? (current-inference-strategy) 'simplicity)
                                   (< (rule-specificity item-rule)
                                       (rule-specificity rule)))
                              (and (eq? (current-inference-strategy) 'complexity)
                                   (> (rule-specificity item-rule)
                                       (rule-specificity rule)))
                              (and (eq? (current-inference-strategy) 'random)
                                   (< (rule-instance-random item)
                                       (rule-instance-random rule-instance)))))
                     (set! previous agenda-tail)
                     (set! agenda-tail (cdr agenda-tail))
                     (loop))
                    (else
                     (void))))))
        (if previous
            (set-cdr! previous (cons rule-instance agenda-tail))
            (current-inference-agenda (cons rule-instance agenda-tail))))))
  
  ;; agenda-remove: rule-node? x match?
  ;; Remove the rule instance for the given rule-node and match from
  ;; the agenda.
  (define (agenda-remove! rule-node match)
    (let loop ((previous #f)
               (agenda-tail (current-inference-agenda)))
      (when (not (null? agenda-tail))
        (let ((item (car agenda-tail)))
          (if (and (eq? rule-node (rule-instance-rule-node item))
                   (eq? match (rule-instance-match item)))
              (if previous
                  (set-cdr! previous (cdr agenda-tail))
                  (current-inference-agenda (cdr agenda-tail)))
              (loop agenda-tail (cdr agenda-tail)))))))
  
  ;; import: pattern?
  ;; Import assertions from the parent environment matching the given
  ;; pattern.
  (define (import pattern)
    (when (not (current-inference-parent))
      (error 'import
             "Current inference environment is not a child environment"))
    (let ((matches '()))
      (with-inference-environment (current-inference-parent)
        (set! matches (query pattern)))
      (for-each
       (lambda (match)
         (assert (assertion-fact (car match))))
       matches)))
  
  ;; export: pattern?
  ;; Exports assertions matching the given pattern to the parent
  ;; environment.
  (define (export pattern)
    (when (not (current-inference-parent))
      (error 'import
             "Current inference environment is not a child environment"))
    (let ((matches (query pattern)))
      (with-inference-environment (current-inference-parent)
        (for-each
         (lambda (match)
           (assert (assertion-fact (car match))))
         matches))))
  
  ;; copy-inference-environment:
  ;;   inference-environment? -> inference-environment?
  ;; Return a copy of the source inference environment.  This is used
  ;; in assumption processing.
  (define (copy-inference-environment source)
    (let ((target (make-inference-environment))
          (hash-table (make-hash-table)))
      ;; Copy rule network nodes from the rule nodes.
      (for-each
       (lambda (rule-node)
         (copy-rule-node rule-node hash-table))
       (inference-environment-rule-nodes source))
      ;; Copy data index
      (let ((target-data-index (inference-environment-data-index target)))
        (hash-table-for-each
         (inference-environment-data-index source)
         (lambda (key value)
           (hash-table-put!
            target-data-index
            key (copy-match-node-list value)))))
      ;; Clone goal index
      (let ((target-goal-index (inference-environment-goal-index target)))
        (hash-table-for-each
         (inference-environment-goal-index source)
         (lambda (key value)
           (hash-table-put!
            target-goal-index
            key (copy-match-node-list value)))))
      ;; Rule nodes will be cloned via the rule network cloning
      ;; Copy exit continuation
      (set-inference-environment-exit!
       target (inference-environment-exit source))
      ;; Copy next assertion id
      (set-inference-environment-next-assertion-id!
       target (inference-environment-next-assertion-id source))
      ;; Copy the assertion index
      (let ((target-assertion-index
             (inference-environment-assertion-index target)))
        (hash-table-for-each
         (inference-environment-assertion-index source)
         (lambda (key value)
           (hash-table-put!
            target-assertion-index key (list-copy value)))))
      ;; Copy the agenda
      (set-inference-environment-agenda!
       target (list-copy (inference-environment-agenda source)))
      ;; Copy the rule
      (set-inference-environment-rule!
       target (inference-environment-rule source))
      ;; Copy the strategy
      (set-inference-environment-strategy!
       target (inference-environment-strategy source))
      ;; Copy the parent
      (set-inference-environment-parent!
       target (inference-environment-parent source))
      ;; Return the target
      target))
  
  ;; copy-node: node? x hash-table? -> node?
  (define (copy-node node hash-table)
    (cond ((match-node? node)
           (copy-match-node node hash-table))
          ((join-node? node)
           (copy-join-node node hash-table))
          ((rule-node? node)
           (copy-rule-node node hash-table))
          (else
           (error 'copy-node
                  "~a is not a type of rule network node" node))))
  
  ;; copy-match-node: match-node? x hash-table? -> match-node?
  (define (copy-match-node match-node hash-table)
    (let ((copied-node (hash-table-get hash-table match-node #f)))
      (unless copied-node
        (set! copied-node
              (make-match-node
               '()
               (if (node-matches match-node)
                   (list-copy (node-matches match-node))
                   #f)
               (match-node-assertion-variable match-node)
               (match-node-pattern match-node)
               (match-node-match-constraint-variables match-node)
               (match-node-match-constraints match-node)
               (match-node-match-constraint-predicate match-node)
               (match-node-n match-node)))
        (hash-table-put! hash-table match-node copied-node))
      copied-node))
  
  ;; copy-join-node: join-node? x hash-table? -> join-node?
  (define (copy-join-node join-node hash-table)
    (let ((copied-node (hash-table-get hash-table join-node #f)))
      (unless copied-node
        (set! copied-node
              (make-join-node
               '()
               (if (node-matches join-node)
                   (list-copy (node-matches join-node))
                   #f)
               (copy-node (join-node-left join-node) hash-table)
               (copy-node (join-node-right join-node) hash-table)
               (join-node-join-constraint-variables join-node)
               (join-node-join-constraints join-node)
               (join-node-join-constraint-predicate join-node)
               (join-node-existential? join-node)
               (alist-copy (join-node-match-counts join-node))))
        (link-nodes (join-node-left copied-node) copied-node)
        (link-nodes (join-node-right copied-node) copied-node)
        (hash-table-put! hash-table join-node copied-node))
      copied-node))
  
  ;; copy-rule-node: rule-node? x hash-table? -> rule-node
  (define (copy-rule-node rule-node hash-table)
    (let ((copied-node (hash-table-get hash-table rule-node #f)))
      (unless copied-node
        (set! copied-node
              (make-rule-node
               '()
               (if (node-matches rule-node)
                   (list-copy (node-matches rule-node))
                   #f)
               (rule-node-rule rule-node)
               (copy-node (rule-node-join rule-node))
               (rule-node-action rule-node)))
        (link-nodes (rule-node-join rule-node) copied-node)
        (hash-table-put! hash-table rule-node copied-node))
      copied-node))
  
  ;; clone-match-node-list: list? x hash-table? -> list?
  ;; Clone a list of match nodes using the given hash table.
  (define (copy-match-node-list match-node-list hash-table)
    match-node-list)
  
  ;; 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 ((agenda (current-inference-agenda)))
          (if (not (null? agenda))
              (let ((rule-instance (car agenda)))
                (current-inference-agenda (cdr agenda))
                (rule-instance-apply rule-instance)
                (loop))
              #f)))))
  
  ;; 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 #:fail))
  
  ;; 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)))

  )