{- |
Module      :  ./CASL/Qualify.hs
Description :  Code out overloading and qualify all names
Copyright   :  (c) Christian Maeder, DFKI GmbH 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Code out overloading and qualify all names
-}

module CASL.Qualify
  ( qualifySig
  , qualifySigExt
  , inverseMorphism
  ) where

import CASL.AS_Basic_CASL
import CASL.Disambiguate
import CASL.Sign
import CASL.Morphism
import CASL.Monoton

import Common.AS_Annotation
import Common.Id
import Common.LibName
import Common.Result
import qualified Common.Lib.MapSet as MapSet

import Control.Monad
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map
import qualified Data.Set as Set

mkOrReuseQualSortName :: Sort_map -> SIMPLE_ID -> LibName -> Id -> Id
mkOrReuseQualSortName :: Sort_map -> SIMPLE_ID -> LibName -> Id -> Id
mkOrReuseQualSortName sm :: Sort_map
sm nodeId :: SIMPLE_ID
nodeId libId :: LibName
libId i :: Id
i =
  case Id -> Sort_map -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i Sort_map
sm of
    Just j :: Id
j | Id -> Bool
isQualName Id
j -> Id
j
    _ -> SIMPLE_ID -> LibName -> Id -> Id
mkQualName SIMPLE_ID
nodeId LibName
libId Id
i

qualifySig :: SIMPLE_ID -> LibName -> Morphism f e () -> Sign f e
           -> Result (Morphism f e (), [Named (FORMULA f)])
qualifySig :: SIMPLE_ID
-> LibName
-> Morphism f e ()
-> Sign f e
-> Result (Morphism f e (), [Named (FORMULA f)])
qualifySig = InducedSign f e () e
-> ()
-> SIMPLE_ID
-> LibName
-> Morphism f e ()
-> Sign f e
-> Result (Morphism f e (), [Named (FORMULA f)])
forall f e m.
InducedSign f e m e
-> m
-> SIMPLE_ID
-> LibName
-> Morphism f e m
-> Sign f e
-> Result (Morphism f e m, [Named (FORMULA f)])
qualifySigExt (\ _ _ _ _ -> Sign f e -> e
forall f e. Sign f e -> e
extendedInfo) ()

qualifySigExt :: InducedSign f e m e -> m -> SIMPLE_ID -> LibName
              -> Morphism f e m -> Sign f e
              -> Result (Morphism f e m, [Named (FORMULA f)])
qualifySigExt :: InducedSign f e m e
-> m
-> SIMPLE_ID
-> LibName
-> Morphism f e m
-> Sign f e
-> Result (Morphism f e m, [Named (FORMULA f)])
qualifySigExt extInd :: InducedSign f e m e
extInd extEm :: m
extEm nodeId :: SIMPLE_ID
nodeId libId :: LibName
libId m :: Morphism f e m
m sig :: Sign f e
sig = do
  let ps :: PredMap
ps = Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sig
      os :: OpMap
os = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sig
      ss :: Set Id
ss = Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
sig
      sm :: Sort_map
sm = (Id -> Sort_map -> Sort_map) -> Sort_map -> Set Id -> Sort_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ s :: Id
s -> Id -> Id -> Sort_map -> Sort_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
s
                    (Id -> Sort_map -> Sort_map) -> Id -> Sort_map -> Sort_map
forall a b. (a -> b) -> a -> b
$ Sort_map -> SIMPLE_ID -> LibName -> Id -> Id
mkOrReuseQualSortName (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m) SIMPLE_ID
nodeId LibName
libId Id
s)
           Sort_map
forall k a. Map k a
Map.empty Set Id
ss
      sMap :: Map Id Int
sMap = (Id -> Map Id Int -> Map Id Int)
-> Map Id Int -> Set Id -> Map Id Int
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Id -> Int -> Map Id Int -> Map Id Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
`Map.insert` 1) Map Id Int
forall k a. Map k a
Map.empty Set Id
ss
      om :: Map (Id, OpType) (Id, OpKind)
