{-# LANGUAGE OverloadedStrings #-}
module Arith where
import DSL
import Language.REST.Internal.Rewrite (Rewrite)
import Language.REST.MetaTerm
import Language.REST.Op
import qualified Data.HashSet as S
neg :: MetaTerm -> MetaTerm
neg :: MetaTerm -> MetaTerm
neg MetaTerm
x1 = Op -> [MetaTerm] -> MetaTerm
RWApp (Text -> Op
Op Text
"neg") [MetaTerm
x1]
double :: MetaTerm -> MetaTerm
double :: MetaTerm -> MetaTerm
double MetaTerm
x1 = Op -> [MetaTerm] -> MetaTerm
RWApp (Text -> Op
Op Text
"double") [MetaTerm
x1]
twicePlus :: MetaTerm -> MetaTerm -> MetaTerm
twicePlus :: MetaTerm -> MetaTerm -> MetaTerm
twicePlus MetaTerm
x1 MetaTerm
y1 = Op -> [MetaTerm] -> MetaTerm
RWApp (Text -> Op
Op Text
"twicePlus") [MetaTerm
x1, MetaTerm
y1]
(<#) :: MetaTerm -> MetaTerm -> MetaTerm
MetaTerm
x1 <# :: MetaTerm -> MetaTerm -> MetaTerm
<# MetaTerm
y1 = Op -> [MetaTerm] -> MetaTerm
RWApp (Text -> Op
Op Text
"<") [MetaTerm
x1, MetaTerm
y1]
evalRWs :: S.HashSet Rewrite
evalRWs :: HashSet Rewrite
evalRWs =
[Rewrite] -> HashSet Rewrite
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
[
MetaTerm -> MetaTerm
suc' MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
<# MetaTerm -> MetaTerm
suc' MetaTerm
y MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
<# MetaTerm
y
, MetaTerm -> MetaTerm
suc' MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
y MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm -> MetaTerm
suc' (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
y)
, MetaTerm
zero' MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
x MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
x
, MetaTerm -> MetaTerm
suc' MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#* MetaTerm
y MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
#+ (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#* MetaTerm
y)
, MetaTerm
zero' MetaTerm -> MetaTerm -> MetaTerm
#* MetaTerm
y MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
zero'
, MetaTerm -> MetaTerm -> MetaTerm
ack' MetaTerm
zero' MetaTerm
x MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm -> MetaTerm
suc' MetaTerm
x
, MetaTerm -> MetaTerm -> MetaTerm
ack' (MetaTerm -> MetaTerm
suc' MetaTerm
x) MetaTerm
zero' MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm -> MetaTerm -> MetaTerm
ack' MetaTerm
x MetaTerm
one'
, MetaTerm -> MetaTerm -> MetaTerm
ack' (MetaTerm -> MetaTerm
suc' MetaTerm
x) (MetaTerm -> MetaTerm
suc' MetaTerm
y) MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm -> MetaTerm -> MetaTerm
ack' MetaTerm
x (MetaTerm -> MetaTerm -> MetaTerm
ack' (MetaTerm -> MetaTerm
suc' MetaTerm
x) MetaTerm
y)
, MetaTerm -> MetaTerm
double MetaTerm
x MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
x
, MetaTerm -> MetaTerm -> MetaTerm
twicePlus MetaTerm
x MetaTerm
y MetaTerm -> MetaTerm -> Rewrite
~> (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
x) MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
y
]
userRWs :: S.HashSet Rewrite
userRWs :: HashSet Rewrite
userRWs =
[Rewrite] -> HashSet Rewrite
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Rewrite] -> HashSet Rewrite) -> [Rewrite] -> HashSet Rewrite
forall a b. (a -> b) -> a -> b
$
[ MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
y MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
x
, MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#* MetaTerm
y MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
#* MetaTerm
x
, (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
y) MetaTerm -> MetaTerm -> MetaTerm
#* MetaTerm
v MetaTerm -> MetaTerm -> Rewrite
~> (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#* MetaTerm
v) MetaTerm -> MetaTerm -> MetaTerm
#+ (MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
#* MetaTerm
v)
, MetaTerm -> MetaTerm
neg MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
x MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
zero'
] [Rewrite] -> [Rewrite] -> [Rewrite]
forall a. [a] -> [a] -> [a]
++ [ MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ (MetaTerm
y MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
v) MetaTerm -> MetaTerm -> Rewrite
~> (MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
y) MetaTerm -> MetaTerm -> MetaTerm
#+ MetaTerm
v]