765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederDescription : adding a parameter to ops and preds
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederCopyright : (c) Christian Maeder, DFKI 2012
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederMaintainer : Christian.Maeder@dfki.de
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederStability : provisional
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederPortability : portable
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederadd a parameter like the world sort for Modal CASL
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport qualified Common.Lib.MapSet as MapSet
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport qualified Data.Map as Map
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport qualified Data.Set as Set
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederworld = genName "World"
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder{- | mixfix identifiers need to be extended by a further place holder. That
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederis, identifiers are renamed, although a wrong number of place holders would
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederallow to use the prefix notation. To avoid a name clashes with existing names
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederthe first place holder is preceded by a further place holder and a generated
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederaddPlace :: Id -> Id
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederaddPlace i@(Id ts ids ps)
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder | isMixfix i = Id ((\ (x, y) -> x ++ placeTok : genToken "W" : y)
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder (break isPlace ts)) ids ps
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder | otherwise = i
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder-- | the changed mapping
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederaddWorld :: Ord a => (a -> a) -> (Id -> Id) -> MapSet.MapSet Id a
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederaddWorld f ren =
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder MapSet.fromMap . Map.mapKeys ren . MapSet.toMap . MapSet.map f
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian MaederworldOpType :: SORT -> OpType -> OpType
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian MaederworldOpType ws t = t { opArgs = ws : opArgs t}
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder-- | the changed op map
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederaddWorldOp :: SORT -> (Id -> Id) -> OpMap -> OpMap
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian MaederaddWorldOp = addWorld . worldOpType
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian MaederworldPredType :: SORT -> PredType -> PredType
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian MaederworldPredType ws t = t { predArgs = ws : predArgs t}
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian Maeder-- | the changed pred map
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederaddWorldPred :: SORT -> (Id -> Id) -> PredMap -> PredMap
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian MaederaddWorldPred = addWorld . worldPredType
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder-- | create a predicate name for time, simple and term modalities
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaederrelOfMod :: Bool -> Bool -> SORT -> Id
17f1de180b775332d98ff24c7ce51d6866272dcdChristian MaederrelOfMod time term m = let s = if time then "T" else "R" in
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder Id [genToken $ if term then s ++ "_t" else s] [m] $ rangeOfId m
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder-- | create a predicate name for simple and term modalities
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaederrelName :: Bool -> SORT -> Id
17f1de180b775332d98ff24c7ce51d6866272dcdChristian MaederrelName = relOfMod False
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder-- | insert a simple or term modality
17f1de180b775332d98ff24c7ce51d6866272dcdChristian MaederinsertModPred :: SORT -> Bool -> Bool -> Id -> PredMap -> PredMap
17f1de180b775332d98ff24c7ce51d6866272dcdChristian MaederinsertModPred ws time term m = MapSet.insert (relOfMod time term m)
16779ccfe622e9db869898f724bc0132b90cb7d7Christian Maeder $ modPredType ws term m
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaedermodPredType :: SORT -> Bool -> SORT -> PredType
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaedermodPredType ws term m = PredType $ (if term then (m :) else id) [ws, ws]
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder-- | the renaming as part of a morphism
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederrenMorphism :: Ord a => (Id -> Id) -> MapSet.MapSet Id a -> Map.Map (Id, a) Id
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederrenMorphism ren = Map.foldWithKey (\ i s ->
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder let j = ren i in
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder if j == i then id else
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder Map.union . Map.fromAscList . map (\ a -> ((j, a), j)) $ Set.toList s)
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederrenOpMorphism :: (Id -> Id) -> OpMap -> Op_map
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederrenOpMorphism ren = Map.mapWithKey (\ (_, t) i -> (i, opKind t))
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder . renMorphism ren
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederrenPredMorphism :: (Id -> Id) -> PredMap -> Pred_map
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederrenPredMorphism = renMorphism