(in-package :vag)

;========================================================================
;computation tests for primitives
;========================================================================

(defun number-test0 ()
  (clear-data-base)
  (list (value-of '(+ 1 2))
	(value-of '(- 5 2))
	(value-of '(/ 6 2))
	(value-of '(* .5 6.0))))

(defun number-test1 ()
  (clear-data-base)
  (list (value-of '(> 2 1))
	(value-of '(>= 2 1))
	(value-of '(>= 2 2))
	(value-of '(< 1 2))
	(value-of '(<= 1 2))
	(value-of '(<= 2 2))))

(defun number-test2 ()
  (clear-data-base)
  (list (value-of '(< 2 2))
	(value-of '(< 2 1))
	(value-of '(<= 3 2))
	(value-of '(> 1 2))
	(value-of '(> 2 2))
	(value-of '(>= 2 3))))

(defun boolean-test0 ()
  (clear-data-base)
  (list (value-of '(true))
	(value-of '(and (true) (true)))
	(value-of '(or (true) (false)))
	(value-of '(or (false) (true)))
	(value-of '(or (true) (true)))
	(value-of '(not (false)))))

(defun boolean-test1 ()
  (clear-data-base)
  (list (value-of '(false))
	(value-of '(or (false) (false)))
	(value-of '(and (true) (false)))
	(value-of '(and (false) (true)))
	(value-of '(and (false) (false)))
	(value-of '(not (true)))))

(defun equality-test0 ()
  (clear-data-base)
  (list (value-of '(= 1 1))
	(value-of '(= 'a 'a))
	(value-of '(=
		    (cons 'a (nil))
		    (cons 'a (nil))))))

(defun equality-test1 ()
  (clear-data-base)
  (list (value-of '(= 1 2))
	(value-of '(= 'a 'b))
	(value-of '(=
		    (cons 'a (nil))
		    (cons 'b (nil))))))

(defun if-test0 ()
  (clear-data-base)
  (list (value-of '(if (true) 'a 'b))
	(value-of '(if (false) 'a 'b))))

(defvar p boolean)

(define (loop)
  (if p 1 (loop)))

(defun if-test1 ()
  (value-of '(loop)))
	
(defun cons-test0 ()
  (clear-data-base)
  (list (value-of '(nil))
	(value-of '(cons 'a (nil)))
	(value-of '(car (cons 'a (nil))))
	(value-of '(cdr (cons 'a (nil))))))

(defun null-test0 ()
  (clear-data-base)
  (list (value-of '(null? (nil)))
	(value-of '(null? (cons 'a (nil))))))

(defun member-test0 ()
  (clear-data-base)
  (list (value-of '(member? 'a (nil)))
	(value-of '(member? 'a (cons 'b (nil))))
	(value-of '(member? 'a (cons 'b (cons 'a (nil)))))))

(defun append-test0 ()
  (clear-data-base)
  (value-of '(append (cons 'a (nil)) (cons 'b (nil)))))

(defun map-test0 ()
  (clear-data-base)
  (value-of '(map (lambda (n) (+ n 1)) (list 1 2 3))))


;========================================================================
;examples from the manual
;========================================================================

(define (foo (n fixnum))
  (if (not (= n n))
      n
      (foo n)))

;;the following is not accepted because an inability to infer the type of foo.
;;
;;(define (foo (n fixnum))
;;  (foo n))

(defstruct drawer
  (drawer-height number)
  (drawer-width number)
  (drawer-depth number))

(defun defstruct-test0 ()
  (clear-data-base)
  (list (value-of '(make-drawer 1 2 3))
	(value-of '(drawer-depth (make-drawer 1 2 3)))))

(define (make-drawers (width number) (depth number) (heights (list-of number)))
  (if (null? heights)
      (nil)
      (cons (make-drawer (car heights) width depth)
	    (make-drawers width depth (cdr heights)))))

(defun make-drawers-test ()
  (clear-data-base)
  (value-of '(make-drawers 1 2 (list 3 4))))

(defstruct (drawer-with-trim (subtype-of drawer))
  (drawer-trim-width number))

(defun trim-test ()
  (clear-data-base)
  (list (value-of '(make-drawer 1 2 3))
	(value-of '(make-drawer-with-trim 1 2 3 4))))

(defblock
  (defvar h number)
  (defvar w number)
  (defvar d number))

(defun context-test ()
  (clear-data-base)
  (goto-context '((consider-expression (make-drawer h w d)) (= d 3))))

;;the following shows type inference through forward references inside
;;bocks

(defblock

  (defstruct (dresser
	       (with-constraint
		   (and (= (sum (map (lambda (x) (drawer-height x))
				     (dresser-drawers self)))
			   (- (dresser-height self) 10))
			(every (map (lambda (drawer)
				      (= (drawer-width drawer)
					 (- (dresser-width self) 5)))
				    (dresser-drawers self))))))
    (dresser-width number)
    (dresser-height number)
    (dresser-drawers (list-of drawer)))

  (define (sum (l (list-of number)))
    (if (null? l)
	0
	(+ (car l) (sum (cdr l)))))

  (define (every (l (list-of boolean)))
    (if (null? l)
	(true)
	(and (car l) (every (cdr l))))))

(defblock
  (defvar w number)
  (defvar h1 number)
  (defvar w1 number)
  (defvar w2 number)
  (defvar d number))

(defun inftest0 ()
  (clear-data-base)
  (goto-context '((consider-expression
		   (make-dresser w 50
		    (list (make-drawer h1 w1 d)
			  (make-drawer 15 w2 d)
			  (make-drawer 15 30 d))))))
  (list (value-of 'w) (value-of 'h1) (value-of 'w1) (value-of 'w2) (value-of 'd)))

(defun proveall ()
  (dolist (test '(number-test0 number-test1 number-test2
		  boolean-test0 boolean-test1
		  equality-test0 equality-test1
		  if-test0 cons-test0 null-test0 member-test0
		  append-test0 map-test0
		  defstruct-test0 make-drawers-test
		  trim-test inftest0))
    (rprint (funcall test)))
  t)


(define (foo (x number))
  (+ x 1))

(defvar x number)