; Brian Alliet
; Programming Language Theory
; 4005-710-01

; This is  the substitution datatype. There are three substitution
; The empty substitution (which does nothing)
; The unit substitution which substitutes a single term for a single symbol
; The composition substitution which combines two substitution into one
; it applies the first then the second
(define-datatype subst subst?
    (empty-subst)
    (unit-subst (id symbol?) (new-term term?))
    (compose-substs (s1 subst?) (s2 subst?)))

; apply-subst applies a substitution to an identifier
(define (apply-subst s id)
    (cases subst s
        (empty-subst () (var-term id))
        (unit-subst (id_ new) (if(eq? id id_) new (var-term id)))
        (compose-substs (s1 s2) (subst-in-term (apply-subst s1 id) s2))))

; In THIS implementation every valid substitution is of type subst
(define valid-subst subst?)