{- |
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 :: SORT
world = String -> SORT
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 :: SORT -> SORT
addPlace i :: SORT
i@(Id ts :: [Token]
ts ids :: [SORT]
ids ps :: Range
ps)
    | SORT -> Bool
isMixfix SORT
i = [Token] -> [SORT] -> Range -> SORT
Id ((\ (x :: [Token]
x, y :: [Token]
y) -> [Token]
x [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Token
placeTok Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: String -> Token
genToken "W" Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
y)
                          ((Token -> Bool) -> [Token] -> ([Token], [Token])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Token -> Bool
isPlace [Token]
ts)) [SORT]
ids Range
ps
    | Bool
otherwise = SORT
i

-- | the changed mapping
addWorld :: Ord a => (a -> a) -> (Id -> Id) -> MapSet.MapSet Id a
  -> MapSet.MapSet Id a
addWorld :: (a -> a) -> (SORT -> SORT) -> MapSet SORT a -> MapSet SORT a
addWorld f :: a -> a
f ren :: SORT -> SORT
ren =
  Map SORT (Set a) -> MapSet SORT a
forall a b. Ord a => Map a (Set b) -> MapSet a b
MapSet.fromMap (Map SORT (Set a) -> MapSet SORT a)
-> (MapSet SORT a -> Map SORT (Set a))
-> MapSet SORT a
-> MapSet SORT a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT -> SORT) -> Map SORT (Set a) -> Map SORT (Set a)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys SORT -> SORT
ren (Map SORT (Set a) -> Map SORT (Set a))
-> (MapSet SORT a -> Map SORT (Set a))
-> MapSet SORT a
-> Map SORT (Set a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet SORT a -> Map SORT (Set a)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet SORT a -> Map SORT (Set a))
-> (MapSet SORT a -> MapSet SORT a)
-> MapSet SORT a
-> Map SORT (Set a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a) -> MapSet SORT a -> MapSet SORT a
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map a -> a
f

worldOpType :: SORT -> OpType -> OpType
worldOpType :: SORT -> OpType -> OpType
worldOpType ws :: SORT
ws t :: OpType
t = OpType
t { opArgs :: [SORT]
opArgs = SORT
ws SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: OpType -> [SORT]
opArgs OpType
t}

-- | the changed op map
addWorldOp :: SORT -> (Id -> Id) -> OpMap -> OpMap
addWorldOp :: SORT -> (SORT -> SORT) -> OpMap -> OpMap
addWorldOp = (OpType -> OpType) -> (SORT -> SORT) -> OpMap -> OpMap
forall a.
Ord a =>
(a -> a) -> (SORT -> SORT) -> MapSet SORT a -> MapSet SORT a
addWorld ((OpType -> OpType) -> (SORT -> SORT) -> OpMap -> OpMap)
-> (SORT -> OpType -> OpType)
-> SORT
-> (SORT -> SORT)
-> OpMap
-> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> OpType -> OpType
worldOpType

worldPredType :: SORT -> PredType -> PredType
worldPredType :: SORT -> PredType -> PredType
worldPredType ws :: SORT
ws t :: PredType
t = PredType
t { predArgs :: [SORT]
predArgs = SORT
ws SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: PredType -> [SORT]
predArgs PredType
t}

-- | the changed pred map
addWorldPred :: SORT -> (Id -> Id) -> PredMap -> PredMap
addWorldPred :: SORT -> (SORT -> SORT) -> PredMap -> PredMap
addWorldPred = (PredType -> PredType) -> (SORT -> SORT) -> PredMap -> PredMap
forall a.
Ord a =>
(a -> a) -> (SORT -> SORT) -> MapSet SORT a -> MapSet SORT a
addWorld ((PredType -> PredType) -> (SORT -> SORT) -> PredMap -> PredMap)
-> (SORT -> PredType -> PredType)
-> SORT
-> (SORT -> SORT)
-> PredMap
-> PredMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> PredType -> PredType
worldPredType

-- | create a predicate name for time, simple and term modalities
relOfMod :: Bool -> Bool -> SORT -> Id
relOfMod :: Bool -> Bool -> SORT -> SORT
relOfMod time :: Bool
time term :: Bool
term m :: SORT
m = let s :: String
s = if Bool
time then "T" else "R" in
  [Token] -> [SORT] -> Range -> SORT
Id [String -> Token
genToken (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ if Bool
term then String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_t" else String
s] [SORT
m] (Range -> SORT) -> Range -> SORT
forall a b. (a -> b) -> a -> b
$ SORT -> Range
rangeOfId SORT
m

-- | create a predicate name for simple and term modalities
relName :: Bool -> SORT -> Id
relName :: Bool -> SORT -> SORT
relName = Bool -> Bool -> SORT -> SORT
relOfMod Bool
False

-- | insert a simple or term modality
insertModPred :: SORT -> Bool -> Bool -> Id -> PredMap -> PredMap
insertModPred :: SORT -> Bool -> Bool -> SORT -> PredMap -> PredMap
insertModPred ws :: SORT
ws time :: Bool
time term :: Bool
term m :: SORT
m = SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (Bool -> Bool -> SORT -> SORT
relOfMod Bool
time Bool
term SORT
m)
   (PredType -> PredMap -> PredMap) -> PredType -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ SORT -> Bool -> SORT -> PredType
modPredType SORT
ws Bool
term SORT
m

modPredType :: SORT -> Bool -> SORT -> PredType
modPredType :: SORT -> Bool -> SORT -> PredType
modPredType ws :: SORT
ws term :: Bool
term m :: SORT
m = [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ (if Bool
term then (SORT
m SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
:) else [SORT] -> [SORT]
forall a. a -> a
id) [SORT
ws, SORT
ws]

-- | the renaming as part of a morphism
renMorphism :: Ord a => (Id -> Id) -> MapSet.MapSet Id a -> Map.Map (Id, a) Id
renMorphism :: (SORT -> SORT) -> MapSet SORT a -> Map (SORT, a) SORT
renMorphism ren :: SORT -> SORT
ren = (SORT -> Set a -> Map (SORT, a) SORT -> Map (SORT, a) SORT)
-> Map (SORT, a) SORT -> Map SORT (Set a) -> Map (SORT, a) SORT
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: SORT
i s :: Set a
s ->
   let j :: SORT
j = SORT -> SORT
ren SORT
i in
   if SORT
j SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
i then Map (SORT, a) SORT -> Map (SORT, a) SORT
forall a. a -> a
id else
       Map (SORT, a) SORT -> Map (SORT, a) SORT -> Map (SORT, a) SORT
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map (SORT, a) SORT -> Map (SORT, a) SORT -> Map (SORT, a) SORT)
-> ([a] -> Map (SORT, a) SORT)
-> [a]
-> Map (SORT, a) SORT
-> Map (SORT, a) SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((SORT, a), SORT)] -> Map (SORT, a) SORT
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList ([((SORT, a), SORT)] -> Map (SORT, a) SORT)
-> ([a] -> [((SORT, a), SORT)]) -> [a] -> Map (SORT, a) SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> ((SORT, a), SORT)) -> [a] -> [((SORT, a), SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: a
a -> ((SORT
j, a
a), SORT
j)) ([a] -> Map (SORT, a) SORT -> Map (SORT, a) SORT)
-> [a] -> Map (SORT, a) SORT -> Map (SORT, a) SORT
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s)
   Map (SORT, a) SORT
