;;; beta-reduction and friends

(define beta                            ; term -> tac
  (lambda (m)
    (if (and (app? m)
             (abs? (app->rator m)))
      (let ((rator (app->rator m))
            (rand (app->rand m)))
        (succeed
          (subst1 (abs->body rator) rand (abs->bv rator))))
      (fail))))

;  old version-- call to (tacfn m) is in the wrong place!
; (define leftmost                        ; (term->tac) -> (term->tac)
;   (lambda (tacfn)
;     (lambda (m)
;       (let leftmost-loop ((m m))
;         ;; find leftmost place in m where tac applies, and apply it,
;         ;; rebuilding the term around the result
;         (record-case m
;           (app (rator rand)
;                (or-else*
;                  (tacfn m)
;                  (and-then
;                    (leftmost-loop rator)
;                    (lambda (rator1)
;                      (succeed (make-app rator1 rand))))
;                  (and-then
;                    (leftmost-loop rand)
;                    (lambda (rand1)
;                      (succeed (make-app rator rand1))))))
;           (abs (bv body)
;                (and-then
;                  (leftmost-loop body)
;                  (lambda (body)
;                    (succeed (make-abs bv body)))))
;           (else (fail)))))))


(define leftmost                        ; (term->tac) -> (term->tac)
  (lambda (tacfn)
    (lambda (m)
      ;; find leftmost place in m where tac applies, and apply it,
      ;; rebuilding the term around the result
      (let leftmost-loop ((m m))
        (or-else
          (tacfn m)
          (record-case m
            (app (rator rand)
                 (or-else
                   (and-then
                     (leftmost-loop rator)
                     (lambda (rator1)
                       (succeed (make-app rator1 rand))))
                   (and-then
                     (leftmost-loop rand)
                     (lambda (rand1)
                       (succeed (make-app rator rand1))))))
            (abs (bv body)
                 (and-then
                   (leftmost-loop body)
                   (lambda (body)
                     (succeed (make-abs bv body)))))
            (else (fail))))))))


(define leftmost-beta-with-trace
  (repeat
    (lambda (m)
      (and-then
        ((leftmost beta) m)             ; : tac
        print-it))))                    ; : val->tac

(define leftmost-beta
  (repeat (leftmost beta)))

(define leftmost-beta-with-trace
  (repeat (trace-tac (leftmost beta))))

(define test-beta-with-trace
  (lambda (term)
    (run-tac 
      (leftmost-beta-with-trace (parse term))
      unparse
      'failed)))

(define test-beta
  (lambda (term)
    (run-tac (leftmost-beta (parse term))
      unparse
      'failed)))