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

(rewrite (Add x y) (Add y x))
(rewrite (Add (Add x y) z) (Add x (Add y z)))
(rewrite (Add (Num x) (Num y)) (Num (+ x y)))
(rule ((= (Add x y) z))
      ((union (Add z (Neg y)) x)))
(rewrite (Neg (Neg x)) x)
(rewrite (Neg (Num n)) (Num (- 0 n)))

(rule ((= x (Var v))) ((union (Mul (Num 1) x) x)))
(rule ((= x (Add x1 x2))) ((union (Mul (Num 1) x) x)))
(rewrite (Add (Mul y x) (Mul z x)) (Mul (Add y z) x))
(rewrite (Mul x y) (Mul y x))
(rule ((= (Mul (Num x) y) (Num z))
       (= (% z x) 0))
      ((union y (Num (/ z x)))))

; system 1: x + 2 = 7
(union (Add (Var "x") (Num 2)) (Num 7))
; system 2: z + y = 6, 2z = y
(union (Add (Var "z") (Var "y")) (Num 6))
(union (Add (Var "z") (Var "z")) (Var "y"))

(run 5)
(query-extract (Var "x"))
(query-extract (Var "y"))
(query-extract (Var "z"))
(check (= (Var "z") (Add (Num 6) (Neg (Var "y")))))
(check (= (Var "y") (Add (Add (Num 6) (Neg (Var "y"))) (Add (Num 6) (Neg (Var "y"))))))
(check (= (Var "y") (Add (Add (Num 12) (Neg (Var "y"))) (Neg (Var "y")))))
(check (= (Add (Var "y") (Var "y")) 
          (Add (Num 12) (Neg (Var "y")))))
(check (= (Add (Add (Var "y") (Var "y")) (Var "y"))
          (Num 12)))
(check (= (Add (Mul (Num 2) (Var "y")) (Var "y"))
          (Num 12)))
(check (= (Mul (Num 3) (Var "y"))
          (Num 12)))