{-# 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 :: (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
commutes MetaTerm -> MetaTerm -> MetaTerm
op      = MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
`op` MetaTerm
y            MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
`op` MetaTerm
x
assocL :: (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
assocL   MetaTerm -> MetaTerm -> MetaTerm
op      = (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
`op` MetaTerm
y) MetaTerm -> MetaTerm -> MetaTerm
`op` MetaTerm
z'   MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
`op` (MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
`op` MetaTerm
z')
assocR :: (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
assocR   MetaTerm -> MetaTerm -> MetaTerm
op      = MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
`op` (MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
`op` MetaTerm
z')   MetaTerm -> MetaTerm -> Rewrite
~> (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
`op` MetaTerm
y) MetaTerm -> MetaTerm -> MetaTerm
`op` MetaTerm
z'

distribL, distribR
  :: (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm)
  -> (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm)
  -> Rewrite
distribL :: (MetaTerm -> MetaTerm -> MetaTerm)
-> (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
distribL MetaTerm -> MetaTerm -> MetaTerm
op1 MetaTerm -> MetaTerm -> MetaTerm
op2 = (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
`op1` MetaTerm
y) MetaTerm -> MetaTerm -> MetaTerm
`op2` MetaTerm
z' MetaTerm -> MetaTerm -> Rewrite
~> (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
`op2` MetaTerm
z') MetaTerm -> MetaTerm -> MetaTerm
`op1` (MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
`op2` MetaTerm
z')
distribR :: (MetaTerm -> MetaTerm -> MetaTerm)
-> (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
distribR MetaTerm -> MetaTerm -> MetaTerm
op1 MetaTerm -> MetaTerm -> MetaTerm
op2 = MetaTerm
z' MetaTerm -> MetaTerm -> MetaTerm
`op2` (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
`op1` MetaTerm
y) MetaTerm -> MetaTerm -> Rewrite
~> (MetaTerm
z' MetaTerm -> MetaTerm -> MetaTerm
`op2` MetaTerm
x) MetaTerm -> MetaTerm -> MetaTerm
`op1` (MetaTerm
z' MetaTerm -> MetaTerm -> MetaTerm
`op2` MetaTerm
y)

ackOp, plus, minus, times :: Op
ackOp :: Op
ackOp  = Text -> Op
Op Text
"ack"
plus :: Op
plus   = Text -> Op
Op Text
"+"
minus :: Op
minus  = Text -> Op
Op Text
"-"
times :: Op
times  = Text -> Op
Op Text
"*"

a, b, c, d :: RuntimeTerm
a :: RuntimeTerm
a = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"a") []
b :: RuntimeTerm
b = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"b") []
c :: RuntimeTerm
c = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"c") []
d :: RuntimeTerm
d = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"d") []

x, y, v, w, z' :: MT.MetaTerm
x :: MetaTerm
x = String -> MetaTerm
MT.Var String
"X"
y :: MetaTerm
y = String -> MetaTerm
MT.Var String
"Y"
v :: MetaTerm
v = String -> MetaTerm
MT.Var String
"V"
w :: MetaTerm
w = String -> MetaTerm
MT.Var String
"W"
z' :: MetaTerm
z' = String -> MetaTerm
MT.Var String
"Z"

f, g, h :: Op
f :: Op
f = Text -> Op
Op Text
"f"
g :: Op
g = Text -> Op
Op Text
"g"
h :: Op
h = Text -> Op
Op Text
"h"

t1Op, t2Op :: Op
t1Op :: Op
t1Op = Text -> Op
Op Text
"t1"
t2Op :: Op
t2Op = Text -> Op
Op Text
"t2"

t1, t2, t3, t4, t5 :: RuntimeTerm
t1 :: RuntimeTerm
t1 = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"t1") []
t2 :: RuntimeTerm
t2 = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"t2") []
t3 :: RuntimeTerm
t3 = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"t3") []
t4 :: RuntimeTerm
t4 = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"t4") []
t5 :: RuntimeTerm
t5 = Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
"t5") []

zero, one, two :: RuntimeTerm
zero :: RuntimeTerm
zero    = Op -> [RuntimeTerm] -> RuntimeTerm
App Op
z []
one :: RuntimeTerm
one     = RuntimeTerm -> RuntimeTerm
suc RuntimeTerm
zero
two :: RuntimeTerm
two     = RuntimeTerm -> RuntimeTerm
suc RuntimeTerm
one

suc :: RuntimeTerm -> RuntimeTerm
suc :: RuntimeTerm -> RuntimeTerm
suc RuntimeTerm
x1   = Op -> [RuntimeTerm] -> RuntimeTerm
App Op
s [RuntimeTerm
x1]

ack :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm
ack :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm
ack RuntimeTerm
x1 RuntimeTerm
y1 = Op -> [RuntimeTerm] -> RuntimeTerm
App Op
ackOp [RuntimeTerm
x1, RuntimeTerm
y1]

zero' :: MT.MetaTerm
zero' :: MetaTerm
zero'    = RuntimeTerm -> MetaTerm
forall a. ToMetaTerm a => a -> MetaTerm
MT.toMetaTerm RuntimeTerm
zero

one' :: MT.MetaTerm
one' :: MetaTerm
one'     = MetaTerm -> MetaTerm
suc' MetaTerm
zero'

suc' :: MT.MetaTerm -> MT.MetaTerm
suc' :: MetaTerm -> MetaTerm
suc' MetaTerm
x1   = Op -> [MetaTerm] -> MetaTerm
MT.RWApp Op
s [MetaTerm
x1]

ack' :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
ack' :: MetaTerm -> MetaTerm -> MetaTerm
ack' MetaTerm
x1 MetaTerm
y1 = Op -> [MetaTerm] -> MetaTerm
MT.RWApp Op
ackOp [MetaTerm
x1, MetaTerm
y1]

infixl 1 .+
(.+) :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm
.+ :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm
(.+) RuntimeTerm
x1 RuntimeTerm
y1 = Op -> [RuntimeTerm] -> RuntimeTerm
App Op
plus [RuntimeTerm
x1, RuntimeTerm
y1]

(#+) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
#+ :: MetaTerm -> MetaTerm -> MetaTerm
(#+) MetaTerm
x1 MetaTerm
y1 = Op -> [MetaTerm] -> MetaTerm
MT.RWApp Op
plus [MetaTerm
x1, MetaTerm
y1]

(#-) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
#- :: MetaTerm -> MetaTerm -> MetaTerm
(#-) MetaTerm
x1 MetaTerm
y1 = Op -> [MetaTerm] -> MetaTerm
MT.RWApp Op
minus [MetaTerm
x1, MetaTerm
y1]

(#*) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
#* :: MetaTerm -> MetaTerm -> MetaTerm
(#*) MetaTerm
x1 MetaTerm
y1 = Op -> [MetaTerm] -> MetaTerm
MT.RWApp Op
times [MetaTerm
x1, MetaTerm
y1]

infix 0 ~>
(~>) :: MT.MetaTerm -> MT.MetaTerm -> Rewrite
MetaTerm
t ~> :: MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
u = MetaTerm -> MetaTerm -> Maybe String -> Rewrite
Rewrite MetaTerm
t MetaTerm
u Maybe String
forall a. Maybe a
Nothing

infix 0 <~>
(<~>) :: MT.MetaTerm -> MT.MetaTerm -> [Rewrite]
MetaTerm
t <~> :: MetaTerm -> MetaTerm -> [Rewrite]
<~> MetaTerm
u = [ MetaTerm
t MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
u, MetaTerm
u MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
t ]