#lang racket
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (new-parameters expression list)
  (let ((old-parameters (lambda-parameter expression)))
    (new-var
     (cond
      ((null? list) old-parameters)
     ((assq (car old-parameters) list) old-parameters)
       (else (map cadr list)))
     (symbol->string (car old-parameters))
	 )
  )
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (all-ids expression)
  (cond
    ((null? expression) '())
    ((var? expression) (list expression))
    ((lambda? expression)
     (union (cons 'lambda (lambda-parameter expression))
            (all-ids (body expression))))
    ((app? expression)
     (union (all-ids (app-fun expression))
            (all-ids (app-arg expression))))
  )
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (free-vars e1)
  (define (fun expression args vars-so-far)
    (cond ((null? expression) vars-so-far)
          ((var? expression)
           (cond ((not (member expression args)) (append (list expression) vars-so-far))
                 (else vars-so-far))
           )
          ((lambda? expression)
           (fun (body expression) (append (lambda-parameter expression) args) vars-so-far)
           )
          ((app? expression)
           (fun (app-fun expression) args (append (fun (app-arg expression) args vars-so-far) vars-so-far)))
          )
    )
  (remove-duplicates(fun e1 `() `()))
  )
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (union e1-list e2-list)
  (cond
    ((null? e2-list) e1-list)
    ((member (car e2-list) e1-list)
     (union e1-list (cdr e2-list)))
    (else (union (cons (car e2-list) e1-list) (cdr e2-list)))
  )
)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (new-var list string)
  (define old-parameters list)
  (define (iter n)
    (let ((new (string->symbol (string-append string (number->string n)))))
      (cond
        ((not (member new old-parameters)) new)
        (else (iter (+ n 1))))))
  (iter 0)
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (lambda? expression)
  (and (pair? expression)
       (eq? (lambda-symbol expression) 'lambda)))
(define (make-expression e1 e2)
  (list e1 e2))
(define (lambda-symbol expression)
  (car expression))
(define (initialize-lambda parameter expression)
  (list 'lambda (list parameter) expression))
(define (body expression)
  (caddr expression))
(define (lambda-parameter expression)
  (cadr expression))
(define (app-fun expression)
  (car expression))
(define (var? expression)
  (symbol? expression))
(define (app-arg expression)
  (cadr expression))
(define (app? expression)
  (
    and (pair? expression)
       (not (eq? (lambda-symbol expression) 'lambda))
  )
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (parameters l)
        (define (fun list element-so-far)
          (cond ((null? list) element-so-far)
                ((member (car list) element-so-far) (fun (cdr list) element-so-far))
                ;((member (car list) (cdr list)) (fun (cdr list) element-so-far))
                (else (fun (cdr list) (append element-so-far (list (car list)))))
                )
          )
  (fun l `())
  )
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (subst e1 e2 var)
  (define (fun expression to-replace expression-made)
     (cond ((null? expression) expression-made)
          ((var? expression)
           (cond ((assq expression to-replace)(append expression-made (cdr (assq expression to-replace))))
                 ((equal? expression var) (append expression-made e2))
                 (else (append expression-made (list expression)))))
          ((lambda? expression)
           (let ((old-parameter (car (lambda-parameter expression)))
             (new-parameter (new-parameters expression to-replace)))
         (if (and
              (member var (free-vars expression))
                  (member old-parameter (all-ids e2))
                  (not (assq var to-replace))
                  (not (equal? var old-parameter)))
                          (fun (body expression) (cons (list old-parameter new-parameter) to-replace) (append expression-made `(lambda) (cons (list new-parameter) `())))
                          (fun (body expression) (cons (list old-parameter old-parameter) to-replace) (append expression-made `(lambda) (cons (lambda-parameter expression) `()))))))
          ((app? expression)
           (fun (app-arg expression) to-replace (append expression-made  (fun (app-fun expression) to-replace `())))
    )))
  (fun e1 `() `())
  )
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(subst '(lambda (x) x) 'x 'y)
(newline)(newline)
(subst '(lambda (x) x) '(x y) 'x)
(newline)(newline)
(subst '(lambda (x) (x y)) '(x y) 'x)
(newline)(newline)
(subst '(lambda (x) (x y)) '(x y) 'y)
(newline)(newline)
(subst '(lambda (x) (x (y (lambda (x) (x z))))) '(x y) 'y)
(newline)(newline)
(subst '(lambda (x) (x y (lambda (x) (x y)))) '(x y) 'y)
(newline)(newline)
(subst '(lambda (x) (x y (lambda (y) (x (lambda (z) (x (y z))))))) '(x (y z)) 'y)  
(newline)(newline)
(subst '(lambda (x) (x (y (lambda (y) (x (lambda (z) (x (y z)))))))) '(x (y z)) 'y)  
(newline)(newline)
(subst '(lambda (x) (x (w (lambda (y) (x (w (lambda (z) (x (y w))))))))) '(x (y z)) 'w)
(newline)(newline)
(subst '(lambda (x) (x ((x y) (lambda (y) (x y))))) 'z 'x)
;;Correctness: The method "subst" checks the free variables in the lambda calculus expression, made its list and then check whether the given variable exists in the list of free variables. If it does not exist, then it doesn't check substtitution. If it exists it create a new list and append the new variables e.g x0 (as binding variable) and all the other occurences of this variable, which do not exist previously in the expression to avoid capturing. It repeatedly checks for all the lambda expressions whether the variables is captured, if so it then substtitute another new binding variable e.g y0 and all its occurences.