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

(define (test)
    (let
        ((try (lambda (t u unified)
            (let*
                ((s (unify-term t u)))
                (if
                    (if unified
                        (and
                            (valid-subst s)
                            (equal? unified (subst-in-term t s))
                            (equal? unified (subst-in-term u s)))
                            (not s))
                    #t
                    (error "Test failed")))))
         (foo (var-term 'foo))
         (bar (var-term 'bar))
         (baz (var-term 'baz))
         (quux (var-term 'quux))
         (one (constant-term 1))
         (two (constant-term 2))
         )
    (begin
        ; Simple variable substitution
        (try foo bar bar)
        ; Substituting an expression for a variable
        (try foo (app-term (list bar baz)) (app-term (list bar baz)))
        ; Equal constants are ok
        (try one one one)
        ; Equal applications are ok (as long as each component can be substituted)
        (try (app-term (list foo bar)) (app-term (list baz quux)) (app-term (list baz quux)))
        ; Substituting an expression for a variable isn't ok always
        (try foo (app-term (list foo bar)) #f)
        ; Unequal constants are not ok
        (try one two #f)
        ; Mismatched non variable types aren't ok
        (try one (app-term (list foo two)) #f)
        )))