4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- |

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederModule : $Header$

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDescription : morphisms implementation

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederMaintainer : Christian.Maeder@dfki.de

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederStability : provisional

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederPortability : portable

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedermapping entities of morphisms

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-}

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedermodule HasCASL.Morphism where

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport HasCASL.Le

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport HasCASL.As

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport HasCASL.TypeAna

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport HasCASL.AsUtils

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport HasCASL.AsToLe

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport HasCASL.MapTerm

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport HasCASL.Merge

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.DocUtils

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Id

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Result

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Data.Map as Map

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Data.List ((\\))

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Eq Morphism where

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder m1 == m2 = (msource m1, mtarget m1, typeIdMap m1, funMap m1) ==

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (msource m2, mtarget m2, typeIdMap m2, funMap m2)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | map type and expand it

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapTypeE :: TypeMap -> IdMap -> Type -> Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapTypeE tm im = expandAliases tm . mapType im

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapTypeScheme :: TypeMap -> IdMap -> TypeScheme -> TypeScheme

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapTypeScheme tm im = mapTypeOfScheme $ mapTypeE tm im

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapSen :: TypeMap -> IdMap -> FunMap -> Term -> Term

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapSen tm im fm = mapTerm (mapFunSym tm im fm, mapTypeE tm im)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapDataEntry :: TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapDataEntry tm im fm (DataEntry dm i k args rk alts) =

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder let tim = compIdMap dm im

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder in DataEntry tim i k args rk $ map

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (mapAlt tm tim fm args $ patToType (Map.findWithDefault i i tim)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder args rk) alts

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapAlt :: TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> AltDefn

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapAlt tm im fm args dt c@(Construct mi ts p sels) =

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder case mi of

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Just i ->

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder let sc = TypeScheme args

(getFunType dt p $ map (mapTypeE tm im) ts) nullRange

(j, TypeScheme _ ty _) = mapFunSym tm im fm (i, sc)

in Construct (Just j) ts (getPartiality ts ty) $

map (map (mapSel tm im fm args dt)) sels

Nothing -> c

mapSel :: TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> Selector

-> Selector

mapSel tm im fm args dt s@(Select mid t p) = case mid of

Nothing -> s

Just i -> let

sc = TypeScheme args (getSelType dt p $ mapTypeE tm im t) nullRange

(j, TypeScheme _ ty _) = mapFunSym tm im fm (i, sc)

in Select (Just j) t $ getPartiality [dt] ty

-- | get the partiality from a constructor type

-- with a given number of curried arguments

getPartiality :: [a] -> Type -> Partiality

getPartiality args t = case getTypeAppl t of

(TypeName i _ _, [_, res]) | isArrow i -> case args of

[] -> Total

[_] -> if isPartialArrow i then Partial else Total

_ : rs -> getPartiality rs res

(TypeName i _ _, [_]) | i == lazyTypeId ->

if null args then Partial else error "getPartiality"

_ -> Total

mapSentence :: Morphism -> Sentence -> Result Sentence

mapSentence m s = let

tm = filterAliases $ typeMap $ mtarget m

im = typeIdMap m

fm = funMap m

f = mapFunSym tm im fm

in return $ case s of

Formula t -> Formula $ mapSen tm im fm t

DatatypeSen td -> DatatypeSen $ map (mapDataEntry tm im fm) td

ProgEqSen i sc pe ->

let (ni, nsc) = f (i, sc)

in ProgEqSen ni nsc $ mapEq (f, mapTypeE tm im) pe

mapFunSym :: TypeMap -> IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)

mapFunSym tm im fm (i, sc) =

let msc = mapTypeScheme tm im sc

in Map.findWithDefault (i, msc) (i, msc) fm

embedMorphism :: Env -> Env -> Morphism

embedMorphism = mkMorphism

ideMor :: Env -> Morphism

ideMor e = embedMorphism e e

compIdMap :: IdMap -> IdMap -> IdMap

compIdMap im1 im2 = Map.foldWithKey ( \ i j ->

let k = Map.findWithDefault j j im2 in

if i == k then id else Map.insert i k)

im2 im1

compMor :: Morphism -> Morphism -> Result Morphism

compMor m1 m2 =

if mtarget m1 == msource m2 then

let tm2 = typeIdMap m2

im = compIdMap (typeIdMap m1) tm2

fm2 = funMap m2

tar = mtarget m2

src = msource m1

tm = filterAliases $ typeMap tar

in return (mkMorphism src tar)

