Lab Tutorial 6

Handin your code for this tutorial via the DrRacket handin-server facility.

In this tutorial you are asked to write a simplified version of the unify! function from the Lecture12 . 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)))
  )