{-# LANGUAGE TypeSynonymInstances #-}
{- |
Module      :  ./Maude/Meta/HasSorts.hs
Description :  Accessing the Sorts of Maude data types
Copyright   :  (c) Martin Kuehl, Uni Bremen 2008-2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  mkhl@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Accessing the Sorts of Maude data types.

Defines a type class 'HasSorts' that lets us access the 'Sort's of Maude
data types as 'SymbolSet's.

Consider importing "Maude.Meta" instead of this module.
-}

module Maude.Meta.HasSorts (
    -- * The HasSorts type class
    HasSorts (..)
) where

import Maude.AS_Maude
import Maude.Symbol
import Maude.Meta.AsSymbol
import Maude.Meta.HasName

import Data.Set (Set)
import Data.Map (Map)
import qualified Data.Set as Set
import qualified Data.Map as Map

import Common.Lib.Rel (Rel)
import qualified Common.Lib.Rel as Rel

-- * The HasSorts type class

-- | Represents something that contains a 'Set' of 'Sort's (as 'Symbol's).
class HasSorts a where
    -- | Extract the 'Sort's contained in the input.
    getSorts :: a -> SymbolSet
    -- | Map the 'Sort's contained in the input.
    mapSorts :: SymbolMap -> a -> a

-- * Predefined instances

instance HasSorts Symbol where
    getSorts :: Symbol -> SymbolSet
getSorts sym :: Symbol
sym = case Symbol
sym of
        Sort _ -> Symbol -> SymbolSet
forall a. a -> Set a
Set.singleton Symbol
sym
        Kind _ -> Symbol -> SymbolSet
forall a. a -> Set a
Set.singleton (Symbol -> SymbolSet) -> Symbol -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
asSort Symbol
sym
        Operator _ dom :: Symbols
dom cod :: Symbol
cod -> (Symbols, Symbol) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Symbols
dom, Symbol
cod)
        OpWildcard _ -> SymbolSet
forall a. Set a
Set.empty
        Labl _ -> SymbolSet
forall a. Set a
Set.empty
    mapSorts :: SymbolMap -> Symbol -> Symbol