{ typeIdMap = Map.intersection im $ typeMap src

, funMap = Map.intersection (Map.foldWithKey ( \ p1 p2 ->

let p3 = mapFunSym tm tm2 fm2 p2 in

if p1 == p3 then id else Map.insert p1 p3)

fm2 $ funMap m1) $ Map.fromList $

concatMap ( \ (k, OpInfos os) ->

map ( \ o -> ((k, mapTypeScheme tm im

$ opType o), ())) os)

$ Map.toList $ assumps src

}

else fail "intermediate signatures of morphisms do not match"

inclusionMor :: Env -> Env -> Result Morphism

inclusionMor e1 e2 =

if isSubEnv e1 e2

then return (embedMorphism e1 e2)

else Result [Diag Error

("Attempt to construct inclusion between non-subsignatures:\n"

++ showEnvDiff e1 e2) nullRange] Nothing

showEnvDiff :: Env -> Env -> String

showEnvDiff e1 e2 =

"Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"

++ showDoc e2 "\nDifference\n" ++ showDoc

(diffEnv e1 e2) ""

legalEnv :: Env -> Bool

legalEnv _ = True -- maybe a closure test?

legalMor :: Morphism -> Bool

legalMor m = let s = msource m

t = mtarget m

ts = typeIdMap m

fs = funMap m

in

all (`elem` (Map.keys $ typeMap s))

(Map.keys ts)

&& all (`elem` (Map.keys $ typeMap t))

(Map.elems ts)

&& all ((`elem` (Map.keys $ assumps s)) . fst)

(Map.keys fs)

&& all ((`elem` (Map.keys $ assumps t)) . fst)

(Map.elems fs)

morphismUnion :: Morphism -> Morphism -> Result Morphism

morphismUnion m1 m2 =

do let s1 = msource m1

s2 = msource m2

tm1 = Map.toList $ typeIdMap m1

tm2 = Map.toList $ typeIdMap m2

-- unchanged types

ut1 = Map.keys (typeMap s1) \\ map fst tm1

ut2 = Map.keys (typeMap s2) \\ map fst tm2

mkP = map ( \ a -> (a, a))

tml = tm1 ++ tm2 ++ mkP (ut1 ++ ut2)

fm1 = Map.toList $ funMap m1

fm2 = Map.toList $ funMap m2

-- all functions

af = concatMap ( \ (i, os) ->

map ( \ o -> (i, opType o)) $ opInfos os) . Map.toList

-- unchanged functions

uf1 = af (assumps s1) \\ map fst fm1

uf2 = af (assumps s2) \\ map fst fm2

fml = fm1 ++ fm2 ++ mkP (uf1 ++ uf2)

s <- merge s1 s2

t <- merge (mtarget m1) $ mtarget m2

let sAs = filterAliases $ typeMap s

tAs = filterAliases $ typeMap t

tm <- foldr ( \ (i, j) rm ->

do m <- rm

case Map.lookup i m of

Nothing -> return $ Map.insert i j m

Just k -> if j == k then return m

else fail ("incompatible mapping of type id: " ++

showId i " to: " ++ showId j " and: "

++ showId k ""))

(return Map.empty) tml

fm <- foldr ( \ (isc@(i, sc), jsc@(j, sc1)) rm -> do

let nsc = expand sAs sc1

nisc = (i, expand tAs sc)

m <- rm

case Map.lookup nisc m of

Nothing -> return $ Map.insert nisc

(j, nsc) m

Just ksc@(k, sc2) -> if j == k &&

nsc == sc2

then return m

else fail ("incompatible mapping of op: " ++

showFun isc " to: " ++ showFun jsc " and: "

++ showFun ksc ""))

(return Map.empty) fml

return (mkMorphism s t)

{ typeIdMap = Map.filterWithKey (/=) tm

, funMap = Map.filterWithKey (/=) fm }

showFun :: (Id, TypeScheme) -> ShowS

showFun (i, ty) = showId i . (" : " ++) . showDoc ty

morphismToSymbMap :: Morphism -> SymbolMap

morphismToSymbMap mor =

let

src = msource mor

tar = mtarget mor

im = typeIdMap mor

tm = filterAliases $ typeMap tar

typeSymMap = Map.foldWithKey ( \ i ti ->

let j = Map.findWithDefault i i im

k = typeKind ti

in Map.insert (idToTypeSymbol src i k)

$ idToTypeSymbol tar j k) Map.empty $ typeMap src

in Map.foldWithKey

( \ i (OpInfos l) m ->

foldr ( \ oi ->

let ty = opType oi

(j, t2) = mapFunSym tm im (funMap mor) (i, ty)

in Map.insert (idToOpSymbol src i ty)

(idToOpSymbol tar j t2)) m l)

typeSymMap $ assumps src