;; Aufbau des Beweisbaums

(define proof-stack ())

(define proof-push
  (lambda (rule)
    (set! proof-stack (cons rule proof-stack))))

(define proof-stack-to-tree
  (lambda ()
    (let ((rule (car proof-stack)))
      (begin
	(set! proof-stack (cdr proof-stack))
	(case rule
	  ((var lit abs)
	   rule)
	  ((if-f if-t op)
	   (let ((subtree2 (proof-stack-to-tree)))
	     (let ((subtree1 (proof-stack-to-tree)))
	       (list rule subtree1 subtree2))))
	  ((app)
	   (let ((subtree3 (proof-stack-to-tree)))
	     (let ((subtree2 (proof-stack-to-tree)))
	       (let ((subtree1 (proof-stack-to-tree)))
		 (list rule subtree1 subtree2 subtree3))))))))))

;; Transitionsregeln

(define literal?
  (lambda (a)
    (or (integer? a) (boolean? a))))
(define interpret-literal
  (lambda (a u)
    (proof-push 'lit)
    a))

(define variable? ...)
(define interpret-variable ...)

(define conditional? ...)
(define interpret-conditional ...)

(define abstraction? ...)
(define interpret-abstraction ...)

(define application? ...)
(define interpret-application ...)

;; Hauptfunktionen

(define interpret
  (lambda (a u)
    (cond ((literal?     a) (interpret-literal     a u))
	  ((variable?    a) (interpret-variable    a u))
	  ((conditional? a) (interpret-conditional a u))
	  ((abstraction? a) (interpret-abstraction a u))
	  ((application? a) (interpret-application a u))
	  (else
	   (error "illegal expression syntax")))))

(define global-environment
  (list (cons '+ (lambda (x) (lambda (y) (+ x y))))
	(cons '- (lambda (x) (lambda (y) (- x y))))
	(cons '* (lambda (x) (lambda (y) (* x y))))
	(cons '< (lambda (x) (lambda (y) (< x y))))))

(define start
  (lambda (a)
    (set! proof-stack ())
    (let ((res (interpret a global-environment)))
      (list res (proof-stack-to-tree)))))