mapSorts mp :: SymbolMap
mp sym :: Symbol
sym = case Symbol
sym of
        Sort _ -> (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
        Kind _ -> (Symbol -> Symbol) -> SymbolMap -> Symbol -> Symbol
forall a. AsSymbol a => (Symbol -> a) -> SymbolMap -> a -> a
mapAsSymbol Symbol -> Symbol
asKind SymbolMap
mp (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
asSort Symbol
sym
        Operator qid :: Qid
qid dom :: Symbols
dom cod :: Symbol
cod -> let
                dom' :: Symbols
dom' = SymbolMap -> Symbols -> Symbols
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Symbols
dom
                cod' :: Symbol
cod' = SymbolMap -> Symbol -> Symbol
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Symbol
cod
            in Qid -> Symbols -> Symbol -> Symbol
Operator Qid
qid Symbols
dom' Symbol
cod'
        OpWildcard _ -> Symbol
sym
        Labl _ -> Symbol
sym

instance (HasSorts a) => HasSorts [a] where
    getSorts :: [a] -> SymbolSet
getSorts = [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. HasSorts a => a -> SymbolSet
getSorts
    mapSorts :: SymbolMap -> [a] -> [a]
mapSorts = (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. HasSorts a => SymbolMap -> a -> a
mapSorts

instance (HasSorts a, HasSorts b) => HasSorts (a, b) where
    getSorts :: (a, b) -> SymbolSet
getSorts (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. HasSorts a => a -> SymbolSet
getSorts a
a) (b -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts b
b)
    mapSorts :: SymbolMap -> (a, b) -> (a, b)
mapSorts mp :: SymbolMap
mp (a :: a
a, b :: b
b) = (SymbolMap -> a -> a
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp a
a, SymbolMap -> b -> b
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp b
b)

instance (HasSorts a, HasSorts b, HasSorts c) => HasSorts (a, b, c) where
    getSorts :: (a, b, c) -> SymbolSet
getSorts (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. HasSorts a => a -> SymbolSet
getSorts a
a) ((b, c) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (b
b, c
c))
    mapSorts :: SymbolMap -> (a, b, c) -> (a, b, c)
mapSorts mp :: SymbolMap
mp (a :: a
a, b :: b
b, c :: c
c) = (SymbolMap -> a -> a
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp a
a, SymbolMap -> b -> b
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp b
b, SymbolMap -> c -> c
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp c
c)

instance (Ord a, HasSorts a) => HasSorts (Set a) where
    getSorts :: Set a -> SymbolSet
getSorts = (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. HasSorts a => a -> SymbolSet
getSorts) SymbolSet
forall a. Set a
Set.empty
    mapSorts :: SymbolMap -> Set a -> Set a
mapSorts = (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. HasSorts a => SymbolMap -> a -> a
mapSorts

instance {-# OVERLAPS #-} (Ord a, HasSorts a) => HasSorts (Map k a) where
    getSorts :: Map k a -> SymbolSet
getSorts = (a -> SymbolSet -> SymbolSet) -> SymbolSet -> Map k a -> SymbolSet
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (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. HasSorts a => a -> SymbolSet
getSorts) SymbolSet
forall a. Set a
Set.empty
    mapSorts :: SymbolMap -> Map k a -> Map k a
mapSorts = (a -> a) -> Map k a -> Map k a
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((a -> a) -> Map k a -> Map k a)
-> (SymbolMap -> a -> a) -> SymbolMap -> Map k a -> Map k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolMap -> a -> a
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts

instance (Ord a, HasSorts a) => HasSorts (Rel a) where
    getSorts :: Rel a -> SymbolSet
getSorts = Set a -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Set a -> SymbolSet) -> (Rel a -> Set a) -> Rel a -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel a -> Set a
forall a. Ord a => Rel a -> Set a
Rel.nodes
    mapSorts :: SymbolMap -> Rel a -> Rel a
mapSorts = (a -> a) -> Rel a -> Rel a
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map ((a -> a) -> Rel a -> Rel a)
-> (SymbolMap -> a -> a) -> SymbolMap -> Rel a -> Rel a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolMap -> a -> a
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts

instance HasSorts Sort where
    getSorts :: Sort -> SymbolSet
getSorts = Sort -> SymbolSet
forall a. AsSymbol a => a -> SymbolSet
asSymbolSet
    mapSorts :: SymbolMap -> Sort -> Sort
mapSorts = (Symbol -> Sort) -> SymbolMap -> Sort -> Sort
forall a. AsSymbol a => (Symbol -> a) -> SymbolMap -> a -> a
mapAsSymbol ((Symbol -> Sort) -> SymbolMap -> Sort -> Sort)
-> (Symbol -> Sort) -> SymbolMap -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Qid -> Sort
SortId (Qid -> Sort) -> (Symbol -> Qid) -> Symbol -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Qid
forall a. HasName a => a -> Qid
getName

instance HasSorts Kind where
    getSorts :: Kind -> SymbolSet
getSorts = Kind -> SymbolSet
forall a. AsSymbol a => a -> SymbolSet
asSymbolSet
    mapSorts :: SymbolMap -> Kind -> Kind
mapSorts = (Symbol -> Kind) -> SymbolMap -> Kind -> Kind
forall a. AsSymbol a => (Symbol -> a) -> SymbolMap -> a -> a
mapAsSymbol ((Symbol -> Kind) -> SymbolMap -> Kind -> Kind)
-> (Symbol -> Kind) -> SymbolMap -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$ Qid -> Kind
KindId (Qid -> Kind) -> (Symbol -> Qid) -> Symbol -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Qid
forall a. HasName a => a -> Qid
getName

instance HasSorts Type where
    getSorts :: Type -> SymbolSet
getSorts typ :: Type
typ = case Type
typ of
        TypeSort sort :: Sort
sort -> Sort -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Sort
sort
        TypeKind kind :: Kind
kind -> Kind -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Kind
kind
    mapSorts :: SymbolMap -> Type -> Type
mapSorts mp :: SymbolMap
mp typ :: Type
typ = case Type
typ of
        TypeSort sort :: Sort
sort -> Sort -> Type
TypeSort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Sort -> Sort
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Sort
sort
        TypeKind kind :: Kind
kind -> Kind -> Type
TypeKind (Kind -> Type) -> Kind -> Type
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Kind -> Kind
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Kind
kind

instance HasSorts Operator where
    getSorts :: Operator -> SymbolSet
getSorts (Op _ dom :: [Type]
dom cod :: Type
cod _) = ([Type], Type) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts ([Type]
dom, Type
cod)
    mapSorts :: SymbolMap -> Operator -> Operator
mapSorts mp :: SymbolMap
mp (Op op :: OpId
op dom :: [Type]
dom cod :: Type
cod as :: [Attr]
as) = let
            dom' :: [Type]
dom' = SymbolMap -> [Type] -> [Type]
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp [Type]
dom
            cod' :: Type
cod' = SymbolMap -> Type -> Type
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Type
cod
        in OpId -> [Type] -> Type -> [Attr] -> Operator
Op OpId
op [Type]
dom' Type
cod' [Attr]
as

instance HasSorts Attr where
    getSorts :: Attr -> SymbolSet
getSorts attr :: Attr
attr = case Attr
attr of
        Id term :: Term
term -> Term -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Term
term
        LeftId term :: Term
term -> Term -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Term
term
        RightId term :: Term
term -> Term -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Term
term
        _ -> SymbolSet
forall a. Set a
Set.empty
    mapSorts :: SymbolMap -> Attr -> Attr
mapSorts 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. HasSorts a => SymbolMap -> a -> a
mapSorts 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. HasSorts a => SymbolMap -> a -> a
mapSorts 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. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
term
        _ -> Attr
attr

instance HasSorts Term where
    getSorts :: Term -> SymbolSet
getSorts term :: Term
term = case Term
term of
        Const _ tp :: Type
tp -> Type -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Type
tp
        Var _ tp :: Type
tp -> Type -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Type
tp
        Apply _ ts :: [Term]
ts tp :: Type
tp -> ([Term], Type) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts ([Term]
ts, Type
tp)
    mapSorts :: SymbolMap -> Term -> Term
mapSorts mp :: SymbolMap
mp term :: Term
term = case Term
term of
        Const con :: Qid
con tp :: Type
tp -> Qid -> Type -> Term
Const Qid
con (SymbolMap -> Type -> Type
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Type
tp)
        Var var :: Qid
var tp :: Type
tp -> Qid -> Type -> Term
Var Qid
var (SymbolMap -> Type -> Type
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Type
tp)
        Apply op :: Qid
op ts :: [Term]
ts tp :: Type
tp -> Qid -> [Term] -> Type -> Term
Apply Qid
op (SymbolMap -> [Term] -> [Term]
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp [Term]
ts) (SymbolMap -> Type -> Type
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Type
tp)

instance HasSorts Condition where
    getSorts :: Condition -> SymbolSet
getSorts cond :: Condition
cond = case Condition
cond of
        EqCond t1 :: Term
t1 t2 :: Term
t2 -> (Term, Term) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Term
t1, Term
t2)
        MbCond t :: Term
t s :: Sort
s -> (Term, Sort) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Term
t, Sort
s)
        MatchCond t1 :: Term
t1 t2 :: Term
t2 -> (Term, Term) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Term
t1, Term
t2)
        RwCond t1 :: Term
t1 t2 :: Term
t2 -> (Term, Term) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Term
t1, Term
t2)
    mapSorts :: SymbolMap -> Condition -> Condition
mapSorts 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. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t1) (SymbolMap -> Term -> Term
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t2)
        MbCond t :: Term
