;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Examples of features that can be used in defining domains.
;;;
;;; Generators. These should take at least a world as an argument.
;;; They can optionally take n-arguments which proceed the world
;;; argument. They should return a generator function. This is a
;;; function of no arguments which on succesive calls returns a LIST.
;;; This list will be used to bind the variables of the quantified
;;; formula. The length of the LIST must be at least as long as the
;;; variable list in the formula where the generator is used.
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Example 1
;;; 1. Clear all world symbols.

(clear-world-symbols)

;;; 2. set up so that we can use the standard lisp predicates

(def-lisp-predicates '(< = >))

;;; 3. define an integer generator. This could be used in an exists
;;;    formula, with no guarantee of termination. In a forall formula
;;;    it definitely will not terminate. Notice: it takes no other
;;;    arguments besides the world. It returns a function of no
;;;    arguments which returns a list of one integer (the next one).  

(def-generator pos-int (world)
   (let ((start -1))
    (lambda () (set! start (+ start 1)) (list start))))

;;; 4. Now we can evaluate.
;;;    This returns T. Note that because we don't have any described
;;;    predicates in the formula we don't need a world structure. Also
;;;    bindings are intially set to nil.

(eval-formula '(exists (?i) (pos-int) (= ?i 10 )) '() '())

;;; 5. To really see what is happening we define a print function for
;;; the binding of ?i

(define (pr world bindings)
  (pp (lookup-var '?i bindings)))

;;; 6. Now we can invoke the evaluator again with a call to call the
;;; print function. Notice, that the call requires an actual function
;;; object as its argument. So we have to use a backquote and , to get
;;; it into the list. 

 (eval-formula `(exists (?i) (pos-int)
			(and (call ,pr) (= ?i 10 ))) '() '())

;;;  this returns

1 
2 
3 
4 
5 
6 
7 
8 
9 
10 
#t

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Example 2. A generator that takes an argument.
;;; It generates all positive integers less than i.

(def-generator <-pos-int (i world)
  (let ((start i))
    (lambda ()
      (if (< start 1)
	  '()
          (begin (set! start (- start 1)) (list start))))))

;;; Now if we evaluate

(eval-formula `(forall (?i) (<-pos-int 20) (call ,pr)) '() '())

;;; we get 
19 
18 
17 
16 
15 
14 
13 
12 
11 
10 
9 
8 
7 
6 
5 
4 
3 
2 
1 
0 
#t