om = Map (Id, OpType) (Id, OpType) -> Map (Id, OpType) (Id, OpKind)
createOpMorMap (Map (Id, OpType) (Id, OpType) -> Map (Id, OpType) (Id, OpKind))
-> Map (Id, OpType) (Id, OpType) -> Map (Id, OpType) (Id, OpKind)
forall a b. (a -> b) -> a -> b
$ Map Id Int
-> Map (Id, OpType) Id
-> SIMPLE_ID
-> LibName
-> (OpType -> OpType)
-> (OpType -> OpType)
-> OpMap
-> Map (Id, OpType) (Id, OpType)
forall a.
Ord a =>
Map Id Int
-> Map (Id, a) Id
-> SIMPLE_ID
-> LibName
-> (a -> a)
-> (a -> a)
-> MapSet Id a
-> Map (Id, a) (Id, a)
qualOverloaded Map Id Int
sMap (((Id, OpKind) -> Id)
-> Map (Id, OpType) (Id, OpKind) -> Map (Id, OpType) Id
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Id, OpKind) -> Id
forall a b. (a, b) -> a
fst (Map (Id, OpType) (Id, OpKind) -> Map (Id, OpType) Id)
-> Map (Id, OpType) (Id, OpKind) -> Map (Id, OpType) Id
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Map (Id, OpType) (Id, OpKind)
forall f e m. Morphism f e m -> Map (Id, OpType) (Id, OpKind)
op_map Morphism f e m
m)
           SIMPLE_ID
nodeId LibName
libId (Sort_map -> OpType -> OpType
mapOpType Sort_map
sm) OpType -> OpType
mkPartial OpMap
os
      oMap :: Map Id Int
oMap = (Id -> Set OpType -> Map Id Int -> Map Id Int)
-> Map Id Int -> Map Id (Set OpType) -> Map Id Int
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i ->
             (Int -> Int -> Int) -> Id -> Int -> Map Id Int -> Map Id Int
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Id
i (Int -> Map Id Int -> Map Id Int)
-> (Set OpType -> Int) -> Set OpType -> Map Id Int -> Map Id Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set OpType -> Int
forall a. Set a -> Int
Set.size) Map Id Int
sMap (Map Id (Set OpType) -> Map Id Int)
-> Map Id (Set OpType) -> Map Id Int
forall a b. (a -> b) -> a -> b
$ OpMap -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
os
      pm :: Map (Id, PredType) Id
pm = ((Id, PredType) -> Id)
-> Map (Id, PredType) (Id, PredType) -> Map (Id, PredType) Id
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Id, PredType) -> Id
forall a b. (a, b) -> a
fst (Map (Id, PredType) (Id, PredType) -> Map (Id, PredType) Id)
-> Map (Id, PredType) (Id, PredType) -> Map (Id, PredType) Id
forall a b. (a -> b) -> a -> b
$ Map Id Int
-> Map (Id, PredType) Id
-> SIMPLE_ID
-> LibName
-> (PredType -> PredType)
-> (PredType -> PredType)
-> PredMap
-> Map (Id, PredType) (Id, PredType)
forall a.
Ord a =>
Map Id Int
-> Map (Id, a) Id
-> SIMPLE_ID
-> LibName
-> (a -> a)
-> (a -> a)
-> MapSet Id a
-> Map (Id, a) (Id, a)
qualOverloaded Map Id Int
oMap (Morphism f e m -> Map (Id, PredType) Id
forall f e m. Morphism f e m -> Map (Id, PredType) Id
pred_map Morphism f e m
m) SIMPLE_ID
nodeId LibName
libId
           (Sort_map -> PredType -> PredType
mapPredType Sort_map
sm) PredType -> PredType
forall a. a -> a
id PredMap
ps
  (Morphism f e m, [Named (FORMULA f)])
-> Result (Morphism f e m, [Named (FORMULA f)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
extEm Sign f e
sig (Sign f e -> Morphism f e m) -> Sign f e -> Morphism f e m
forall a b. (a -> b) -> a -> b
$ InducedSign f e m e -> InducedSign f e m (Sign f e)
forall f e m. InducedSign f e m e -> InducedSign f e m (Sign f e)
inducedSignAux InducedSign f e m e
extInd Sort_map
sm Map (Id, OpType) (Id, OpKind)
om Map (Id, PredType) Id
pm m
extEm Sign f e
sig)
    { sort_map :: Sort_map
sort_map = Sort_map
sm
    , op_map :: Map (Id, OpType) (Id, OpKind)
op_map = Map (Id, OpType) (Id, OpKind)
om
    , pred_map :: Map (Id, PredType) Id
pred_map = Map (Id, PredType) Id
pm }, Sign f e -> [Named (FORMULA f)]
forall f e. Sign f e -> [Named (FORMULA f)]
monotonicities Sign f e
sig)

