You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
39 lines
919 B
39 lines
919 B
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")]]
|
|
|