CS4613 Tutorial 6: Unification

In this tutorial you are asked to write a simplified version of the unify! function from the lectures. Instead of trees representing the types of expressions, you are asked to unify two trees with the following type:

(define-type BoxTree
  [mt]
  [node (b : (Boxof (Optionof Number))) (l : BoxTree) (r : BoxTree)])

In particular there is no type variables (boxes) shared between different locations in the tree.

You should complete the given skeleton for unify-trees! so that the following tests pass:

(module+ test
  ;; Same shape, one "variable" in each
  (let ([t1 (node (box (some 0))
                  (node (box (some 1)) (mt) (mt))
                  (node (box (none)) (mt) (mt)))]
        [t2 (node (box (some 0))
                  (node (box (none)) (mt) (mt))
                  (node (box (some 2)) (mt) (mt)))]
        [result (node (box (some 0))
                      (node (box (some 1)) (mt) (mt))
                      (node (box (some 2)) (mt) (mt)))])
    (begin
      (unify-trees! t1 t2)
      (test t1 result)
      (test t2 result)))

  (test/exn (unify-trees! (node (box (some 1))
                                (node (box (none)) (mt) (mt))
                                (mt))
                          (node (box (none)) (mt) (mt)))
            "shape mismatch")
  (test/exn (unify-trees! (node (box (some 1)) (mt) (mt))
                          (node (box (some 2)) (mt) (mt))) "value mismatch")

  ;; Only variables
  (let ([t1 (node (box (none)) (mt) (mt))]
        [t2 (node (box (none)) (mt) (mt))]
        [result (node (box (none)) (mt) (mt))])
    (begin
      (unify-trees! t1 t2)
      (test t1 result)
      (test t2 result)))

  ;; compatible elements, different shape
  (test/exn
   (unify-trees!
    (node (box (some 0))
          (node (box (some 1)) (mt) (node (box (none)) (mt) (mt)))
          (mt))
    (node (box (some 0))
          (mt)
          (node (box (some 1)) (node (box (none)) (mt) (mt)) (mt))))
   "shape mismatch")

  ;; deeper trees
  (let ([result (node
                 (box (some 0))
                 (node
                  (box (some 1))
                  (node (box (some 2))
                        (node (box (some 3))
                              (node (box (some 4)) (mt) (mt))
                              (mt))
                        (mt))
                  (mt))
                 (mt))]
        [t1  (node
              (box (none))
              (node
               (box (some 1))
               (node (box (none))
                     (node (box (some 3))
                           (node (box (some 4)) (mt) (mt))
                           (mt))
                     (mt))
               (mt))
              (mt))]
        [t2  (node
              (box (some 0))
              (node
               (box (none))
               (node (box (some 2))
                     (node (box (none))
                           (node (box (some 4)) (mt) (mt))
                           (mt))
                     (mt))
               (mt))
              (mt))])
    (begin
      (unify-trees! t1 t2)
      (test t1 t2)
      (test t1 result)
      (test t2 result)))
  )