qualOverloaded :: Ord a => Map.Map Id Int -> Map.Map (Id, a) Id -> SIMPLE_ID
               -> LibName -> (a -> a) -> (a -> a) -> MapSet.MapSet Id a
               -> Map.Map (Id, a) (Id, a)
qualOverloaded :: Map Id Int
-> Map (Id, a) Id
-> SIMPLE_ID
-> LibName
-> (a -> a)
-> (a -> a)
-> MapSet Id a
-> Map (Id, a) (Id, a)
qualOverloaded oMap :: Map Id Int
oMap rn :: Map (Id, a) Id
rn nodeId :: SIMPLE_ID
nodeId libId :: LibName
libId f :: a -> a
f g :: a -> a
g =
  (Id -> Set a -> Map (Id, a) (Id, a) -> Map (Id, a) (Id, a))
-> Map (Id, a) (Id, a) -> Map Id (Set a) -> Map (Id, a) (Id, a)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i s :: Set a
s m :: Map (Id, a) (Id, a)
m -> ((a, Int) -> Map (Id, a) (Id, a) -> Map (Id, a) (Id, a))
-> Map (Id, a) (Id, a) -> [(a, Int)] -> Map (Id, a) (Id, a)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (e :: a
e, n :: Int
n) -> let ge :: a
ge = a -> a
g a
e in
    (Id, a) -> (Id, a) -> Map (Id, a) (Id, a) -> Map (Id, a) (Id, a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id
i, a
ge)
      (case (Id, a) -> Map (Id, a) Id -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id
i, a
ge) Map (Id, a) Id
rn of
         Just j :: Id
j | Id -> Bool
isQualName Id
j -> Id
j
         _ -> SIMPLE_ID -> LibName -> Id -> Id
mkQualName SIMPLE_ID
nodeId LibName
libId (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$ Int -> Id -> Id
mkOverloadedId Int
n Id
i, a -> a
f a
e)) Map (Id, a) (Id, a)
m
                  ([(a, Int)] -> Map (Id, a) (Id, a))
-> [(a, Int)] -> Map (Id, a) (Id, a)
forall a b. (a -> b) -> a -> b
$ [a] -> [Int] -> [(a, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s) [1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Id -> Map Id Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault 0 Id
i Map Id Int
oMap ..])
    Map (Id, a) (Id, a)
forall k a. Map k a
Map.empty (Map Id (Set a) -> Map (Id, a) (Id, a))
-> (MapSet Id a -> Map Id (Set a))
-> MapSet Id a
-> Map (Id, a) (Id, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id a -> Map Id (Set a)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap

inverseMorphism :: (Morphism f e m -> Result m) -> Morphism f e m
  -> Result (Morphism f e m)
inverseMorphism :: (Morphism f e m -> Result m)
-> Morphism f e m -> Result (Morphism f e m)
inverseMorphism invExt :: Morphism f e m -> Result m
invExt m :: Morphism f e m
m = do
  m
iExt <- Morphism f e m -> Result m
invExt Morphism f e m
m
  let src :: Sign f e
src = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m
      ss :: Set Id
ss = Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
src
      os :: OpMap
os = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
src
      ps :: PredMap
ps = Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
src
      sm :: Sort_map
sm = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m
      om :: Map (Id, OpType) (Id, OpKind)
om = Morphism f e m -> Map (Id, OpType) (Id, OpKind)
forall f e m. Morphism f e m -> Map (Id, OpType) (Id, OpKind)
op_map Morphism f e m
m
      pm :: Map (Id, PredType) Id
pm = Morphism f e m -> Map (Id, PredType) Id
forall f e m. Morphism f e m -> Map (Id, PredType) Id
pred_map Morphism f e m
m
      ism :: Sort_map
ism = [(Id, Id)] -> Sort_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, Id)] -> Sort_map) -> [(Id, Id)] -> Sort_map
forall a b. (a -> b) -> a -> b
$ ((Id, Id) -> (Id, Id)) -> [(Id, Id)] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s1 :: Id
s1, s2 :: Id
s2) -> (Id
s2, Id
s1)) ([(Id, Id)] -> [(Id, Id)]) -> [(Id, Id)] -> [(Id, Id)]
forall a b. (a -> b) -> a -> b
$ Sort_map -> [(Id, Id)]
forall k a. Map k a -> [(k, a)]
Map.toList Sort_map
sm
      iom :: Map (Id, OpType) (Id, OpKind)
