#lang scheme

(require scheme/match test-engine/scheme-tests)

;; Exp[X] = X | (λ Symbol Exp) | (Exp Exp)

;; db : Exp[Symbol] -> Exp[Nat]
;; assume: e is closed 

(check-expect (db '(λ x x)) '(λ x 0))
(check-expect (db '(λ x (x x))) '(λ x (0 0)))
(check-expect (db '(λ x (λ y (x x)))) '(λ x (λ y (1 1))))
(check-expect (db '(λ x (λ y (y x)))) '(λ x (λ y (0 1))))
(check-expect (db '(λ x (x (λ y (y x))))) '(λ x (0 (λ y (0 1)))))

;; -----------------------------------------------------------------------------
;; structural design with accumulator 
(define (db.v0 e0)
  ;; Exp[Symbol] [Listof Symbol] -> Exp[Nat]
  ;; accumulator: env the list of symbols seen between e and e0
  (define (db e env)
    (match e
      [(? symbol? e) (depth e env)]
      [`(λ ,(? symbol? X) ,Body) `(λ ,X ,(db Body (cons X env)))]
      [`(,Fun ,Arg) `(,(db Fun env) ,(db Arg env))]))
  ;; Symbol [Listof Symbol] -> Nat 
  (define (depth s env)
    (cond
      [(empty? env) (error 'db "can't happen: ~s" s)]
      [(eq? (first env) s) 0]
      [else (+ 1 (depth s (rest env)))]))
  (db e0 '()))

;; -----------------------------------------------------------------------------
;; structural design 
(define (db e0)
  ;; Exp[Symbol] -> Exp[(list Nat Symbol)]
  (define (db e)
    (match e
      [(? symbol? e) (list -1 e)]
      [`(λ ,(? symbol? X) ,Body) `(λ ,X ,(push-not-X X (db Body)))]
      [`(,Fun ,Arg) `(,(db Fun) ,(db Arg))]))
  ;; Symbol Exp[(list Nat Symbol)] -> Exp[(list Nat Symbol)]
  (define (push-not-X y e)
    (match e
      [`(,(? integer? n) ,(? symbol? e)) (if (eq? e y) `(,n ,e) `(,(+ n 1) ,e))]
      [`(λ ,(? symbol? X) ,Body) `(λ ,X ,(push-not-X X (push-not-X y Body)))]
      [`(,Fun ,Arg) `(,(push-not-X y Fun) ,(push-not-X y Arg))]))
  ;; Exp[(list Nat Symbol)] -> Exp[Nat]
  (define (strip e)
    (match e
      [`(,(? integer? n) ,(? symbol? e)) (if (= n -1) 0 n)]
      [`(λ ,(? symbol? X) ,Body) `(λ ,X ,(strip Body))]
      [`(,Fun ,Arg) `(,(strip Fun) ,(strip Arg))]))
  (strip (db e0)))

;; -----------------------------------------------------------------------------
(test)