{-# LANGUAGE OverloadedStrings #-}
module DSL where
import Language.REST.Op
import qualified Language.REST.MetaTerm as MT
import Language.REST.RuntimeTerm as RT
import Language.REST.Rewrite
import Nat
type MetaTerm = MT.MetaTerm
commutes op = x `op` y ~> y `op` x
assocL op = (x `op` y) `op` z' ~> x `op` (y `op` z')
assocR op = x `op` (y `op` z') ~> (x `op` y) `op` z'
distribL op1 op2 = (x `op1` y) `op2` z' ~> (x `op2` z') `op1` (y `op2` z')
distribR op1 op2 = z' `op2` (x `op1` y) ~> (z' `op2` x) `op1` (z' `op2` y)
ackOp = Op "ack"
plus = Op "+"
minus = Op "-"
times = Op "*"
a = App (Op "a") []
b = App (Op "b") []
c = App (Op "c") []
d = App (Op "d") []
x = MT.Var "x"
y = MT.Var "y"
v = MT.Var "v"
w = MT.Var "w"
z' = MT.Var "z"
f = Op "f"
g = Op "g"
h = Op "h"
t1Op = Op "t1"
t2Op = Op "t2"
t1 = App (Op "t1") []
t2 = App (Op "t2") []
t3 = App (Op "t3") []
t4 = App (Op "t4") []
t5 = App (Op "t5") []
zero = App z []
one = suc zero
two = suc one
suc x = App s [x]
ack x y = App ackOp [x, y]
zero' = MT.toMetaTerm zero
one' = suc' zero'
suc' x = MT.RWApp s [x]
ack' x y = MT.RWApp ackOp [x, y]
infixl 1 .+
(.+) :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm
(.+) x y = App plus [x, y]
(#+) :: MetaTerm -> MetaTerm -> MetaTerm
(#+) x y = MT.RWApp plus [x, y]
(#-) :: MetaTerm -> MetaTerm -> MetaTerm
(#-) x y = MT.RWApp minus [x, y]
(#*) :: MetaTerm -> MetaTerm -> MetaTerm
(#*) x y = MT.RWApp times [x, y]
infix 0 ~>
(~>) :: MetaTerm -> MetaTerm -> Rewrite
t ~> u = Rewrite t u Nothing
infix 0 <~>
(<~>) :: MetaTerm -> MetaTerm -> [Rewrite]
t <~> u = [ t ~> u, u ~> t ]