{-# 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
(/\)
, 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₀))"