content: {- |
  Module      :  ./CASL/World.hs
  Description :  adding a parameter to ops and preds
  Copyright   :  (c) Christian Maeder, DFKI 2012
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  add a parameter like the world sort for Modal CASL
  -}
  
  module CASL.World where
  
  import Common.Id
  import qualified Common.Lib.MapSet as MapSet
  
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.Morphism
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  world :: SORT
  world = genName "World"
  
  {- | mixfix identifiers need to be extended by a further place holder.  That
  is, identifiers are renamed, although a wrong number of place holders would
  allow to use the prefix notation. To avoid a name clashes with existing names
  the first place holder is preceded by a further place holder and a generated
  token. -}
  addPlace :: Id -> Id
  addPlace i@(Id ts ids ps)
      | isMixfix i = Id ((\ (x, y) -> x ++ placeTok : genToken "W" : y)
                            (break isPlace ts)) ids ps
      | otherwise = i
  
  -- | the changed mapping
  addWorld :: Ord a => (a -> a) -> (Id -> Id) -> MapSet.MapSet Id a
    -> MapSet.MapSet Id a
  addWorld f ren =
    MapSet.fromMap . Map.mapKeys ren . MapSet.toMap . MapSet.map f
  
  worldOpType :: SORT -> OpType -> OpType
  worldOpType ws t = t { opArgs = ws : opArgs t}
  
  -- | the changed op map
  addWorldOp :: SORT -> (Id -> Id) -> OpMap -> OpMap
  addWorldOp = addWorld . worldOpType
  
  worldPredType :: SORT -> PredType -> PredType
  worldPredType ws t = t { predArgs = ws : predArgs t}
  
  -- | the changed pred map
  addWorldPred :: SORT -> (Id -> Id) -> PredMap -> PredMap
  addWorldPred = addWorld . worldPredType
  
  -- | create a predicate name for time, simple and term modalities
  relOfMod :: Bool -> Bool -> SORT -> Id
  relOfMod time term m = let s = if time then "T" else "R" in
    Id [genToken $ if term then s ++ "_t" else s] [m] $ rangeOfId m
  
  -- | create a predicate name for simple and term modalities
  relName :: Bool -> SORT -> Id
  relName = relOfMod False
  
  -- | insert a simple or term modality
  insertModPred :: SORT -> Bool -> Bool -> Id -> PredMap -> PredMap
  insertModPred ws time term m = MapSet.insert (relOfMod time term m)
     $ modPredType ws term m
  
  modPredType :: SORT -> Bool -> SORT -> PredType
  modPredType ws term m = PredType $ (if term then (m :) else id) [ws, ws]
  
  -- | the renaming as part of a morphism
  renMorphism :: Ord a => (Id -> Id) -> MapSet.MapSet Id a -> Map.Map (Id, a) Id
  renMorphism ren = Map.foldrWithKey (\ i s ->
     let j = ren i in
     if j == i then id else
         Map.union . Map.fromAscList . map (\ a -> ((j, a), j)) $ Set.toList s)
     Map.empty . MapSet.toMap
  
  renOpMorphism :: (Id -> Id) -> OpMap -> Op_map
  renOpMorphism ren = Map.mapWithKey (\ (_, t) i -> (i, opKind t))
    . renMorphism ren
  
  renPredMorphism :: (Id -> Id) -> PredMap -> Pred_map
  renPredMorphism = renMorphism
  