{-# LANGUAGE OverloadedStrings #-}
module Multiset where
import Data.Text ()
import DSL hiding (a, b, c)
import Language.REST.MetaTerm
import Language.REST.Internal.Rewrite
import qualified Data.HashSet as S
(\/) :: MetaTerm -> MetaTerm -> MetaTerm
x1 \/ y1 = RWApp "union" [x1, y1]
singleton, multisetOf :: MetaTerm -> MetaTerm
singleton x1 = RWApp "m" [x1]
multisetOf x1 = RWApp "toMS" [x1]
cons :: MetaTerm -> MetaTerm -> MetaTerm
cons x1 y1 = RWApp "cons" [x1, y1]
ite :: MetaTerm -> MetaTerm -> MetaTerm -> MetaTerm
ite a b c = RWApp "ite" [a,b,c]
hd, tl, isEmpty :: MetaTerm -> MetaTerm
hd x1 = RWApp "head" [x1]
tl x1 = RWApp "tail" [x1]
isEmpty x1 = RWApp "isEmpty" [x1]
empty :: MetaTerm
empty = RWApp "empty" []
xs, ys :: MetaTerm
xs = RWApp "xs" []
ys = RWApp "ys" []
expandM :: MetaTerm -> Rewrite
expandM xs0 = multisetOf xs0 ~> ite (isEmpty xs0) empty (singleton (hd xs0) \/ multisetOf (tl xs0))
userRWs :: S.HashSet Rewrite
userRWs = S.fromList $
[
commutes (\/) `named` "mpComm"
, assocL (\/) `named` "mpAssoc"
, assocR (\/) `named` "mpAssoc"
, (singleton x) \/ (multisetOf y) ~> multisetOf (cons x y)
]
evalRWs :: S.HashSet Rewrite
evalRWs = S.fromList
[ multisetOf (cons x y) ~> (singleton x) \/ (multisetOf y)
, expandM xs
, expandM ys
]
perm1t, perm1s :: String
perm1s = "union(m(y), union(toMS(cons(a,xs)),toMS(ys)))"
perm1t = "union(m(a), union(toMS(xs), toMS(cons(y,ys))))"