{-# LANGUAGE OverloadedStrings #-}
module Lists where
import Prelude hiding (reverse)
import Language.REST.Internal.Rewrite (Rewrite)
import qualified Language.REST.MetaTerm as MT
import DSL hiding (t1, t2)
import qualified Data.HashSet as S
xs, ys, nil :: MT.MetaTerm
xs = MT.Var "xs"
ys = MT.Var "ys"
nil = MT.RWApp "nil" []
(.:) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
(.:) t1 t2 = MT.RWApp "cons" [t1, t2]
reverse :: MT.MetaTerm -> MT.MetaTerm
reverse t = MT.RWApp "reverse" [t]
(.++) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm
(.++) lhs rhs = MT.RWApp "append" [lhs, rhs]
evalRWs :: S.HashSet Rewrite
evalRWs = S.fromList [
reverse (x .: xs) ~> reverse xs .++ (x .: nil)
, reverse nil ~> nil
, nil .++ xs ~> xs
, (x .: xs) .++ ys ~> x .: (xs .++ ys)
, reverse (reverse (MT.RWApp "xs" [])) ~> MT.RWApp "xs" []
]
userRWs :: S.HashSet Rewrite
userRWs = S.fromList [
reverse (xs .++ ys) ~> (reverse ys) .++ (reverse xs)
, (reverse ys) .++ (reverse xs) ~> reverse (xs .++ ys)
]