{-# 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.Internal.Rewrite
import Nat
commutes, assocL, assocR :: (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm) -> Rewrite
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, distribR
:: (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm)
-> (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm)
-> Rewrite
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, plus, minus, times :: Op
ackOp = Op "ack"
plus = Op "+"
minus = Op "-"
times = Op "*"
a, b, c, d :: RuntimeTerm
a = App (Op "a") []
b = App (Op "b") []
c = App (Op "c") []
d = App (Op "d") []
x, y, v, w, z' :: MT.MetaTerm
x = MT.Var "x"
y = MT.Var "y"
v = MT.Var "v"
w = MT.Var "w"
z' = MT.Var "z"
f, g, h :: Op
f = Op "f"
g = Op "g"
h = Op "h"
t1Op, t2Op :: Op
t1Op = Op "t1"
t2Op = Op "t2"
t1, t2, t3, t4, t5 :: RuntimeTerm
t1 = App (Op "t1") []
t2 = App (Op "t2") []
t3 = App (Op "t3") []
t4 = App (Op "t4") []
t5 = App (Op "t5") []
zero, one, two :: RuntimeTerm
zero = App z []
one = suc zero
two = suc one
suc :: RuntimeTerm -> RuntimeTerm
suc x1 = App s [x1]
ack :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm
ack x1 y1 = App ackOp [x1, y1]
zero' :: MT.MetaTerm
zero' = MT.toMetaTerm zero
one' :: MT.MetaTerm
one' = suc' zero'
suc' :: MT.MetaTerm -> MT.MetaTerm
suc' x1 = MT.RWApp s [x1]
ack' :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
ack' x1 y1 = MT.RWApp ackOp [x1, y1]
infixl 1 .+
(.+) :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm
(.+) x1 y1 = App plus [x1, y1]
(#+) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
(#+) x1 y1 = MT.RWApp plus [x1, y1]
(#-) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
(#-) x1 y1 = MT.RWApp minus [x1, y1]
(#*) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
(#*) x1 y1 = MT.RWApp times [x1, y1]
infix 0 ~>
(~>) :: MT.MetaTerm -> MT.MetaTerm -> Rewrite
t ~> u = Rewrite t u Nothing
infix 0 <~>
(<~>) :: MT.MetaTerm -> MT.MetaTerm -> [Rewrite]
t <~> u = [ t ~> u, u ~> t ]