t s :: Sort
s -> Term -> Sort -> Condition
MbCond (SymbolMap -> Term -> Term
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t) (SymbolMap -> Sort -> Sort
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Sort
s)
        MatchCond t1 :: Term
t1 t2 :: Term
t2 -> Term -> Term -> Condition
MatchCond (SymbolMap -> Term -> Term
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t1) (SymbolMap -> Term -> Term
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t2)
        RwCond t1 :: Term
t1 t2 :: Term
t2 -> Term -> Term -> Condition
RwCond (SymbolMap -> Term -> Term
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t1) (SymbolMap -> Term -> Term
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t2)

instance HasSorts Membership where
    getSorts :: Membership -> SymbolSet
getSorts (Mb t :: Term
t s :: Sort
s cs :: [Condition]
cs _) = (Term, Sort, [Condition]) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Term
t, Sort
s, [Condition]
cs)
    mapSorts :: SymbolMap -> Membership -> Membership
mapSorts 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. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t
            s' :: Sort
s' = SymbolMap -> Sort -> Sort
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Sort
s
            cs' :: [Condition]
cs' = SymbolMap -> [Condition] -> [Condition]
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp [Condition]
cs
        in Term -> Sort -> [Condition] -> [StmntAttr] -> Membership
Mb Term
t' Sort
s' [Condition]
cs' [StmntAttr]
as

instance HasSorts Equation where
    getSorts :: Equation -> SymbolSet
getSorts (Eq t1 :: Term
t1 t2 :: Term
t2 cs :: [Condition]
cs _) = (Term, Term, [Condition]) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Term
t1, Term
t2, [Condition]
cs)
    mapSorts :: SymbolMap -> Equation -> Equation
mapSorts 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. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t1
            t2' :: Term
t2' = SymbolMap -> Term -> Term
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t2
            cs' :: [Condition]
cs' = SymbolMap -> [Condition] -> [Condition]
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp [Condition]
cs
        in Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t1' Term
t2' [Condition]
cs' [StmntAttr]
as

instance HasSorts Rule where
    getSorts :: Rule -> SymbolSet
getSorts (Rl t1 :: Term
t1 t2 :: Term
t2 cs :: [Condition]
cs _) = (Term, Term, [Condition]) -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts (Term
t1, Term
t2, [Condition]
cs)
    mapSorts :: SymbolMap -> Rule -> Rule
mapSorts 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. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t1
            t2' :: Term
t2' = SymbolMap -> Term -> Term
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Term
t2
            cs' :: [Condition]
cs' = SymbolMap -> [Condition] -> [Condition]
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp [Condition]
cs
        in Term -> Term -> [Condition] -> [StmntAttr] -> Rule
Rl Term
t1' Term
t2' [Condition]
cs' [StmntAttr]
as