(datatype Expr
  (Num i64)
  (Var String)
  (Add Expr Expr))

(rewrite (Add x y) (Add y x))
(rewrite (Add (Num x) (Num y)) (Num (+ x y)))

;; antiunificaiton returns an expression that could unify with either
;; of the input expressions
;; (AU x y) can be considered a placeholder variable
(function AU (Expr Expr) Expr)

(rewrite (AU x x) x)
(rewrite
 (AU (Add a b) (Add c d))
 (Add (AU a c) (AU b d)))

(let e1 (Add (Var "x") (Add (Num 1) (Num 2))))
(let e2 (Add (Num 3) (Var "y")))

(let au12 (AU e1 e2))

(run 4)
(check (= au12 (Add (Num 3) (AU (Var "x") (Var "y")))))
(query-extract au12)