forall k a. Map k a
Map.empty (Map SORT (Set a) -> Map (SORT, a) SORT)
-> (MapSet SORT a -> Map SORT (Set a))
-> MapSet SORT a
-> Map (SORT, a) SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet SORT a -> Map SORT (Set a)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap

renOpMorphism :: (Id -> Id) -> OpMap -> Op_map
renOpMorphism :: (SORT -> SORT) -> OpMap -> Op_map
renOpMorphism ren :: SORT -> SORT
ren = ((SORT, OpType) -> SORT -> (SORT, OpKind))
-> Map (SORT, OpType) SORT -> Op_map
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\ (_, t :: OpType
t) i :: SORT
i -> (SORT
i, OpType -> OpKind
opKind OpType
t))
  (Map (SORT, OpType) SORT -> Op_map)
-> (OpMap -> Map (SORT, OpType) SORT) -> OpMap -> Op_map
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT -> SORT) -> OpMap -> Map (SORT, OpType) SORT
forall a.
Ord a =>
(SORT -> SORT) -> MapSet SORT a -> Map (SORT, a) SORT
renMorphism SORT -> SORT
ren

renPredMorphism :: (Id -> Id) -> PredMap -> Pred_map
renPredMorphism :: (SORT -> SORT) -> PredMap -> Pred_map
renPredMorphism = (SORT -> SORT) -> PredMap -> Pred_map
forall a.
Ord a =>
(SORT -> SORT) -> MapSet SORT a -> Map (SORT, a) SORT
renMorphism