{-# LANGUAGE OverloadedStrings #-}

module Set where

import Arith as A
import DSL
import Language.REST.Internal.Rewrite (Rewrite)
import Language.REST.MetaTerm

import qualified Data.HashSet as S

emptyset :: MetaTerm
emptyset :: MetaTerm
emptyset  = Op -> [MetaTerm] -> MetaTerm
RWApp Op
"∅" []

(/\), (\/) :: MetaTerm -> MetaTerm -> MetaTerm
MetaTerm
x1 /\ :: MetaTerm -> MetaTerm -> MetaTerm
/\ MetaTerm
y1 = Op -> [MetaTerm] -> MetaTerm
RWApp Op
"intersect" [MetaTerm
x1, MetaTerm
y1]
MetaTerm
x1 \/ :: MetaTerm -> MetaTerm -> MetaTerm
\/ MetaTerm
y1  = Op -> [MetaTerm] -> MetaTerm
RWApp Op
"union" [MetaTerm
x1, MetaTerm
y1]

s0, s1 :: MetaTerm
s0 :: MetaTerm
s0 = Op -> [MetaTerm] -> MetaTerm
RWApp Op
"s₀" []
s1 :: MetaTerm
s1 = Op -> [MetaTerm] -> MetaTerm
RWApp Op
"s₁" []

isSubset :: MetaTerm -> MetaTerm -> Rewrite
isSubset :: MetaTerm -> MetaTerm -> Rewrite
isSubset MetaTerm
mt1 MetaTerm
mt2 = MetaTerm
mt1 MetaTerm -> MetaTerm -> MetaTerm
\/ MetaTerm
mt2 MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
mt2

userRWs :: S.HashSet Rewrite
userRWs :: HashSet Rewrite
userRWs = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet Rewrite
A.evalRWs forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
  [
    (MetaTerm -> MetaTerm -> MetaTerm)
-> (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
distribL MetaTerm -> MetaTerm -> MetaTerm
(/\) MetaTerm -> MetaTerm -> MetaTerm
(\/)
  , (MetaTerm -> MetaTerm -> MetaTerm)
-> (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
distribR MetaTerm -> MetaTerm -> MetaTerm
(/\) MetaTerm -> MetaTerm -> MetaTerm
(\/)
  , (MetaTerm -> MetaTerm -> MetaTerm)
-> (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
distribL MetaTerm -> MetaTerm -> MetaTerm
(\/) MetaTerm -> MetaTerm -> MetaTerm
(/\)
  , (MetaTerm -> MetaTerm -> MetaTerm)
-> (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
distribR MetaTerm -> MetaTerm -> MetaTerm
(\/) MetaTerm -> MetaTerm -> MetaTerm
(/\)
  , (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
assocL MetaTerm -> MetaTerm -> MetaTerm
(\/)
  , (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
assocL MetaTerm -> MetaTerm -> MetaTerm
(/\)
  , MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
/\ MetaTerm
x        MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
x
  , MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
\/ MetaTerm
x        MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
x
  , MetaTerm
x MetaTerm -> MetaTerm -> MetaTerm
\/ MetaTerm
emptyset MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
x
  , (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
commutes MetaTerm -> MetaTerm -> MetaTerm
(\/)
  , (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite
commutes MetaTerm -> MetaTerm -> MetaTerm
(/\)

  -- Example 1
  -- , s1 /\ s0      ~> emptyset

  -- Example 2
  , MetaTerm
s0 MetaTerm -> MetaTerm -> MetaTerm
\/ MetaTerm
s1      MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
s0
  ]

evalRWs :: S.HashSet Rewrite
evalRWs :: HashSet Rewrite
evalRWs = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet Rewrite
A.userRWs forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList --
  [ Op -> [MetaTerm] -> MetaTerm
RWApp Op
"t2" [] MetaTerm -> MetaTerm -> Rewrite
~> MetaTerm
emptyset
  , MetaTerm -> MetaTerm -> Rewrite
isSubset (Op -> [MetaTerm] -> MetaTerm
RWApp Op
"right1" []) (Op -> [MetaTerm] -> MetaTerm
RWApp Op
"right" [])
  ]

disjointExample, disjointExample2 :: String
disjointExample :: String
disjointExample  = String
"union(union(left, right1), union(left,right))"
disjointExample2 :: String
disjointExample2 = String
"union(left, union(right1, union(left,right)))"

example1, example2 :: String
example1 :: String
example1 = String
"f(intersect(union(s₀,s₁), s₀))"
example2 :: String
example2 = String
"f(union(intersect(s₀,s₁), s₀))"