#lang racket/base (require redex/reduction-semantics "tut-subst.rkt" racket/set) (define (an-x? x) (memq x '(a b c x y z z2 z2 q))) (test-equal (fvs an-x? (term (+ x a b))) (set 'x 'a 'b)) (test-equal (fvs an-x? (term (λ (x num) (+ x y)))) (set 'y)) (test-equal (fvs an-x? (term (λ (x num) (y num) (+ x y)))) (set)) (define-language L) (define-metafunction L [(subst (any_x any_b) ... any_body) ,(subst/proc an-x? (term (any_x ...)) (term (any_b ...)) (term any_body))]) (test-equal (term (subst (x y) x)) (term y)) (test-equal (term (subst (x y) z)) (term z)) (test-equal (term (subst (x y) (x (y z)))) (term (y (y z)))) (test-equal (term (subst (x y) ((λ (x num) x) ((λ (y1 num) y1) (λ (x num) z))))) (term ((λ (x num) x) ((λ (y1 num) y1) (λ (x num) z))))) (test-equal (term (subst (x y) (if0 (+ 1 x) x x))) (term (if0 (+ 1 y) y y))) (test-equal (term (subst (x (λ (z num) y)) (λ (y num) x))) (term (λ (y1 num) (λ (z num) y)))) (test-equal (term (subst (x 1) (λ (y num) x))) (term (λ (y num) 1))) (test-equal (term (subst (x y) (λ (y num) x))) (term (λ (y1 num) y))) (test-equal (term (subst (x (λ (y num) y)) (λ (z num) (z2 z)))) (term (λ (z num) (z2 z)))) (test-equal (term (subst (x (λ (z num) z)) (λ (z num) (z1 z)))) (term (λ (z num) (z1 z)))) (test-equal (term (subst (x z) (λ (z num) (z1 z)))) (term (λ (z2 num) (z1 z2)))) (test-equal (term (subst (x3 5) (λ (x2 num) x2))) (term (λ (x2 num) x2))) (test-equal (term (subst (z *) (λ (z num) (x num) 1))) (term (λ (z num) (x num) 1))) (test-equal (term (subst (q (λ (x num) z)) (λ (z num) (x num) q))) (term (λ (z1 num) (x num) (λ (x num) z)))) (test-equal (term (subst (x 1) (λ (x num) (x num) x))) (term (λ (x num) (x num) x))) (test-equal (term (subst (x (y z)) (λ (z num) (z (x y))))) (term (λ (z1 num) (z1 ((y z) y))))) (test-equal (term (subst (x 1) (λ (a (→ num (→ num num))) (λ (b (→ num (→ num num))) x)))) (term (λ (a (→ num (→ num num))) (λ (b (→ num (→ num num))) 1)))) (test-results)