iom = [((Id, OpType), (Id, OpKind))] -> Map (Id, OpType) (Id, OpKind)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((Id, OpType), (Id, OpKind))] -> Map (Id, OpType) (Id, OpKind))
-> [((Id, OpType), (Id, OpKind))] -> Map (Id, OpType) (Id, OpKind)
forall a b. (a -> b) -> a -> b
$ (((Id, OpType), (Id, OpKind)) -> ((Id, OpType), (Id, OpKind)))
-> [((Id, OpType), (Id, OpKind))] -> [((Id, OpType), (Id, OpKind))]
forall a b. (a -> b) -> [a] -> [b]
map (\ ((i :: Id
i, t :: OpType
t), (j :: Id
j, k :: OpKind
k)) ->
                  ((Id
j, Sort_map -> OpType -> OpType
mapOpType Sort_map
sm OpType
t), (Id
i, OpKind
k))) ([((Id, OpType), (Id, OpKind))] -> [((Id, OpType), (Id, OpKind))])
-> [((Id, OpType), (Id, OpKind))] -> [((Id, OpType), (Id, OpKind))]
forall a b. (a -> b) -> a -> b
$ Map (Id, OpType) (Id, OpKind) -> [((Id, OpType), (Id, OpKind))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Id, OpType) (Id, OpKind)
om
      ipm :: Map (Id, PredType) Id
ipm = [((Id, PredType), Id)] -> Map (Id, PredType) Id
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((Id, PredType), Id)] -> Map (Id, PredType) Id)
-> [((Id, PredType), Id)] -> Map (Id, PredType) Id
forall a b. (a -> b) -> a -> b
$ (((Id, PredType), Id) -> ((Id, PredType), Id))
-> [((Id, PredType), Id)] -> [((Id, PredType), Id)]
forall a b. (a -> b) -> [a] -> [b]
map (\ ((i :: Id
i, t :: PredType
t), j :: Id
j) ->
                  ((Id
j, Sort_map -> PredType -> PredType
mapPredType Sort_map
sm PredType
t), Id
i)) ([((Id, PredType), Id)] -> [((Id, PredType), Id)])
-> [((Id, PredType), Id)] -> [((Id, PredType), Id)]
forall a b. (a -> b) -> a -> b
$ Map (Id, PredType) Id -> [((Id, PredType), Id)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Id, PredType) Id
pm
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Id
ss Set Id -> Set Id -> Bool
forall a. Eq a => a -> a -> Bool
== (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Sort_map -> Id -> Id
mapSort Sort_map
ism (Id -> Id) -> (Id -> Id) -> Id -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort_map -> Id -> Id
mapSort Sort_map
sm) Set Id
ss)
    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "no injective CASL sort mapping"
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (OpMap
os OpMap -> OpMap -> Bool
forall a. Eq a => a -> a -> Bool
== Sort_map -> Map (Id, OpType) (Id, OpKind) -> OpMap -> OpMap
inducedOpMap Sort_map
ism Map (Id, OpType) (Id, OpKind)
iom (Sort_map -> Map (Id, OpType) (Id, OpKind) -> OpMap -> OpMap
inducedOpMap Sort_map
sm Map (Id, OpType) (Id, OpKind)
om OpMap
os))
    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "no injective CASL op mapping"
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PredMap
ps PredMap -> PredMap -> Bool
forall a. Eq a => a -> a -> Bool
== Sort_map -> Map (Id, PredType) Id -> PredMap -> PredMap
inducedPredMap Sort_map
ism Map (Id, PredType) Id
ipm (Sort_map -> Map (Id, PredType) Id -> PredMap -> PredMap
inducedPredMap Sort_map
sm Map (Id, PredType) Id
pm PredMap
ps))
    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "no injective CASL pred mapping"
  Morphism f e m -> Result (Morphism f e m)
forall (m :: * -> *) a. Monad m => a -> m a
return (m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
iExt (Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
imageOfMorphism Morphism f e m
m) Sign f e
src)
    { sort_map :: Sort_map
sort_map = Sort_map
ism
    , op_map :: Map (Id, OpType) (Id, OpKind)
op_map = Map (Id, OpType) (Id, OpKind)
iom
    , pred_map :: Map (Id, PredType) Id
pred_map = Map (Id, PredType) Id
ipm }