Untitled

'(Testing the substitute)

; 1) Is x in list?
(fun in?
  (x ()) ()
  (x (y . ys)) (if (equal x y) 'T (in? x ys)))

; 2) Remove elements of B from A
(fun difference
  (() B) ()
  ((a . as) B) (
    if (in? a B) 
      (difference as B) 
      (:: a (difference as B)))
  )

(fun free-vars
  ; If the term is (quote e), strip off quote and recurse
  ((quote e)) (free-vars e)

  ; If the term is a pair (head . tail)
  ((head . tail))
    (if (equal head '\)
        ; If head = '\, handle a multi-parameter lambda
        (handle-lambda tail)
        ; Otherwise, gather free vars from both
        (append (free-vars head) (free-vars tail)))

  ; If it’s a bare symbol, return (x), else empty
  (x) (if (symbol? x) (list x) ())
)

; handle-lambda expects tail to be ( (p1 p2 ...) . (body . ()) )
(fun handle-lambda
  ((params . (body . ())))
    (difference (free-vars body) params)
  (anything)
    ()
)

(free-vars '(\ (x) (x y)))
(free-vars '(\ (x y) (x y)))
(free-vars '(\ () (x y)))

; 2) fresh2: helper to pick a fresh variable
;    If no candidates left, return 'NoFreshVariables instead of throwing an error.
(fun fresh2
  (avoid ())
    'NoFreshVariables

  (avoid (cand . cands))
    (if (in? cand avoid)
        (fresh2 avoid cands)
        cand))

; 3) fresh: picks a fresh variable not in AVOID from a fixed list
(fun fresh
  (avoid) (fresh2 avoid '(a b c d e f g h i j k l m n o p q r s t u v w x y z)))

(fresh '(x y z))
(fresh '(a b c d e f g h i j k l m n o p q r s t u v w x y z))

(fun substitute
  ; If the term is (quote e), unwrap and recurse
  ((quote e) x t2) (substitute e x t2)

  ; 3) If term is an application (t3 . t4),
  ;    build a 2-element list: (sub(t3) sub(t4))
  ((t3 . t4) x t2)
    (:: (substitute t3 x t2)
        (substitute t4 x t2))

  ; 4) If term is a lambda (\ (y) body),
  ;    do alpha-conversion if y is in free-vars(t2)+free-vars(body).
  ((\ (y) body) x t2)
    (if (equal x y)
        (\ (y) body)
        (let fvT2 (free-vars t2)
          (let fvBody (free-vars body)
            (let avoid (append fvT2 fvBody)
              (if (in? y avoid)
                  (let z (fresh avoid)
                    (\ (z)
                       (substitute (substitute body y z)
                                   x t2)))
                  (\ (y)
                     (substitute body x t2)))))))
                     
  ; 1) If term is exactly x, replace it with t2
  (term x t2) (if (equal term x) t2 term)

  ; 2) If term is a symbol, keep it
  ((? symbol? term) x t2) term
  ; 5) Numbers or anything else
  (term x t2) term)
  
; Test
(substitute '((\ x (x y)) y) 'y 'z)