{- |
Module      :  ./CASL/Disambiguate.hs
Description :  disambiguate 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

Disambiguate all names that are not in the overload relation for CASL2OWL
-}

module CASL.Disambiguate where

import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Overload

import Common.Id
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import qualified Data.Map as Map
import qualified Data.Set as Set

mkOverloadedId :: Int -> Id -> Id
mkOverloadedId :: Int -> Id -> Id
mkOverloadedId n :: Int
n i :: Id
i@(Id ts :: [Token]
ts cs :: [Id]
cs rs :: Range
rs) = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 1 then Id
i else
  [Token] -> [Id] -> Range -> Id
Id ([Token]
ts [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String -> String
forall a. Show a => a -> String -> String
shows Int
n "o"]) [Id]
cs Range
rs

disambigSig :: Sign f e -> Morphism f e ()
disambigSig :: Sign f e -> Morphism f e ()
disambigSig = InducedSign f e () e -> () -> Sign f e -> Morphism f e ()
forall f e m.
InducedSign f e m e -> m -> Sign f e -> Morphism f e m
disambigSigExt (\ _ _ _ _ -> Sign f e -> e
forall f e. Sign f e -> e
extendedInfo) ()

-- note that op-type keys are always partial!
disambigSigExt :: InducedSign f e m e -> m -> Sign f e -> Morphism f e m
disambigSigExt :: InducedSign f e m e -> m -> Sign f e -> Morphism f e m
disambigSigExt extInd :: InducedSign f e m e
extInd extEm :: m
extEm sig :: Sign f e
sig =
  let ps :: Map Id [Set PredType]
ps = (Set PredType -> [Set PredType])
-> Map Id (Set PredType) -> Map Id [Set PredType]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((PredType -> PredType -> Bool) -> Set PredType -> [Set PredType]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet ((PredType -> PredType -> Bool) -> Set PredType -> [Set PredType])
-> (PredType -> PredType -> Bool) -> Set PredType -> [Set PredType]
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
sig) (Map Id (Set PredType) -> Map Id [Set PredType])
-> Map Id (Set PredType) -> Map Id [Set PredType]
forall a b. (a -> b) -> a -> b
$ MapSet Id PredType -> Map Id (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id PredType -> Map Id (Set PredType))
-> MapSet Id PredType -> Map Id (Set PredType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sig
      os :: Map Id [Set OpType]
os = (Set OpType -> [Set OpType])
-> Map Id (Set OpType) -> Map Id [Set OpType]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((OpType -> OpType -> Bool) -> Set OpType -> [Set OpType]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet ((OpType -> OpType -> Bool) -> Set OpType -> [Set OpType])
-> (OpType -> OpType -> Bool) -> Set OpType -> [Set OpType]
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
sig) (Map Id (Set OpType) -> Map Id [Set OpType])
-> Map Id (Set OpType) -> Map Id [Set OpType]
forall a b. (a -> b) -> a -> b
$ MapSet Id OpType -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id OpType -> Map Id (Set OpType))
-> MapSet Id OpType -> Map Id (Set OpType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
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
      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
-> (OpType -> OpType)
-> Map Id [Set OpType]
-> Map (Id, OpType) (Id, OpType)
forall a.
Ord a =>
Map Id Int -> (a -> a) -> Map Id [Set a] -> Map (Id, a) (Id, a)
disambOverloaded Map Id Int
sMap OpType -> OpType
mkPartial Map Id [Set OpType]
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 (t :: * -> *) a. Foldable t => t a -> Int
length) Map Id Int
sMap Map Id [Set OpType]
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
-> (PredType -> PredType)
-> Map Id [Set PredType]
-> Map (Id, PredType) (Id, PredType)
forall a.
Ord a =>
Map Id Int -> (a -> a) -> Map Id [Set a] -> Map (Id, a) (Id, a)
disambOverloaded Map Id Int
oMap PredType -> PredType
forall a. a -> a
id Map Id [Set PredType]
ps
  in (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 Map Id Id
forall k a. Map k a
Map.empty Map (Id, OpType) (Id, OpKind)
om Map (Id, PredType) Id
pm m
extEm Sign f e
sig)
    { 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 }

disambOverloaded :: Ord a => Map.Map Id Int
               -> (a -> a)
               -> Map.Map Id [Set.Set a]
               -> Map.Map (Id, a) (Id, a)
disambOverloaded :: Map Id Int -> (a -> a) -> Map Id [Set a] -> Map (Id, a) (Id, a)
disambOverloaded oMap :: Map Id Int
oMap 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 l :: [Set a]
l m :: Map (Id, a) (Id, a)
m ->
    ((Set a, Int) -> Map (Id, a) (Id, a) -> Map (Id, a) (Id, a))
-> Map (Id, a) (Id, a) -> [(Set a, Int)] -> Map (Id, a) (Id, a)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (s :: Set a
s, n :: Int
n) m2 :: Map (Id, a) (Id, a)
m2 -> let j :: Id
j = Int -> Id -> Id
mkOverloadedId Int
n Id
i in
      (a -> Map (Id, a) (Id, a) -> Map (Id, a) (Id, a))
-> Map (Id, a) (Id, a) -> Set a -> Map (Id, a) (Id, a)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ t :: a
t -> (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 -> a
g a
t) (Id
j, a
t)) Map (Id, a) (Id, a)
m2 Set a
s) Map (Id, a) (Id, a)
m
    ([(Set a, Int)] -> Map (Id, a) (Id, a))
-> [(Set a, Int)] -> Map (Id, a) (Id, a)
forall a b. (a -> b) -> a -> b
$ [Set a] -> [Int] -> [(Set a, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Set a]
l [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

createOpMorMap :: Map.Map (Id, OpType) (Id, OpType)
             -> Map.Map (Id, OpType) (Id, OpKind)
createOpMorMap :: Map (Id, OpType) (Id, OpType) -> Map (Id, OpType) (Id, OpKind)
createOpMorMap = ((Id, OpType) -> (Id, OpKind))
-> Map (Id, OpType) (Id, OpType) -> Map (Id, OpType) (Id, OpKind)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (i :: Id
i, t :: OpType
t) -> (Id
i, OpType -> OpKind
opKind OpType
t))