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

(define compiler-rules
  '((('compiler ('sum e1 e2) t)
     ('compiler e1 ('compiler e2 ('add-inst t))))))

(define machine-denotation-rules
  '((('target-semantics ('add-inst t) r z)
     ('add-cps ('cadr z) ('car z)
       (lambda (v) ('target-semantics t r ('cons v ('cddr z))))))))

(define source-semantics-rules
  '((('source-meaning ('sum e1 e2) r k)
     ('source-meaning e1 r
       (lambda (v1)
         ('source-meaning e2 r (lambda (v2) ('add-cps v1 v2 k))))))))

(define list-rules
  '((('car ('cons a d)) a)
    (('cadr ('cons a1 ('cons a2 dd))) a2)
    (('cddr ('cons a1 ('cons a2 dd))) dd)))

(define lhs 
  (lambda (pgm)
    `('target-semantics ('compiler ,pgm t) r z)))

(define rhs
  (lambda (pgm)
    `('source-meaning ,pgm r (lambda (v) (('target-semantics t) r ('cons v z))))))

(define ih
  (lambda (pgm)
    (list (lhs pgm) (rhs pgm))))

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

(define proof-tac
  (lambda ()
    (repeat
      (or-else-use*
        (report-tac "beta" (leftmost beta))
        (report-tac "definition of compiler"  (rules->tac compiler-rules))
        (report-tac "definition of T"   (rules->tac machine-denotation-rules))
        (report-tac "definition of E"   (rules->tac source-semantics-rules))
        (report-tac "list operations" (rules->tac list-rules))
        (report-tac "ih at e1"        (rules->tac (list (ih 'e1))))
        (report-tac "ih at e2"        (rules->tac (list (ih 'e2))))
        ))))

(define prove-it
  (lambda (pgm)
    (let* ((dummy1 (printf "~%Reducing left-hand side...~%"))
           (d2 (pretty-print (lhs pgm)))
           (lhs (test-tacfn (lhs pgm) (proof-tac)))
           (dummy (printf "~%Reducing right-hand side...~%"))
           (d3 (pretty-print (rhs pgm)))
           (rhs (test-tacfn (rhs pgm) (proof-tac))))
      (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 test-it
  (lambda ()
    (prove-it '('sum 'e1 'e2))))