(herald boyer (env tsys) (syntax-table (*value orbit-env 'primop-syntax-table)))

#|
(define-local-syntax (future exp)
  `(if (inline? 1)
       ,exp
       (*future (lambda () ,exp))))

(define-constant inline?
  (primop inline? ()
    ((primop.test-code self node #f)
     (destructure (((then else #f #f #f) (call-args node)))
	 (emit n32/cmpi d ($ 50) (reg-offset cpu cpu/queue-length))
	 (emit-jump jump-op/j< then else)))
    ((primop.presimplify self node)
     (presimplify-predicate node))
    ((primop.type-predicate? self) t)
    ((primop.type self node)
     '#[type (proc #f (proc #f boolean) top)])
    ((primop.predicate-type self node)
     '#[type (proc #f (proc #f) (proc #f) top top top)])))
|#

(define (test)
  (taut?
        (apply-subst
         (quote ((x f (plus (plus a b)
                            (plus c (zero))))
                 (y f (times (times a b)
                             (plus c d)))
                 (z f (reverse (append (append a b)
                                       (nil))))
                 (u equal (plus a b)
                          (difference x y))
                 (w lessp (remainder a b)
                          (member a (length b)))))
         (quote (implies (and (implies x y)
                              (and (implies y z)
                                   (and (implies z u)
                                        (implies u w))))
                         (implies x w))))))

(define true 1)
(define false nil)

; Tautology detection checks forms (if predicate consequent alternate)
;	If the predicate is known true then we just check the consequent
;	If the predicate is known false then we just check the alternate
;	Otherwise we see if the consequent is true assuming the predicate is true
;	and that the alternate is true assuming the predicate is false

(define (taut? form)
  (tautology? (rewrite form) () ()))

(define (tautology? form true-list false-list)
  (cond ((known-true? form true-list) true)
	((known-false? form false-list) false)
	((eq? (car form) 'if)
	 (cond ((known-true? (cadr form) true-list)
		(tautology? (caddr form) true-list false-list))
	       ((known-false? (cadr form) false-list)
		(tautology? (cadddr form) true-list false-list))
	       (else
		(let ((temp (future (tautology? (cadddr form) true-list (cons (cadr form)
				      false-list)))))
		  (and
		   (tautology? (caddr form) (cons (cadr form) true-list)
			       false-list)
		   temp)))))
	(else false)))

(define (known-true? form true-list)
  (if (equal? form '(t))
      true
      (member form true-list)))

(define (known-false? form false-list)
  (if (equal? form '(f))
      true
      (member form false-list)))


; Rewriting matches a form against the list of lemmas associated with the car
;	of the form and first rewrites the remainder of the form before
;	finding the first lemma which matches and expanding it accordingly.

(define (rewrite form)
  (if (atom? form)
      form
      (rewrite-with-lemmas (cons (car form) (rewrite-args (cdr form)))
			     (get (car form) 'lemmas))))

(define (rewrite-args args)
  (if (null? args)
      ()
      (cons (future (rewrite (car args))) (rewrite-args (cdr args)))))

(define (rewrite-with-lemmas form lemmas)
  (if (null? lemmas)
      form
      (let ((subst-list (one-way-unify-util form (cadr (car lemmas)) ())))
	(if (not (eq? subst-list 'failed))
	    (rewrite (apply-subst subst-list (caddr (car lemmas))))
	    (rewrite-with-lemmas form (cdr lemmas))))))

; Weak unificiation works by a recursive pattern match.

(define (one-way-unify-util form pattern frame)
  (cond ((eq? frame 'failed) 'failed)
	((atom? pattern)
	 (let ((already-matched (assq pattern frame)))
	   (cond (already-matched		; if matched verify rematch
		  (if (equal? form (cdr already-matched)) frame 'failed))
		 (else
		  (cons (cons pattern form) frame)))))
	((atom? form) 'failed)
	((eq? (car form) (car pattern))
	 (one-way-unify-list (cdr form) (cdr pattern) frame))
	(else 'failed)))

(define (one-way-unify-list form pattern frame)
  (if (null? form)
      frame
      (one-way-unify-list (cdr form) (cdr pattern)
			  (one-way-unify-util (car form) (car pattern) frame))))

; Very simple substituter used by rewrite with the result of the unification.

(define (apply-subst subst-list form)
  (if (atom? form)
      (let ((value (assq form subst-list)))
	(if value (cdr value) form))
      (cons (car form) (apply-subst-list subst-list (cdr form)))))

(define (apply-subst-list subst-list form)
  (if (null? form)
      ()
      (cons (future (apply-subst subst-list (car form)))
	    (apply-subst-list subst-list (cdr form)))))