#lang racket

;; x,y ∈ Vars
;; LExp ::= y | (λ (x) LExp) | (LExp LExp)

;; Save this somewhere, you'll want it.
;; (define ...
;;   (lambda (exp ...)
;;     (match exp
;;       [`,y #:when (symbol? y) ...]
;;       [`(λ (,x) ,body) ...]
;;       [`(,rator ,rand) ...])))

;; (define v-o?
;;   (lambda (v e)
;;     (match e
;;       [`,y #:when (symbol? y) <think!>]
;;       [`(λ (,x) ,body) (<think!> (v-o? v body))]
;;       [`(,rator ,rand)
;;        (<think!>
;;         (v-o? v rator)
;;         (v-o? v rand))])))

;; A variable /occurs-free?/ in an expression if the variable /occurs/
;; in the expression and one of the occurrences of that variable is
;; not within the /scope/ of an enclosing lambda /binding/ that same
;; variable

(define v-o-f?
  (lambda (v e acc)
    (match e
      [`,y #:when (symbol? y)
        (and (not (memv v acc)) (eqv? v y))]
      [`(λ (,x) ,body)
       (v-o-f? v body (cons x acc))]
      [`(,rator ,rand)
       (or
        (v-o-f? v rator acc)
        (v-o-f? v rand acc))])))

;; A variable /occurs-bound?/ in an expression if the variable
;; /occurs/ in the expression and one of the occurrences of that
;; variable is within the /scope/ of an enclosing lambda /binding/
;; that same variable

(define v-o-b?
  (lambda (v e acc)
    (match e
      [`,y #:when (symbol? y)
       (and (memv v acc) (eqv? v y))]
      [`(λ (,x) ,body)
       (v-o-b? v body (cons x acc))]
      [`(,rator ,rand)
       (or
        (v-o-b? v rator acc)
        (v-o-b? v rand acc))])))

;; | Expression        | xo? | xf? | xb? | yo? | yf? | yb? |
;; | x                 | y   | y   | n   | n   | n   | n   |
;; | z                 | n   | n   | n   | n   | n   | n   |
;; | (λ (x) y)         | n   | n   | n   | y   | y   | n   |
;; | (λ (x) x)         | y   | n   | y   | n   | n   | n   |
;; | (λ (y) z)         | n   | n   | n   | n   | n   | n   |
;; | (λ (x) (λ (x) x)) | y   | n   | y   | n   | n   | n   |
;; | (λ (x) (λ (y) x)) | y   | n   | y   | n   | n   | n   |
;; | (x y)             | y   | y   | n   | y   | y   | n   |
;; | ((λ (x) x) x)     | y   | y   | y   | n   | n   | n   |
;; |                   |     |     |     |     |     |     |

;; The /lexical address/ of a variable occurrence is the number of
;; enclosing lambda abstractions before reaching the binding of that
;; variable occurrence. (i.e. the number of abstractions you have to
;; "jump over" before reaching the one you want.)

;; Also known as "de Bruijn index" of the variables.

;; (λ (a) 
;;   (λ (b) 
;;     (λ (c)
;;       (λ (a)
;;         ((a b) (c d))))))

;; lexes to 

;; (λ  
;;   (λ 
;;     (λ
;;       (λ 
;;         ((0 2) (1 d))))))
;; d is a /free variable/.
;; Don't have those.

;; 'As Will Rogers might have said, "There's no such thing as a free
;; variable."'
;; – Alan J. Perlis