module Maude.Meta.HasOps (
HasOps (..)
) where
import Maude.AS_Maude
import Maude.Symbol
import Maude.Meta.AsSymbol
import Maude.Meta.HasName
import Data.Set (Set)
import qualified Data.Set as Set
class HasOps a where
getOps :: a -> SymbolSet
mapOps :: SymbolMap -> a -> a
instance HasOps Symbol where
getOps :: Symbol -> SymbolSet
getOps sym :: Symbol
sym = case Symbol
sym of
Operator {} -> Symbol -> SymbolSet
forall a. a -> Set a
Set.singleton Symbol
sym
OpWildcard _ -> Symbol -> SymbolSet
forall a. a -> Set a
Set.singleton Symbol
sym
_ -> SymbolSet
forall a. Set a
Set.empty
mapOps :: SymbolMap -> Symbol -> Symbol
mapOps mp :: SymbolMap
mp sym :: Symbol
sym = case Symbol
sym of
Operator {} -> (Symbol -> Symbol) -> SymbolMap -> Symbol -> Symbol
forall a. AsSymbol a => (Symbol -> a) -> SymbolMap -> a -> a
mapAsSymbol Symbol -> Symbol
forall a. a -> a
id SymbolMap
mp Symbol
sym
OpWildcard _ -> (Symbol -> Symbol) -> SymbolMap -> Symbol -> Symbol
forall a. AsSymbol a => (Symbol -> a) -> SymbolMap -> a -> a
mapAsSymbol Symbol -> Symbol
forall a. a -> a
id SymbolMap
mp Symbol
sym
_ -> Symbol
sym
instance (HasOps a) => HasOps [a] where
getOps :: [a] -> SymbolSet
getOps = [SymbolSet] -> SymbolSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([SymbolSet] -> SymbolSet)
-> ([a] -> [SymbolSet]) -> [a] -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SymbolSet) -> [a] -> [SymbolSet]
forall a b. (a -> b) -> [a] -> [b]
map a -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps
mapOps :: SymbolMap -> [a] -> [a]
mapOps = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> a) -> [a] -> [a])
-> (SymbolMap -> a -> a) -> SymbolMap -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolMap -> a -> a
forall a. HasOps a => SymbolMap -> a -> a
mapOps
instance (HasOps a, HasOps b) => HasOps (a, b) where
getOps :: (a, b) -> SymbolSet
getOps (a :: a
a, b :: b
b) = SymbolSet -> SymbolSet -> SymbolSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (a -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps a
a) (b -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps b
b)
mapOps :: SymbolMap -> (a, b) -> (a, b)
mapOps mp :: SymbolMap
mp (a :: a
a, b :: b
b) = (SymbolMap -> a -> a
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp a
a, SymbolMap -> b -> b
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp b
b)
instance (HasOps a, HasOps b, HasOps c) => HasOps (a, b, c) where
getOps :: (a, b, c) -> SymbolSet
getOps (a :: a
a, b :: b
b, c :: c
c) = SymbolSet -> SymbolSet -> SymbolSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (a -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps a
a) ((b, c) -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps (b
b, c
c))
mapOps :: SymbolMap -> (a, b, c) -> (a, b, c)
mapOps mp :: SymbolMap
mp (a :: a
a, b :: b
b, c :: c
c) = (SymbolMap -> a -> a
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp a
a, SymbolMap -> b -> b
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp b
b, SymbolMap -> c -> c
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp c
c)
instance (Ord a, HasOps a) => HasOps (Set a) where
getOps :: Set a -> SymbolSet
getOps = (a -> SymbolSet -> SymbolSet) -> SymbolSet -> Set a -> SymbolSet
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (SymbolSet -> SymbolSet -> SymbolSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (SymbolSet -> SymbolSet -> SymbolSet)
-> (a -> SymbolSet) -> a -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps) SymbolSet
forall a. Set a
Set.empty
mapOps :: SymbolMap -> Set a -> Set a
mapOps = (a -> a) -> Set a -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((a -> a) -> Set a -> Set a)
-> (SymbolMap -> a -> a) -> SymbolMap -> Set a -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolMap -> a -> a
forall a. HasOps a => SymbolMap -> a -> a
mapOps
instance HasOps Operator where
getOps :: Operator -> SymbolSet
getOps = Operator -> SymbolSet
forall a. AsSymbol a => a -> SymbolSet
asSymbolSet
mapOps :: SymbolMap -> Operator -> Operator
mapOps mp :: SymbolMap
mp op :: Operator
op@(Op _ _ _ as :: [Attr]
as) = let
swapAttrs :: Operator -> Operator
swapAttrs (Op qid :: OpId
qid dom :: [Type]
dom cod :: Type
cod _) = OpId -> [Type] -> Type -> [Attr] -> Operator
Op OpId
qid [Type]
dom Type
cod [Attr]
as
in (Symbol -> Operator) -> SymbolMap -> Operator -> Operator
forall a. AsSymbol a => (Symbol -> a) -> SymbolMap -> a -> a
mapAsSymbol (Operator -> Operator
swapAttrs (Operator -> Operator)
-> (Symbol -> Operator) -> Symbol -> Operator
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Operator
toOperator) SymbolMap
mp Operator
op
instance HasOps Attr where
getOps :: Attr -> SymbolSet
getOps attr :: Attr
attr = case Attr
attr of
Id term :: Term
term -> Term -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps Term
term
LeftId term :: Term
term -> Term -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps Term
term
RightId term :: Term
term -> Term -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps Term
term
_ -> SymbolSet
forall a. Set a
Set.empty
mapOps :: SymbolMap -> Attr -> Attr
mapOps mp :: SymbolMap
mp attr :: Attr
attr = case Attr
attr of
Id term :: Term
term -> Term -> Attr
Id (Term -> Attr) -> Term -> Attr
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
term
LeftId term :: Term
term -> Term -> Attr
LeftId (Term -> Attr) -> Term -> Attr
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
term
RightId term :: Term
term -> Term -> Attr
RightId (Term -> Attr) -> Term -> Attr
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
term
_ -> Attr
attr
instance HasOps Term where
getOps :: Term -> SymbolSet
getOps term :: Term
term = case Term
term of
Apply _ ts :: [Term]
ts _ -> Symbol -> SymbolSet -> SymbolSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (Term -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Term
term) ([Term] -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps [Term]
ts)
_ -> SymbolSet
forall a. Set a
Set.empty
mapOps :: SymbolMap -> Term -> Term
mapOps mp :: SymbolMap
mp term :: Term
term = case Term
term of
Apply _ ts :: [Term]
ts tp :: Type
tp -> let
op :: Qid
op = Symbol -> Qid
forall a. HasName a => a -> Qid
getName (Symbol -> Qid) -> Symbol -> Qid
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Symbol -> Symbol
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Term -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Term
term
in Qid -> [Term] -> Type -> Term
Apply Qid
op (SymbolMap -> [Term] -> [Term]
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp [Term]
ts) Type
tp
_ -> Term
term
instance HasOps Condition where
getOps :: Condition -> SymbolSet
getOps cond :: Condition
cond = case Condition
cond of
EqCond t1 :: Term
t1 t2 :: Term
t2 -> (Term, Term) -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps (Term
t1, Term
t2)
MbCond t :: Term
t _ -> Term -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps Term
t
MatchCond t1 :: Term
t1 t2 :: Term
t2 -> (Term, Term) -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps (Term
t1, Term
t2)
RwCond t1 :: Term
t1 t2 :: Term
t2 -> (Term, Term) -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps (Term
t1, Term
t2)
mapOps :: SymbolMap -> Condition -> Condition
mapOps mp :: SymbolMap
mp cond :: Condition
cond = case Condition
cond of
EqCond t1 :: Term
t1 t2 :: Term
t2 -> Term -> Term -> Condition
EqCond (SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t1) (SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t2)
MbCond t :: Term
t s :: Sort
s -> Term -> Sort -> Condition
MbCond (SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t) Sort
s
MatchCond t1 :: Term
t1 t2 :: Term
t2 -> Term -> Term -> Condition
MatchCond (SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t1) (SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t2)
RwCond t1 :: Term
t1 t2 :: Term
t2 -> Term -> Term -> Condition
RwCond (SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t1) (SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t2)
instance HasOps Membership where
getOps :: Membership -> SymbolSet
getOps (Mb t :: Term
t _ cs :: [Condition]
cs _) = (Term, [Condition]) -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps (Term
t, [Condition]
cs)
mapOps :: SymbolMap -> Membership -> Membership
mapOps mp :: SymbolMap
mp (Mb t :: Term
t s :: Sort
s cs :: [Condition]
cs as :: [StmntAttr]
as) = let
t' :: Term
t' = SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t
cs' :: [Condition]
cs' = SymbolMap -> [Condition] -> [Condition]
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp [Condition]
cs
in Term -> Sort -> [Condition] -> [StmntAttr] -> Membership
Mb Term
t' Sort
s [Condition]
cs' [StmntAttr]
as
instance HasOps Equation where
getOps :: Equation -> SymbolSet
getOps (Eq t1 :: Term
t1 t2 :: Term
t2 cs :: [Condition]
cs _) = (Term, Term, [Condition]) -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps (Term
t1, Term
t2, [Condition]
cs)
mapOps :: SymbolMap -> Equation -> Equation
mapOps mp :: SymbolMap
mp (Eq t1 :: Term
t1 t2 :: Term
t2 cs :: [Condition]
cs as :: [StmntAttr]
as) = let
t1' :: Term
t1' = SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t1
t2' :: Term
t2' = SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t2
cs' :: [Condition]
cs' = SymbolMap -> [Condition] -> [Condition]
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp [Condition]
cs
in Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t1' Term
t2' [Condition]
cs' [StmntAttr]
as
instance HasOps Rule where
getOps :: Rule -> SymbolSet
getOps (Rl t1 :: Term
t1 t2 :: Term
t2 cs :: [Condition]
cs _) = (Term, Term, [Condition]) -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps (Term
t1, Term
t2, [Condition]
cs)
mapOps :: SymbolMap -> Rule -> Rule
mapOps mp :: SymbolMap
mp (Rl t1 :: Term
t1 t2 :: Term
t2 cs :: [Condition]
cs as :: [StmntAttr]
as) = let
t1' :: Term
t1' = SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t1
t2' :: Term
t2' = SymbolMap -> Term -> Term
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Term
t2
cs' :: [Condition]
cs' = SymbolMap -> [Condition] -> [Condition]
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp [Condition]
cs
in Term -> Term -> [Condition] -> [StmntAttr] -> Rule
Rl Term
t1' Term
t2' [Condition]
cs' [StmntAttr]
as