#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)
