module ArithmeticsPL where
import Unification
import Resolution
import Data.Semigroup
import Data.Maybe

vw = Var "w"
vx = Var "x"
vy = Var "y"
vz = Var "z"
z = Func "0" []
s n = Func "s" [n]

sn 0 b = b
sn n b = s (sn (n-1) b)

add x y z = Func "add" [x, y, z]
mult x y z = Func "mult" [x, y, z]

s1 = Star [Pos (add z vy vy)]
s2 = Star [Pos (add (s vx) vy (s vz)), Neg (add vx vy vz)]

cadd :: Constellation
cadd = Const [
   Star [Pos (add z vy vy)],
   Star [Pos (add (s vx) vy (s vz)), Neg (add vx vy vz)]]

qadd :: Int -> Int -> Constellation
qadd n m = cadd <>
   Const [Star [Neg (add (sn n z) (sn m z) (Var "r")), NC (Var "r")]]

cmult :: Constellation
cmult = Const [
  Star [Pos (mult z vx z)],
  Star [Pos (mult (s vx) vy vz), Neg (mult vx vy vw), Neg (add vy vw vz)]]

qmult :: Int -> Int -> Constellation
qmult n m = cadd <> cmult <>
   Const [Star [Neg (mult (sn n z) (sn m z) (Var "r")), NC (Var "r")]]