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

(define (unify-trees! t1 t2)
  (cond
    [(and (mt? t1) (mt? t2)) (void)]
    [(or (mt? t1) (mt? t2)) (error 'unify-trees! "shape mismatch")]
    [else ....]))

(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)))
  )