{- |

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 Data.Map as Map

import qualified Data.Set as Set

mkOrReuseQualSortName :: Sort_map -> SIMPLE_ID -> LibName -> Id -> Id

mkOrReuseQualSortName sm nodeId libId i =

case Map.lookup i sm of

Just j | isQualName j -> j

_ -> mkQualName nodeId libId i

qualifySig :: SIMPLE_ID -> LibName -> Morphism f e () -> Sign f e

-> Result (Morphism f e (), [Named (FORMULA f)])

qualifySig = qualifySigExt (\ _ _ _ _ -> 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 extInd extEm nodeId libId m sig = do

let ps = predMap sig

os = opMap sig

ss = sortSet sig

sm = Set.fold (\ s -> Map.insert s

$ mkOrReuseQualSortName (sort_map m) nodeId libId s)

Map.empty ss

sMap = Set.fold (`Map.insert` 1) Map.empty ss

om = createOpMorMap $ qualOverloaded sMap (Map.map fst $ op_map m)

nodeId libId (mapOpType sm) mkPartial os

oMap = Map.foldWithKey (\ i ->

Map.insertWith (+) i . Set.size) sMap $ MapSet.toMap os

pm = Map.map fst $ qualOverloaded oMap (pred_map m) nodeId libId

(mapPredType sm) id ps

return ((embedMorphism extEm sig $ inducedSignAux extInd sm om pm extEm sig)

{ sort_map = sm

, op_map = om

, pred_map = pm }, monotonicities 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 oMap rn nodeId libId f g =

Map.foldWithKey (\ i s m -> foldr (\ (e, n) -> let ge = g e in

Map.insert (i, ge)

(case Map.lookup (i, ge) rn of

Just j | isQualName j -> j

_ -> mkQualName nodeId libId $ mkOverloadedId n i, f e)) m

$ zip (Set.toList s) [1 + Map.findWithDefault 0 i oMap ..])

Map.empty . MapSet.toMap

inverseMorphism :: (Morphism f e m -> Result m) -> Morphism f e m

-> Result (Morphism f e m)

inverseMorphism invExt m = do

iExt <- invExt m

let src = msource m

ss = sortSet src

os = opMap src

ps = predMap src

sm = sort_map m

om = op_map m

pm = pred_map m

ism = Map.fromList $ map (\ (s1, s2) -> (s2, s1)) $ Map.toList sm

iom = Map.fromList $ map (\ ((i, t), (j, k)) ->

((j, mapOpType sm t), (i, k))) $ Map.toList om

ipm = Map.fromList $ map (\ ((i, t), j) ->

((j, mapPredType sm t), i)) $ Map.toList pm

unless (ss == Set.map (mapSort ism . mapSort sm) ss)

$ fail "no injective CASL sort mapping"

unless (os == inducedOpMap ism iom (inducedOpMap sm om os))

$ fail "no injective CASL op mapping"

unless (ps == inducedPredMap ism ipm (inducedPredMap sm pm ps))

$ fail "no injective CASL pred mapping"

return (embedMorphism iExt (imageOfMorphism m) src)

{ sort_map = ism

, op_map = iom

, pred_map = ipm }