{-# 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'
      -- , (x #* v) #+ (y #* v) ~> (x #+ y) #* v

      --  , x ~> x #+ 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]