content: {-# 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 sym = case sym of
          Sort _ -> Set.singleton sym
          Kind _ -> Set.singleton $ asSort sym
          Operator _ dom cod -> getSorts (dom, cod)
          OpWildcard _ -> Set.empty
          Labl _ -> Set.empty
      mapSorts mp sym = case sym of
          Sort _ -> mapAsSymbol id mp sym
          Kind _ -> mapAsSymbol asKind mp $ asSort sym
          Operator qid dom cod -> let
                  dom' = mapSorts mp dom
                  cod' = mapSorts mp cod
              in Operator qid dom' cod'
          OpWildcard _ -> sym
          Labl _ -> sym
  
  instance (HasSorts a) => HasSorts [a] where
      getSorts = Set.unions . map getSorts
      mapSorts = map . mapSorts
  
  instance (HasSorts a, HasSorts b) => HasSorts (a, b) where
      getSorts (a, b) = Set.union (getSorts a) (getSorts b)
      mapSorts mp (a, b) = (mapSorts mp a, mapSorts mp b)
  
  instance (HasSorts a, HasSorts b, HasSorts c) => HasSorts (a, b, c) where
      getSorts (a, b, c) = Set.union (getSorts a) (getSorts (b, c))
      mapSorts mp (a, b, c) = (mapSorts mp a, mapSorts mp b, mapSorts mp c)
  
  instance (Ord a, HasSorts a) => HasSorts (Set a) where
      getSorts = Set.fold (Set.union . getSorts) Set.empty
      mapSorts = Set.map . mapSorts
  
  instance {-# OVERLAPS #-} (Ord a, HasSorts a) => HasSorts (Map k a) where
      getSorts = Map.foldr (Set.union . getSorts) Set.empty
      mapSorts = Map.map . mapSorts
  
  instance (Ord a, HasSorts a) => HasSorts (Rel a) where
      getSorts = getSorts . Rel.nodes
      mapSorts = Rel.map . mapSorts
  
  instance HasSorts Sort where
      getSorts = asSymbolSet
      mapSorts = mapAsSymbol $ SortId . getName
  
  instance HasSorts Kind where
      getSorts = asSymbolSet
      mapSorts = mapAsSymbol $ KindId . getName
  
  instance HasSorts Type where
      getSorts typ = case typ of
          TypeSort sort -> getSorts sort
          TypeKind kind -> getSorts kind
      mapSorts mp typ = case typ of
          TypeSort sort -> TypeSort $ mapSorts mp sort
          TypeKind kind -> TypeKind $ mapSorts mp kind
  
  instance HasSorts Operator where
      getSorts (Op _ dom cod _) = getSorts (dom, cod)
      mapSorts mp (Op op dom cod as) = let
              dom' = mapSorts mp dom
              cod' = mapSorts mp cod
          in Op op dom' cod' as
  
  instance HasSorts Attr where
      getSorts attr = case attr of
          Id term -> getSorts term
          LeftId term -> getSorts term
          RightId term -> getSorts term
          _ -> Set.empty
      mapSorts mp attr = case attr of
          Id term -> Id $ mapSorts mp term
          LeftId term -> LeftId $ mapSorts mp term
          RightId term -> RightId $ mapSorts mp term
          _ -> attr
  
  instance HasSorts Term where
      getSorts term = case term of
          Const _ tp -> getSorts tp
          Var _ tp -> getSorts tp
          Apply _ ts tp -> getSorts (ts, tp)
      mapSorts mp term = case term of
          Const con tp -> Const con (mapSorts mp tp)
          Var var tp -> Var var (mapSorts mp tp)
          Apply op ts tp -> Apply op (mapSorts mp ts) (mapSorts mp tp)
  
  instance HasSorts Condition where
      getSorts cond = case cond of
          EqCond t1 t2 -> getSorts (t1, t2)
          MbCond t s -> getSorts (t, s)
          MatchCond t1 t2 -> getSorts (t1, t2)
          RwCond t1 t2 -> getSorts (t1, t2)
      mapSorts mp cond = case cond of
          EqCond t1 t2 -> EqCond (mapSorts mp t1) (mapSorts mp t2)
          MbCond t s -> MbCond (mapSorts mp t) (mapSorts mp s)
          MatchCond t1 t2 -> MatchCond (mapSorts mp t1) (mapSorts mp t2)
          RwCond t1 t2 -> RwCond (mapSorts mp t1) (mapSorts mp t2)
  
  instance HasSorts Membership where
      getSorts (Mb t s cs _) = getSorts (t, s, cs)
      mapSorts mp (Mb t s cs as) = let
              t' = mapSorts mp t
              s' = mapSorts mp s
              cs' = mapSorts mp cs
          in Mb t' s' cs' as
  
  instance HasSorts Equation where
      getSorts (Eq t1 t2 cs _) = getSorts (t1, t2, cs)
      mapSorts mp (Eq t1 t2 cs as) = let
              t1' = mapSorts mp t1
              t2' = mapSorts mp t2
              cs' = mapSorts mp cs
          in Eq t1' t2' cs' as
  
  instance HasSorts Rule where
      getSorts (Rl t1 t2 cs _) = getSorts (t1, t2, cs)
      mapSorts mp (Rl t1 t2 cs as) = let
              t1' = mapSorts mp t1
              t2' = mapSorts mp t2
              cs' = mapSorts mp cs
          in Rl t1' t2' cs' as
  