hw4-base.scm: The necessary (commented) procedures to make unify-term work
hw4-test.scm: The test procedures
hw4-newsubst.scm: The new substitution representation

To run the unification program load hw4-base.scm
> ,load hw4-base.scm

Define some terms
> (define t (var-term 'foo))
> (define u (var-term 'bar))

Run unify
> (define s (unify-term t u))

Try to view unify (it is a procedure)
> s

Test (they are equal)
> (subst-in-term t s)
> (subst-in-term u s)

Run the full test (should throw no errors and return #t)
> ,load hw4-test.sc,
> (test)

Load the new substitution representation
> ,load hw4-newsubst.scm

Recalculate the substitution
> (define s (unify-term t u))

Try to view it (should be a readable datatype)
> s

Test (they are equal)
> (subst-in-term t s)
> (subst-in-term u s)

Run the full test
> (test)