;;; rules for compiler, machine, evaluator, etc.

(define compiler-rules
  '((('compile ('var-ref x) p)
     ('fetch x p))
    (('compile ('sum e1 e2) p)
     ('compile e1 ('compile e2 ('add-inst p))))))

(define machine-rules
  '((('add-inst p u
       ('cons v2 ('cons v1 z)) k)
     (p u ('cons ('plus v1 v2) z) k))))

(define eval-rules
  '((('eval ('sum e1 e2) r k)
     ('eval e1 r
       (lambda (v1)
         ('eval e2 r (lambda (v2) (k ('plus v1 v2)))))))))

(define lhs 
  (lambda (pgm)
    `('compile ,pgm pi u z k)))

(define rhs
  (lambda (pgm)
    `('eval ,pgm u (lambda (v) (pi u ('cons v z) k)))))

(define ih
  (lambda (pgm)
    `(('compile ',pgm pi u z k)
      ('eval ',pgm u (lambda (v) (pi u ('cons v z) k))))))

(define rules->tac
  (lambda (rules) (leftmost (rewrite-rules (parse-rules rules)))))

(define tacfn2
  (lambda ()
    (repeat
      (or-else-use*
        (report-tac "beta" (leftmost beta))
        (report-tac "compiler rules"  (rules->tac compiler-rules))
        (report-tac "machine rules"   (rules->tac machine-rules))
        (report-tac "eval rules"      (rules->tac eval-rules))
        (report-tac "ih at e1"        (rules->tac (list (ih 'e1))))
        (report-tac "ih at e2"        (rules->tac (list (ih 'e2))))
        ))))

(define prove2
  (lambda (pgm)
    (let* ((dummy1 (printf "~%Reducing left-hand side...~%"))
           (d2 (pretty-print (lhs pgm)))
           (lhs (test-tacfn (lhs pgm) (tacfn2)))
           (dummy (printf "~%Reducing right-hand side...~%"))
           (d3 (pretty-print (rhs pgm)))
           (rhs (test-tacfn (rhs pgm) (tacfn2))))
      (printf "~%lhs reduces to:~%")
      (pretty-print lhs)
      (printf "~%rhs reduces to:~%")
      (pretty-print rhs)
      ;; who's unparsing these?  probably test-tacfn.  Let's just
      ;; reparse them for now.
      (printf "~%checking for alpha-congruence...  ")
      (alpha-congruent? (parse lhs) (parse rhs) '() '()))))
        
(define test2
  (lambda ()
    (prove2 '('sum 'e1 'e2))))


(define prove3
  (lambda (pgm1 pgm2 tacfn2)
    (let* ((dummy1 (printf "~%Reducing left-hand side...~%"))
           (d2 (pretty-print pgm1))
           (lhs (test-tacfn pgm1 (tacfn2)))
           (dummy (printf "~%Reducing right-hand side...~%"))
           (d3 (pretty-print pgm2))
           (rhs (test-tacfn pgm2 (tacfn2))))
      (printf "~%lhs reduces to:~%")
      (pretty-print lhs)
      (printf "~%rhs reduces to:~%")
      (pretty-print rhs)
      ;; who's unparsing these?  probably test-tacfn.  Let's just
      ;; reparse them for now.
      (printf "~%checking for alpha-congruence...  ")
      (alpha-congruent? (parse lhs) (parse rhs) '() '()))))


(define tacfn3
  (lambda ()
    (repeat
      (or-else-use*
        (report-tac "top-eta" (rules->tac '(((lambda (x) (k x)) k))))
        ))))


(define tacfn4
  (lambda ()
    (or-else-use*
      (report-tac "top-eta" (rules->tac '(((lambda (x) (k x)) k)))))))