;;; Copyright (c) 1994-1995 Fahiem Bacchus and Froduald Kabanza
;;;  All right reserved. Use of this software is permitted for non-commercial
;;;  research purposes, and it may be copied only for that use. All
;;;  copies must include this copyright message.
;;;
;;;  This software and any documentation and/or information supplied with it
;;;  is distributed on an as is basis. Fahiem Bacchus, Froduald Kabanza
;;;  and the University of Waterloo make no warranties, express or implied,
;;;  including but not limited to implied warranties of merchantability and
;;;  fitness for a particular purpose, regarding the documentation,
;;;  functions or performance of such software, documentation and/or
;;;  information."
;;;
;;;;-----------------------------------------------------------------------
;;;; The TLPlan system is a forward chaining planner that utilizes        
;;;; temporal logic expressions to perform search control. Its central    
;;;; thesis is that temporal logics provide a powerful tool for expressing
;;;; the natural strategic knowledge we often seem to possess about various
;;;; domains.                                                             
;;;;                                                                      
;;;; The TLPlan system is in development, and we have a number of         
;;;; extensions/improvements planned. If you send e-mail to               
;;;; tlplan@logos.uwaterloo.ca                                            
;;;; you get yourself placed on news list, and we will send you information
;;;; about new releases of TLPlan as they become available.               
;;;;                                                                      
;;;; We are also interested in hearing about your experiences using TLPLan,
;;;; suggestions for improvement, comments etc. If you extend TLPLan, or  
;;;; implement a new domain we would also like to hear about it, and would 
;;;; encourage you to consider adding your extensions to the TLPlan        
;;;; distribution. Let us via the above e-mail address.                    
;;;;
;;;;----------------------------------------------------------------------
;;;;                                                                       
;;;; This version put together on Wed Mar 22 14:05:21 1995                 
;;;;                                                                       
;;;; This file is divided into the following modules. (Search for ">>>n"). 
;;;;                                                                       
;;;; 0) Package definitions
;;;; *) INSTALLATION STUFF.
;;;; +) A Scheme Interface to some Common Lisp functions
;;;; 1) Generic search algorithms.
;;;; 2) Persistent Binary trees (data structure used in representing worlds).
;;;; 3) Variables (utilities for dealing with variables).
;;;; 4) Unify (unification routines).
;;;; 5) Worlds (function for maintaining world databases).
;;;; 6) Eval (evaluate first order formulas on a world).
;;;; 7) Actions (the interface between the planner and actions).
;;;; 8) STRIPS operators
;;;; 9) ADL operators
;;;; 10) Temporal Progressor (progress temporal formulas over a world)
;;;; 11) Plan (the top level planner).
;;;; 12) Define-Domain (Routines for defining a domain).
;;;; 13) Interface (routines to support the interface).
;;;;
;;;; MTL Changes:
;;;; 14) Interval specs (routines to support interval specifications).
;;;;-----------------------------------------------------------------------

;;;;-----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>* INSTALLATION STUFF
;;;;     Look here for parameters to be modified during installation.
;;;;
;;;;-----------------------------------------------------------------------

(define *system-directory* "e:/tlplan-v3.0/scheme-version/")

(define *.rc-file* "tlplanrc")

;;;;-----------------------------------------------------------------------
;;;;                                                                       
;;;;>>> + Common Lisp Interface
;;;;      Look here for definitions of Common Lisp functions
;;;;
;;;;-----------------------------------------------------------------------
(declare (usual-integrations))

(declare (integrate put! get acons get-internal-run-time convert-to-string
		    every some first second third fourth rest
		    sublis-eq intersection remove-if remove-if-not
		    union set-difference merge-sorted-lists)) 

