find-free-var.rkt free variable finder. Nacessesary while closure conversion is operated.

find-free-var.rkt

#lang racket
;; find-free-var.rkt free variable finder. Nacessesary while closure conversion is operated.
;; ref: the algorithm from Definition 1.4.1, Type Theory andd Formal Proof: An Introdution

;; remove items from a list
(define (remove-items items list)
  (if (eq? items empty)
      list
      (remove-items (cdr items) (remove (car items) list)))
)

; flatten-and-remove-duplicates
(define (flatten-and-remove-dup x)
  (remove-duplicates (flatten x))
  )

(define (find-free-var-lines term-lines)
  (remove-items basic-operator (find-free-var-lines-aux term-lines)))

(define basic-operators '(+ - * /))

(define (find-free-var-lines-aux term-lines)
  (cond
    [(not (pair? term-lines)) (find-free-var term-lines)]
    [(eq? term-lines empty) '()]
    (else (flatten-and-remove-dup (cons (find-free-var (car term-lines)) (find-free-var-lines-aux (cdr term-lines)))))))

(define (find-free-var term)
  (if
    (pair? term)
    (cond
      ((eq? (car term) 'lambda) (remove-items (cadr term) (find-free-var-lines-aux (cddr term))))
      ((eq? (car term) 'define) (remove-items `(,(second term)) (find-free-var (third term))))
      (else (flatten-and-remove-dup (for/list [(i term)] (find-free-var i))))
    )
    (cond
      ((symbol? term) `(,term))
      (else '()))
   )
)

; => (a b)
(find-free-var-lines '((lambda (x y) (lambda (w g c) (+ a b w g x y)))))

; (=> y z w q)
(find-free-var-lines
 '((lambda (a b c)
    (define x1 12)
    (define x2 y)
    (define x3 (+ z c))
    (+ w a b c)
    (lambda (g1)
      (define v10 (+ v10 q a)))))
)

; (=> y z w q)
(find-free-var-lines
 '((lambda (a b c)
    (define x1 12)
    (define x2 y)
    (define x3 (+ z c))
    (+ w a b c)
    (define f1 (lambda (g1)
      (define v10 (+ v10 q a))))))
)