#lang racket/base
#|
The substitution function in this file has been designed
to work with any expression language so long as the only
binding form is λ and the shape of λ terms is:
(λ (x t) ... e)
|#
(require racket/set racket/match
redex/reduction-semantics
rackunit)
(provide subst/proc fvs)
(define (subst/proc x? vars replacements body)
(define replacements-ht
(for/fold ([m (hash)])
([v (in-list vars)]
[rep (in-list replacements)])
(hash-set m v rep)))
(define replacements-free-vars (for/list ([x (in-set (fvs x? replacements))]) x))
(define replacements-fresh-vars (variables-not-in (cons vars body)
replacements-free-vars))
(define init-fv-map
(for/fold ([m (hash)])
([fresh (in-list replacements-fresh-vars)]
[free (in-list replacements-free-vars)])
(hash-set m free fresh)))
(let loop ([body body]
[fvs-inactive init-fv-map]
[fvs-active (hash)]
[replacements replacements-ht])
(match body
[`(λ (,xs ,ts) ... ,body)
(define-values (new-xs new-inactive new-active new-replacements)
(adjust-active-inactive xs fvs-inactive fvs-active replacements))
`(λ ,@(map (λ (x t) `(,x ,t)) new-xs ts)
,(loop body new-inactive new-active new-replacements))]
[(? x? x)
(cond
[(hash-ref fvs-active x #f) => values]
[(hash-ref replacements x #f) => values]
[else x])]
[(? list?)
(map (λ (x) (loop x fvs-inactive fvs-active replacements))
body)]
[_ body])))
(define (adjust-active-inactive xs fvs-inactive fvs-active replacements)
(let loop ([xs xs]
[new-xs '()]
[fvs-inactive fvs-inactive]
[fvs-active fvs-active]
[replacements replacements])
(cond
[(null? xs)
(values (reverse new-xs)
fvs-inactive
fvs-active
replacements)]
[else
(define x (car xs))
(define inactive-var? (hash-has-key? fvs-inactive x))
(define active-var? (hash-has-key? fvs-active x))
(define new-x
(cond
[inactive-var? (hash-ref fvs-inactive x)]
[active-var? (hash-ref fvs-active x)]
[else x]))
(loop (cdr xs)
(cons new-x new-xs)
(if inactive-var?
(hash-remove fvs-inactive x)
fvs-inactive)
(if inactive-var?
(hash-set fvs-active x (hash-ref fvs-inactive x))
fvs-active)
(if (hash-has-key? replacements x)
(hash-remove replacements x)
replacements))])))
(define (fvs x? body)
(let loop ([body body])
(match body
[`(λ (,xs ,ts) ... ,body)
(set-subtract (loop body) (apply set xs))]
[(? x?)
(set body)]
[(? list?)
(for/fold ([fvs (set)])
([e (in-list body)])
(set-union fvs (loop e)))]
[_ (set)])))