(load-option 'format)

;;;TLPLAN uses recursive structures, so invariably printing causes
;;;major problems.

(set! *unparser-list-depth-limit* 6)
(set! *unparser-list-breadth-limit* 7)

;;; The two following functions are usually defined in most
;;; Scheme implementations. However, MIT Scheme uses 2d-put! and 
;;; 2d-get.

(define put! 2d-put!)
(define get 2d-get)

(define (get-internal-run-time) (runtime))
(define internal-time-units-per-second 1)

(define (acons x y a) (cons (cons x y) a))

(define (convert-to-string x)
  (cond((string? x) x)
       ((symbol? x) (symbol->string x))
       ((number? x) (number->string x))
       ((list? x) (list->string x))
       (else (error 'convert-to-string 
		    x "cannot be converted to a string"))))

;;; MIT Scheme have there-exists? and forall? functions. However,
;;; they are not standard (R4RS). For portability I define 
;;; every and some using for-each.
;;;

(define (every predicate set . &rest)
  ;;;test whether or not predicate holds of every sequence
  ;;;of arguments specified in set and &rest
  ;;;e.g. (every (lambda (x y) (> (+ x y) 2)) '(1 2 3) (10 10 10))
  ;;;should return true.
  (or (null? set)
      (and (apply predicate (first set) (map first &rest))
	   (apply every predicate (rest set) (map rest &rest)))))

(define (some predicate set . &rest)
  ;;;Like every but only looks for some
  (and (not (null? set))
      (or (apply predicate (first set) (map first &rest))
	  (apply some predicate (rest set) (map rest &rest)))))

;;; Scheme has a list-ref function. However, it causes an error
;;; for an index out of bound instead of returning nil.

(define (nth n set)
  (cond
   ((or (null? set) (< n 0)) set)
       ((= n 0) (car set))
       (else (nth (- n 1) (cdr set)))))

;;; atom is defined in most Schemes, but not in MIT Scheme

(define (atom? exp) (not (pair? exp)))

;;; Common Lisp sublis function with eq? test

(define (sublis-eq pairs exp)
  (define (sublis exp)
    (cond
     ((null? exp) exp)
     ((atom? exp) 
      (let ((val (assq exp pairs)))
	(if (pair? val) (rest val) exp)))
     (else (cons (sublis (first exp)) (sublis (rest exp))))))
  (sublis exp))

(define (copy-list lst)
  (letrec ((loop (lambda (result l)
		(cond ((null? l) (reverse result))
		      (else (loop (cons (first l) result) (rest l)))))))
    (loop '() lst)))

;;; first, second, ... are already defined in MIT Scheme except rest.
;;; However, they are not standard. Moreover, like car and cdr
;;; they cannot be applied to the empty list. 

(define *gensym* -1)

(define (gensym string)
  (set! *gensym* (+ 1 *gensym*))
  (string->symbol (string-append string (number->string *gensym*))))


(define (first x) (nth 0 x))
(define (second x) (nth 1 x))
(define (third x) (nth 2 x))
(define (fourth x) (nth 3 x))
(define (rest x) (if (null? x) '() (cdr x)))


;;; MIT Scheme has a last-pair function. But it's not standard.
;;; Moreover, it does work for the empty list.

(define (last x) 
  (if (pair? (rest x)) (last (rest x)) x))

;;; The compile-file function in MIT Scheme
(define compile-file (lambda (file) (sf file)))

;;; Keywords that can be passed as arguments to functions.
;;; These keywords should never be redefined. This is awkward ...
;;; In a later update they should be implemented by macros.

(define :world-index ':world-index)
(define :test ':test)
(define :key ':key)
(define :transform ':transform)
(define :var-gens ':var-gens)
(define :form ':form)
(define :lit ':lit)
(define :name ':name)
(define :pre ':pre)
(define :add ':add)
(define :del ':del)
(define :duration ':duration)
(define :cost ':cost)
(define :priority ':priority)
(define :update ':update)
(define :eval-object ':eval-object)
(define :type ':type)
(define :arity ':arity)
(define :eval-type ':eval-type)

;;; MIT Scheme has a delete, list-transform-positive, and
;;; list-transform-negative function. However, they do not take
;;; keywords. Furthermore, they are not standard.

(define (remove-if predicate set . keyword-args)
  (let ((key (lambda (x) x)))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:key (set! key (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (letrec ((remove-iter 
	      (lambda (done todo)
		(cond((null? todo) (reverse done))
		     ((predicate (key (first todo)))
		      (remove-iter done (rest todo)))
		     (else (remove-iter (cons (first todo) done) (rest todo)))))))
      (remove-iter '() set))))

(define (remove-if-not predicate set . keyword-args)
  (let ((key (lambda (x) x)))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:key (set! key (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (remove-if (lambda(x) (not (apply predicate (list (key x))))) set)))

;;; Scheme has a member function, but without keywords.

(define (find element set . keyword-args)
  (let ((test (lambda (x y) (eq? x y)))
	(key (lambda (x) x)))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:test (set! test (cadr keyword-args)))
	(:key (set! key (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (letrec ((iter
	      (lambda (set)
		(cond((null? set) '()) 
		     ((test element (key (first set))) (first set))
		     (else (iter (rest set)))))))
      (iter set))))

(define (intersection list1 list2)
  (letrec ((iter
	    (lambda(list1 result)
	      (cond ((null? list1) result)
		    ((memq (first list1) list2)
		     (iter (rest list1) (cons (first list1) result)))
		    (else (iter (rest list1) result))))))
    (if (or (null? list1) (null? list2))
	'()
	(iter list1 '()))))

(define (union list1 list2)
  (letrec ((iter
	    (lambda (list1 result)
	      (cond ((null? list1) result)
		    ((memq (first list1) result)
		     (iter (rest list1) result))
		    (else (iter (rest list1) (cons (first list1) result)))))))
    (cond ((null? list1) list2)
	  ((null? list2) list1)
	  (else (iter list1 list2)))))


(define (set-difference list1 list2)
  (letrec ((iter
	    (lambda(list1 result)
	      (cond ((null? list1) result)
		    ((memq (first list1) list2)
		     (iter (rest list1) result))
		    (else (iter (rest list1) (cons (first list1) result)))))))
    (cond ((null? list1) '())
	  ((null? list2) list1)
	  (else (iter list1 '())))))

(define (every-other list)
 (cond ((null? list) '())
       ((null? (rest list)) list)
       (else (cons (first list) (every-other (rest (rest list)))))))


(define (merge list1 list2 predicate)
 (cond
  ((null? list1) list2)
  ((null? list2) list1)
  ((predicate (first list1) (first list2))
   (cons (first list1) (merge (rest list1) list2 predicate)))
  (else (cons (first list2) (merge list1 (rest list2) predicate)))))

(define (sort list predicate)
 (if (or (null? list) (null? (rest list)))
     list
     (merge (sort (every-other list) predicate)
	    (sort (every-other (rest list)) predicate)
	    predicate
	    )))

(define (merge-sorted-lists list1 list2 predicate . keyword-args)
  "This a special case of CL merge function when the two lists are
   sorted."
  (let ((key (lambda (x) x)))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:key (set! key (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (letrec ((iter 
	      (lambda (list1 list2 res)
		(cond((null? list1) (append! (reverse res) list2))
		     ((null? list2) (append! (reverse res) list1))
		     ((predicate (key (first list1)) (key (first list2)))
		      (iter (rest list1) list2 (cons (first list1) res)))
		     (else (iter list1 (rest list2) (cons (first list2) 
							  res)))))))
      (iter list1 list2 '()))))

;;;;-----------------------------------------------------------------------
;;;;
;;;;>>>1 GENERIC SEARCH ALGORITHMS
;;;;    a) graph searchers
;;;;    b) space efficient depth first search.
;;;;    c) iterative deepening search.
;;;;-----------------------------------------------------------------------
;;;
;;; (a) Basic Graph Search
;;;     graph-search can realize various search strategies dependent on
;;;     the "combiner-fn" and the "new-state-filter" function.
;;;

(define (graph-search start goal? successor-fn combiner-fn state= limit
		      . optional-args)
  "Find a state that satisfies goal?. Start from start,
  and search according to successor-fn and combiner-fn.
  Don't try the same state twice. Return goal state and lengths of
  OPEN and CLOSED in list (goal-state (length OPEN) (length CLOSED)).
  only expand a maximum of limit states"

  (do ((CLOSED '())
       (OPEN '())
       (new-states-filter (if (null? optional-args) 
			      filter-old-states 
			      (first optional-args)))
       (current-state start)
       (children-states '()))

      ;;In the termination condition below, if we terminate because
      ;;we find a plan we ensure that limit is not 0 so that we can
      ;;properly distinguish the rare case where a plan has been found
      ;;just as the resources run out. Also we return (length closed)
      ;;+ 1 as the number of states examined, as we need to also count
      ;;the current state.

      ((or (null? current-state)
           (and (goal? current-state)
                (set! limit (if (>= 0 limit) 1 limit)))
           (>= 0 limit))
       (list
        (if (>= 0 limit) 
	    'RESOURCES
	    (if (null? current-state) 
		'NO-PLAN
		current-state))
        (length OPEN) 
	(+ 1 (length CLOSED))))
    (set! limit (- limit 1))
    (set! children-states (successor-fn current-state))
    (set! CLOSED (cons current-state CLOSED))
    (if children-states
	(set! children-states
	      (new-states-filter children-states OPEN CLOSED state=)))
    (if children-states
	(set! OPEN (combiner-fn children-states OPEN)))
    (set! current-state (if (null? OPEN) '() (first OPEN)))
    (set! OPEN (rest OPEN))))

;;;;----------------------------------------------------------------------
;; Filters on the successor state allow us to implement A* search using
;; graph-search. Here we define two filters.
;;
;; Two types of filters for the successor states.                     
;; filter-old-states: The default. Always remove successor states that
;;                    have been seen before. Won't find optimal       
;;                    solutions.                                      
;;                                                                    
;; filter-worst-old-states: Returns a filter function that keeps      
;;                          successor states that have been seen      
;;                          before but which have a lower cost than   
;;                          the previous time they were seen.         
;;                                                                    
;; To explain further:                                                
;; We assume here that the search states have two components          
;; <path><terminal state>, that "state=" tests for equality of the    
;; <terminal state>, that "cost-fn" evaluates cost of <path>, and that
;; "successor-fn" works on these two component states. That is, the   
;; burden of maintaining path information is put on the user of these 
;; search routines.                                                   
;;                                                                    
;; filter-worst-old-states will effectively cause a re-search of      
;; certain states, ones to which we have found a better path.         
;;;;----------------------------------------------------------------------

(define (filter-old-states new-states OPEN CLOSED state=)
  "Remove successor states that have been seen before. I.e., are on
   either of the lists OPEN or CLOSED"
  (remove-if
   (lambda (state)
     (or (find state OPEN   :test state=)
	 (find state CLOSED :test state=)))
   new-states))

(define (filter-worst-old-states cost-fn)
  "Return a filter function that removes successors states that have
   been seen before unless they are lower cost than all previous instances
   according to cost-fn"
  (lambda (new-states OPEN CLOSED state=)
    (do ((result '())
	 (new-state '()))
	((null? new-states) result)
      (set! new-state (first new-states))
      (set! new-states (rest new-states))
      (let ((old-copies (append!  (find-all new-state OPEN   state=)
				  (find-all new-state CLOSED state=)))
	    (new-cost (cost-fn new-state)))
	(if (every (lambda (old-copy) (> (cost-fn old-copy) new-cost))
		   old-copies)
	    (set! result (cons new-state result)))))))

(define (find-all item list match-fn)
  "Return all matching members of states"
  (remove-if-not (lambda (element)  (match-fn item element))
		 list))

;;;;----------------------------------------------------------------------
;; Search routines that are implemented as specializations of graph-search
;;;;----------------------------------------------------------------------

(define (BREADTH-FIRST start goal? successor-fn state= cost-fn priority-fn
		       limit)
  "Search old states first until goal is reached."
  (graph-search start goal? successor-fn prepend state= limit))

(define (prepend x y) 
  "Prepend y to start of x" 
  (append! y x))

(define (BEST-FIRST start goal? successor-fn state= cost-fn priority-fn limit)
  "Search lowest cost states first until goal is reached."
  
  (graph-search start goal? successor-fn (merger cost-fn) state= limit
                (filter-worst-old-states cost-fn)))

(define (merger cost-fn)
  "Return a combiner function that merges new-states onto OPEN
   so that minimum cost-fn states are explored first. It also sorts
   the list of new states.
   The combiner function is DESTRUCTIVE"
  (lambda (new old)
    (merge-sorted-lists (sort new (lambda (x1 x2) 
				    (< (cost-fn x1) (cost-fn x2))))
			old 
			< 
			:key cost-fn)))

(define (BREADTH-FIRST-PRIORITY start goal? successor-fn state=
				cost-fn priority-fn limit)
  "Do breadth-first search but expand highest priority
   nodes first."
  (breadth-first start goal? (sorted successor-fn priority-fn)
                 state= cost-fn priority-fn limit))

(define (sorted successor-fn priority-fn)
  "Return a state successor-fn that produces list of successors sorted
   by priority-fn"
  (lambda (state)
    (sort (successor-fn state) 
	  (lambda (x1 x2) (> (priority-fn x1) (priority-fn x2))))))

;;;;----------------------------------------------------------------------
;;;
;;; (b) Space efficient Depth-first. Stores only the current path, but
;;;     checks for cycles on that path. 
;;;  For other applications there may be different ways for cycle checking. 
;;;;----------------------------------------------------------------------

(define (cycle-filter new-states)
  "Check if any of these states contains a cycle. Depends on plan structure."
  (remove-if plan-has-cycle new-states))

(define (DEPTH-FIRST start goal? successor-fn state= cost-fn priority-fn limit
		     . optional-args)
  "Search new states first until goal is reached."
  (do ((current-state start)
       (children-states '())
       (OPEN '())
       (cycle-filter-fn (if (null? optional-args)
			    cycle-filter
			    (first optional-args)))
       (states-expanded 0))
      
      ((or (null? current-state)
	   (and (goal? current-state)
		(set! limit (if (>= 0 limit) 1 limit)))
	   (>= 0 limit))
       (list
	(if (>= 0 limit) 'RESOURCES
	    (if (null? current-state) 'NO-PLAN
		current-state))
	(length OPEN) (+ 1 states-expanded)))
    (set! limit (- limit 1))
    (set! states-expanded (+ 1 states-expanded))
    (set! children-states (successor-fn current-state))
    (if children-states
	(set! children-states
	      (cycle-filter-fn children-states)))
    (if children-states
	(set! OPEN (append! children-states OPEN)))
    (set! current-state (if (null? OPEN) '() (first OPEN)))
    (set! OPEN (rest OPEN))))


(define (DEPTH-FIRST-PRIORITY start goal? successor-fn state= cost-fn
			      priority-fn limit)
  "Do depth-first search but explore highest priority
   children first."
  (depth-first start goal? (sorted successor-fn priority-fn)
	       state= cost-fn priority-fn limit))

;;;;----------------------------------------------------------------------
;;;
;;; c) Iterative deepening search.
;;;
;;; ID search. Uses two special parameters.                              
;;; (1) id-initial-depth      : the inital depth limit                   
;;; (2) id-depth-increment    : the depth increment                      
;;; These parameters are settable via the interface code.                
;;; Iteratively call depth-search with increasing depth bounds.          
;;; But keep track of total number of nodes expanded so that limit has   
;;; same semantics as other searcher. (i.e., count duplicate expansions).
;;; Implemented by augmenting the search state so that it also contains  
;;; its depth, and by changing the successor function so that states at  
;;; the depth bound don't generate any successors. All this is set       
;;; up and then depth-search is called.                                  
;;; Also keep track of the maximum level at which successors were        
;;; generated. If during any iteration this maximum level is less than   
;;; the depth bound we have exhausted the search space.                  
;;; Finally return the same value as the other search functions.
;;;
;;; Depth-first returns as its search result either the current
;;; state, or the symbols RESOURCES or NO-PLAN. id-search depends on
;;; the assumption that a non-cons object returned from depth-first
;;; indicates failure, a pair? object indicates a plan was found.
;;; This is probably a bad dependency.
;;;;----------------------------------------------------------------------

(define (id-cycle-filter new-states)
  "Check if any of these states contains a cycle. States have extras
   in id-seach."
  (remove-if plan-has-cycle new-states :key second))


(define (ID-SEARCH start goal? successor-fn state=
		   cost-fn priority-fn limit)
  "Do iterative deeping search."
  (let ((f-depth     (get-id-initial-depth))
	(max-f-depth (get-id-initial-depth)))
    (do ((nodes-expanded 0)
	 (nodes-not-expanded 0)
	 (finished '())
	 (search-result (list '() 0 0))
	 (id-start (list 0 start))
	 (id-goal?
	  (lambda (depth-state) (goal? (second depth-state))))
	 (id-successor-fn
	  (lambda (depth-state)
	    (let ((successors (successor-fn (second depth-state)))
		  (new-depth (+ 1 (first depth-state))))
	      (if successors
		  (set! max-f-depth
			(max max-f-depth new-depth)))
	      (if (>= (first depth-state) f-depth)
		  '()
		  (map (lambda (state) (list new-depth state))
		       successors)))))
	 (id-state=
	  (lambda (depth-state1 depth-state2)
	    (state= (second depth-state1) (second depth-state2))))
	 (id-cost-fn
	  (lambda (depth-state) (cost-fn (second depth-state))))
	 (id-priority-fn
	  (lambda (depth-state) (priority-fn (second depth-state)))))
	(finished
	 (list
	  (if (pair? (first search-result)) (second (first search-result))
	      (first search-result))
	  nodes-not-expanded nodes-expanded))

      (set! search-result
	    (depth-first id-start id-goal? id-successor-fn id-state=
			 id-cost-fn id-priority-fn limit id-cycle-filter))
      (set! finished (or (pair? (first search-result))
			 (> f-depth max-f-depth)
			 (>= 0 limit)))
      (set! nodes-not-expanded (+ nodes-not-expanded (second search-result)))
      (set! nodes-expanded (+ nodes-expanded (third search-result)))
      (set! limit (- limit (third search-result)))
      (set! f-depth (+ f-depth (get-id-depth-increment))))))

;;;;----------------------------------------------------------------------
;;;;
;;;;>>>2 PERSISTENT BINARY TREES.
;;;;   a) constructor, Selectors, Modifiers, copier, and predicate
;;;;   b) comparing arguments
;;;;   c) The tree utilities. 
;;;; 
;;;; Worlds are lists of atomic formulas, the set of atomic formulas
;;;; that are true in the current world. Instead of maintaining these
;;;; as unstructured lists, we maintain these as argument trees.
;;;; Each world is a set of argument trees, one tree for each predicate.
;;;; The predicate's argument tree contains the instances that are true
;;;; of that predicate in this world. For example, if in the current
;;;; world {on(A,B), on(B,C), on(C,D)} are the true instances of "on",
;;;; then the argument tree for "on" will contain the lists (A B), (B C)
;;;; and (C D). The argument tree is a binary tree, so we can test if
;;;; a particular instance of "on" is true or false in the current world
;;;; quite efficiently. When we modify a world by applying an action we
;;;; generate a new set of argument trees by updating them according to the
;;;; actions add and delete lists. Persistent comes from the fact that
;;;; these new argument trees share as much structure as is possible with
;;;; the old trees, hence they are "persistent binary trees" in the
;;;; data structures terminology.
;;;;
;;;; This module contains functions for dealing with argument trees.
;;;; Note that this implementation does not allow an argument tree to
;;;; contain duplicates (equal? keys are not allowed). Furthermore
;;;; insert tree will not insert an item that is already in the tree. 
;;;;----------------------------------------------------------------------

;;;;----------------------------------------------------------------------
;;;
;;; (a) B-TREE structure. Note that the constructor has no keywords.
;;;
;;;;----------------------------------------------------------------------

(declare (integrate make-b-tree b-tree-key b-tree-value b-tree-left
		    b-tree-right b-tree-owner copy-b-tree b-tree?
		    set-b-tree-key! set-b-tree-key! set-b-tree-value!
		    set-b-tree-left! set-b-tree-right! set-b-tree-owner!))

;;; Constructor
(define (make-b-tree key value left right owner)
  (vector 'b-tree key value left right owner))

;;; Predicate
(define (b-tree? x) 
  (and (vector? x) (= 6 (vector-length x)) (eq? 'b-tree (vector-ref x 0))))

;;; Selectors
(define b-tree-key (lambda (tree) (vector-ref tree 1)))
(define b-tree-value (lambda (tree) (vector-ref tree 2)))
(define b-tree-left (lambda (tree) (vector-ref tree 3)))
(define b-tree-right (lambda (tree) (vector-ref tree 4)))
(define b-tree-owner (lambda (tree) (vector-ref tree 5)))

;;; Modifiers
(define set-b-tree-key! (lambda (tree val) (vector-set! tree 1 val)))
(define set-b-tree-value! (lambda (tree val) (vector-set! tree 2 val)))
(define set-b-tree-left! (lambda (tree val) (vector-set! tree 3 val)))
(define set-b-tree-right! (lambda (tree val) (vector-set! tree 4 val)))
(define set-b-tree-owner! (lambda (tree val) (vector-set! tree 5 val)))

;;; Copier
(define copy-b-tree vector-copy)
;;;;----------------------------------------------------------------------
;;; b) Comparing arguments.
;;;    To allow this module to be ported to other applications, there
;;;    are functions to specify the default key comparisions in the
;;;    binary tree operations.
;;;;----------------------------------------------------------------------

(define (args< arg-list1 arg-list2)
  "Return #t iff arg-list1 should be sorted prior to arg-list2, this
   function must be called with identical size lists"
  (let ((x1 (convert-to-string (first arg-list1)))
	(x2 (convert-to-string (first arg-list2))))
    (cond
     ((string=? x1 x2) (args< (rest arg-list1) (rest arg-list2)))
     (else (string<? x1 x2)))))

(define *key<* args<)
;;;Default key comparator

(define *key=* equal?)
;;Default key equality test

(define (set-tree-default< fn)
  "Reset the default key comparator"
  (set! *key<* fn))

(define (set-tree-default= fn)
  "Reset the default key equality"
  (set! *key=* fn))

;;;;----------------------------------------------------------------------
;;; c) Tree utilities.
;;;;----------------------------------------------------------------------

;;  1. tree-search: locate an item in a tree. The item might be a tree
;;    (node) itself, or just a key.



(define (tree-search item tree)
  "Top-level tree-search, looks for tree-node or a key in tree"
  (let ((key (if (b-tree? item) (b-tree-key item) item)))
    (letrec ((b-search 
	      (lambda (tree)
		(if (or (null? tree)
			(*key=* key (b-tree-key tree)))
		    tree
		    (if (*key<* key (b-tree-key tree))
			(b-search (b-tree-left tree))
			(b-search (b-tree-right tree)))))))

      (b-search tree))))

;;
;; 2.  Get-reversed-path is special internal utility. It returns a list
;;     containing the path to a node, or a path to where the node should
;;     be if it was in the tree.

(define (get-reversed-path key tree)
  "Return path from key to root"
  (let ((accumulator '()))
    (letrec ((get-path 
	      (lambda (tree)
		(cond
		 ((null? tree) accumulator)
		 (else (set! accumulator (cons tree accumulator))
		       (if (*key=* key (b-tree-key tree))
			   accumulator
			   (if (*key<* key (b-tree-key tree))
			       (get-path (b-tree-left tree))
			       (get-path (b-tree-right tree)))))))))
      (get-path tree))))

;;
;; 3. Min and Max.
;;

(define (tree-min tree)
  "Get max key element of tree"
  (if (null? (b-tree-left tree))
      tree
      (tree-min (b-tree-left tree))))

(define (tree-max tree)
  "Get min key element of tree"
  (if (null? (b-tree-right tree))
      tree
      (tree-max (b-tree-right tree))))

;;
;; 4. Successor.
;;    Find an item's successor, or '() if it is the max or is not a
;;    member of the tree. (check Cormen Leiserson Rivest for algorithm,
;;    and note that final do loop returns '() if no ancestor of item is
;;    its successor. 
;;

(define (tree-successor item tree)
  "Find item's successor in tree if it exists, '() otherwise"
  (let* ((key (if (b-tree? item) (b-tree-key item) item))
         (rev-path-to-item (get-reversed-path key tree))
         (item-node (first rev-path-to-item))) ;This should be the item.
    (cond
     ((not (*key=* key (b-tree-key item-node))) ;Item not in tree!
      '()) 
     ((not (null? (b-tree-right item-node)))
      (tree-min (b-tree-right item-node)))
     (else (do ((parents (rest rev-path-to-item))
		(found #f)
		(parent '()))
	       ((or found (null? parents)) (if found parent '()))
	     (set! parent (first parents))
	     (set! parents (rest parents))
	     (if (and parent (eq? item-node (b-tree-right parent)))
		 (set! item-node parent)
		 (set! found #t)))))))  ;The do loop returns '() if it
;runs out of parent.

;;
;; 5. Insert and delete.
;;    The heart of the matter. Insert and delete that make new trees, but
;;    at the same time reuse structure. Check Corment et al. above, for
;;    presistent data structures. The algorithm is not in their book, but
;;    it's not hard with recursion, look at the way it is done without
;;    persistence. The "owner" field of the tree node is used to decide
;;    when a tree node can be modified and when a copy needs to be made.
;;
;; tree-insert. Must be called with a key that is not in tree already.
;; If called with a node that has subtree under it this will corrupt the
;; data structure. So tree-insert REMOVES these subtrees! This makes
;; it more useful, but perhaps more dangerous, as it does this
;; silently. 
;;

(define (tree-insert owner node tree)
  "Insert a node into the tree."
  (let* ((new-key (b-tree-key node)))
    (set-b-tree-right! node '())  ;Ensure only single node is
    (set-b-tree-left! node '())  ;inserted.
    (letrec ((insert 
	      (lambda (tree)
		(cond
		 ;No tree return single node tree.
		 ((null? tree) node)
		 ;else put into correct side.
		 ((*key<* new-key (b-tree-key tree))
		  (let ((new-tree
			 (if (eq? (b-tree-owner tree) owner) 
			     tree
			     (copy-b-tree tree))))
		    (set-b-tree-left! new-tree
				      (insert (b-tree-left tree)))
		    (set-b-tree-owner! new-tree owner)
		    new-tree))
		 
		 (else 
		  (let ((new-tree
			 (if (eq? (b-tree-owner tree) owner) 
			     tree
			     (copy-b-tree tree))))
		    (set-b-tree-right! new-tree
				       (insert (b-tree-right tree)))
		    (set-b-tree-owner! new-tree owner)
		    new-tree))))))
      (insert tree))))

;;
;; 6. Tree-delete, delete a key. Note difference from insert, it takes a
;; key as an argument not a tree-node. Also the Key must be in the
;; tree.       
;;

(define (tree-delete owner key tree)
  "Delete an item, a key or a tree node, from a tree"
  (letrec ((b-delete 
	    (lambda (key tree)
	      (cond
	       ;Need to delete root.
	       ((*key=* key (b-tree-key tree))
		(cond
		 ;Has two children
		 ((and (b-tree-right tree) (b-tree-left tree))
		  (let* ((successor-node (tree-successor key tree))
			 (new-tree
			  (if (eq? (b-tree-owner successor-node) owner)
			      successor-node
			      (copy-b-tree successor-node))))
		    (set-b-tree-right! new-tree
				       (b-delete (b-tree-key successor-node)
						 (b-tree-right tree)))
		    (set-b-tree-owner! new-tree owner)
		    (set-b-tree-left! new-tree (b-tree-left tree))
		    new-tree))
		 ((not (null? (b-tree-right tree))) (b-tree-right tree))
		 ;has only right child, return it.
		 ((not (null? (b-tree-left tree))) (b-tree-left tree))
		 ;has only left child return it.
		 (else '())))             ;no children return '()
	       ((*key<* key (b-tree-key tree))
		(let ((new-tree
		       (if (eq? (b-tree-owner tree) owner)
			   tree
			   (copy-b-tree tree))))
		  (set-b-tree-left! new-tree
				    (b-delete key (b-tree-left tree)))
		  (set-b-tree-owner! new-tree owner)
		  (set-b-tree-right! new-tree (b-tree-right tree))
		  new-tree))
	       (else 
		(let ((new-tree
		       (if (eq? (b-tree-owner tree) owner)
			   tree
			   (copy-b-tree tree))))
		  (set-b-tree-right! new-tree
				     (b-delete key (b-tree-right tree)))
		  (set-b-tree-owner! new-tree owner)
		  (set-b-tree-left! new-tree (b-tree-left tree))
		  new-tree))))))
    (b-delete key tree)))

;;
;; 7. Now for some other useful functions.
;;
;; tree-to-list: Convert tree to a list of Tree nodes. Then you can
;; map across this list getting what you want. Since we are
;; constructing a list it is easiest to visit the tree nodes in
;; reverse order.
;;
;; Also while we are at it, make it take a filter that it can apply to
;; elements. And a mapping function that can transform the raw nodes
;; into something more useful.
;; Use an internal recursive function to avoid having to invoke a
;; keyword parameter function recursively.
;;
;; In particular. :key   --- apply to node prior for testing.
;;                :test  --- only add to list if passes test (after
;;                           applying key!)
;;                :transform apply to nodes that past the test.
;; Returned value is list of transformed nodes that passed the test.
;;

(define (tree= tree1 tree2)
  "Test if two trees are equal"
  (letrec
      ((tree-check 
	(lambda (t1 t2)
	  (cond
	   ((and (null? t1) (null? t2)) #t)
	   ((or (null? t1) (null? t2)) #f)
	   ((and (*key=* (b-tree-key t1) (b-tree-key t2))
		 (eqv? (b-tree-value t1) (b-tree-value t2))
		 (tree-check (tree-successor t1 tree1)
			     (tree-successor t2 tree2))))
	   (else #f)))))
    (cond
     ((and (null? tree1) (null? tree2)) #t)
     ((or  (null? tree1) (null? tree2)) #f)
     (else (tree-check (tree-min tree1) (tree-min tree2))))))


(define (tree-to-list tree . keyword-args)
  "Return a list of the tree nodes that satisfy :test transformed by :key"
  (let ((accumulator '())
	(test '())
	(key '())
	(transform '()))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:test (set! test (cadr keyword-args)))
	(:key (set! key (cadr keyword-args)))
	(:transform (set! transform (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (letrec
        ((tree-walk 
	  (lambda (tree)
	    (cond
	     ((null? tree) accumulator)
	     (else 
	      (tree-walk (b-tree-right tree))
	      (if (or (and (not (null? test)) (not (null? key))
			   (test (key tree)))
		      (and (not (null? test)) (null? key) (test tree))
		      (and (null? test) (null? key)))
		  (set! accumulator
			(cons (if transform (transform tree) tree)
			      accumulator)))
	      (tree-walk (b-tree-left tree)))))))
      (tree-walk tree)
      accumulator)))

(define (tree-to-nested-list tree . keyword-args)
  "Return a nested list representing the tree structure where the
   nodes are transformed by the function transform."
  (let ((transform '()))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:transform (set! transform (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (letrec
	((tree-walk 
	  (lambda (tree)
	    (cond ((null? tree) '())
		  (else (list
			 (if (not (null? transform)) (transform tree) tree)
			 (tree-walk (b-tree-left tree))
			 (tree-walk (b-tree-right tree))))))))
      (tree-walk tree))))
  
(define (make-tree-generator tree transform)
  "Return a function that is a generator for the tree arguments.
   The tree nodes are transformed, by default to the key."
  (let ((current-node '())
	(next-node (tree-min tree)))
    (lambda ()
      (cond
       (next-node
	(set! current-node next-node)
	(set! next-node (tree-successor current-node tree))
	(if transform
	    (transform current-node)
	    (b-tree-key current-node)))
       (else '())))))

;;;;----------------------------------------------------------------------
;;;;
;;;;>>>3 VARIABLES
;;;;     Routines to handle variables.
;;;; a) var?          test is symbol is variable.
;;;; b) rename        rename all variables in clause to unique variables
;;;; c) variables-in  return list of all variables in clause.
;;;; d) not-occurs?  true if var does not occur in exp.
;;;;----------------------------------------------------------------------

(define (var? x)
  "Is x a variable (a symbol beginning with `?') ?"
  (and (symbol? x) (char-ci=? (string-ref (symbol->string x) 0) #\?)))

(define (rename-variables exp)
  "Rename all of the variables in exp DESTRUCTIVE"
  (sublis-eq (map (lambda (var) (cons var (gensym (convert-to-string var))))
		  (variables-in exp))
	     exp))

(define (variables-in exp)
  "Return list of all variables in exp"
  (cond ((var? exp) (list exp))
	((atom? exp) '())
	(else (union (variables-in (first exp))
		     (variables-in (rest exp))))))

(define (not-occurs? var exp)
  "Return #t if var does not appear in exp"
  (cond ((eq? var exp) '())
	((pair? exp)
	 (and (not-occurs? var (first exp))
	      (not-occurs? var (rest exp))))
	(else #t)))

(define (occurs? var exp)
  "Return #t if var appears in exp"
  (cond ((eq? var exp) #t)
	((pair? exp)
	 (or (occurs? var (first exp))
	     (occurs? var (rest exp))))
	(else #f)))

(define (variable-free? exp)
  "Return #t if expression has no variables"
  (cond ((null? exp) #t)
	((var? exp) #f)
	((atom? exp) #t)
	(else (and (variable-free? (first exp))
		   (variable-free? (rest exp))))))

;;;;----------------------------------------------------------------------
;;;;
;;;;>>>4 UNIFY
;;;;     Routines to do unification.
;;;;
;;;
;;; A) Conventions and Data Structures.
;;;
;;;    Atomic formulas are represented using nested lists.
;;;    e.g., P(f(?x,g(?y)), h(?y))
;;;         (P (f ?x (g ?y)) (h ?y))
;;; 
;;;    Variables are symbols that start with `?'
;;;
;;;    Substitutions are represented as lists of cons cells
;;;    e.g. ((?x . a) (?y . ?x))
;;;    Each pair is a cons cell and its first element is the variable.
;;;    The null? substitution is represented as
;;;    (())
;;;;----------------------------------------------------------------------

;;-----------------------------------------------------------------
;; Primitives for dealing with substitution pairs
;;

(define (get-var var-term)
  "Return the variable in a variable = term cell"
  (first var-term))

(define (get-term var-term)
  "Return the term in a variable = term cell"
  (if (null? var-term) '() (rest var-term)))

(define (make-var-term var term)
  "Return a variable = term cell"
  (cons var term))

;;-----------------------------------------------------------------
;; Primitives for accessing substitutions, i.e., lists of pairs
;; Define special empty-subsitution distinct from empty list
;;        want to preserve empty list as denoting failure.
;;

(define (make-sub var term)
  "Return a new substitution with one variable = term pair"
  (list (make-var-term var term)))

(define (get-binding var sub)
  "Return the binding for var in the substitution sub or '() if none"
  (get-term (assoc var sub)))

(define *empty-sub* '(()))
;;;The empty substitution


;;-----------------------------------------------------------------
;; Compose two substitutions
;; Apply as substitution to a term
;;       Treat empty substitution specially.
;;

(define (compose sub1 sub2)
  "Compute the composition of sub1*sub2 note order!"
  (if (equal? *empty-sub* sub1)
      sub2
      (if (equal? *empty-sub* sub2)
	  sub1
	  (let ((s1 
		 (map 
		  (lambda (var-term)
		    (make-var-term
		     (get-var var-term) 
		     (apply-sub sub2 (get-term var-term))))
		  sub1)))
	    (append! (remove-if
		      (lambda (var-term) 
			(eq? (get-var var-term) (get-term var-term)))
		      s1)
		     (remove-if 
		      (lambda (var-term) 
			(find (get-var var-term) sub1 :key get-var))
		      sub2))))))

(define (apply-sub sub exp)
  "Apply a substitution to an expression"
  (cond ((equal? *empty-sub* sub) exp)
	((var? exp)
	 (or (get-binding exp sub) exp))
	((pair? exp)
	 (cons (apply-sub sub (first exp))
	       (apply-sub sub (rest exp))))
	(else exp)))

;;-----------------------------------------------------------------
;; Compute Disagreement set
;; Unify two substitutions returning
;;       '()       --- fail
;;       empty-sub --- already match without substitution.
;;       m.g.u.    --- if they can be unified
;;

(define (dis-set x y)
  "Return the disagreement set of x and y"
  (cond ((eq? x y) '())
	((and (pair? x) (pair? y))
	 (or (dis-set (first x) (first y))
	     (dis-set (rest  x) (rest  y))))
	(else (cons x y))))


(define (unify x y . optional-args)
  "Return the m.g.u. of x and y or '() if it does not exist"
  (let* ((dis (dis-set x y))
	 (t1 (if (null? dis) '() (first dis)))
	 (t2 (if (null? dis) '() (rest dis)))
	 (subs *empty-sub*))
    (if (not (null? optional-args))
	(begin (set! subs (first optional-args))
	       (set! optional-args (rest optional-args))))
    (cond ((and (var? t1) (not-occurs? t1 t2))
	   (unify (apply-sub (make-sub t1 t2) x)
		  (apply-sub (make-sub t1 t2) y)
		  (compose subs (make-sub t1 t2))))
	  ((and (var? t2) (not-occurs? t2 t1))
	   (unify (apply-sub (make-sub t2 t1) x)
		  (apply-sub (make-sub t2 t1) y)
		  (compose subs (make-sub t2 t1))))
	  ((null? dis) subs)
	  (else '()))))

;;-----------------------------------------------------------------
;; Some useful applications of unify/substitute

(define (umatch-list literal lit-list)
  "Return non-'() if literal matches one of the literals in list lit-list"
  (some (lambda (lit) (unify literal lit)) lit-list))

(define (apply-sub-list sub lit-list)
  "Apply sub(stitution) to each expression in list lit-list"
  (map (lambda (lit) (apply-sub sub lit)) lit-list))

(define (apply-list-of-subs sub-list literal)
  "Apply a list of subs to a literal generating a list of literals"
  (map (lambda (sub) (apply-sub sub literal)) sub-list))

(define (find-all-unifiers literal lit-list)
  "Return a list of subs that allow literal to match a member of lit-list"
  (remove-if null? (map (lambda (lit) (unify literal lit)) lit-list)))

;;-----------------------------------------------------------------
;;find-all-list-unifiers. This function takes two lists and finds
;;all of the bindings that can make the first list a subset of the 
;;second. The algorithm is subtle, and built in (for efficiency sake)
;;is the assumption that the second list contains ground literals only.
;;To remove this assumption, it should be sufficient to compose substitutions
;;instead of just unioning them. 
;;
;;The algorithm is: start with the empty-substitution. First we find
;;all bindings that will make the first literal in list1 match a literal 
;;list2. Then we recurse with this list of bindings and the rest of list1.
;;At any stage we must apply all the bindings to the first literal 
;;that remains in list1. This generates a list of literals. For each of 
;;these literals we must determine all the ways it can be made to 
;;match list2. Each such binding unioned, composed with if list2 has
;;variables, with the binding used to generate the literal goes into the 
;;list of new bindings passed, along with the rest of the list, to the 
;;next level of recursion. At the bottom of the recursion we return the
;;list of bindings.

(define (find-all-list-unifiers lit-list1 lit-list2 . optional-args)
  "Return a list of subs that allow list1 to be subset of (fully-bound) list2"
  (let ((sub-list (list *empty-sub*)))
    (if (not (null? optional-args))
	(begin (set! sub-list (first optional-args))
	       (set! optional-args (rest optional-args))))
    (if (null? lit-list1)                  
	sub-list                          ;at bottom of recursion.
	(do ((sub '())
	     (match-lit '())
	     (new-bindings '())
	     (new-sub-list '()))
	    ((null? sub-list)
	     (if (null? new-sub-list) ;was unable to match next literal
		 '()
		 (find-all-list-unifiers (rest lit-list1) 
					 lit-list2 new-sub-list)))
	  (set! sub (first sub-list))
	  (set! sub-list (rest sub-list))
	  (set! match-lit (apply-sub sub (first lit-list1)))
	  (set! new-bindings (find-all-unifiers match-lit lit-list2))
	  (cond ((null? new-bindings));failed to match, this sub terminates
		(else (set! new-sub-list 
			    (append
			     (map (lambda (binding) 
				    (simple-compose binding sub))
				  ;change this to compose
				  ;if list2 has variables.
				  new-bindings)
			     new-sub-list))))))))

(define (simple-compose sub1 sub2)
  "Compute the simple composition of sub1*sub2 where not variables are shared"
  (if (equal? *empty-sub* sub1)
      sub2
      (if (equal? *empty-sub* sub2)
	  sub1
	  (append sub1 sub2))))

;;;;----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>5 Worlds
;;;; Functions for maintaining world states (i.e., databases describing
;;;; a world state.)
;;;; 
;;;;---------------------------------------------------------------------
;;;; Worlds:
;;;; The current world is defined by a database. On top of the database
;;;; are other parasitic functions and defined predicates. However
;;;; these are dealt with elsewhere. Here we have functions for
;;;; maintaining/updating the world database. Note that the only
;;;; dynamics in a world (parts that change) are generated via changes
;;;; to the database of described predicates/functions. The parasitic
;;;; functions/predicates might also change, but only as a result of
;;;; changes to the described predicates/functions.
;;;;
;;;; For each described predicate we have a full list of all positive
;;;; instances. For each described function we have a full list of all
;;;; function values (those values we do not have have the special
;;;; value *no-value*.
;;;;
;;;;----------------------------------------------------------------------
;;;; Internally world structures are stored in arrays. Each
;;;; predicate/function symbols is given an index into this array. This
;;;; index is stored on the symbols property list during the setup of
;;;; the domain (see the domains module). The array at the symbol's index
;;;; stores an argument tree, containing all positive tuples in the
;;;; case of a predicate, and all tuples that have a value in the case
;;;; of a function. For The argument tree is implemented as a binary
;;;; tree, where the tuple acts as a key into this tree, and in the
;;;; case of a function the value associated with the key is the function
;;;; value. 
;;;;
;;;;----------------------------------------------------------------------

(define (make-world )
  "Construct an empty internal world"
  (do ((world (make-vector *number-of-described-symbols*))
       (i 0 (+ 1 i)))
      ((=  i *number-of-described-symbols*) world)
    (vector-set! world i (cons '() 0))))

(define (copy-world world)
  "Generate a copy of a world, but share substructures"
  (do ((new-world (make-world))
       (i 0 (+ 1 i)))
      ((>= i *number-of-described-symbols*) new-world)
    (put-symbol-args new-world i (get-symbol-args world i))
    (put-symbol-args-# new-world i (get-symbol-args-# world i))))

(declare (integrate get-symbol-args put-symbol-args
		    get-symbol-args-# put-symbol-args-#))

(define (get-symbol-args world symbol-index)
  "Return the argument tree of a described symbol in world"
  (first (vector-ref world symbol-index)))

(define (put-symbol-args world symbol-index new-args)
  "Set the argument tree of a described symbol in world"
  (set-car! (vector-ref world symbol-index) new-args))

(define (get-symbol-args-# world symbol-index)
  "Return the number of arguments in the arg-tree"
  (rest (vector-ref world symbol-index)))

(define (put-symbol-args-# world symbol-index number)
  "Return the number of arguments in the arg-tree"
  (set-cdr! (vector-ref world symbol-index) number))

(define (incr-symbol-args-# world symbol-index)
  "Increment the number of arguments in the arg-tree"
  (set-cdr! (vector-ref world symbol-index)
	    (+ 1 (rest (vector-ref world symbol-index)))))

(define (decr-symbol-args-# world symbol-index)
  "Decrement the number of arguments in the arg-tree"
  (set-cdr! (vector-ref world symbol-index)
	    (- (rest (vector-ref world symbol-index)) 1)))


;;;;----------------------------------------------------------------------
;;; Interface routines. Convert to and from described lists of
;;; predicates/functions. Equality predicates are used to set function
;;; values.
;;;;----------------------------------------------------------------------

(define (create-world description)
  "Construct an internal world from a list of literals/functions."
  (do ((world (make-world))
       (index '())
       (lit '()))
      ((null? description) world)
    (set! lit (first description))
    (set! description (rest description))
    (if (fn-lit? lit)
	(set! index (get-symbol-index (get-fn-name lit)))
	(set! index (get-symbol-index (get-operator lit))))
    (cond
     ((and (predicate? index)
	   (not (search-arg-tree (get-args lit)
				 (get-symbol-args world index))))
      (put-symbol-args
       world index
       (insert-arg-tree world
			(get-args lit)
			(get-symbol-args world index)
			'()))
      (incr-symbol-args-# world index))
     ;;otherwise it is a (= (fn x) y) literal
     ((fn-lit? lit)
      (if (not
	   (search-arg-tree (get-fn-args lit) (get-symbol-args world index)))
	  (incr-symbol-args-# world index))
      (put-symbol-args
       world index
       (insert-arg-tree world
			(get-fn-args lit)
			(get-symbol-args world index)
			(get-fn-value lit)))))))

(define (list-world world)
  "Construct a list description of a world"
  (do ((description '())
       (i 0 (+ 1 i)))
      ((>= i *number-of-described-symbols*) description)
    (set! description
	  (append!
	   (arg-tree-to-list (get-symbol-name i)
			     (get-symbol-args world i))
	   description))))

(define (default-print-world world/action . optional-args)
  "Print a list description of a world"
  (do ((world (world/action-world world/action))
       (i 0 (+ 1 i))
       (stream (if (null? optional-args)
		   *trace-stream*
		   (first optional-args))))
      ((>= i *number-of-described-symbols*))
    (format stream "~%<~S,~S>:~@4A"
	    (get-symbol-name i) (get-symbol-args-# world i)
	    (arg-tree-to-list (get-symbol-name i) 
			      (get-symbol-args world i)))))

;;;----------------------------------------------------------------------
;;; Argument trees are simply a list of all distinct arguments of a
;;; predicate true in the current world. They are implemented as sorted
;;; binary trees, and we use the binary-tree support code.
;;;
;;; Throw up an abstraction layer between binary trees and argument
;;; trees.
;;;----------------------------------------------------------------------

(define (insert-arg-tree owner new-arg arg-tree value)
  "Insert NEW arg owned by owner into arg-tree
   (perhaps owned by someone else)."
  (if value
      (tree-insert owner
		   (make-b-tree new-arg value '() '() owner)
		   arg-tree)
      (tree-insert owner
		   (make-b-tree new-arg '() '() '() owner)
		   arg-tree)))

(define (delete-arg-tree owner arg arg-tree)
  "Delete OLD argument owned by owner from arg tree
   (perhaps owned by someone else)." 
  (tree-delete owner arg arg-tree))

(define (search-arg-tree arg arg-tree)
  "Return #t if arg is found in arg-tree"
  (if (tree-search arg arg-tree) #t #f))

(define *no-value* "novalue")
;;;Special value for unknown function value

(define (find-value-arg-tree arg arg-tree)
  (let ((node (tree-search arg arg-tree)))
    (if node (b-tree-value node) *no-value*)))

(define (arg-tree-to-list symbol-name arg-tree)
  "Generate sorted list from tree"
  (tree-to-list arg-tree
		:transform
		(lambda (b-tree-node)
		  (if (b-tree-value b-tree-node)
		      (list '=
			    (cons symbol-name (b-tree-key b-tree-node))
			    (b-tree-value b-tree-node))
		      (cons symbol-name (b-tree-key b-tree-node))))))

;;;----------------------------------------------------------------------
;;; World equality test
;;;----------------------------------------------------------------------

(define (world= world1 world2)
  "Do a series of tests in order of complexity to determine if two
   worlds are equal"
  (cond
   ((eq? world1 world2)
    #t)
   ((do ((i 0 (+ 1 i)) 
	 (found? #f))
	((or (>= i *number-of-described-symbols*) found?)
	 found?)
      (set! found? (not (= (get-symbol-args-# world1 i) 
			   (get-symbol-args-# world2 i)))))
    #f)
   ((do ((i 0 (+ 1 i)) 
	 (found? #f))
	((or (>= i *number-of-described-symbols*) found?)
	 found?)
      (set! found? (not (tree= (get-symbol-args world1 i) 
			       (get-symbol-args world2 i)))))
    #f)
   (else #t)))

;;;;----------------------------------------------------------------------
;;; Actions interface. Note that these functions should be called with
;;; a copy of an old world so that the old world remains intact.
;;;----------------------------------------------------------------------

(define (add-world-lit pred-sym args world)
  "Update the current world by adding a literal."
  (let ((arg-tree '())
	(index '()))
    (set! index (get-symbol-index pred-sym))
    (set! arg-tree (get-symbol-args world index))
    (if (not (search-arg-tree args arg-tree))
	(begin
	  (put-symbol-args
	   world index (insert-arg-tree world args arg-tree '()))
	  (incr-symbol-args-# world index)))
    world))

(define (delete-world-lit pred-sym args world)
  "Update the current world by deleteing a literal."
  (let ((arg-tree '())
	(index '()))
    (set! index (get-symbol-index pred-sym))
    (set! arg-tree (get-symbol-args world index))
    (if (search-arg-tree args arg-tree)
	(begin (put-symbol-args
		world index (delete-arg-tree world args arg-tree))
	       (decr-symbol-args-# world index)))
    world))

(define (update-world-fn fn-sym args value world)
  "Update the current world by modifying a function value."
  (let ((arg-tree '())
	(index '()))
    (set! index (get-symbol-index fn-sym))
    (set! arg-tree (get-symbol-args world index))
    (if (search-arg-tree args arg-tree)
	(set! arg-tree (delete-arg-tree world args arg-tree))
	(incr-symbol-args-# world index))
    (put-symbol-args
     world index (insert-arg-tree world args arg-tree value))
    world))

;;;----------------------------------------------------------------------
;;; Evaluator interface. Provide information about the current world.
;;; 1. Evaluate ground literal for described predicate in world.
;;; 2. Return generator for described predicate in world.
;;; 3. Evaluate ground function for descrbibed function in world.
;;;    *Alternate compile lisp functions to do these tasks*
;;;----------------------------------------------------------------------

(define (eval-desc-predicate index args world/action)
  "Evaluate lit in world"
  (search-arg-tree 
   args (get-symbol-args (world/action-world world/action) index)))

(define (eval-desc-function index args world/action)
  "Evaluate function in world, args are fully evaluated"
  (find-value-arg-tree 
   args 
   (get-symbol-args (world/action-world world/action) index)))

(define (desc-predicate-generator index world/action)
  "Return a generator (function) for the tuples satisfying pred."
  (let ((arg-tree 
	 (get-symbol-args (world/action-world world/action) index)))
    (if arg-tree
	(make-tree-generator arg-tree '())
	'())))


;;;----------------------------------------------------------------------
;;; Planner interface to handle creation of goal-world.
;;;----------------------------------------------------------------------

(define goal-world '())
(define (create-goal-world/action goal-list)
  "Set up a goal world"
  (set! goal-world 
	(make-world/action (create-world goal-list)
			   '() 0 0 0)))

(define (get-goal-world )
  goal-world)

;;;;----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>6 EVAL
;;;;
;;;; Routines to evaluate first-order formulas on worlds.
;;;;----------------------------------------------------------------------
;;;
;;; Formula Syntax.
;;; Predicates are specified via literal lists, e.g.,
;;; (Pred x1 x2)
;;; Functions are specified via equality literals where the function
;;; always comes first and the function value comes second, e.g.,
;;; (= (fn x1) y1)
;;; Quantified Formulas have the syntax, e.g.,
;;; (forall (?x ?y) (on ?x ?y) formula)
;;; Binding formulas are internal: used only by the temporal goal progressor.
;;;;----------------------------------------------------------------------

(define (get-operator formula)
  (first formula))

(define (get-args formula)
  (rest formula))

(define (fn-lit? lit)
  (eq? (first lit) '=))

(define (get-fn-name fn-lit)
  (first (second fn-lit)))

(define (get-fn-args fn-lit)
  (rest (second fn-lit)))

(define (get-fn-value fn-lit)
  (third fn-lit))

(define (=-formp form)
  "Test if formula is an = formula."
  (eq? (get-operator form) '=))

(define (and-formp form)
  "Test if formula is an AND formula."
  (eq? (get-operator form) 'AND))

(define (or-formp form)
  "Test if formula is an OR formula."
  (eq? (get-operator form) 'OR))

(define (xor-formp form)
  "Test if formula is an XOR  formula."
  (eq? (get-operator form) 'XOR))

(define (if-then-else-formp form)
  "Test if formula is an if-then-else formula."
  (eq? (get-operator form) 'IF-THEN-ELSE))

(define (not-formp form)
  "Test if formula is a NOT formula."
  (eq? (get-operator form) 'NOT))

(define (implies-formp form)
  "Test if formula is a IMPLIES formula."
  (eq? (get-operator form) 'IMPLIES))

(define (goal-formp form)
  "Test if formula is a GOAL modality formula."
  (eq? (get-operator form) 'GOAL))

(define (call-formp form)
  "Test if formula is a CALL formula."
  (eq? (get-operator form) 'CALL))

(define (forall-formp form)
  "Test if formula is a FORALL formula."
  (eq? (get-operator form) 'FORALL))

(define (exists-formp form)
  "Test if formula is an EXISTS formula."
  (eq? (get-operator form) 'EXISTS))

(define (exists!-formp form)
  "Test if formula is an EXISTS! (exists unique) formula."
  (eq? (get-operator form) 'EXISTS!))

(define (next-formp form)
  "Test if formula is a NEXT formula."
  (eq? (get-operator form) 'NEXT))

(define (eventually-formp form)
  "Test if formula is an EVENTUALLY formula."
  (eq? (get-operator form) 'EVENTUALLY))

(define (always-formp form)
  "Test if formula is an ALWAYS  formula."
  (eq? (get-operator form) 'ALWAYS))

(define (until-formp form)
  "Test if formula is an UNTIL  formula."
  (eq? (get-operator form) 'UNTIL))

;;
;; MTL Changes. Syntax checkers for bounded temporal operators.
;;

(define (t-until-formp form)
  "Test if formula is a bounded until."
  (eq? (get-operator form) 'T-UNTIL))

(define (t-eventually-formp form)
  "Test if formula is a bounded eventually."
  (eq? (get-operator form) 'T-EVENTUALLY))

(define (t-always-formp form)
  "Test if formula is a bounded always."
  (eq? (get-operator form) 'T-ALWAYS))

(define (delta-formp form)
  "Test if formula is a DELTA formula."
  (eq? (get-operator form) 'DELTA))

;;
;;

(define (binding-formp form)
  "Test if formula is a BINDING formula."
  (eq? (get-operator form) 'BINDING))

(define (atomic-formp form)
  "Test if formula is an atomic formula."
  (not
   (or (or-formp form)
       (and-formp form)
       (forall-formp form)
       (exists-formp form)
       (not-formp form)
       (implies-formp form)
       (goal-formp form)
       (call-formp form)
       (next-formp form)
       (eventually-formp form)
       (always-formp form)
       (until-formp form)
       (t-until-formp form)
       (t-eventually-formp form)
       (t-always-formp form)
       (delta-formp form)
       (binding-formp form))))

(define (fn-value-generator? gen-lit)
  "Is gen-lit a function evaluation generator?"
  (eq? (first gen-lit) '=))

(define (get-fn-lit-gen gen-lit)
  "Return the function literal from a function evaluation generator"
  (second gen-lit))

(define (make-and-form args)
  "Make an AND formula"
  (cons 'AND args))

(define (make-or-form args)
  "Make an OR formula."
  (cons 'OR args))

(define (make-xor-form args)
  "Make an XOR formula."
  (cons 'XOR args))

(define (make-not-form arg)
  "Make a NOT formula"
  (list 'NOT arg))

(define (make-implies-form arg1 arg2)
  "Make an IMPLIES formula."
  (cons 'IMPLIES (list arg1 arg2)))

(define (make-if-then-else-form arg1 arg2 arg3)
  "Make and IF-THEN-ELSE formula."
  (cons 'IF-THEN-ELSE (list arg1 arg2 arg3)))

(define (make-binding-form vars vals formula)
  "Make a bindings formula."
  (cons 'BINDING (list vars vals formula)))

(define (get-binding-formula binding-form)
  (third (rest binding-form)))

(define (set-binding-formula binding-form value)
  (set-car! (cddr (rest binding-form)) value))

(define (get-binding-vars binding-form)
  (first (rest binding-form)))

(define (get-binding-vals binding-form)
  (second (rest binding-form)))

;; MTL Changes.
;;

(define (make-delta-form formula)
  "Make a delta (time shift formula)."
  (cons 'DELTA formula))

(define (get-delta-formula delta-form)
  (rest delta-form))

(define (get-bf-ispec bf-form)
  "Get the interval specification from the arguments of a bounded 
   formula."
  (second bf-form))

(define (get-bf-formulas bf-form)
  "Get the formulas arguments of a bounded formula."
  (rest (rest bf-form)))

;;
;;

(define (function-term? term)
  (pair? term))

(define (get-qf-variables qf-args)
  "Get the variables from the arguments of a quantified formula"
  (first qf-args))

(define (get-qf-generator qf-args)
  "Get the generator literal from the arguments of a quantified formula"
  (second qf-args))

(define (get-qf-formula qf-args)
  "Get the formula from the arguments of a quantified formula"
  (if (< (length qf-args) 3) '()
	 (third qf-args)))

(define (find-free-vars form . optional-args)
  "Return the free variables of a formula."
  (let ((bound-vars '()) 
	(free-vars '()))
    (if (not (null? optional-args))
	(begin (set! bound-vars (first optional-args))
	       (set! optional-args (rest optional-args))))
    (if (not (null? optional-args))
	(begin (set! free-vars (first optional-args))
	       (set! optional-args (rest optional-args))))
    (cond 
     ((or (call-formp form) (null? form)) free-vars)
     ((or (forall-formp form) (exists-formp form))
      (map (lambda (var) 
	     (if (not (memq var bound-vars))
		 (set! bound-vars (cons var bound-vars))))
	   (get-qf-variables (get-args form)))
      (map (lambda (var) 
	     (if (not (memq var free-vars))
		 (set! free-vars (cons var free-vars))))
	   (set-difference (variables-in (get-qf-generator (get-args form)))
			   bound-vars))
      (find-free-vars (get-qf-formula (get-args form))
		      bound-vars free-vars))
     ((binding-formp form)
      (map (lambda (var) 
	     (if (not (memq var bound-vars))
		 (set! bound-vars (cons var bound-vars))))
	   (get-binding-vars form))
      (find-free-vars (get-binding-formula form)
		      bound-vars free-vars))
     ((atomic-formp form)
      (map (lambda (var) 
	     (if (not (memq var free-vars))
		 (set! free-vars (cons var free-vars))))
	   (set-difference (variables-in form) bound-vars))
      free-vars)
     (else 
      (do ((args (get-args form))
	   (current-free-vars free-vars)
	   (arg '()))
	  ((null? args) free-vars)
	(set! arg (first args))
	(set! args (rest args))
	(for-each (lambda (var) 
		    (if (not (memq var free-vars))
			(set! free-vars (cons var free-vars))))
		  (find-free-vars arg bound-vars current-free-vars)))))))

;;;----------------------------------------------------------------------
;;; Evaluator dispatch table
;;;----------------------------------------------------------------------

(define operator-eval-table '())
  ;;Table of functions for evalutating various types of operators

(define (lookup-operator-eval operator)
  (let ((x (assoc operator operator-eval-table)))
    (if x (rest x) '())))

(define (place-operator-eval operator eval-fn)
  (set! operator-eval-table (acons operator eval-fn operator-eval-table)))

(define (replace-operator-eval operator eval-fn)
  (let ((cell (assoc operator operator-eval-table)))
    (set-cdr! cell eval-fn)))


;;;----------------------------------------------------------------------
;;; Bindings.
;;;----------------------------------------------------------------------

(define (lookup-var var bindings)
  "Find variable binding, or complain if none"
  (let ((cell (assoc var bindings)))
    (if cell
	(rest cell)
	(error "Formula contains unbound variable ~S" var))))

(define (lookup-var-silent var bindings)
  "Find variable binding, or complain if none"
  (let ((cell (assoc var bindings)))
    (if cell
	(rest cell)
	#f)))

(define (set-var! var val bindings)
  "Destructively set var's binding in bindings"
  (let ((cell (assoc var bindings)))
    (if cell
	(set-cdr! cell val)
	(error "Formula contains unbound variable ~S" var))))

(define (extend-bindings vars vals bindings)
  "Extend the current set of bindings by the var val pairs"
  (append! (map cons vars vals) bindings))

(define (adjoin-bindings new-bindings old-bindings)
  "Extend the old bindings by placing new bindings in front"
  (append new-bindings old-bindings))

;;;----------------------------------------------------------------------
;;; The evaluator itself.
;;;----------------------------------------------------------------------

(define (eval-formula formula world/action bindings)
  "Top level formula evaluator, dispatch on non-atomic formulas"
  (let ((dispatch-fn (lookup-operator-eval (get-operator formula)))
	(args (get-args formula)))
    (if (not (null? dispatch-fn))
	(dispatch-fn args world/action bindings)
	(eval-atomic (get-operator formula)
		     (eval-terms args world/action bindings)
		     world/action))))

(define (eval-terms terms world/action bindings)
  "Evaluate a sequence of terms"
  (map (lambda (term) (eval-term term world/action bindings))
       terms))

(define (eval-term term world/action bindings)
  (cond
   ((var? term) (lookup-var term bindings))
   ((atom? term) term)
   ((function-term? term)
    (eval-function (get-operator term)
		   (eval-terms (get-args term) world/action bindings)
		   world/action))
   (else (error "Illegal term in formula ~S" term))))

(define (eval-function fn args world/action)
  "Evaluate a function where all the arguments have already been evaluated."
  (let ((index (get-symbol-index fn)))
    (cond
     ((not index)
      (error "Unknown function symbol in term ~S" fn))
     ((computed? index)
      ((get-symbol-eval-object index) args world/action))
     ((described? index)
      (eval-desc-function index args world/action))
     (else 
      (error "Function of unknown type in term ~S" fn)))))

(define (eval-atomic pred args world/action)
  "Evaluate an atomic formula where all the arguments have been evaluated."
  (let ((index (get-symbol-index pred)))
    (cond
     ((not index)
      (error "Unknown predicate symbol in term" pred))
     ((computed? index)
      ((get-symbol-eval-object index) args world/action))
     ((described? index)
      (eval-desc-predicate index args world/action))
     ((defined? index)
      (eval-def-predicate index args world/action))
     (else 
      (error "Predicate on unknown type in term ~S" pred)))))

(define (eval-def-predicate index args world/action)
  (let* ((df (get-symbol-eval-object index))
         (bindings (extend-bindings (get-def-parameters df) args '())))
    (eval-formula (get-def-formula df) world/action bindings)))


;;;----------------------------------------------------------------------
;;; Dispatched operators.
;;;----------------------------------------------------------------------
;;; Booleans
;;;----------------------------------------------------------------------

(define (eval-and args world/action bindings)
  "Evaluate an AND"
  (every (lambda (formula) (eval-formula formula world/action bindings))
         args))

(define (eval-or args world/action bindings)
  "Evaluate an OR"
  (some (lambda (formula) (eval-formula formula world/action bindings))
        args))

(define (eval-xor args world/action bindings)
  "Evaluate an exclusive or"
  (letrec
      ((loop (lambda (forms found-one)
	       (cond ((null? forms) found-one)
		     ((eval-formula (first forms) world/action bindings)
		      (if found-one #f (loop (rest forms) #t)))
		     (else (loop (rest forms) found-one))))))
    (loop args #f)))
    
(define (eval-implies args world/action bindings)
  "Evaluate an IMPLIES"
  (if (eval-formula (first args) world/action bindings)
      (eval-formula (second args) world/action bindings)
    #t))

(define (eval-if-then-else args world/action bindings)
  "Evaluate an IF-THEN-ELSE. (IF-THEN-ELSE A B C) is equivalent to,
   (and (IMPLIES A B) (IMPLIES (not A) C). But is nice syntactic sugar."
  (if (eval-formula (first args) world/action bindings)
      (eval-formula (second args) world/action bindings)
    (eval-formula (third args) world/action bindings)))

(define (eval-not args world/action bindings)
  "Evaluate a NOT"
  (not (eval-formula (first args) world/action bindings)))


(define (eval-= args world/action bindings)
  (eqv? (eval-term (first args) world/action bindings)
	(eval-term (second args) world/action bindings)))

(define (eval-true args world/action bindings)
  #t)

(define (eval-false args world/action bindings)
  #f)

(define (eval-binding args world/action bindings)
  "eval a binding node, by extending the current bindings." 
  (let ((b-vars (first args))
	(b-vals (second args))
	(b-form (third args)))
    (eval-formula b-form world/action
		  (extend-bindings b-vars b-vals bindings))))

(for-each place-operator-eval
        '(AND OR XOR
	      NOT IMPLIES IF-THEN-ELSE
	      TRUE FALSE = BINDING)
        (list eval-and eval-or eval-xor
              eval-not eval-implies eval-if-then-else
              eval-true eval-false eval-= eval-binding))

;;;----------------------------------------------------------------------
;;; Quantifiers.
;;;----------------------------------------------------------------------

(define (eval-forall args world/action bindings)
  "Evaluate a FORALL formula"
  (let* ((variables (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (formula   (get-qf-formula args))
         (generator '()))
    (set! bindings (extend-bindings variables variables bindings))
    (set! generator
      (make-generator gen-lit variables world/action bindings))
    (if generator
        (do ((finish? #f)
             (result '()))
            (finish? result)
          (cond((generator)
		(if (not (eval-formula formula world/action bindings))
		    (begin (set! finish? #t)
			   (set! result #f))))
	       (else (set! finish? #t)
		     (set! result #t))))
	#t)))
  

(define (eval-exists! args world/action bindings)
  "Evaluate an EXISTS! (exists unique) formula"
  (let* ((variables (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (formula   (get-qf-formula args))
         (generator '()))
    (set! bindings (extend-bindings variables variables bindings))
    (set! generator
      (make-generator gen-lit variables world/action bindings))
    (if generator
        (do ((finish? #f)
             (result '())
             (found-one? #f))
            (finish? result)
          (if (generator)
	      (if (or (null? formula) 
		      (eval-formula formula world/action bindings))
		  (cond(found-one?
			(set! finish? #t)
			(set! result '()))
		       (else (set! found-one? #t))))
	      (cond(found-one?
		    (set! finish? #t)
		    (set! result #t))
		   (else (set! finish? #t)
			 (set! result '())))))
	#f)))


(define (eval-exists args world/action bindings)
  "Evaluate an EXISTS formula"
  (let* ((variables (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (formula   (get-qf-formula args))
         (generator '()))
    (set! bindings (extend-bindings variables variables bindings))
    (set! generator
      (make-generator gen-lit variables world/action bindings))
    (if generator
        (do ((finish? #f)
             (result '()))
            (finish? result)
          (cond((generator)
		(if (or (null? formula)
			(eval-formula formula world/action bindings))
		    (begin (set! finish? #t)
			   (set! result #t))))
	       (else (set! finish? #t)
		     (set! result #f))))
	#f)))

(for-each place-operator-eval
        '(FORALL EXISTS EXISTS!)
        (list eval-forall eval-exists eval-exists!))

(define (make-generator gen-lit variables world/action bindings)
  "Return a function that on every call modifies bindings, the manner
   this is done will depend on the type of gen-lit."
  (cond
   ((fn-value-generator? gen-lit)
    (make-fn-value-generator gen-lit variables world/action bindings))
   ((goal-formp gen-lit)
    (make-goal-generator gen-lit variables world/action bindings))
   (else 
    (let ((index (get-symbol-index (get-operator gen-lit))))
      (cond
       ((null? index)
        (error "Unknown predicate in quantifier ~S" gen-lit))
       ((generator? index)
        (make-computed-generator gen-lit variables world/action bindings))
       ((and (predicate? index) (described? index))
        (make-desc-pred-generator gen-lit variables world/action bindings))
       (else 
        (error "Unknown type of generator-literal ~S" gen-lit)))))))

(define (make-fn-value-generator gen-lit variables world/action bindings)
  "Make a generator that returns a single function value"
  (let* ((value (eval-term (get-fn-lit-gen gen-lit) world/action bindings))
         (first-time #t))
    (lambda ()
        (if first-time
          (begin (set-var! (first variables) value bindings)
                   (set! first-time #f)
                   #t)
          #f))))

(define (make-goal-generator gen-lit variables world/action bindings)
  "Make a generator that is computed in the goal world."
  (make-generator (second gen-lit) variables (get-goal-world) bindings))
    
(define (make-desc-pred-generator gen-lit variables world/action bindings)
  "Make a generator for a described predicate"
  (let* ((index (get-symbol-index (get-operator gen-lit)))
        (args (eval-terms (get-args gen-lit) world/action bindings))
        (tuple '())
        (generator (desc-predicate-generator index world/action)))
    (letrec ((find-next 
	      (lambda ()
		(set! tuple (generator))
		(if tuple 
		    (if (test-tuple)
			(begin (set-bindings) #t)
			(find-next))
		    #f)))
	     (test-tuple 
	      (lambda ()
		(every (lambda (val arg) (if (var? arg) #t (eqv? val arg)))
			tuple 
			args)))
	     (set-bindings 
	      (lambda ()
		(for-each
		 (lambda (val arg)
		   (if (var? arg) (set-var! arg val bindings)))
		 tuple args))))
      (if generator
	  (lambda ()
	    (find-next))
	  #f))))
  

(define (make-computed-generator gen-lit variables world/action bindings)
  "Make a generator that calls a user defined lisp generator. The user
   defined generator must return a list."
  (let* ((fn (get-symbol-eval-object
	      (get-symbol-index (get-operator gen-lit))))
	 (args (eval-terms (get-args gen-lit) world/action bindings))
	 (tuple '())
	 (generator (fn args world/action)))
    (letrec ((next 
	      (lambda ()
		(set! tuple (generator))
		(if tuple
		    (begin (set-bindings) #t)
		    #f)))

             (set-bindings 
	      (lambda ()
		(for-each (lambda (var val) (set-var! var val bindings))
			  variables tuple))))
      (lambda () (next)))))

;;;----------------------------------------------------------------------
;;; Modalities.
;;;----------------------------------------------------------------------

(define (eval-goal args world/action bindings)
  "Evalutate the truth of a goal formula"
  (eval-formula (first args) (get-goal-world) bindings))

(place-operator-eval 'GOAL eval-goal)


;;;----------------------------------------------------------------------
;;; Special Call for side-effects during formula evaluation.
;;; Always returns T! Used by eval-lambda
;;;----------------------------------------------------------------------

(define (eval-call args world/action bindings)
  ((first args) world/action bindings)
  #t)

(place-operator-eval 'CALL eval-call)


;;;----------------------------------------------------------------------
;;; A utility function, not used directly.
;;; EVAL-LAMBDA. Return a list of bindings which satisfy a formula.
;;; This is not an eval-operator. That is we cannot embed a LAMBDA
;;; inside of another formula. But we can eval an arbitary lambda
;;; formula (i.e., formula with free-variables).
;;; The syntax of a lambda-expression, is
;;;
;;; (var-gen-pairs [formula])
;;; var-gen-pairs = (var-gen-pair1 var-gen-pair2 ...)
;;; var-gen-pairi = (vars gen-lit)
;;; vars          = (var1 var2 ....)
;;; gen-lit       = literal.
;;;
;;; Each variable in gen-lit must appear in vars, unless that variable
;;; has already appeared in a previous var-gen-pair. No variable can
;;; appear more than once in the collection of vars taken over all of
;;; the var-gen-pairs.
;;;
;;; formula = arbitrary first order formula all of whose free
;;; variables must be variables in var-gen-pairs. Formula can be missing.
;;;;----------------------------------------------------------------------

(define (eval-lambda lambda-exp world/action bindings)
  "Return a list of all bindings that satisfy the lambda-exp under the
   current set of bindings."
  (let ((count 0)
        (b-list '())
        (formula '())
        (accumulator '())
        (new-bindings '()))
    (letrec ((make-forall-formula
	      (lambda (var-gens)
		(cond
		 ((length=1 var-gens)
		  (list 'FORALL
			(get-l-exp-vars (first var-gens))
			(get-l-exp-gen (first var-gens))
			(if (get-l-exp-formula lambda-exp)
			    (list 'IMPLIES (get-l-exp-formula lambda-exp)
				  (list 'CALL accumulator))
			    (list 'CALL accumulator))))
		 (else (list 'FORALL
			     (get-l-exp-vars (first var-gens))
			     (get-l-exp-gen (first var-gens))
			     (make-forall-formula (rest var-gens))))))))
      
      (for-each (lambda (var-gen)
		  (set! count (+ count (length (get-l-exp-vars var-gen)))))
		(get-l-exp-var-gens lambda-exp))
      (set! accumulator
	    (lambda (world/action bind) 
	      (set! new-bindings '())
	      (do ((i 0 (+ 1 i)))
		  ((>= i count))
		(set! new-bindings
                      (cons (copy-list (first bind)) new-bindings))
		(set! bind (rest bind)))
	      (set! new-bindings (cons b-list new-bindings))))
      (set! formula
	    (make-forall-formula
	     (get-l-exp-var-gens lambda-exp)))
      ;;(format #t "~%~S~%~%" formula)
      (eval-formula formula world/action bindings)
      b-list)))

                
(define (get-l-exp-var-gens l-exp)
  (first l-exp))

(define (get-l-exp-formula l-exp)
  (second l-exp))

(define (get-l-exp-vars var-gen)
  (first var-gen))

(define (get-l-exp-gen var-gen)
  (second var-gen))

(define (length=1 x)
  "Is x a list of length 1?"
  (and (pair? x) (null? (rest x))))

;;;;----------------------------------------------------------------------
;;;;>>>7 Actions
;;;;   The interface between actions and the planner.
;;;;   And structures for holding the various components of an operator.
;;;;   To implement a particular type of action, e.g., STRIPS or ADL
;;;;   actions the routines specified below must be implemented.
;;;;   a) Data structure for opertors.
;;;;   b) *operators* 
;;;;   c) the action structure, readers of the structure.
;;;;   d) Higher level action interface.
;;;;----------------------------------------------------------------------
;;;
;;; (a) Data structure for operators. An operator is an action template,
;;;     i.e., it contains unbound variables.
;;;     Operators are stored in a structure with the following fields.
;;; 
;;;   name
;;;   pre
;;;   add
;;;   del
;;;   update
;;;   duration  ;MTL change.
;;;   cost
;;;   priority
;;;                                                                
;;; * name: a list of the form (symbol var1 ... varn)             
;;;    When var1 ... varn are instantiated this becomes the name of
;;;    the action generated from the operator template.            
;;;    The vari must be among the actions parameters specified when
;;;    matching the preconditions against the current world.       
;;;
;;; * pre: Precondition.
;;; * Add: Adds.        
;;; * Del: Deletes.     
;;; * update: update functions (used by adl-operators only)
;;; * Duration [Optional]: Specify the duration of the action.
;;;       defaults to 1.
;;; * cost [Optional]: Specify cost of action/operator. Can be used
;;;    by search routines that search for optimizing solution in   
;;;    situations where each action has varying costs. Defaults to 1.
;;;                                                                
;;; * priority [Optional]: Specify which actions/operators should
;;;    be explored first. This can be used in search to prioritize the
;;;    successors of a world (e.g., in depth-first search we can      
;;;    achieve a one-step best first)                                 
;;;                                                                   
;;; * eval-object, the function that can be applied to worlds to find
;;;    all successor worlds (if implemented in this manner!).
;;;----------------------------------------------------------------------

(declare (integrate make-operator 
		    operator-name operator-pre operator-add operator-del
		    operator-update operator-duration operator-cost
		    operator-priority operator-eval-object
		    set-operator-name! set-operator-pre!
		    set-operator-add! set-operator-del!
		    set-operator-update! set-operator-duration!
		    set-operator-cost!
		    set-operator-priority! set-operator-eval-object!
		    operator? copy-operator))


;;; Predicate

(define (operator? x)
  (and (vector? x) (= 10 (vector-length x)) (eq? 'operator (vector-ref x 0))))

;;; Constructor
(define (make-operator . keyword-args)
  (let ((name '()) (pre '()) (add '()) (del '())
       (duration 1) (cost 1) (priority 0) (update '()) (eval-object '()))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:name (set! name (cadr keyword-args)))
	(:pre (set! pre (cadr keyword-args)))
	(:add (set! add (cadr keyword-args)))
	(:del (set! del (cadr keyword-args)))
	(:duration (set! duration (cadr keyword-args)))
	(:cost (set! cost (cadr keyword-args)))
	(:priority (set! priority (cadr keyword-args)))
	(:update (set! update (cadr keyword-args)))
	(:eval-object (set! eval-object (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (vector 'operator name pre add del update duration cost priority 
	    eval-object)))

;;; Selectors
(define (operator-name op) (vector-ref op 1))
(define (operator-pre op) (vector-ref op 2))
(define (operator-add op) (vector-ref op 3))
(define (operator-del op) (vector-ref op 4))
(define (operator-update op) (vector-ref op 5))
(define (operator-duration op) (vector-ref op 6))
(define (operator-cost op) (vector-ref op 7))
(define (operator-priority op) (vector-ref op 8))
(define (operator-eval-object op) (vector-ref op 9))

;;; Modifiers
(define (set-operator-name! op val) (vector-set! op 1 val))
(define (set-operator-pre! op val) (vector-set! op 2 val))
(define (set-operator-add! op val) (vector-set! op 3 val))
(define (set-operator-del! op val) (vector-set! op 4 val))
(define (set-operator-update! op val) (vector-set! op 5 val))
(define (set-operator-duration! op val) (vector-set! op 6 val))
(define (set-operator-cost! op val) (vector-set! op 7 val))
(define (set-operator-priority! op val) (vector-set! op 8 val))
(define (set-operator-eval-object! op val) (vector-set! op 9 val))

;;; Copier

(define copy-operator vector-copy)

;;;----------------------------------------------------------------------
;; b) *operators* --- holds list of the current domains operators 
;;    various access functions to *operators*                     
;;;----------------------------------------------------------------------

(define *operators* '())
;;;Complete list of domain's operators

(declare (integrate clear-ops add-op del-op find-op))

(define (clear-ops )
  "Re-initialize list of operators"
  (set! *operators* '()))

(define (add-op op)
  "Add new operator"
  (set! *operators* (cons op *operators*)))

(define (del-op op-name)
  "Remove all operators with op-name (a literal)"
  (set! *operators*
	(remove-if (lambda (op) (unify op-name (operator-name op)))
		   *operators*)))

(define (find-op op-name)
  "Return first operator with name = literal"
  (find op-name *operators*
        :test (lambda (op) (unify op-name (operator-name op)))))

(define (get-names )
  "Return the list of operator names"
  (map (lambda (op) (operator-name op)) *operators*))

;;;----------------------------------------------------------------------
;;; c) The action structure. 
;;;
;;; MTL changes: Define an extended world/action structure.
;;;                                                                 
;;; The planner is passed a list of "world/action" structures, giving 
;;; information 
;;; about all of the worlds reachable from this world via some action, 
;;; i.e., via some instance of an operator. 
;;; Each world/action is a structure containing the new world structure
;;; instantiated name of the action, the action cost, the action priority 
;;; ranking, and the action duration. 
;;;----------------------------------------------------------------------

(declare (integrate make-world/action world/action-world
		    world/action-action-name world/action-action-duration
		    world/action-action-cost world/action-action-priority
		    set-world/action-world!
		    set-world/action-action-name! 
		    set-world/action-action-duration! 
		    set-world/action-action-cost! 
		    set-world/action-action-priority! 
		    ))

;;; Predicate

(define (world/action? x)
  (and (vector? x) (= 6 (vector-length x))
       (eq? 'world/action (vector-ref x 0))))

;;; Constructor

(define (make-world/action world action-name action-duration action-cost
			   action-priority)
  (vector 'world/action
	  world action-name action-duration action-cost action-priority))

;;; Acccessors

(define (world/action-world w/a) (vector-ref w/a 1))
(define (world/action-action-name w/a) (vector-ref w/a 2))
(define (world/action-action-duration w/a) (vector-ref w/a 3))
(define (world/action-action-cost w/a) (vector-ref w/a 4))
(define (world/action-action-priority w/a) (vector-ref w/a 5))

;;; Modifiers

(define (set-world/action-world! w/a val) (vector-set! w/a 1 val))
(define (set-world/action-action-name! w/a val) (vector-set! w/a 2 val))
(define (set-world/action-action-duration! w/a val) (vector-set! w/a 3 val))
(define (set-world/action-action-cost! w/a val) (vector-set! w/a 4 val))
(define (set-world/action-action-priority! w/a val) (vector-set! w/a 5 val))

;;; Copier

(define copy-world/action vector-copy)

;; Print function

(define (print-action world/action . optional-args)
  (let ((stream (if (null? optional-args) 
		    #t
		    (first optional-args))))
    (format stream "~&Action:~%<Name: ~s>"
	    (world/action-action-name world/action))))

;;;----------------------------------------------------------------------
;;; d) Higher level action functionality.                                
;;; Higher level functionality interfaces with functions that         
;;; should be defined in the implementation of the operator type.     
;;; This allows us to deal with STRIPS and ADL style operators  as    
;;; well as making it easy to implement new operator types.           
;;;                                                                   
;;; There is only one interface to a particular operator              
;;; implementation: apply-operator                                    
;;;
;;; This function takes as input an operator and a world, and applies
;;; the operator's eval-object to the world. This eval-object is a
;;; function that should be created by the STRIPS or ADL add-operator
;;; functions. This function should return a list containing all pairs
;;; of new-world/action-names that can be generated from the current
;;; world by applying instances of the operator.
;;;----------------------------------------------------------------------

(define (apply-operator op world/action)
  "Apply operator to world, generating a list of successors:
   all the world generated by instances of the operator
   applicable in the current world. Each instance yields a world/action 
   structure."
  ((operator-eval-object op) world/action))

(define (generate-successors world/action)
  "Return successors of a world applying all applicable actions."
  (do ((successors '())
       (operators *operators*)
       (op '()))
      ((null? operators) successors)
    (set! op (first operators))
    (set! operators (rest operators))
    (set! successors
	  (append! (apply-operator op world/action) successors))))

;;;;----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>8 STRIPS Operators.
;;;;
;;;; Implementation of STRIPS style operators.
;;;; We use the first-order evaluator to implement STRIPS operators.
;;;; To test if an action is applicable in a world we evalutate its
;;;; preconditions on the world, and use the formula evaluator to
;;;; generate all the correct bindings.
;;;; A STRIPS operator consists of
;;;;
;;;;   pre          --- Preconditions, list of literals that may have
;;;;                    variables. 
;;;;   add          --- Add list   
;;;;   del          --- del list
;;;;
;;;;
;;;; We compile the preconditions into a quantified formula
;;;; every instantiation that satisfies the conjunction of the precondtion
;;;; literals calls a function that returns a new world where the
;;;; add and delete lists (using the current satisfying instantiation)
;;;; have been used to modify the old world.
;;;;----------------------------------------------------------------------
;;;
;;; Because of simplicity of STRIPS operators we can add some extra
;;; operator functionality.
;;;;----------------------------------------------------------------------

(define (strips-find-adders literal)
  "Return list of operators that can add literal"
  (remove-if-not (lambda (op) (umatch-list literal (operator-add op))) 
		 *operators*))

(define (strips-find-deleters literal)
  "Return list of operators that can delete literal"
  (remove-if-not (lambda (op) (umatch-list literal (operator-del op))) 
		 *operators*))

(define (strips-find-preconditioners literal)
  "Return list of operators that have literal as precondition"
  (remove-if-not (lambda (op) (umatch-list literal (operator-pre op))) 
		 *operators*))

;;;;----------------------------------------------------------------------
;;; Instantiate the action-interface for strips-operators
;;; The add-strips-op sets up an operator template with a function in
;;; eval-object slot that correctly generates a list of successor
;;; world. This function takes the current world as an argument and
;;; returns a list of all successors than can be
;;; generated from the current world by applying instances of the
;;; operator. 
;;;;----------------------------------------------------------------------

(define (add-strips-op . keyword-args)
  "Compile the operator into a function that can be applied to a world,
   then place it on the list of operators."
  (let ((op '()) 
	(successors '())
	(update-formula '())
	(preconds '())
	(name '()) (pre '((TRUE))) (add '()) (del '())
	(duration 1) (cost 1) (priority 0))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:name (set! name (cadr keyword-args)))
	(:pre (set! pre (cadr keyword-args)))
	(:add (set! add (cadr keyword-args)))
	(:del (set! del (cadr keyword-args)))
	(:duration (set! duration (cadr keyword-args)))
	(:cost (set! cost (cadr keyword-args)))
	(:priority (set! priority (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (set! op (make-operator :name name :pre pre :add add :del del
			    :duration duration
			    :cost cost :priority priority))
    (set! preconds (operator-pre op))
    (let ((vars-remaining (variables-in preconds))
	  (without-variables '())
	  (with-variables '())
	  (modify-world '()))
      (do ((lit '()))
	  ((null? preconds))
	(set! lit (first preconds))
	(set! preconds (rest preconds))
	(if (variable-free? lit)
	    (set! without-variables (cons lit without-variables))
	    (set! with-variables (cons lit with-variables))))
      (set! with-variables (reverse! with-variables))
      
      (set! modify-world
	    (lambda (world/action bindings)
	      ;;(format #t "~%modify world called, bindings:~S" bindings)
	      (let ((new-world (copy-world (world/action-world world/action))))
		
		(do ((literals del)
		     (del-lit '()))
		    ((null? literals))
		  (set! del-lit (first literals))
		  (set! literals (rest literals))
		  ;;(format #t "~%del-lit~S" del-lit)
		  (delete-world-lit (get-operator del-lit)
				    (eval-terms (get-args del-lit) 
						world/action bindings)
				    new-world))
		(do ((literals add)
		     (add-lit '()))
		    ((null? literals))
		  (set! add-lit (first literals))
		  (set! literals (rest literals))
		  ;;(format #t "~%Add-lit~S" add-lit)
		  (add-world-lit (get-operator add-lit)
				 (eval-terms (get-args add-lit) 
					     world/action bindings)
				 new-world))
		;;(format #t "~%name~S  ~S" name bindings)
		(set! successors 
		      (cons (make-world/action 
			     new-world
			     (cons (get-operator name)
				   (eval-terms (get-args name) 
					       world/action bindings))
			     (eval-term duration world/action bindings)
			     (eval-term cost world/action bindings)
			     priority)
			    successors)))))
      
      (letrec ((make-forall 
		(lambda (lits)
		  (cond
		   ((null? vars-remaining)
		    (if (null? lits)
			`(CALL ,modify-world)
			(list 'IMPLIES
			      (if (length=1 lits)
				  (first lits)
				  `(AND ,@lits))
			      `(CALL ,modify-world))))
		   (else 
		    (let ((new-vars
			   (intersection vars-remaining 
					 (variables-in (first lits)))))
		      (set! vars-remaining
			    (set-difference vars-remaining new-vars))
		      (if (not (null? new-vars))
			  `(FORALL ,new-vars ,(first lits) ,(make-forall (rest lits)))
			  `(AND ,(first lits) ,(make-forall (rest lits))))))))))
	
	(set! update-formula
	      (if without-variables
		  `(AND ,@without-variables 
			,(make-forall with-variables))
		  (make-forall with-variables)))))
    
    (if *verbose*
        (begin
	  (format *trace-stream*
		  "~%STRIPS operator ~S compiled into formula:" name)
	  (format #t "~%~S~%~%" update-formula)))
    (set-operator-eval-object! op
			       (lambda (world/action)
				 (set! successors '())
				 (eval-formula update-formula world/action '())
				 successors))
    (add-op op)))

;;;;----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>9 ADL Operators
;;;;
;;;; Implementation of ADL Operators. Like STRIPS this ADL operators are
;;;; implemented using the first order evaluator.
;;;;
;;;; ADL operators are stored in the standard operator structure.
;;;  But the preconditions, add and delete lists    
;;; and update lists  have a special structure.                          
;;;                                                                      
;;; a. pre: Preconditions. This is a list with the following syntax.     
;;;                                                                      
;;; (var-gen-pairs [formula])
;;; var-gen-pairs = (var-gen-pair1 var-gen-pair2 ...)
;;; var-gen-pairi = (vars gen-lit)
;;; vars          = (var1 var2 ....)
;;; gen-lit       = generator literal.
;;;
;;; Each variable in gen-lit must appear in vars, unless that variable
;;; has already appeared in a previous var-gen-pair. No variable can
;;; appear more than once in the collection of vars taken over all of
;;; the var-gen-pairs.
;;; var-gen-pairs can be the empty list.
;;;
;;; formula = arbitrary first order formula all of whose free
;;; variables must be variables in var-gen-pairs. 
;;;
;;;                                                                      
;;;    A precondition specifies a lambda expression over the variables   
;;;    mentioned in the variable generators. Each binding of the         
;;;    variables that satifies "formula" in the current world is an      
;;;    action-instance of this operator schema that can be applied in    
;;;    this world. If formula is missing it is taken to be the formula
;;;    TRUE. If var-gen-pairs is the empty list then formula must be a
;;;    sentence, i.e., contain no free variables. In particular if
;;;    var-gen-pairs is the empty list and formula is missing the
;;;    action corresponds to one that is always applicable. 
;;;                                                                      
;;; b. Add: This is a list with the following syntax.                    
;;;                                                                      
;;;    add             ==> (list-of-adds)
;;;    list-of-adds    ==> (add-condition1 ... add-conditionK)
;;;    add-conditioni  ==> (var-gen-pairs [formula] pos-literal)
;;;                                                                      
;;;    var-gen-pairs   ==> A list of variable generators as above.
;;;                        may be the empty list.
;;;                                                                      
;;;    formula              ==> First order formula whose free           
;;;                             variables have appeared in variable
;;;                             generators either in the preconditions
;;;                             or in this specific add-condition.
;;;                             If missing it is taken to be the
;;;                             formula TRUE.
;;;                                                                      
;;;    pos-literal         ==>  (Predicate t1 ... tm)                    
;;;    Predicate           ==>  Described predicate symbol.
;;;    ti                  ==>  a term that can have free variables.     
;;;                             All of the free variables must be        
;;;                             either action parameters or mentioned    
;;;                             in one of the variable generators of     
;;;                             the add condition. The terms can also
;;;                             have function applications. But on
;;;                             update those function applications are
;;;                             evaluated in the current world not the
;;;                             updated world.   
;;;                                                                      
;;;    The different add conditions can have identical variables in      
;;;    their variable generators...the conditions are evaluated          
;;;    separately, but in conjunction with the precondition so if they
;;;    are identical to the variables in the preconditions they will
;;;    have the effect of masking those variables. (In the standard
;;;    way that this occurs in first-order formula, e.g.
;;;    \forall x. ontable(x) ==> \exists x. on(x,x).
;;;    Both x's in the formula on(x,x) are bound by the \exists
;;;    quantifier, and the \forall quantifier's x is masked out.
;;;                                                                      
;;;   An add condition specifies a lambda expression. All of the         
;;;   instantiations of the variables in the variable generators that    
;;;   satisfy "formula" in the current world (this formula may also      
;;;   depend on the binding generated in matching the preconditions)
;;;   specify an instantiation of the "pos-literal" that is added to
;;;   the world description. 
;;;                                                                      
;;; c. Del: Identical, except that the delete conditions specify (in     
;;;    an identical manner to the add conditions) instantiations of      
;;;    positive literals that are to be deleted from the current world   
;;;    description.                                                      
;;;                                                                      
;;; d. update: Like the delete and add conditions this is a list of      
;;;    function update conditions. Each is identical in form to the      
;;;    add/del conditions except that the "pos-literal" component is     
;;;    replaced by a list of the form                                    
;;;       (=( fn t1 ... tm) v) 
;;;    where the ti are terms evaluated in the current world. The
;;;    function "fn" is updated so that in the new world it evaluates
;;;    to v (another term like the ti) on the argument vector
;;;    <t1...tm>. Note that all terms are evaluated, so they can
;;;    include function applications which will be evaluated in the
;;;    current world (not the updated world).
;;;----------------------------------------------------------------------
;;; Instantiate the action-interface for adl-operaators.
;;;
;;; Adl actions contain conditions for which all matching bindings
;;; must be found---each matching binding generates a ground predicate
;;; that is added or deleted. Similarily we can update function
;;; values. 
;;;----------------------------------------------------------------------
;;;  Readers of adl components.
;;;

(define (adl-pre-var-gens pre)
  "Get the variable generators of precondition"
  (first pre))

(define (adl-pre-formula pre)
  "Get the precondition formula"
  (second pre))

(define (adl-get-vars var-gen-pair)
  "Get the list of variables from a var-generator pair"
  (first var-gen-pair))

(define (adl-get-gen var-gen-pair)
  "Get the generator literal from a var-generator pair"
  (second var-gen-pair))

(define (adl-mod-var-gens mod-condition)
  "Get the list of var-gens from a modifier condition (add/delete/update)."
  (first mod-condition))

(define (adl-mod-literal mod-condition)
  "Get the positive literal from a modifier (add/delete/update) condition."
  (first (last mod-condition)))

(define (adl-mod-has-formula? mod-condition)
  "Test if the modifier (add/delete/update) condition has a
   formula."
  (= 3 (length mod-condition)))

(define (adl-mod-formula mod-condition)
  "Return the modifier (add/delete/update) condition formula."
  (if (adl-mod-has-formula? mod-condition)
      (second mod-condition)
    '()))

;;;----------------------------------------------------------------------
;;; Instantiate the action-interface for adl-operators            
;;; The add-adl-op sets up an operator template with a function in
;;; eval-object slot that correctly generates a list of successor
;;; world. This function takes the current world as an argument and
;;; returns a list of all successors than can be
;;; generated from the current world by applying instances of the
;;; operator. 
;;;----------------------------------------------------------------------

(define (add-adl-op . keyword-args)
  "Compile an adl operator into a function that can be applied to a
   world, then place the opertor structure on the list of operators."
  (let ((op '())
        (modifier-formulas '())
        (update-form '())
        (new-world '())
        (call-fn '())
        (name-op '())
        (name-args '())
        (successors '())
	(name '()) (pre '(())) (add '()) (del '())
	(duration 1) (cost 1) (priority 0) (update '()))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:name (set! name (cadr keyword-args)))
	(:pre (set! pre (cadr keyword-args)))
	(:add (set! add (cadr keyword-args)))
	(:del (set! del (cadr keyword-args)))
	(:duration (set! duration (cadr keyword-args)))
	(:cost (set! cost (cadr keyword-args)))
	(:priority (set! priority (cadr keyword-args)))
	(:update (set! update (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (set! op (make-operator :name name :pre pre :add add :del del
			    :duration duration :update update
			    :cost cost :priority priority))
    (set! name-op (get-operator name))
    (set! name-args (get-args name))
;;;
;;; First construct the modifier formula. This formula will be
;;; evaluated if the precondition formula succeeds.
;;; The modifier formula is an AND formula whose last conjunct is a
;;; CALL that pushes the new world onto the list of new worlds along
;;; with the world name.
;;;    
    (set! call-fn
      (lambda (world/action bindings)
	(set! successors
	      (cons (make-world/action
		     new-world
		     (cons name-op (eval-terms name-args 
					       world/action bindings))
		     (eval-term duration world/action bindings)
		     (eval-term cost world/action bindings)
		     priority)
		    successors))))
;;;          (format #t "~Pushing new world, computed via action")
    (set! modifier-formulas (cons `(CALL ,call-fn) modifier-formulas))
;;;
;;; The middle conjuncts are formulas that do conditional updates to
;;; the new world, depending on the type of condition
;;; (add/delete/update). 
;;;    
    (for-each 
     (lambda (type)
       (let ((conditions (if (eq? type 'del) del add)))
	 (for-each
	  (lambda (condition)
	    (let* ((mod-literal (adl-mod-literal condition))
		   (mod-operator (get-operator mod-literal))
		   (mod-args (get-args mod-literal))
		   (update-formula '()))
	      (set! call-fn
		    (if (eq? type 'del)
			(lambda (world/action bindings)
			  (delete-world-lit
			   mod-operator (eval-terms mod-args world/action 
						    bindings)
			   new-world))
			(lambda (world/action bindings)
			  (add-world-lit
			   mod-operator (eval-terms mod-args world/action 
						    bindings)
			   new-world))))
	      (set! update-formula
		    (adl-compile-lambda (adl-mod-var-gens condition)
					(adl-mod-formula condition)
					`(CALL ,call-fn)))
	      (set! modifier-formulas (cons update-formula 
					    modifier-formulas))))
	  conditions)))
     '(add del))  ;Do Deletes prior to adds!
    
    (for-each 
     (lambda (conditions)
       (for-each 
	(lambda (condition)
	  (let* ((mod-literal (adl-mod-literal condition))
		 (mod-operator (get-fn-name mod-literal))
		 (mod-args     (get-fn-args mod-literal))
		 (mod-value    (get-fn-value mod-literal))
		 (update-formula '()))
	    (set! call-fn
		  (lambda (world/action bindings)
		    (update-world-fn
		     mod-operator (eval-terms mod-args world/action bindings)
		     (eval-term mod-value world/action bindings) new-world)))
	    (set! update-formula
		  (adl-compile-lambda (adl-mod-var-gens condition)
				      (adl-mod-formula condition)
				      `(CALL ,call-fn)))
	    (set! modifier-formulas (cons update-formula modifier-formulas))))
	conditions))
     update)
;;;    
;;; Finally the first conjunct creates a new world. This world is only
;;; created if the preconditions succeed.
;;;    
    (set! call-fn
	  (lambda (world/action bindings)
	    (set! new-world (copy-world (world/action-world world/action)))))
    (set! modifier-formulas (cons `(CALL ,call-fn) modifier-formulas))
    (set! modifier-formulas (cons 'AND modifier-formulas))
;;;
;;; The final formula to be evaluated is an implication that starts
;;; with an evaluation of the preconditions.
;;;    
    (set! update-form
      (adl-compile-lambda (adl-pre-var-gens pre)
                          (adl-pre-formula pre)
                          modifier-formulas))
;;;
;;; Print out the formula for information.
;;;    
    (if *verbose*
        (begin
          (format #t "~%ADL ~S operator compiled into formula:" name)
          (format #t  "~%~S~%~%" update-form)))
;;;
;;; The actual function that updates the world evaluates the update
;;; formula and then returns the list of updated worlds.
;;;    
    (set-operator-eval-object! op
			       (lambda (world/action)
				 (set! successors '())
				 (eval-formula update-form world/action '())
				 successors))
    (add-op op)))
                                          
(define (adl-compile-lambda var-gens formula final-form)
  "Generate a forall formula which evals final-form for every variable
   binding that satisfies (var-gens formula)"
  ;;
  ;;special optimizations possible when we have and formula
  ;;Call special subroutine for this case.
  ;;
  (cond
   ((and formula (or (and-formp formula) (atomic-formp formula)))
    (adl-compile-and-lambda var-gens formula final-form))
   (else 
    (adl-compile-others-lambda var-gens formula final-form))))

(define (adl-compile-others-lambda var-gens formula final-form)
  "Generate a forall formula for a formula other than an and formula."
  (cond
   ((and (null? var-gens) (null? formula))
    final-form)
   ((null? var-gens)
    (list 'IMPLIES formula final-form))
   (else 
    `(FORALL ,(adl-get-vars (first var-gens))
             ,(adl-get-gen (first var-gens))
             ,(adl-compile-others-lambda
               (rest var-gens) formula final-form)))))

;;; And formulas should have conjuncts move up to the place where the
;;; variables are first generated. E.g., if we have the var-gens
;;; (((?x) (R ?x)) ((?y) (Q ?x ?y))
;;; and the formula
;;; (and (P ?x) (A ?x ?y))
;;; we want to generate
;;; (FORALL (?x) (R ?x)
;;;     (implies (P ?x) (FORALL (?y) (Q ?x ?y) (A ?x ?y))))
;;;
;;; adl-compile-others-lambda would generate the followin less efficient to
;;; evaluate formula:
;;; (FORALL (?x) (R ?x) (FORALL (?y) (Q ?x ?y) (and (P ?x) (A ?x ?y))))
;;;
;;; The formula generated by adl-compile-and-lambda is logically
;;; equivalent (of course).
;;;
;;;

(define (adl-compile-and-lambda var-gens formula final-form)
  "Generate a forall formula for an and or an atomic formula."
  (let ((conjuncts '())
        (sentences '())
        (recursive-form '())
        (var-gen-forms '()))
    (set! conjuncts (if (and-formp formula)
                        (get-args formula)
                      (list formula)))  ;handle atomic as single argument and
    (set! var-gen-forms
      (reverse (map
                (lambda (var-gen) (list var-gen '()))
                var-gens)))
    (for-each 
     (lambda (conj)
       (let ((vars (find-free-vars conj))
	     (outer #t))
	 (if (null? vars)
	     (set! sentences (cons conj sentences))
	     (begin
	       (call-with-current-continuation
		(lambda (return)
		  (for-each 
		   (lambda (var-gen-form)
		     (if (not (null? (intersection 
				      vars 
				      (adl-get-vars (first var-gen-form)))))
			 (begin
			   (set-car! (rest var-gen-form)
				     (cons conj (cadr var-gen-form)))
			   (set! outer '())
			   (return #t))))
		   var-gen-forms)))
	       (if outer (set! sentences (cons conj sentences)))))))
     conjuncts)
    (set! var-gen-forms (reverse var-gen-forms))
    (for-each (lambda (var-gen-form)
                (set-car! (rest var-gen-form)
			  (reverse (second var-gen-form))))
	      var-gen-forms)
    (set! recursive-form (adl-compile-and-recurse var-gen-forms final-form))
    (cond
     ((and sentences recursive-form (length=1 sentences))
      `(IMPLIES ,@sentences ,recursive-form))
     ((and sentences recursive-form)
      `(IMPLIES (AND ,@sentences) ,recursive-form))
     (else 
      recursive-form))))
     

(define (adl-compile-and-recurse var-gen-forms final-form)
  "Formulas have been placed in their correct place, now build formula."
  (let ((var-gen-form (first var-gen-forms)))
    (cond
     ((null? var-gen-form)
      final-form)
     ((null? (second var-gen-form))     ;No formula, just generator.
      `(FORALL ,(adl-get-vars (first var-gen-form))
               ,(adl-get-gen (first var-gen-form))
               ,(adl-compile-and-recurse (rest var-gen-forms) final-form)))
     (else                                 ;Formula.
      `(FORALL ,(adl-get-vars (first var-gen-form))
               ,(adl-get-gen (first var-gen-form))
               (IMPLIES
                ,(if (length=1 (second var-gen-form))
                     (first (second var-gen-form))
                   (cons 'AND (second var-gen-form)))
                ,(adl-compile-and-recurse
                  (rest var-gen-forms) final-form)))))))
                     
;;;----------------------------------------------------------------------
;;; Some interface functions to permit easy in specifying ADL actions.
;;;----------------------------------------------------------------------

(define (adl-pre . keyword-args)
  (let ((var-gens '())
	(form '()))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:var-gens (set! var-gens (cadr keyword-args)))
	(:form (set! form (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (if form
	(list (adl-var-gens var-gens) form)
	(list (adl-var-gens var-gens)))))

(define (adl-add . conditions)
  conditions)

(define (adl-del . conditions)
  conditions)

(define (adl-update . conditions)
  conditions)

(define (adl-cond . keyword-args)
  (let ((var-gens '())
	(form '())
	(lit '()))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:var-gens (set! var-gens (cadr keyword-args)))
	(:form (set! form (cadr keyword-args)))
	(:lit (set! lit (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (if form
	(list (adl-var-gens var-gens) form lit)
	(list (adl-var-gens var-gens) lit))))

(define (adl-var-gens var-gen-list)
  (if (not (even? (length var-gen-list)))
      (error "~%Illegal variable generator: not collection of pairs~
              ~%~S" var-gen-list))
  (let ((var-gens '()))
    (letrec ((recur 
	      (lambda (lst)
		(if lst
		    (begin 
		      (set! var-gens (cons (list (first lst) (second lst)) 
					   var-gens))
		      (recur (rest (rest lst))))))))
      (recur var-gen-list)
      (reverse var-gens))))

;;;;----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>10 Temporal Progressor. The heart of the TLPlan technique.
;;;;
;;;; Functions that manage temporal formulas expressed in LTL
;;;;----------------------------------------------------------------------

(define progress-eval-table '())
;;Table of functions for progressing various types of operators

(define (lookup-progress-eval operator)
  (let((x (assoc operator progress-eval-table)))
    (if x (rest x) '())))

(define (place-progress-eval operator eval-fn)
  (set! progress-eval-table (acons operator eval-fn progress-eval-table)))

(define (replace-progress-eval operator eval-fn)
  (let ((cell (assoc operator progress-eval-table)))
    (set-cdr! cell eval-fn)))

;;;----------------------------------------------------------------------
;;; Progress-formula takes advantage of the fact that progression of
;;; atomic formulas is identical to evaluating them. So it calls the
;;; evaluator.
;;;----------------------------------------------------------------------

(define (progress-formula form world/action bindings)
  "Top level progress evaluator, dispatch on non-atomic formulas."
  (if (or (eq? form #t) (eq? form #f))
      form
    (let ((dispatch-fn (lookup-progress-eval (get-operator form))))
      (if dispatch-fn
          (dispatch-fn form world/action bindings)
        (eval-atomic (get-operator form)
                     (eval-terms (get-args form) world/action bindings)
                   world/action)))))

;;;----------------------------------------------------------------------
;;; Dispatched operators.
;;;----------------------------------------------------------------------
;;; Booleans
;;;----------------------------------------------------------------------

(define (progress-and form world/action bindings)
  "Progress an and-formula checking for true/false and compressing same
   level ands."
  (let ((new-subforms '())
        (new-subform #f)
        (make-new #f)
	(false? #f))
    (do ((subforms (get-args form))
	 (subform '()))
	((or (null? subforms) false?))
      (set! subform (first subforms))
      (set! subforms (rest subforms))
      (set! new-subform (progress-formula subform world/action bindings))
      (cond ((not new-subform)
             (set! new-subforms '())
             (set! false? #t))
            ((eq? new-subform #t)
             (set! make-new #t))
            ((eq? new-subform subform)
             (set! new-subforms (cons subform new-subforms)))
            ((and-formp new-subform)
             (set! make-new #t)
             (set! new-subforms (append (get-args new-subform) new-subforms)))
            (else 
             (set! make-new #t)
             (set! new-subforms (cons new-subform new-subforms)))))
    
    (cond (false? #f)
	  ((null? new-subforms) #t)
          ((not make-new) form)
          ((length=1 new-subforms) (first new-subforms))
          (else (make-and-form new-subforms)))))


(define (progress-or form world/action bindings)
  "Progress an or-formula checking for true/false and compressing same
   level ors." 
  (let ((new-subforms '())
        (new-subform '())
        (make-new '())
	(true? #f))
    (do ((subforms (get-args form))
	 (subform '()))
	((or (null? subforms) true?))
      (set! subform (first subforms))
      (set! subforms (rest subforms))
      (set! new-subform (progress-formula subform world/action bindings))
      (cond ((eq? #t new-subform)
             (set! new-subforms '())
             (set! true? #t))
            ((not new-subform)
             (set! make-new #t))
            ((eq? new-subform subform)
             (set! new-subforms (cons subform new-subforms)))
            ((or-formp new-subform)
             (set! make-new #t)
            (set! new-subforms (append (get-args new-subform) new-subforms)))
            (else 
             (set! make-new #t)
             (set! new-subforms (cons new-subform new-subforms)))))
    
    (cond (true? #t)
	  ((null? new-subforms) #f)
          ((not make-new) form)
          ((length=1 new-subforms) (first new-subforms))
          (else (make-or-form new-subforms)))))

(define (progress-xor form world/action bindings)
  "Progress an xor-formula checking for true/false and compressing same
   level xors."
  (let ((new-subforms '())
        (new-subform '())
        (make-new '())
        (found-one? '())
	(false? #f))
    (do ((subforms (get-args form))
	 (subform '()))
	((or (null? subforms) false?))
      (set! subform (first subforms))
      (set! subforms (rest subforms))
      (set! new-subform (progress-formula subform world/action bindings))
      (cond ((and (eq? #t new-subform) found-one?)
             (set! new-subforms '())
             (set! false? #t))
            ((eq? #t new-subform)
             (set! found-one? #t))
            ((not new-subform)
             (set! make-new #t))
            ((eq? new-subform subform)
             (set! new-subforms (cons subform new-subforms)))
            ((xor-formp new-subform)
             (set! make-new #t)
             (set! new-subforms (append (get-args new-subform) new-subforms)))
            (else 
             (set! make-new #t)
             (set! new-subforms (cons new-subform new-subforms)))))
    
    (cond ((or (null? new-subforms) false?) 
	   #f)
          ((and found-one? (length=1 new-subforms))
           (make-not-form new-subforms))
          (found-one?
           (make-not-form (make-or-form new-subforms)))
          ((not make-new)
           form)
          ((length=1 new-subforms)
           (first new-subforms))
          (else (make-xor-form new-subforms)))))

(define (progress-implies form world/action bindings)
  "Progress an implies-formula checking for true/false."
  (let* ((subforms (get-args form))
         (new-arg1 (progress-formula (first subforms) world/action bindings)))
    (if (not new-arg1)
        #t
	(let ((new-arg2 (progress-formula (second subforms) 
					  world/action bindings)))
	  (cond ((eq? #t new-arg2)
		 #t)
		((eq? #t new-arg1)
		 new-arg2)
		((not new-arg2)
		 (make-not-form new-arg1))
		((and (eq? new-arg1 (first subforms))
		      (eq? new-arg2 (second subforms)))
		 form)
		(else 
		 (make-implies-form new-arg1 new-arg2)))))))

(define (progress-if-then-else form world/action bindings)
  "Progress an if-then-else formula checking for true/false."
  (let* ((subforms (get-args form))
         (arg1 (first subforms))
         (arg2 (second subforms))
         (arg3 (third subforms))
         (new-arg1 (progress-formula arg1 world/action bindings))
         (new-arg2 #f)
	 (new-arg3 #f))
    (cond
     ((eq? new-arg1 #t) (progress-formula arg2 world/action bindings))
     ((not new-arg1) (progress-formula arg3 world/action bindings))
     (else 
      (set! new-arg2 (progress-formula arg2 world/action bindings))
      (set! new-arg3 (progress-formula arg3 world/action bindings))
      (cond
       ((eq? new-arg2 #t)
        (if (eq? new-arg3 #t)
            #t
	    (if (not new-arg3)
		new-arg1
		(make-implies-form (make-not-form new-arg1) new-arg3))))
       ((not new-arg2)
        (if (eq? new-arg3 #t)
            (make-not-form new-arg1)
	    (if (not new-arg3)
		#f
		(make-and-form (list (make-not-form new-arg1) new-arg3)))))
       (else 
        (if (eq? new-arg3 #t)
            (make-implies-form new-arg1 new-arg2)
	    (if (not new-arg3)
		(make-and-form (list new-arg1 new-arg2))
		(if (and (eq? new-arg1 arg1) 
			 (eq? new-arg2 arg2) 
			 (eq? new-arg3 arg3))
		    form
		    (make-if-then-else-form 
		     new-arg1 new-arg2 new-arg3))))))))))

(define (progress-not form world/action bindings)
  "Progress a not-formula checking for true/false."
  (let* ((subform (first (get-args form)))
         (new-subform (progress-formula subform world/action bindings)))
    (cond ((not new-subform) #t)
          ((eq? #t new-subform) #f)
          ((eq? new-subform subform) form)
          (else (make-not-form new-subform)))))


(define (progress-= form world/action bindings)
  "Progress an = formula."
  (eval-= (get-args form) world/action bindings))

(define (progress-false form world/action bindings)
  #f)

(define (progress-true form world/action bindings)
  #t)

(for-each place-progress-eval
	  '(AND OR XOR
		IMPLIES IF-THEN-ELSE NOT
		TRUE FALSE =)
	  (list progress-and progress-or progress-xor
		progress-implies progress-if-then-else progress-not
		progress-true progress-false progress-=))


;;;----------------------------------------------------------------------
;;; Temporal modalities.
;;;----------------------------------------------------------------------

(define (progress-next form world/action bindings)
  "Progress a NEXT modality."
  (first (get-args form)))

(define (progress-eventually form world/action bindings)
  "Progress an EVENTUALLY modality."
  (let ((progressed-form
         (progress-formula (first (get-args form)) world/action bindings)))
    (cond ((not progressed-form) form)
          ((eq? progressed-form #t) #t)
          ((or-formp progressed-form) 
           (make-or-form (append (get-args progressed-form) (list form))))
          (else (make-or-form (list progressed-form form))))))

(define (progress-always form world/action bindings)
  "Progress an ALWAYS modality."
  (let ((progressed-form
         (progress-formula (first (get-args form)) world/action bindings)))
    (cond ((eq? progressed-form #t) form)
          ((not progressed-form) #f)
          ((and-formp progressed-form)
           (make-and-form (append (get-args progressed-form) (list form))))
          (else (make-and-form (list progressed-form form))))))

(define (progress-until form world/action bindings)
  "Progress an UNTIL modality of the form (condition UNTIL achievement)"
  (let ((progressed-achievement
         (progress-formula (second (get-args form)) world/action bindings)))
    (if (eq? progressed-achievement #t)
        #t
	(let ((progressed-condition
	       (progress-formula (first (get-args form)) 
				 world/action bindings)))
	  (set! progressed-condition
		(cond ((not progressed-condition) #f)
		      ((eq? progressed-condition #t) form)
		      ((and-formp progressed-condition)
		       (make-and-form
			(append (get-args progressed-condition) (list form))))
		      (else (make-and-form (list progressed-condition form)))))
	  (cond ((not progressed-achievement) progressed-condition)
		((not progressed-condition) progressed-achievement)
		((or-formp progressed-achievement)
		 (make-or-form (cons progressed-condition 
				     (get-args progressed-achievement))))
		(else (make-or-form (list progressed-achievement
					  progressed-condition))))))))

(for-each place-progress-eval
        '(NEXT EVENTUALLY ALWAYS UNTIL)
        (list progress-next progress-eventually progress-always
              progress-until))


;;;----------------------------------------------------------------------
;;; MTL timed modalities.
;;;----------------------------------------------------------------------

(define (progress-t-until form world/action bindings)
  "Progress a timed UNTIL modality of the form (condition UNTIL achievement)"
  (let ((ispec (get-bf-ispec form))
        (forms (get-bf-formulas form))
        (shifted-form (make-delta-form form)))
    (cond
     ((ispec<0  ispec) #f) ;timed out
     ((ispec0in ispec)
      (let ((progressed-achievement
             (progress-formula (second forms) world/action bindings)))
        (if (eq? progressed-achievement #t)
            #t
	    (let ((progressed-condition
		   (progress-formula (first forms) world/action bindings)))
	      (set! progressed-condition
		    (cond
		     ((not progressed-condition) #f)
		     ((eq? progressed-condition #t) shifted-form)
		     ((and-formp progressed-condition)
		      (make-and-form
		       (append (get-args progressed-condition) 
			       (list shifted-form))))
		     (else (make-and-form 
			    (list progressed-condition shifted-form)))))
	      (cond 
	       ((not progressed-achievement) progressed-condition)
	       ((not progressed-condition) progressed-achievement)
	       ((or-formp progressed-achievement)
		(make-or-form
		 (cons progressed-condition 
		       (get-args progressed-achievement))))
	       (else (make-or-form (list progressed-achievement
					 progressed-condition))))))))
     (else (let ((progressed-condition
		  (progress-formula (first forms) world/action bindings)))
	     (set! progressed-condition
		   (cond
		    ((not progressed-condition) #f)
		    ((eq? progressed-condition #t) shifted-form)
		    ((and-formp progressed-condition)
		     (make-and-form
		      (append (get-args progressed-condition) 
			      (list shifted-form))))
		    (else (make-and-form 
			   (list progressed-condition shifted-form))))))))))


(define (progress-t-eventually form world/action bindings)
  "Progress a timed EVENTUALLY modality."
  (let ((ispec (get-bf-ispec form))
        (forms (get-bf-formulas form))
        (shifted-form (make-delta-form form)))
    (cond
     ((ispec<0  ispec) #f) ;timed out
     ((ispec0in ispec)
      (let ((progressed-form
             (progress-formula (first forms) world/action bindings)))
        (cond
         ((not progressed-form) shifted-form)
         ((eq? progressed-form #t) #t)
         ((or-formp progressed-form)
          (make-or-form (append (get-args progressed-form)
                                (list shifted-form))))
         (else (make-or-form (list progressed-form shifted-form))))))
     (else shifted-form))))

(define (progress-t-always form world/action bindings)
  "Progress a timed ALWAYS modality."
  (let ((ispec (get-bf-ispec form))
        (forms (get-bf-formulas form))
        (shifted-form (make-delta-form form)))
    (cond
     ((ispec<0 ispec) #t) ;timed out
     ((ispec0in ispec)
      (let ((progressed-form
             (progress-formula (first forms) world/action bindings)))
        (cond
         ((eq? progressed-form #t) shifted-form)
         ((not progressed-form) #f)
         ((and-formp progressed-form)
          (make-and-form (append (get-args progressed-form)
                                 (list shifted-form))))
	 (else (make-and-form (list progressed-form shifted-form))))))
     (else shifted-form))))

(define (progress-delta form world/action bindings)
  "Progress a delta formula. This involves building a shifted formula
   and then progressing that."
  (let* ((formula (get-delta-formula form))
         (ispec (get-bf-ispec formula))
         (shifted-form
          (append  (list
                    (get-operator formula)
                    (ispec-lshift
                     ispec
                     (world/action-action-duration world/action)))
                   (get-bf-formulas formula))))
         (progress-formula shifted-form world/action bindings)))


(for-each place-progress-eval
        '(T-UNTIL T-EVENTUALLY T-ALWAYS DELTA)
        (list progress-t-until progress-t-eventually
              progress-t-always progress-delta))


;;;----------------------------------------------------------------------
;;; Quantifiers. Relies on parts of the evaluator code. 
;;;----------------------------------------------------------------------
          
(define (progress-forall form world/action bindings)
  "Progress a forall quantifier, by reducing to instances"
  (let* ((args (get-args form))
         (qf-vars (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (qf-form   (get-qf-formula args))
         (generator '())
	 (false? #f)
         (progressed-form #f)
         (new-subforms '()))
    (set! bindings (extend-bindings qf-vars qf-vars bindings))
    (set! generator (make-generator gen-lit qf-vars world/action bindings))
    (if generator
        (do ((finish? #f))
	    (finish? #f)
          (cond
           ((generator)
            (set! progressed-form 
		  (progress-formula qf-form world/action bindings))
            (cond ((eq? progressed-form #t))
                  ((not progressed-form)
                   (set! finish? #t)
		   (set! false? #t)
		   (set! new-subforms '()))
                  (else (set! new-subforms
			      (cons
			       (make-binding-form
				qf-vars (eval-terms qf-vars 
						    world/action bindings)
				progressed-form)
			       new-subforms)))))
           (else 
            (set! finish? #t)))))

    (cond (false? #f)
	  ((null? new-subforms) #t)
          ((length=1 new-subforms) (first new-subforms))
          (else (make-and-form new-subforms)))))

(define (progress-exists form world/action bindings)
  "Progress an exists quantifier, by reducing to instances"
  (let* ((args (get-args form))
         (qf-vars (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (qf-form   (get-qf-formula args))
         (generator '())
	 (true? #f)
         (progressed-form #f)
         (new-subforms '()))
    (set! bindings (extend-bindings qf-vars qf-vars bindings))
    (set! generator (make-generator gen-lit qf-vars world/action bindings))
    (if generator
        (do ((finish? #f))
             (finish? #f)
          (cond
           ((generator)
            (set! progressed-form 
		  (if (not qf-form) 
		      #t
		      (progress-formula qf-form world/action bindings)))
            (cond ((eq? progressed-form #t)
                   (set! finish? #t)
		   (set! true? #t)
		   (set! new-subforms '()))
                  ((not progressed-form))
                  (else (set! new-subforms 
			      (cons 
			       (make-binding-form 
				qf-vars (eval-terms qf-vars 
						    world/action bindings)
				progressed-form)
			       new-subforms)))))
           (else (set! finish? #t)))))
    
    (cond (true? #t)
	  ((null? new-subforms) #f)
          ((length=1 new-subforms) (first new-subforms))
          (else (make-or-form new-subforms)))))

(define (progress-exists! form world/action bindings)
  "Progress an exists! quantifier, by reducing to instances"
  (let* ((args (get-args form))
         (qf-vars (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (qf-form   (get-qf-formula args))
         (generator '())
	 (false? #f)
         (progressed-form #f)
         (new-subforms '())
         (found-one? #f))
    (set! bindings (extend-bindings qf-vars qf-vars bindings))
    (set! generator
      (make-generator gen-lit qf-vars world/action bindings))
    (if generator
        (do ((finish? #f))
             (finish? #f)
          (cond
           ((generator)
            (set! progressed-form 
              (if (not qf-form) 
		  #t
		  (progress-formula qf-form world/action bindings)))
            (cond ((and (eq? progressed-form #t) found-one?)
                   (set! finish? #t)
		   (set! false? #t)
		   (set! new-subforms '()))
                  ((eq? progressed-form #t)
                   (set! found-one? #t))
                  ((not progressed-form))
                  (else (set! new-subforms
			      (cons (make-binding-form 
				     qf-vars (eval-terms qf-vars 
							 world/action bindings)
				     progressed-form)
				    new-subforms)))))
           (else 
            (set! finish? #t)))))
    (cond (false? #f)
	  ((null? new-subforms) (if found-one? #t #f))
	  ((and found-one? (length=1 new-subforms))
	   (make-not-form new-subforms))
	  (found-one? (make-not-form (make-or-form new-subforms)))
	  ((length=1 new-subforms)
	   (first new-subforms))
	  (else (make-xor-form new-subforms)))))


(define (progress-binding form world/action bindings)
  "Progress a binding node, by extending the current bindings. Also if
   internal formula is not #t or #f preserve the bindings but reset
   the formula to be the progressed formula."
  (let ((progressed-form #f))
    (set! progressed-form
	  (progress-formula
	   (get-binding-formula form) world/action
	   (extend-bindings (get-binding-vars form)
			    (get-binding-vals form)
			    bindings)))
    (cond
     ((or (eq? progressed-form #t) (not progressed-form))  progressed-form)
     ((eq? progressed-form (get-binding-formula form))  form)
     (else (make-binding-form (get-binding-vars form)
			      (get-binding-vals form)
			      progressed-form)))))

(for-each place-progress-eval
        '(FORALL EXISTS EXISTS! BINDING)
        (list progress-forall progress-exists
              progress-exists! progress-binding))


;;;----------------------------------------------------------------------
;;; Goal Modality.
;;;----------------------------------------------------------------------

(define (progress-goal form world/action bindings)
  "Progress a goal formula. Should not have modalities inside."
  (eval-formula (first (get-args form)) (get-goal-world) bindings))

(place-progress-eval 'GOAL progress-goal)

;;;----------------------------------------------------------------------
;;; Temporally extended goals. Test to see if a formula is true in
;;; an sequence consisting of infinitely replicating a single world.
;;; For timed modalities things will be true for all time.
;;;----------------------------------------------------------------------

(define idle-eval-table '())

(define (lookup-idle-eval operator)
  (let((x (assoc operator idle-eval-table)))
    (if x (rest x) '())))
  
(define (place-idle-eval operator eval-fn)
  (set! idle-eval-table (acons operator eval-fn idle-eval-table)))

(define (replace-idle-eval operator eval-fn)
  (let ((cell (assoc operator idle-eval-table)))
    (set-cdr! cell eval-fn)))

(define (idle-formula form world/action bindings)
  "Test a formula on a world that idles (i.e., is true for all future
   times. Use an evaluator table to handle the temporal language."
  (if (or (eq? form #t) (eq? form #f))
      form
    (let ((dispatch-fn (lookup-idle-eval (get-operator form))))
      (if dispatch-fn
          (dispatch-fn form world/action bindings)
        (eval-atomic (get-operator form)
                     (eval-terms (get-args form) world/action bindings)
                     world/action)))))


;;;----------------------------------------------------------------------
;;; Dispatched operators.
;;;----------------------------------------------------------------------
;;; Booleans
;;;----------------------------------------------------------------------

(define (idle-and form world/action bindings)
  "test if an and-formula is true on an idling world"
  (every (lambda (formula) (idle-formula formula world/action bindings))
	 (get-args form)))


(define (idle-or form world/action bindings)
  "idle an OR"
  (some (lambda (formula) (idle-formula formula world/action bindings))
        (get-args form)))


(define (idle-xor form world/action bindings)
  "Evaluate an exclusive or"
  (do ((found-one? #f)
       (args (get-args form))
       (false? #f)
       (arg '()))
      ((null? args) (and found-one? (not false?)))
    (set! arg (first args))
    (set! args (rest args))
    (if (idle-formula arg world/action bindings)
	(if found-one? (set! false? #t) (set! found-one? #t)))))


(define (idle-implies form world/action bindings)
  "idle an IMPLIES"
  (if (idle-formula (first (get-args form)) world/action bindings)
      (idle-formula (second (get-args form)) world/action bindings)
      #t))

(define (idle-if-then-else form world/action bindings)
  "idle an IF-THEN-ELSE."
  (let ((args (get-args form)))
    (if (idle-formula (first args) world/action bindings)
        (idle-formula (second args) world/action bindings)
	(idle-formula (third args) world/action bindings))))

(define (idle-not form world/action bindings)
  "Evaluate a NOT"
  (not (idle-formula (first (get-args form)) world/action bindings)))

(define (idle-= form world/action bindings)
  (eqv? (eval-term (first (get-args form)) world/action bindings)
	(eval-term (second (get-args form)) world/action bindings)))

(define (idle-false form world/action bindings)
  #f)

(define (idle-true form world/action bindings)
  #t)

(for-each place-idle-eval
       '(AND OR XOR
         IMPLIES IF-THEN-ELSE NOT
         TRUE FALSE =)
       (list idle-and idle-or idle-xor
             idle-implies idle-if-then-else idle-not
             idle-true idle-false idle-=))


;;;----------------------------------------------------------------------
;;; Temporal modalities.
;;;----------------------------------------------------------------------

(define (idle-ignore-op form world/action bindings)
  "idle by ignoring the operator. Works for next, eventually, always."
  (idle-formula (first (get-args form)) world/action bindings))

(define (idle-until form world/action bindings)
  "idle an UNTIL modality."
  (idle-formula (second (get-args form)) world/action bindings))

(for-each place-idle-eval
        '(NEXT EVENTUALLY ALWAYS UNTIL)
        (list idle-ignore-op idle-ignore-op idle-ignore-op
              progress-until))

;;;----------------------------------------------------------------------
;;; MTL timed modalities.
;;;----------------------------------------------------------------------

(define (idle-t-until form world/action bindings)
  "idle a timed UNTIL modality. (Can be timed-out.)"
  (if (ispec<0 (get-bf-ispec form))
      #f                               ;timed out
      (idle-formula
       (second (get-bf-formulas form)) world/action bindings)))

(define (idle-t-eventually form world/action bindings)
  "idle a timed EVENTUALLY modality."
  (if (ispec<0  (get-bf-ispec form))
      #f                               ;timed out
      (idle-formula
       (first (get-bf-formulas form)) world/action bindings)))

(define (idle-t-always form world/action bindings)
  "idle a timed ALWAYS modality."
  (if (ispec<0 (get-bf-ispec form))
      #t                                ;timed out
      (idle-formula
       (first (get-bf-formulas form)) world/action bindings)))

(define (idle-delta form world/action bindings)
  "idle a delta formula. This involves building a shifted formula
   and then idling that."
  (let* ((formula (get-delta-formula form))
         (ispec (get-bf-ispec formula)))
    (idle-formula
     (append (list (get-operator formula)
                   (ispec-lshift ispec
                                 (world/action-action-duration world/action)))
             (get-bf-formulas formula))
     world/action bindings)))


(for-each place-idle-eval
	  '(T-UNTIL T-EVENTUALLY T-ALWAYS DELTA)
        (list idle-t-until idle-t-eventually
              idle-t-always idle-delta))


;;;----------------------------------------------------------------------
;;; Quantifiers. Relies on parts of the evaluator code. 
;;;----------------------------------------------------------------------
          
(define (idle-forall form world/action bindings)
  "idle a FORALL formula"
  (let* ((args (get-args form))
         (variables (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (formula   (get-qf-formula args))
         (generator '()))
    (set! bindings (extend-bindings variables variables bindings))
    (set! generator
	  (make-generator gen-lit variables world/action bindings))
    (if generator
        (do ((finish? #f)
             (result #f))
            (finish? result)
          (cond((generator)
		(if (not (idle-formula formula world/action bindings))
		    (begin (set! finish? #t)
			   (set! result #f))))
	       (else (set! finish? #t)
		     (set! result #t))))
	#t)))
  

(define (idle-exists! form world/action bindings)
  "idle an EXISTS! (exists unique) formula"
  (let* ((args (get-args form))
         (variables (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (formula   (get-qf-formula args))
         (generator '()))
    (set! bindings (extend-bindings variables variables bindings))
    (set! generator
      (make-generator gen-lit variables world/action bindings))
    (if generator
        (do ((finish? #f)
             (result #f)
             (found-one? #f))
            (finish? result)
          (if (generator)
              (if (or (null? formula)
                      (idle-formula formula world/action bindings))
                  (cond(found-one?
			(set! finish? #t)
			(set! result #f))
		       (else (set! found-one? #t))))
	      (cond(found-one?
		    (set! finish? #t)
		    (set! result #t))
		   (else (set! finish? #t)
			 (set! result #f)))))
	#f)))


(define (idle-exists form world/action bindings)
  "idle an EXISTS formula"
  (let* ((args (get-args form))
         (variables (get-qf-variables args))
         (gen-lit   (get-qf-generator args))
         (formula   (get-qf-formula args))
         (generator '()))
    (set! bindings (extend-bindings variables variables bindings))
    (set! generator
      (make-generator gen-lit variables world/action bindings))
    (if generator
        (do ((finish? #f)
             (result #f))
            (finish? result)
          (cond((generator)
		(if (or (null? formula)
			(idle-formula formula world/action bindings))
		    (begin (set! finish? #t)
			   (set! result #t))))
	       (else (set! finish? #t)
		     (set! result #f))))
	#f)))

(define (idle-binding form world/action bindings)
  "idle a binding node, by extending the current bindings."
  (idle-formula
   (get-binding-formula form)
   world/action
   (extend-bindings (get-binding-vars form)
                    (get-binding-vals form)
                    bindings)))

(for-each place-idle-eval
        '(FORALL EXISTS EXISTS! BINDING)
        (list idle-forall idle-exists
              idle-exists! idle-binding))

;;;;----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>10.5 Compute a currentcondition formula from a temporal formula.
;;;;   (cc <TLFORM>)
;;;;  Produces as output a list of 2 formulas
;;;;  (Tform Fform)
;;;;  with the following properties
;;;; a) these two formulas are Atemporal.
;;;; c) for every world W
;;;;
;;;;       if Tform != NIL then 
;;;;         (eval-formula Tform W '()) = #T
;;;;               ==> (progress-formula <TLFORM> W '()) = (TRUE)
;;;; 
;;;;       if Fform != NIL then
;;;;         (eval-formula Fform W '()) = #F
;;;;             ==> (progress-formula <TLFORM> W '()) = (FALSE)
;;;; 
;;;;----------------------------------------------------------------------

(define cc-eval-table '())
;;Table of functions for progressing various types of operators

(define (lookup-cc-eval operator)
  (let((x (assoc operator cc-eval-table)))
    (if x (rest x) '())))

(define (place-cc-eval operator eval-fn)
  (set! cc-eval-table (acons operator eval-fn cc-eval-table)))

(define (replace-cc-eval operator eval-fn)
  (let ((cell (assoc operator cc-eval-table)))
    (set-cdr! cell eval-fn)))

(define (make-cc-return Tform Fform)
  (list Tform Fform))

(define (get-Tform cc-return)
  (first cc-return))

(define (get-Fform cc-return)
  (second cc-return))

(define (remove-nulls list)
  (define (remove-recursive-nulls lst result)
    (cond
     ((null? lst)
      result)
     ((null? (first lst))
      (remove-recursive-nulls (rest lst) result))
     (else
      (remove-recursive-nulls (rest lst)
			      (append! result (cons (first lst) '()))))))
  (remove-recursive-nulls list '()))


(define (count predicate lst)
  ;;;test number of element of lst satisfy predicate
  (define (count-recursive predicate lst N)
    (cond
     ((null? lst) N)
     ((predicate (first lst))
      (count-recursive predicate (rest lst) (+ 1 N)))
     (else
      (count-recursive predicate (rest lst) N))))
  (count-recursive predicate lst 0))


(define (equal-list? lst1 lst2)
  (cond ((and (null? lst1)
	      (null? lst2))
	 #t)
	((or (null? lst1)
	     (null? lst2))
	 #f) ;mismatched list sizes
	((eq? (first lst1) (first lst2))
	 (equal-list? (rest lst1) (rest lst2)))
	(else
	 #f)))
	 
;;;----------------------------------------------------------------------

(define (cc form)
  "Top level cc computation. Dispatch on type of operator"
  (let ((dispatch-fn (lookup-cc-eval (get-operator form))))
    (if dispatch-fn
	(dispatch-fn form)
	;;For (true) (false) (atomic ...)
	(make-cc-return form form))))

;;;----------------------------------------------------------------------
;;; Dispatched operators.
;;;----------------------------------------------------------------------
;;; Booleans
;;;----------------------------------------------------------------------

(define (cc-and form)
  "Return Current condition formulas for an and formula"
  (let*
      ;;1. Compute all cc's of the and's arguments.
      ((cc-subforms (map cc (get-args form)))
       (tsubforms (remove-nulls (map get-tform cc-subforms)))
       (fsubforms (remove-nulls (map get-fform cc-subforms)))
       (tform '())
       (fform '()))
    
    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (get-args form))
      (set! tform form)
      (set! fform form))

     (else
      ;; if every argument has a tform then we can make a tform
      (if (every (lambda (cc) (not (null? (get-tform cc)))) cc-subforms)
	  (set! tform (make-and-form tsubforms)))
      
      ;; the fform however are simply the conjunction of the ones that exist.
      (let ((len (length fsubforms)))
	(cond 
	 ((> len 1)
	  (set! fform (make-and-form fsubforms)))
	 ((= len 1)
	  (set! fform (first fsubforms)))))))
     
     (make-cc-return tform fform)))

(define (cc-or form)
  "Return Current condition formulas for an or formula"
  (let*
      ;;1. Compute all cc's of the and's arguments.
      ((cc-subforms (map cc (get-args form)))
       (tsubforms (remove-nulls (map get-tform cc-subforms)))
       (fsubforms (remove-nulls (map get-fform cc-subforms)))
       (tform '())
       (fform '()))
    
    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (get-args form))
      (set! tform form)
      (set! fform form))

     (else
      ;; if every argument has an fform then we can make a fform
      (if (every (lambda (cc) (not (null? (get-fform cc)))) cc-subforms)
	  (set! fform (make-or-form fsubforms)))
      
      ;; the tform however are simply the conjunction of the ones that exist.
      (let ((len (length tsubforms)))
	(cond 
	 ((> len 1)
	  (set! tform (make-or-form tsubforms)))
	 ((= len 1)
	  (set! tform (first tsubforms)))))))
     
     (make-cc-return tform fform)))

(define (cc-xor form)
  "Return Current condition formulas for an xor formula"
  (let*
      ;;1. Compute all cc's of the and's arguments.
      ((cc-subforms (map cc (get-args form)))
       (tsubforms (remove-nulls (map get-tform cc-subforms)))
       (fsubforms (remove-nulls (map get-fform cc-subforms)))
       (tform '())
       (fform '()))
    
    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (get-args form))
      (set! tform form)
      (set! fform form))

     (else
      ;;The xor can be tested for true if every subform has a Tform and
      ;;also a Fform. In which case it will be true if
      ;;(and (xor tforms) (xor fforms))---one and only one *must* be
      ;;true, and all but one *must* be false. Note these formulas
      ;;are one-sided, i.e., if one of the tforms==False it does not
      ;;mean its subform will not progress to true!
      (cond
       ((and (every (lambda (cc) (not (null? (get-tform cc)))) cc-subforms)
	     (every (lambda (cc) (not (null? (get-fform cc)))) cc-subforms))
	(set! tform
	      (make-and-form
	       (list (make-xor-form tsubforms)
		     (make-xor-form fsubforms))))))

      ;;
      ;;The xor is false if more than one of the tforms is
      ;;true. Note that if all of the tforms are false this does not
      ;;mean anythin. 
      ;;Also if all of the subforms has an fform and they all
      ;;evaluate to false, then this will be a failure as well.
      ;;
      
      (let
	((more-than-one-has-tform (> 1 (count get-tform cc-subforms)))
	 (all-have-fforms 
	  (every (lambda (cc) (not (null? (get-fform cc)))) cc-subforms)))
	;;
	(cond 
	 ((and more-than-one-has-tform all-have-fforms)
	  (set! fform (make-and-form
		       (list (make-or-form
			      (list (make-xor-form tsubforms)
				    (make-not-form (make-or-form tsubforms))))
			     ;;
			     (make-or-form fsubforms)))))
	 ;;
	 (more-than-one-has-tform
	  (set! fform (make-or-form
		       (list
			(make-xor-form tsubforms)
			(make-not-form (make-or-form tsubforms))))))

	 ;;
	 (all-have-fforms
	  (set! fform (make-or-form fsubforms)))))))
    
     (make-cc-return tform fform)))

(define (cc-implies form)
  "return a current condition formula for an implies."
  (let*
      ;;1. Compute all cc's 
      ((cc-subforms (map cc (get-args form)))
       (tsubforms (remove-nulls (map get-tform cc-subforms)))
       (fsubforms (remove-nulls (map get-fform cc-subforms)))
       (tform '())
       (fform '()))
    
    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (get-args form))
      (set! tform form)
      (set! fform form))

     (else
      (let ((A-cc (first cc-subforms))
	    (C-cc (second cc-subforms)))

	;;there is a tform if antecedent has fform or consequent has tform.
	(cond
	 ((and (not (null? (get-tform C-cc)))
	       (not (null? (get-fform A-cc))))
	  (set! tform (make-or-form (list (make-not-form (get-fform A-cc))
					  (get-tform C-cc)))))
	 ;;
	 ((not (null? (get-tform C-cc)))
	  (set! tform (get-tform C-cc)))
	 ;;
	 ((not (null? (get-fform A-cc)))
	  (set! tform (make-not-form (get-fform A-cc)))))

	(if
	 ;;there is a fform if the atntecedent has a tform and the
	 ;;consequent has a fform.
	 (and (not (null? (get-fform C-cc)))
	      (not (null? (get-tform A-cc))))
	 (set! fform (make-or-form (list (make-not-form (get-tform A-cc))
					  (get-fform C-cc))))))))

    (make-cc-return tform fform)))
    
(define (cc-if-then-else form)
  "return a current condition formula for an if-then-else."
  (let*
      ;;1. Compute all cc's 
      ((cc-subforms (map cc (get-args form)))
       (tsubforms (remove-nulls (map get-tform cc-subforms)))
       (fsubforms (remove-nulls (map get-fform cc-subforms)))
       (tform '())
       (fform '()))
    
    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (get-args form))
      (set! tform form)
      (set! fform form))

     (else
      (let ((ccarg1 (first cc-subforms))
	    (ccarg2 (second cc-subforms))
	    (ccarg3 (third cc-subforms)))
	;;
	;; four cases where we can get a true form
	(cond
	 ((and (not (null? (get-tform ccarg1)))
	       (not (null? (get-fform ccarg1)))
	       (not (null? (get-tform ccarg2)))
	       (not (null? (get-tform ccarg3))))
	  (set! tform
		(make-or-form
		 (list (make-and-form (list (get-tform ccarg1)
					    (get-tform ccarg2)))
		       (make-and-form (list (make-not-form (get-fform ccarg1))
					    (get-tform ccarg2)))))))
	 ;;
	 ((and (not (null? (get-tform ccarg1)))
	       (not (null? (get-tform ccarg2))))
	  (set! tform (make-and-form (list (get-tform ccarg1)
					   (get-tform ccarg2)))))
	 ;;
	 ((and (not (null? (get-fform ccarg1)))
	       (not (null? (get-tform ccarg3))))
	  (set! tform (make-and-form (list (make-not-form (get-fform ccarg1))
					   (get-tform ccarg3)))))
	 ;;
	 ((and (not (null? (get-tform ccarg2)))
	       (not (null? (get-tform ccarg3))))
	  (set! tform (make-and-form (list (get-tform ccarg2)
					   (get-tform ccarg3))))))

	;;
	;; cases where we get a false form. Rember the logic
	;; that fform==false ==> progression is false!
	;;
	(cond
	 ((and (not (null? (get-tform ccarg1)))
	       (not (null? (get-fform ccarg1)))
	       (not (null? (get-fform ccarg2)))
	       (not (null? (get-fform ccarg3))))

	  (set! fform
		(make-and-form
		 (list (make-or-form (list (make-not-form (get-tform ccarg1))
					   (get-fform ccarg2)))
		       (make-or-form (list (get-fform ccarg1)
					   (get-fform ccarg2)))))))
	 ;;

	 ((and (not (null? (get-tform ccarg1)))
	       (not (null? (get-fform ccarg2))))
	  (set! fform (make-or-form (list (make-not-form (get-tform ccarg1))
					  (get-fform ccarg2)))))
	 ;;
	 ((and (not (null? (get-fform ccarg1)))
	       (not (null? (get-fform ccarg3))))
	  (set! tform (make-or-form (list (get-fform ccarg1)
					  (get-fform ccarg3)))))
	 ;;
	 ((and (not (null? (get-fform ccarg2)))
	       (not (null? (get-fform ccarg3))))
	  (set! tform (make-or-form (list (get-fform ccarg2)
					  (get-fform ccarg3)))))))))

	(make-cc-return tform fform)))

(define (cc-not form)
  "return a current condition formula for a not-form"
  (let*
      ;;1. Compute all cc's 
      ((cc-subforms (map cc (get-args form)))
       (tsubforms (remove-nulls (map get-tform cc-subforms)))
       (fsubforms (remove-nulls (map get-fform cc-subforms)))
       (tform '())
       (fform '()))

    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (get-args form))
      (set! tform form)
      (set! fform form))

     (else
      (let ((ccarg (first cc-subforms)))
	(if (not (null? (get-fform ccarg)))
	    (set! tform (make-not-form (get-fform ccarg))))
	(if (not (null? (get-tform ccarg)))
	    (set! fform (make-not-form (get-tform ccarg)))))))

    (make-cc-return tform fform)))
	
(for-each place-cc-eval
	  '(AND OR XOR
		IMPLIES IF-THEN-ELSE NOT)
	  (list cc-and cc-or cc-xor
		cc-implies cc-if-then-else cc-not))

;;;----------------------------------------------------------------------
;;; Temporal modalities.
;;;----------------------------------------------------------------------

(define (cc-next form)
  "current component of a next formula"
  (make-cc-return '() '()))

(define (cc-eventually form)
  "current component of an eventually modality"
  (let ((cc-subform (cc (first (get-args form)))))
    (make-cc-return (get-tform cc-subform) '())))
	
(define (cc-always form)
  "current component of an always modality"
  (let ((cc-subform (cc (first (get-args form)))))
    (make-cc-return (get-tform cc-subform)
		    (get-fform cc-subform))))

(define (cc-until form)
  "current component of an until modality"
  (let* ((cc-subforms (map cc (get-args form)))
	 (cc-subform1 (first cc-subforms))
	 (cc-subform2 (second cc-subforms))
	 (tform '())
	 (fform '()))
    ;;
    ;; (Until A B) is true if B is true
    ;;
    (set! tform (get-tform cc-subform2))
    ;;
    ;; (until a b) is false if A and B progress to false
    (if (and (not (null? (get-fform cc-subform1)))
	     (not (null? (get-fform cc-subform2))))
	(set! fform (make-or-form
		     (list
		      (get-fform cc-subform1)
		      (get-fform cc-subform2)))))

    (make-cc-return tform fform)))
     
(for-each place-cc-eval
        '(NEXT EVENTUALLY ALWAYS UNTIL)
        (list cc-next cc-eventually cc-always
              cc-until))

;;;----------------------------------------------------------------------
;;; MTL timed modalities.
;;;----------------------------------------------------------------------

;;; I suppose these could be done. But not sure if worth while right now. 


;;;----------------------------------------------------------------------
;;; Quantifiers. Relies on parts of the evaluator code. 
;;;----------------------------------------------------------------------
;;;
;;; These are easy. All of the dirty work is done recursively
          
(define (cc-forall form)
  "return a current condition formula for an forall."
  (let* ((args (get-args form))
         (qf-vars (get-qf-variables args))
         (gen-lit  (get-qf-generator args))
         (qf-form  (list (get-qf-formula args)))
	 (cc-subforms (map cc qf-form))
	 (tsubforms (remove-nulls (map get-tform cc-subforms)))
	 (fsubforms (remove-nulls (map get-fform cc-subforms)))
	 (tform '())
	 (fform '()))

    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (first qf-form))
      (set! tform form)
      (set! fform form))

     (else
      (if (not (null? tsubforms))
	  (set! tform (list 'FORALL qf-vars gen-lit (first tsubforms))))

      (if (not (null? fsubforms))
	  (set! fform (list 'FORALL qf-vars gen-lit (first fsubforms))))))

     (make-cc-return tform fform)))

(define (cc-exists form)
  "return a current condition formula for an exists."
  (let* ((args (get-args form))
         (qf-vars (get-qf-variables args))
         (gen-lit  (get-qf-generator args))
         (qf-form  (list (get-qf-formula args)))
	 (cc-subforms (map cc qf-form))
	 (tsubforms (remove-nulls (map get-tform cc-subforms)))
	 (fsubforms (remove-nulls (map get-fform cc-subforms)))
	 (tform '())
	 (fform '()))

    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (first qf-form))
      (set! tform form)
      (set! fform form))

     (else
      (if (not (null? tsubforms))
	  (set! tform (list 'EXISTS qf-vars gen-lit (first tsubforms))))

      (if (not (null? fsubforms))
	  (set! fform (list 'EXISTS qf-vars gen-lit (first fsubforms))))))

     (make-cc-return tform fform)))

(define (cc-exists! form)
  "return a current condition formula for an exists!"
  (let* ((args (get-args form))
         (qf-vars (get-qf-variables args))
         (gen-lit  (get-qf-generator args))
         (qf-form  (list (get-qf-formula args)))
	 (cc-subforms (map cc qf-form))
	 (tsubforms (remove-nulls (map get-tform cc-subforms)))
	 (fsubforms (remove-nulls (map get-fform cc-subforms)))
	 (tform '())
	 (fform '()))

    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (first qf-form))
      (set! tform form)
      (set! fform form))

     (else
      ;;Only tricky one
      ;;exist! will be true if at one and only binding is certain
      ;;to generate a true progression and all but one binding
      ;;is certain to generate false progressions
      (if (and (not (null? tsubforms))
	       (not (null? fsubforms)))
	  (set! tform
		(make-and-form
		 (list 'EXISTS! qf-vars gen-lit (first tsubforms))
		 (list 'EXISTS! qf-vars gen-lit (first fsubforms)))))

      ;;it will be false if more than one binding is certain to be true
      ;;(accounting for the case where all are true tests fail)
      (cond
       ((and (not (null? tsubforms))
	     (not (null? fsubforms)))
	(set! fform
	      (make-and-form
	       (list (make-or-form
		      (list 'EXISTS! qf-vars gen-lit (first tsubforms))
		      (list 'FORALL qf-vars gen-lit (make-not-form
						     (first tsubforms))))
		     (list 'EXISTS qf-vars gen-lit fsubforms)))))
       ;;
       ((not (null? tsubform))
	(set! fform
	      (make-or-form
	       (list 'EXISTS! qf-vars gen-lit (first tsubforms))
	       (list 'FORALL qf-vars gen-lit (make-not-form
					      (first tsubforms))))))

       ((not (null? fsubforms))
	(set! fform (list 'EXISTS qf-vars gen-lit fsubforms))))))

     (make-cc-return tform fform)))


(define (cc-binding form)
  "Return Current condition formulas for a binding formula"
  (let* ((b-forms (list (get-binding-formula form)))
	 (b-vars (get-binding-vars form))
	 (b-vals (get-binding-vals form))
	 (cc-subforms (map cc b-forms))
	 (tsubforms (remove-nulls (map get-tform cc-subforms)))
	 (fsubforms (remove-nulls (map get-fform cc-subforms)))
	 (tform '())
	 (fform '()))
    
    (cond
     ;; test for special case where we can reuse form.
     ;; note should be sufficient to test only one of tforms
     ;; or fforms.
     ((equal-list? tsubforms (get-args form))
      (set! tform form)
      (set! fform form))

     (else
      (let ((ccarg (first cc-subforms)))
	(if (not (null? (get-tform ccarg)))
	    (set! tform (make-binding-form b-vars b-vals (get-tform ccarg))))
	(if (not (null? (get-fform ccarg)))
	    (set! fform (make-binding-form b-vars b-vals (get-fform ccarg)))))))

    (make-cc-return tform fform)))

(for-each place-cc-eval
        '(FORALL EXISTS EXISTS! BINDING)
        (list cc-forall cc-exists
              cc-exists! cc-binding))

;;;;-----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>11 Plan
;;;;
;;;; The planner itself.
;;;;
;;;; a. Data structures for Planner. Access Functions.
;;;; b. Plan successor function. Search occurs among the space of totally
;;;;     ordered forward chaining plans. Hence the world state that exists
;;;;     at plan termination is fully known.
;;;; c. Plan equality test (equality if terminal state is identical).
;;;; d. Plan termination test (terminate if terminal state satisfies goal).
;;;
;;;;-----------------------------------------------------------------------
;;; A plan is a linear sequence of plan "states"
;;; Each plan "state" consists of the triple world, tl-formula, action
;;; A World is a STRIPS state.
;;; A temporal-formula is a temporal formula used to prune the search.
;;; An action is an action structure defined by the action-interface code
;;;;-----------------------------------------------------------------------

;;;----------------------------------------------------------------------
;; Later we might want to explore non-linear plans
;; Set up a layer of abstraction to facilitate this
;; We need a lot of dynamically created plan steps so use a more efficient
;; constructor.
;;;----------------------------------------------------------------------

(declare (integrate make-linear-plan 
		    linear-plan-world/action linear-plan-tlform
		    linear-plan-ccform
		    linear-plan-duration linear-plan-cost
		    linear-plan-length linear-plan-user  linear-plan-previous 
		    set-linear-plan-world/action! set-linear-plan-tlform!
		    set-linear-plan-duration! set-linear-plan-cost!
		    set-linear-plan-length! set-linear-plan-user!
		    set-linear-plan-previous!
		    linear-plan? copy-linear-plan))

;;; Predicate

(define (linear-plan? x)
  (and (vector? x) (= 8 (vector-length x))
       (eq? 'linear-plan (vector-ref x 0))))

;;; Constructor

(define (make-linear-plan world/action tlform ccform duration 
			  cost length user previous)
  (vector 'linear-plan world/action tlform ccform duration 
	  cost length user previous))

;;; Selectors

(define (linear-plan-world/action lp) (vector-ref lp 1))
(define (linear-plan-tlform lp) (vector-ref lp 2))
(define (linear-plan-ccform lp) (vector-ref lp 3))
(define (linear-plan-duration lp) (vector-ref lp 4))
(define (linear-plan-cost lp) (vector-ref lp 5))
(define (linear-plan-length lp) (vector-ref lp 6))
(define (linear-plan-user lp) (vector-ref lp 7))
(define (linear-plan-previous lp) (vector-ref lp 8))

;;; Modifiers

(define (set-linear-plan-world/action! lp val) (vector-set! lp 1 val))
(define (set-linear-plan-tlform! lp val) (vector-set! lp 2 val))
(define (set-linear-plan-ccform! lp val) (vector-set! lp 3 val))
(define (set-linear-plan-duration! lp val) (vector-set! lp 4 val))
(define (set-linear-plan-cost! lp val) (vector-set! lp 5 val))
(define (set-linear-plan-length! lp val) (vector-set! lp 6 val))
(define (set-linear-plan-user! lp val) (vector-set! lp 7 val))
(define (set-linear-plan-previous! lp val) (vector-set! lp 8 val))

;;; Copier

(define copy-linear-plan vector-copy)

(declare (integrate plan-world plan-tlform  plan-ccform plan-action-name 
		    plan-action-priority
		    plan-world/action
		    plan-length plan-cost
		    plan-duration
		    plan-previous make-plan))

(define (plan-world/action plan)
  (linear-plan-world/action plan))

(define (plan-world plan)
    (world/action-world (linear-plan-world/action plan)))

(define (plan-tlform plan)
  (linear-plan-tlform plan))

(define (plan-ccform plan)
  (linear-plan-ccform plan))

(define (plan-action-name plan)
  (world/action-action-name (linear-plan-world/action plan)))

(define (plan-action-priority plan)
  (world/action-action-priority (linear-plan-world/action plan)))

(define (plan-length plan)
  (linear-plan-length plan))

(define (plan-cost plan)
  (linear-plan-cost plan))

(define (plan-duration plan)
  (linear-plan-duration plan))

(define (plan-previous plan)
  (linear-plan-previous plan))

(define (plan-user plan)
  (linear-plan-user plan))

(define (set-plan-user plan value)
  (set-linear-plan-user! plan value))

(define (make-plan world/action tlform ccform duration cost length previous)
  (make-linear-plan world/action tlform ccform duration cost length '() previous))

;;;----------------------------------------------------------------------
;;; Plan successor function used in search.
;;; To extend a plan we examine the final world
;;; 1. Progress the temporal formula through the world.
;;; 2. If the progressed formual is not '()
;;; 3. Generate all successor worlds by applying all applicable
;;;    actions.
;;; 4. Build up the plan extensions.
;;;----------------------------------------------------------------------

;;;Without cc

(define (ss-fn1 plan)
  "Grow a plan in all possible ways"
  (let ((progressed-tlform
	 (progress-formula (plan-tlform  plan)
			   (plan-world/action plan)
			   '()))
	(new-plans '()))
    (if progressed-tlform
	(do ((successors (generate-successors (plan-world/action plan)))
	     (successor '()))
	    ((null? successors))
	  (set! successor (first successors))
	  (set! successors (rest successors))
	  (set! new-plans (cons (plan-extend successor progressed-tlform '() plan)
				new-plans)))
	(set! *pruned-worlds* (+ *pruned-worlds* 1)))
    ;; TRACE, pass it all of the things you might want to trace.
    (tl-tracer 'plan-successors (list plan progressed-tlform new-plans))
    new-plans))


;;;to check cc
(define (ss-fn2 plan)
  "Grow a plan in all possible ways"
  (let ((progressed-tlform (progress-formula (plan-tlform  plan)
                                             (plan-world/action plan)
					     '()))
	(cc-form (second (cc (plan-tlform plan))))
	(new-plans '()))
    (cond
     (progressed-tlform
      (cond
       ;;check for errors
       ((and cc-form (not (eval-formula cc-form (plan-world/action plan) '())))
	(format *trace-stream* "~%ERROR BY CC!~%")
	(fluid-let ((*unparser-list-breadth-limit* #f)
		    (*unparser-list-depth-limit* #f))
	  (format *trace-stream* "~%Temporal formula is:~%")
	  (pp (plan-tlform plan) *trace-stream*)
	  (format *trace-stream* "~%It progressed to:~%")
	  (pp progressed-tlform *trace-stream*)
	  (format *trace-stream* "~%On world:~%")
	  (default-print-world (plan-world/action plan))
	  (format *trace-stream* "~%Current component is:~%")
	  (pp (second cc-form)  *trace-stream*))))
      
      (do ((successors (generate-successors (plan-world/action plan)))
	   (successor '()))
	  ((null? successors))
	(set! successor (first successors))
	(set! successors (rest successors))
	(set! new-plans (cons (plan-extend successor progressed-tlform '() plan)
			      new-plans))))
     (else
      (cond
       ;;check for misses
       ((and cc-form (eval-formula cc-form (plan-world/action plan) '()))
	(format *trace-stream* "~%MISS BY CC!~%")
	(fluid-let ((*unparser-list-breadth-limit* #f)
		    (*unparser-list-depth-limit* #f))
	  (format *trace-stream* "~%Temporal formula is:~%")
	  (pp (plan-tlform plan) *trace-stream*)
	  (format *trace-stream* "~%It progressed to:~%")
	  (pp progressed-tlform)
	  (format *trace-stream* "~%On world:~%")
	  (default-print-world (plan-world/action plan))
	  (format *trace-stream* "~%Current component is:~%")
	  (pp (second cc-form)  *trace-stream*))))

      (set! *pruned-worlds* (+ *pruned-worlds* 1))))

     (tl-tracer 'plan-successors (list plan progressed-tlform new-plans))
   new-plans))

; with CC

(define (ss-fn3 plan)
   "Grow a plan in all possible ways"
   (let ((cc-form (plan-ccform plan))
	 (progressed-tlform '())
	 (new-ccform '())
         (new-plans '()))
     (cond
      ((and cc-form (not (eval-formula cc-form (plan-world/action plan) '())))
       (set! *pruned-worlds* (+ *pruned-worlds* 1)))
      (else
       (set! progressed-tlform
	     (progress-formula (plan-tlform plan) (plan-world/action plan) '()))
       (set! new-ccform (second (cc progressed-tlform)))
       (if progressed-tlform
	   (do ((successors (generate-successors (plan-world/action plan)))
		(successor '()))
	       ((null? successors))
	     (set! successor (first successors))
	     (set! successors (rest successors))
	     (set! new-plans (cons (plan-extend successor progressed-tlform
						new-ccform plan)
				   new-plans)))
	   (set! *pruned-worlds* (+ *pruned-worlds* 1)))))
     
     (tl-tracer 'plan-successors (list plan progressed-tlform new-plans))
     new-plans))

(define plan-successor-fn ss-fn1)

(define (plan-extend new-world/action new-tlform new-ccform plan)
  "Extend a plan by appending the new world/action struct to it."
    (make-plan new-world/action new-tlform new-ccform
               (+ (world/action-action-duration new-world/action) 
		  (plan-duration plan))
               (+ (world/action-action-cost new-world/action) (plan-cost plan))
               (+ 1 (plan-length plan))
               plan))

;;;----------------------------------------------------------------------
;;; Plan equality test used in graph searcher routines.
;;; Two plans are equal if they lead to the same world.
;;;----------------------------------------------------------------------

(define (plan-extended= plan1 plan2)
  (and (eqv? (plan-duration plan1) (plan-duration plan2))
       (world= (plan-world plan1) (plan-world plan2))))

(define (plan-classic= plan1 plan2)
  (world= (plan-world plan1) (plan-world plan2)))

;;;The function plan= will be set by the interface to deal with the
;;;correct type of control formulas.
;;;

(define plan= #t)

;;;----------------------------------------------------------------------
;;; Plan cycle test used in depth-first search routine.
;;; Plan has cycle if its final world appears in the previous subplan
;;;----------------------------------------------------------------------

(define (plan-has-cycle plan)
  (cond
   ((null? plan) #f)
   ((null? (plan-previous plan)) #f)
   (else (plan-has-cycle-recurse plan (plan-previous plan)))))

(define (plan-has-cycle-recurse plan previous)
  (cond
   ((plan= plan previous) #t)
   ((null? (plan-previous previous)) #f)
   (else (plan-has-cycle-recurse plan (plan-previous previous)))))
    

;;;----------------------------------------------------------------------
;;; Plan termination test used in graph searcher routines.
;;; Test if plan's final state achieves the goal. The routine
;;; final-world-goal?
;;; is set to detect the particular goal being planned for. Its function
;;; will also depend on the type of goal beind planned for. For example,
;;; if we have a temporal goal we need to use the temporal formula. If
;;; we have a classic goal of achievement we only need to use the
;;; final world.
;;;----------------------------------------------------------------------

(define (plan-goal? plan)
  (final-world-goal? (plan-tlform plan) (plan-world/action plan)))

;;;----------------------------------------------------------------------
;;; Cost functions. Used for various forms of search.
;;; These functions should return a numeric rank given a plan.
;;; First we have priority functions, these are used to rank the
;;;   successors of a plan. Thus they only need worry about the final
;;;   action or final world.
;;;  Second we have cost functions these are used to rank all plans, so
;;;    they should take into account the entire sequence of
;;;    actions/world in the plan. These cost functions can include
;;;    heuristic estimates for getting to the goal which will give A*
;;;    behavior.
;;;  NOTE the search routines explore LOWEST COST first but HIGHEST
;;;  PRIORITY first
;;;----------------------------------------------------------------------

(define (best-action plan)
  "A priority function, explore the successor plans that arose from
   highest priority actions."
  (plan-action-priority plan))

(define (optimal-cost plan)
  "A cost function, explore lowest cost plans first"
  (plan-cost plan))

(define (a* heuristic)
  "Return a cost function that explores lowest cost + heuristic estimate
   plans first"
  (lambda (plan) (+ (plan-cost plan) (heuristic plan))))

(define (plan-worlds plan)
  "Generate a list of the worlds in a plan, starting from the initial state"
  (reverse (map-plan plan-world plan)))

(define (plan-action-names plan)
  "Generate a list of the actions in a plan, starting from the initial action
   (the very first action is '() so skip that one)."
  (rest (reverse (map-plan plan-action-name plan))))

(define (plan-world/actions plan)
  "Generate a list of the plan world/action nodes, reversed."
  (reverse (map-plan plan-world/action plan)))

(define (map-plan fn plan)
  "Call fn on each step in the plan, collecting results."
  (if (null? plan)
      '()
    (cons (fn plan) (map-plan fn (plan-previous plan)))))

;;;----------------------------------------------------------------------
;;; The planner itself.
;;; You don't want to call this directly unless you know what you are
;;; doing.
;;;
;;; It takes the following arguments.
;;; start-world/action --- a world/action structure (as set up by worlds.cl)
;;; temporal-control a temporal formula to be used for search control
;;; It assumes that "final-world-goal?" has been properly configured
;;; to detect the achievement of the particular goal being searched for
;;;
;;; The caller must also set up the functions 
;;; search-fn    --- return the search mode used.
;;; priority-fn  --- return the depth-first priority function.
;;; cost-fn      --- return the best-first cost function.
;;;
;;; Returns a SOLUTION information structure.
;;;----------------------------------------------------------------------

(define *pruned-worlds* 0)
;;;Counter to keep track of number of worlds pruned by the temporal
;;;control formula

(define (tlplanner start-world/action tlform search-fn priority-fn cost-fn)
  (let* ((initial-plan
          (make-plan start-world/action 
           tlform (second (cc tlform)) 0 0 0 '()))
         (search-result '())
         (plan-time 0))
    (if *verbose*
        (begin
          (format *trace-stream* "~%----------------------------------~
                                  ------------------------------------")
          (format *trace-stream* "~%Planner invoked. Initial world:")
          (print-world start-world/action *trace-stream*)
          (format *trace-stream* "~%Goal is:")
          (format *trace-stream* "~%~S" (get-goal))))
    (set! plan-time (get-internal-run-time))
    (set! *pruned-worlds* 0)
    (set! search-result
      (search-fn initial-plan plan-goal? plan-successor-fn plan=
		 cost-fn priority-fn (get-search-limit)))
    (set! plan-time (- (get-internal-run-time) plan-time))
    
    (if *verbose*
        (begin
          (format *trace-stream*
                  "~%Planning completed. CPU time taken ~%~S sec."
                  (/ plan-time internal-time-units-per-second))
          (cond
           ((eq? (first search-result) 'RESOURCES)
            (format *trace-stream*
                    "~%Resource bounds exhausted, no plan found."))
           ((eq? (first search-result) 'NO-PLAN)
            (format *trace-stream* "~%All possible plans exhaused. ~
                                    Goal is unachievable."))
           (else (format *trace-stream* "~%~%Found plan, final world:")
              (print-world (plan-world/action (first search-result))
                           *trace-stream*)))
          
          (format *trace-stream* "~%Worlds searched  = ~S"
                  (- (third search-result) *pruned-worlds*))
          (format *trace-stream* "~%Worlds pruned by temporal control = ~S"
                  *pruned-worlds*)
          (format *trace-stream* "~%Worlds unexamined  = ~S"
                  (second search-result))
          (if (not (or (eq? (first search-result) 'RESOURCES)
		       (eq? (first search-result) 'NO-PLAN)))
	      (begin 
		(format *trace-stream* "~%Plan length = ~A"
			(plan-length (first search-result)))
		(do ((time (get-initial-time))
		     (successors (rest (plan-world/actions 
				       (first search-result))))
		     (successor '()))
		    ((null? successors)
		     (format *trace-stream* "~%At time ~A: Plan completed"
			     time))
		  (set! successor (first successors))
		  (set! successors (rest successors))
		  (format *trace-stream* "~%At time ~A: ~A"
			  time (world/action-action-name successor))
		  (set! time (+ time (world/action-action-duration 
				      successor))))
		;;Return the planning time, and search-result.
		(format *trace-stream* "~%Plan cost: ~A" 
		    (plan-cost (first search-result)))))
	  (format *trace-stream* "~%-----------------------------------------~
                                  -----------------------------")))
    (list plan-time (first search-result)
	  (- (third search-result) *pruned-worlds*)
	  *pruned-worlds* (second search-result))))

;;;;-----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>12 Define Domain.
;;;;
;;;; Functions that interface with the internal data structures that
;;;; maintain the world state (i.e., a database describing the current
;;;; world).
;;;;
;;;;
;;;; The interface is defined in terms of list descriptions of worlds.
;;;; Worlds are specified as fully bound lists of literals and function
;;;; definitions. Each literal is a list with the following form:
;;;;
;;;;    literal        = (predicate-name arg1 arg2 ... argn)
;;;;    predicate-name = symbol.
;;;;    argi           = symbol | number
;;;;
;;;; Each function definition has the form:
;;;;
;;;;    function-defn  = (= (function-name arg1 arg2 ... argn) value)
;;;;    function-name  = symbol.
;;;;    argi           = symbol | number
;;;;    value          = symbol | number
;;;;
;;;; Notes
;;;; 1. Nested function applications are not allowed in world
;;;;    descriptions. They are allowed in goals, temporal goals, and
;;;;    actions.
;;;; 2. Even 0-ary predicates are lists.
;;;;
;;;; In order to distinguish between the different types of predicates
;;;; and functions the user must supply information about the symbols
;;;; used in the current domain. This is accomplished via various functions.
;;;; 
;;;;
;;;; There are 5 types of domain symbols that the user has to inform
;;;; the system about:
;;;;
;;;; 1. Described predicates: these are predicates for which we 
;;;;    maintain a list of all positive instances.
;;;; 2. Computed predicates: these are predicates whose truth is
;;;;    evaluated by calling a user defined lisp function.
;;;; 3. Defined predicates: these are predicates for which the user
;;;;    provides a definition by way of a first-order formula. This
;;;;    formula is interpreted in a manner that allows for recursive
;;;;    definitions.
;;;; 4. Described functions: these are functions for which we maintain
;;;;    a list of all function values. Functions values not on this
;;;;    list are assumed to be equal to a special *no-value*.
;;;; 5. Computed functions: these are functions that are evaluated by
;;;;    a user provided lisp function.
;;;;
;;;;-----------------------------------------------------------------------

;;;----------------------------------------------------------------------
;;; Structures for maintaining information about the symbols in the
;;; domain.
;;;
;;;----------------------------------------------------------------------
;;;
;;;  "symbol-info" structure holds information about the domain
;;;    predicate and function symbols.
;;;    
;;;    name      symbol name
;;;    type      predicate, function, or generator
;;;    artity    arity of predicate or function.
;;;    eval-type How evaluated, fintitely described?, computable?, defined?
;;;    eval-object Many symbols use this field to implement their evaluation.
;;;
;;;----------------------------------------------------------------------

(declare (integrate make-symbol-info 
		    symbol-info-name symbol-info-type
		    symbol-info-arity symbol-info-eval-type
		    symbol-info-eval-object
		    set-symbol-info-name! set-symbol-info-type!
		    set-symbol-info-arity! set-symbol-info-eval-type!
		    set-symbol-info-eval-object! copy-symbol-info
		    symbol-info?))

;;; Predicate

(define (symbol-info? x)
  (and (vector? x) (= 6 (vector-length x)) 
       (eq? 'symbol-info (vector-ref x 0))))

;;; Constructor

(define (make-symbol-info . keyword-args)
  (let ((name '()) (type '()) (arity '()) (eval-type '()) (eval-object '()))
    (do ()
	((null? keyword-args))
      (case (first keyword-args)
	(:name (set! name (cadr keyword-args)))
	(:type (set! type (cadr keyword-args)))
	(:arity (set! arity (cadr keyword-args)))
	(:eval-type (set! eval-type (cadr keyword-args)))
	(:eval-object (set! eval-object (cadr keyword-args)))
	(else (error "Illegal keyword: ~A" (first keyword-args))))
      (set! keyword-args (cddr keyword-args)))
    (vector 'symbol-info name type arity eval-type eval-object)))


;;; Selectors

(define (symbol-info-name si) (vector-ref si 1))
(define (symbol-info-type si) (vector-ref si 2))
(define (symbol-info-arity si) (vector-ref si 3))
(define (symbol-info-eval-type si) (vector-ref si 4))
(define (symbol-info-eval-object si) (vector-ref si 5))

;;; Modifiers

(define (set-symbol-info-name! si val) (vector-set! si 1 val))
(define (set-symbol-info-type! si val) (vector-set! si 2 val))
(define (set-symbol-info-arity! si val) (vector-set! si 3 val))
(define (set-symbol-info-eval-type! si val) (vector-set! si 4 val))
(define (set-symbol-info-eval-object! si val) (vector-set! si 5 val))

;;; Copier

(define copy-symbol-info vector-copy)

(define *world-symbols* (make-vector 0))
;;;A array of symbol-info structures, one for each domain symbol

(define *number-of-world-symbols* 0)
;;;The number of symbols used in these worlds

(define *number-of-described-symbols* 0)
;;;The number of symbols used in these worlds

(declare (integrate get-symbol-type get-symbol-name
		    get-symbol-arity get-symbol-eval-type get-symbol-index))

(define (get-symbol-type index)
  "Return the symbol-type (predicate or function) given symbol index"
  (symbol-info-type (vector-ref *world-symbols* index)))

(define (get-symbol-name index)
  "Return the symbol name given symbol index"
  (symbol-info-name (vector-ref *world-symbols* index)))

(define (get-symbol-arity index)
  "Return the arity of a symbol given symbol index"
  (symbol-info-arity (vector-ref *world-symbols* index)))

(define (get-symbol-eval-type index)
  "Return the eval-type of a symbol given symbol index"
  (symbol-info-eval-type (vector-ref *world-symbols* index)))

(define (get-symbol-eval-object index)
  "Return the eval-object of a symbol given symbol index"
  (symbol-info-eval-object (vector-ref *world-symbols* index)))

(define (put-symbol-type index type)
  "Change the symbol-type (predicate or function) given symbol index"
  (set-symbol-info-type! (vector-ref *world-symbols* index) type))

(define (put-symbol-name index name)
  "Change the symbol name given symbol index"
  (set-symbol-info-name! (vector-ref *world-symbols* index) name))

(define (put-symbol-arity index arity)
  "Change the arity of a symbol given symbol index"
  (set-symbol-info-arity! (vector-ref *world-symbols* index) arity))

(define (put-symbol-eval-type index eval-type)
  "Change the eval-type of a symbol given symbol index"
  (set-symbol-info-eval-type! (vector-ref *world-symbols* index) eval-type))

(define (put-symbol-eval-object index eval-object)
  "Change the eval-object of a symbol given symbol index"
  (set-symbol-info-eval-object! (vector-ref *world-symbols* index) 
				eval-object))

;;;----------------------------------------------------------------------
;;; Symbols are dealt with internally via their indicies. Each symbol
;;; is given a symbol index which is places on its property list.
;;;----------------------------------------------------------------------

(define (get-symbol-index symbol)
  "Return the index of a predicate or function symbol"
  (get symbol :world-index))

(define (put-symbol-index symbol i)
  "Set the index of a symbol"
  (put! symbol :world-index i))

;;;----------------------------------------------------------------------
;;; C. Functions for setting up the domain symbol information.
;;;----------------------------------------------------------------------

(define (clear-world-symbols)
  "Clean up the current world symbols"
  (do ((i 0 (+ 1 i)))
      ((>= i *number-of-described-symbols*))
    (put-symbol-index (get-symbol-name i) '()))
  (set! *world-symbols* (make-vector 0))
  (set! *number-of-world-symbols* 0)
  (set! *number-of-described-symbols* 0)
  (reset-tl-control)
  (reset-print-world-fn))

;;; 1 ;;;


(define (insert-symbol-info symbol type arity eval-type . optional-args)
  (let ((eval-object (if (null? optional-args)
			 '()
			 (first optional-args))))
    (put-symbol-index symbol *number-of-world-symbols*)
    (set! *world-symbols*
	  (apply vector 
		 (append! (vector->list *world-symbols*)
			  (list (make-symbol-info :name symbol
						  :type  type
						  :arity arity
						  :eval-type eval-type
						  :eval-object eval-object)))))
    (set! *number-of-world-symbols* (+ 1 *number-of-world-symbols*))
    (list (get-symbol-index symbol)
	  (vector-ref *world-symbols* (get-symbol-index symbol)))))

(define (def-described-symbols symbol-info-list)
  "Given a list of described symbols, set up the world-symbols
   information array. Symbol-info-list is a list of the form
   (name type[function|predictate] arity)"
  (if (not (eqv? *number-of-world-symbols* 0))
      (error "Described symbols must be defined first. Call 
            ~%(clear-world-symbols) and try again."))
  (do ((symbol-info-item '()))
      ((null? symbol-info-list))
    (set! symbol-info-item (first symbol-info-list))
    (set! symbol-info-list (rest symbol-info-list))
    (if (or (eqv? (second symbol-info-item) 'predicate)
	    (eqv? (second symbol-info-item) 'function))
	(insert-symbol-info
	 (first symbol-info-item) (second symbol-info-item)
	 (third symbol-info-item) 'DESCRIBED)
	(error "In def-described-symbols second item of symbol-info-item~
             ~%Should be one of the symbols ~S or ~S"
	       'predicate 'function)))
  (set! *number-of-described-symbols* (vector-length *world-symbols*)))

;;; 2 ;;;

(define (def-lisp-predicates symbol-list)
  "Given a list of ordinary lisp predicates, set them up so that they
   can be used by the formula evaluator."
  (for-each (lambda (symbol)
	      (let((symbol-fn (eval symbol (the-environment))))
		(insert-symbol-info
		 symbol 'PREDICATE 'UNKNOWN 'COMPUTED
		 (lambda (args world) 
		   (if (apply symbol-fn args) #t #f)))))
	    symbol-list))


;;; 3 ;;;


(define (def-lisp-fns symbol-list)
  "Given a list of ordinary lisp predicates, set them up so that they
   can be used by the formula evaluator."
  (for-each (lambda (symbol) 
	      (let((symbol-fn (eval symbol (the-environment))))
		(insert-symbol-info
		 symbol 'FUNCTION 'UNKNOWN 'COMPUTED
		 (lambda (args world) (apply symbol-fn args)))))
	    symbol-list))

;;; 4 ;;;

(define-macro (def-defined-predicate name parameters formula)
  `(insert-symbol-info
    ',name 'PREDICATE ,(length parameters) 'DEFINED
    (list ',parameters ',formula)))

;;; Accessors to defined predicate eval-object

(define (get-def-parameters df-eval-object)
  (first df-eval-object))

(define (get-def-formula df-eval-object)
  (second df-eval-object))

;;; 5 ;;;

(define (define-computed-function fn-name fn arity)
  "Setup a computed function"
  (insert-symbol-info
   fn-name 'FUNCTION arity 'COMPUTED
   (lambda (args world)
     (apply fn (append! args (list world))))))

(define-macro (def-computed-fn name parameters . body)
  `(begin
     (define (,name ,@parameters) ,@body)
     (define-computed-function ',name ,name ,(length parameters))))


;;; 7 ;;;  

(define (define-computed-predicate pred-name pred arity)
  "Setup a computed predicate"
  (insert-symbol-info
   pred-name 'PREDICATE arity 'COMPUTED
   (lambda (args world)
     (apply pred (append! args (list world))))))

(define-macro (def-computed-predicate name parameters . body)
  `(begin
     (define (,name ,@parameters) ,@body)
     (define-computed-predicate ',name ,name ,(length parameters))))

;;; 8 ;;;

(define (define-computed-generator gen-name gen arity)
  "Setup a computed generator"
  (insert-symbol-info
   gen-name 'GENERATOR arity 'COMPUTED
   (lambda (args world)
     (apply gen (append! args (list world))))))

(define-macro (def-generator name parameters . body)
  `(begin
     (define (,name ,@parameters) ,@body)
     (define-computed-generator ',name ,name ,(length parameters))))
  
;;;----------------------------------------------------------------------
;;; D. Some predicates on symbol, keyed by their indices
;;;----------------------------------------------------------------------

(define (predicate? index)
  (eq? (get-symbol-type index) 'PREDICATE))

(define (function? index)
  (eq? (get-symbol-type index) 'FUNCTION))

(define (generator? index)
  (eq? (get-symbol-type index) 'GENERATOR))

(define (computed? index)
  (eq? (get-symbol-eval-type index) 'COMPUTED))

(define (described? index)
  (eq? (get-symbol-eval-type index) 'DESCRIBED))

(define (defined? index)
  (eq? (get-symbol-eval-type index) 'DEFINED))

;;;;-----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>13 Interface
;;;;
;;;; Functions to handle the interface.
;;;;-----------------------------------------------------------------------

;;;-----------------------------------------------------------------------
;;; Interface with the planner.
;;;;
;;; 1. The search limit.


(define *search-limit* 100000)
;;;The number of nodes expanded by the planner.

(define (set-search-limit limit)
  "Set the number of nodes expanded by the planner."
  (set! *search-limit* limit))

(define (get-search-limit )
  "Return the planner's current search limit."
  *search-limit*)

(define (reset-search-limit )
  "Reset the search  limit to its default value."
  (set! *search-limit* 10000))

;;; 2. The search strategy.

(define search-strategy depth-first-priority)
(define (set-search-strategy strategy)
  "Set the search strategy to be used by the planner."
  (cond ((eqv? strategy 'depth-first-priority)
	 (set! search-strategy depth-first-priority))
	((eqv? strategy 'depth-first)
	 (set! search-strategy depth-first))
	((eqv? strategy 'breadth-first-priority)
	 (set! search-strategy breadth-first-priority))
	((eqv? strategy 'breadth-first)
	 (set! search-strategy breadth-first))
	((eqv? strategy 'best-first)
	 (set! search-strategy best-first))
	((eqv? strategy 'id-search)
	 (set! search-strategy id-search))
	(else 
	 (format #t "~%Search strategy must be one of the symbols:~
                    ~%depth-first-priority~
                    ~%breadth-first-priority~
                    ~%depth-first~
                    ~%breadth-first~
                    ~%best-first~
                    ~%id-search"))))

(define (get-search-strategy )
  "Return the current search strategy."
  search-strategy)

(define (reset-search-strategy )
  "Reset the search strategy to the default."
  (reset-priority-fn)
  (set! search-strategy depth-first-priority))

(define priority-fn  best-action)
(define (set-priority-fn fn)
  "Set the priority function. Either set to a previously defined fn.
     Or to a new function that must take a plan and return a
    numeric ranking indicating the merit of exploring this plan first."
  (cond ((procedure? fn)
	 (set! priority-fn fn))
	((eqv? fn 'best-action)
	 (set! priority-fn best-action))
	(else (format #t "%Priority function must be a function
                         or the symbol 'best-action"))))

(define (get-priority-fn )
  "Return the current priority function."
  priority-fn)

(define (reset-priority-fn )
  "Reset the priority function to its default."
  (set! priority-fn best-action))

(define cost-fn optimal-cost)
(define (set-cost-fn fn)
  "Set the cost function used by best first search.
     Either set to a previously defined fn (via a symbolic name).
     Or to a cost function that evaluates the cost of plan."
  (cond ((procedure? fn)
	 (set! cost-fn fn))
	((eqv? fn 'optimal-cost)
	 (set! cost-fn optimal-cost))
	(else (format #t "%Cost  function must be a function 
                        ~%or the symbol 'optimal-cost"))))

(define (get-cost-fn)
  "Return the current cost function used by the planner."
  cost-fn)

(define (reset-cost-fn )
  "Reset the cost function to its default."
  (set! cost-fn optimal-cost))

(define id-initial-depth 2)
(define id-depth-increment 2)
(define (set-id-initial-depth depth)
  "Set the initial search depth for id-search."
  (set! id-initial-depth depth))

(define (set-id-depth-increment incr)
  "Set the depth increment for id-search."
  (set! id-depth-increment incr))

(define (reset-id-search-parameters )
  "Reset the id-search parameters to their defaults."
  (set! id-initial-depth 2)
  (set! id-depth-increment 2))

(define (get-id-initial-depth )
  "Return the current initial search depth for id-search."
  id-initial-depth)

(define (get-id-depth-increment )
  "Return the current search depth increment for id-search."
  id-depth-increment)

;;; 3. Set the type of goal
;;;    By classic goals I mean a list of positive literals to be
;;;    achieved.
;;;    To check for such goals, we can construct a goal world (used to
;;;    evaluate goal modalities), and set "final-world-goal?" to
;;;    simply evaluate the conjunction  of the goal literals in the
;;;    world. 
;;;    Later on we have to do other things for different types of goals.

(define (final-world-goal? tlform world/action)
    "This symbols is set to a function that tests if a world
     is a goal world."
    #f)

(define (process-classic-goal goal-list)
  "This function set up the planner to find a classic conjunctive goal."
  (create-goal-world/action  goal-list)
  (set! final-world-goal?
	(lambda (tlform world/action)
	  (eval-formula `(and ,@goal-list) world/action '()))))

;;;
;;; MTL extension. Goal formulas are dealt with by labeling the
;;; initial world with them and progressing through all worlds
;;; generated. To test completion we see if the formula will be
;;; satisfied by a final world that idles.
;;; The function that does this is part of the progress-formula code.
;;;

(define (process-extended-goal goal-formula)
  "This function sets up the plan to find a temporally extended goal."
  (set-tl-control goal-formula)
  (set! final-world-goal? (lambda (tlform world/action)
			    (idle-formula tlform world/action '()))))

;;; 4. Set the components for a planning problem.
;;;
  
(define process-goal process-classic-goal)
(define initial-world/action '())
(define goal-list '())
(define initial-time 0)
(define goal-type 'classic)
(define plan= plan-classic=)
(define tlform '(always (TRUE)))        ;This provides no search control.

(define (set-goal-type type)
  "Set the type of goal being planned for."
  (cond
   ((eq? type 'classic)
    (set! goal-type 'classic)
    (set! plan= plan-classic=)
    (set! process-goal process-classic-goal))
   ((eq? type 'extended)
    (set! goal-type 'extended)
    (set! plan= plan-extended=)
    (set! process-goal process-extended-goal))
   (else 
    (format  #t "~%Only classic and extended goals are implemented so far, 
                  ~%setting to classic by  default.")
    (set! process-goal process-classic-goal))))

(define (get-goal-type )
  "Return the goal type."
  goal-type)

(define (set-goal goal)
  "Set the current goal for the planner."
  (set! goal-list goal)
  (process-goal goal)
  goal-list)

(define (get-goal )
  "Return the goal"
  goal-list)

(define (set-initial-time time)
  (set! initial-time time))

(define (reset-initial-time )
  (set! initial-time 0))

(define (get-initial-time )
  initial-time)

(define (set-initial-world  world-list)
  "Set the current initial world for the planner."
  (set! initial-world/action
	(make-world/action (create-world world-list) '() 0 0 0))
  world-list)

(define (set-tl-control formula)
  "Set the temporal control formula to be used by the planner."
  (set! tlform formula))

(define (get-initial-world )
  "Return the initial world of the current planning problem."
  initial-world/action)

(define (get-tl-control )
  "Return the temporal  control formula being used by the planner."
  tlform)

(define (reset-tl-control )
  "Set the temporal control formula to be no search control."
  (set! tlform '(always (TRUE))))

;;; 5. Invoke the planner.

(define (plan)
  "Invoke the planner on current world, goal"
  (tlplanner (get-initial-world) (get-tl-control) (get-search-strategy)
             (get-priority-fn) (get-cost-fn)))

;;; 6. Trace control.


(define (set-trace-level i)
  "Set the trace level."
  (set! *trace* i))

(define (get-trace-level )
  "Return the current trace level."
  *trace*)

;;;  7. Output control.

(define print-world default-print-world)

(define (set-print-world-fn fn)
  "Set the world print function used during tracing etc."
  (set! print-world fn))

(define (reset-print-world-fn )
  "Reset the world print function to its default."
  (set! print-world default-print-world))

;;; 8. Domains
;;; Functions to load various domains.
;;; Later the function should do various forms of clean up and initializing.
;;; And allow for the running of various planning problems.
;;;

(define *domains* '())
;;;This holds a list of domains.

(define (reset-domains )
  "Reset the known domains to '()"
  (set! *domains* '()))

(define (def-domain domain-name file-list description)
  "Add a domain to the list of domains *domains*"
  (set! *domains* (cons (list domain-name file-list description) *domains*)))

(define (list-domains)
  "Print out a list of the known domains."
  (format #t "~%The known domains are")
  (for-each (lambda (domain)
	      (format #t "~%~@20S , ~A" (first domain) (third domain)))
	    *domains*))

(define (load-domain . optional-args)
  "Load the appropriate files for the domain"
  (let ((domain-name
	 (if (null? optional-args)
	     '()
	     (first optional-args))))
    (let ((domain
	   (find domain-name *domains*
		 :test (lambda (name domain)
			 (eqv? name (first domain))))))
      (if domain
	  (for-each (lambda(file) (load file)) (second domain))
	  (begin
	    (format #t "~%Unknown domain ~S." domain-name)
	    (list-domains))))))

(define (compile-domain . optional-args)
  "Compile the appropriate files for the domain"
  (let ((domain-name (if (null? optional-args)
			 '()
			 (first optional-args))))
    (if (not (null? optional-args))
	(begin (set! stream (first optional-args))
	       (set! optional-args (rest optional-args))))
    (let ((domain (find domain-name *domains*
			:test (lambda (name domain)
				(eqv? name (first domain))))))
      (if domain
	  (for-each (lambda(file) (compile-file file)) (second domain))
	  (begin
	    (format #t "~%Unknown domain ~S." domain-name)
	    (list-domains))))))

(define (compile-all-domains )
  "Compile all of the known domains"
  (for-each (lambda(domain)
		(for-each (lambda (file) (compile-file file))
			  (second domain)))
	    *domains*))

;;;
;;; 9. The trace function.
;;;

(define *trace* 0)
;;;Trace level

(define *verbose* #t)
;;;The planner should be verbose?

(define (verbose-on )
  (set! *verbose* #t))

(define (verbose-off )
  (set! *verbose* #f))

(define *trace-stream* #t)
;;;The output stream for trace information.

;;; Put an inline interface so that a function call is not required if
;;; we have tracing turned off.
;;;

(define (tl-tracer key data)
  (if (not (= 0 *trace*))
      (function-tracer key data)))

(define (function-tracer key data)
  (cond
   ((eq? key 'plan-successors)
    (format *trace-stream*
            "~%~%Expanding world at depth ~S:"
            (plan-length (first data)))
    (print-world (plan-world/action (first data)) *trace-stream*)
    (format *trace-stream* 
            "~%This world was obtained by the action: ~S"
            (plan-action-name (first data)))
    (if (second data)
        (format *trace-stream*
                "~%Progression successful, generating world successors.")
      (format *trace-stream*
              "~%Progression FAILED, pruning world."))
    (if (and (>= *trace* 2) (second data))
	(begin
	  (fluid-let ((*unparser-list-breadth-limit* #f)
		      (*unparser-list-depth-limit* #f))
	    (format *trace-stream* "~%Progressed temporal formula is:~%")
	    (pp (second data) *trace-stream*)
	    (format *trace-stream* "~%Current component is:~%")
	    (pp (cc (second data)) *trace-stream*))))
    (if (and (>= *trace* 3) (second data))
	(begin 
	  (format *trace-stream*
		  "~%Number of successor worlds = ~S."
		  (length (third data)))
	  (for-each (lambda (plan)
		      (format *trace-stream*
			      "~%Action: ~S"
			      (plan-action-name plan))
		      (print-world (plan-world/action plan) *trace-stream*)
		      (format *trace-stream*  "~%"))
		    (third data)))))
   (else #t)))

;;;;-----------------------------------------------------------------------
;;;;                                                                       
;;;;>>>14 Interval Specs.
;;;;
;;;; Functions to handle interval specs.
;;;;-----------------------------------------------------------------------
;;;
;;; Internally interval specs are all represented by four element lists.
;;; ("<|>" number number+ "<|>")
;;; number is the lower bound of the interval. This number should be
;;; greater than 0. number+ is the upper bound of the interval or the 
;;; special symbol inf+ (indicating plus infinity). The square bracket
;;; < is used to indicate that the bound is included in the interval, 
;;; > is used to indicate that the bound is not included in the interval.
;;;
;;; E.G. < 5 6 >  == <5,6>
;;;      > 5 inf+ == > 5
;;;

(define ispec-inf 'inf+)

(define (is-infinity number+)
  (if (eq? number+ ispec-inf) #t #f))

(define (ispec- number+ delta)
  (if (is-infinity number+) ispec-inf (- number+ delta)))

(define (ispec< number1 number2)
  (or
   (and (number? number1) (number? number2) (< number1 number2))
   (and (is-infinity number2) (number? number1))))

(define (ispec> number1 number2)
  (or
   (and (number? number1) (number? number2) (> number1 number2))
   (and (is-infinity number1) (number? number2))))


(define (ispec= number1 number2)
  (or (and (number? number1) (number? number2) (= number1 number2))
      (and (is-infinity number1) (is-infinity number2))))

(define (ispec-lshift ispec delta)
  "Compute a new ispec shifted to the left by delta; i.e., ispec - delta."
  (let ((lb (ispec- (second ispec) delta))
        (ub (ispec- (third ispec) delta)))
    (list (first ispec) lb ub (fourth ispec))))

(define (ispec<0 ispec)
  "Test if ispec has timed out, i.e. ispec < 0."
  (or (ispec< (third ispec) 0) 
      (and (ispec= 0 (third ispec)) (eq? (fourth ispec) '<))))

(define (ispec0in ispec)
  "Test if ispec overlaps 0."
  (or (and (ispec< (second ispec) 0) (ispec> (third ispec) 0))
      (and (ispec= 0 (second ispec)) (eq? (first ispec) '<))
      (and (ispec= 0 (third ispec)) (eq? (fourth ispec) '>))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Load the setup file
;;; 

(load (string-append *system-directory* *.rc-file*))


