Morphism.hs revision 4fb19f237193a3bd6778f8aee3b6dd8da5856665
a78048ccbdb6256da15e6b0e7e95355e480c2301ndModule : $Header$
fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
fd9abdda70912b99b24e3bf1a38f26fde908a74cndLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
a78048ccbdb6256da15e6b0e7e95355e480c2301ndMaintainer : maeder@tzi.de
a78048ccbdb6256da15e6b0e7e95355e480c2301ndStability : provisional
a78048ccbdb6256da15e6b0e7e95355e480c2301ndPortability : portable
96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcMorphism on 'Env' (as for CASL)
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungimport qualified Common.Lib.Map as Map
4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluemtype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)
a78048ccbdb6256da15e6b0e7e95355e480c2301nddata Morphism = Morphism { msource :: Env
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , mtarget :: Env
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , classIdMap :: IdMap -- ignore
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , typeIdMap :: IdMap
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , funMap :: FunMap }
a78048ccbdb6256da15e6b0e7e95355e480c2301nd deriving (Eq, Show)
a78048ccbdb6256da15e6b0e7e95355e480c2301ndinstance PrettyPrint Morphism where
a78048ccbdb6256da15e6b0e7e95355e480c2301nd printText0 ga m =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let tm = typeIdMap m
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh fm = funMap m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ds = Map.foldWithKey ( \ (i, s) (j, t) l ->
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (printText0 ga i <+> colon <+> printText0 ga s
a78048ccbdb6256da15e6b0e7e95355e480c2301nd <+> text mapsTo <+>
a78048ccbdb6256da15e6b0e7e95355e480c2301nd printText0 ga j <+> colon <+> printText0 ga t) : l)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in (if Map.isEmpty tm then empty
a78048ccbdb6256da15e6b0e7e95355e480c2301nd else text (typeS ++ sS) <+> printText0 ga tm)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $$ (if Map.isEmpty fm then empty
a78048ccbdb6256da15e6b0e7e95355e480c2301nd else text (opS ++ sS) <+> fsep (punctuate comma ds))
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $$ nest 1 colon <+> braces (printText0 ga $ msource m)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $$ nest 1 (text mapsTo)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd <+> braces (printText0 ga $ mtarget m)
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapTypeScheme :: IdMap -> TypeScheme -> TypeScheme
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapTypeScheme im = mapTypeOfScheme $ mapType im
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapSen :: Morphism -> Term -> Term
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapSen m = let im = typeIdMap m in
a78048ccbdb6256da15e6b0e7e95355e480c2301nd mapTerm (mapFunSym im (funMap m), mapType im)
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapDataEntry :: Morphism -> DataEntry -> DataEntry
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapDataEntry m (DataEntry tm i k args alts) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let tim = compIdMap tm $ typeIdMap m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in DataEntry tim i k args $ map
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (mapAlt m tim args (Map.findWithDefault i i tim, args, star)) alts
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapAlt :: Morphism -> IdMap -> [TypeArg] -> DataPat -> AltDefn -> AltDefn
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapAlt m tm args dt c@(Construct mi ts p sels) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd case mi of
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let sc = TypeScheme args
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (getConstrType dt p (map (mapType tm) ts)) []
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (j, TypeScheme _ ty _) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd mapFunSym (typeIdMap m) (funMap m) (i, sc)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in Construct (Just j) ts (getPartiality ts ty) sels
a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- do not change (unused) selectors
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Nothing -> c
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapSentence :: Morphism -> Sentence -> Result Sentence
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapSentence m s = return $ case s of
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Formula t -> Formula $ mapSen m t
a78048ccbdb6256da15e6b0e7e95355e480c2301nd DatatypeSen td -> DatatypeSen $ map (mapDataEntry m) td
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ProgEqSen i sc pe ->
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let tm = typeIdMap m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd fm = funMap m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd f = mapFunSym tm fm
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (ni, nsc) = f (i, sc)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in ProgEqSen ni nsc $ mapEq (f, mapType tm) pe
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapFunSym im fm (i, sc) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let (j, sc2) = Map.findWithDefault (i, mapTypeScheme im sc)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (i, sc) fm in
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmkMorphism :: Env -> Env -> Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty
a78048ccbdb6256da15e6b0e7e95355e480c2301ndembedMorphism :: Env -> Env -> Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndembedMorphism = mkMorphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndideMor :: Env -> Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndideMor e = embedMorphism e e
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcompIdMap :: IdMap -> IdMap -> IdMap
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcompIdMap im1 im2 = Map.foldWithKey ( \ i j ->
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcompMor :: Morphism -> Morphism -> Maybe Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcompMor m1 m2 =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd if isSubEnv (mtarget m1) (msource m2) &&
a78048ccbdb6256da15e6b0e7e95355e480c2301nd isSubEnv (msource m2) (mtarget m1) then
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let tm2 = typeIdMap m2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd fm2 = funMap m2 in Just
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (mkMorphism (msource m1) (mtarget m2))
a78048ccbdb6256da15e6b0e7e95355e480c2301nd { classIdMap = compIdMap (classIdMap m1) $ classIdMap m2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , typeIdMap = compIdMap (typeIdMap m1) tm2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , funMap = Map.foldWithKey ( \ p1 p2 ->
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $ mapFunSym tm2 fm2 p2) fm2 $ funMap m1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd else Nothing
a78048ccbdb6256da15e6b0e7e95355e480c2301ndinclusionMor :: Env -> Env -> Result Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndinclusionMor e1 e2 =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd if isSubEnv e1 e2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd then return (embedMorphism e1 e2)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd else pplain_error (ideMor initialEnv)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (ptext "Attempt to construct inclusion between non-subsignatures:"
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $$ ptext "Signature 1:" $$ printText e1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $$ ptext "Signature 2:" $$ printText e2)
a78048ccbdb6256da15e6b0e7e95355e480c2301ndsymbMapToMorphism :: Env -> Env -> SymbolMap -> Result Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- consider partial symbol map
a78048ccbdb6256da15e6b0e7e95355e480c2301ndsymbMapToMorphism sigma1 sigma2 smap = do
a78048ccbdb6256da15e6b0e7e95355e480c2301nd type_map1 <- Map.foldWithKey myIdMap (return Map.empty) $ typeMap sigma1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd fun_map1 <- Map.foldWithKey myAsMap (return Map.empty) $ assumps sigma1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return (mkMorphism sigma1 sigma2)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd { typeIdMap = type_map1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , funMap = fun_map1}
a78048ccbdb6256da15e6b0e7e95355e480c2301nd myIdMap i k m = do
a78048ccbdb6256da15e6b0e7e95355e480c2301nd sym <- maybeToResult nullPos
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ("symbMapToMorphism - Could not map type "++showId i "")
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $ Map.lookup (Symbol { symName = i
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , symType = TypeAsItemType
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $ typeKind k
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , symEnv = sigma1 }) smap
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return (Map.insert i (symName sym) m1)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd myAsMap i (OpInfos ots) m = foldr (insFun i) m ots
a78048ccbdb6256da15e6b0e7e95355e480c2301nd insFun i ot m = do
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let osc = opType ot
a78048ccbdb6256da15e6b0e7e95355e480c2301nd sym <- maybeToResult nullPos
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ("symbMapToMorphism - Could not map op "++showId i "")
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $ Map.lookup (Symbol { symName = i
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , symType = OpAsItemType osc
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , symEnv = sigma1 }) smap
a78048ccbdb6256da15e6b0e7e95355e480c2301nd k <- case symType sym of
a78048ccbdb6256da15e6b0e7e95355e480c2301nd OpAsItemType sc -> return sc
a78048ccbdb6256da15e6b0e7e95355e480c2301nd _ -> plain_error (osc)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ("symbMapToMorphism - Wrong result symbol type for op"
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ++showId i "") nullPos
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return (Map.insert (i, osc) (symName sym, k) m1)
a78048ccbdb6256da15e6b0e7e95355e480c2301ndlegalEnv :: Env -> Bool
a78048ccbdb6256da15e6b0e7e95355e480c2301ndlegalEnv _ = True -- maybe a closure test?
a78048ccbdb6256da15e6b0e7e95355e480c2301ndlegalMor :: Morphism -> Bool
a78048ccbdb6256da15e6b0e7e95355e480c2301ndlegalMor m = let s = msource m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd t = mtarget m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ts = typeIdMap m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd fs = funMap m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd all (`elem` (Map.keys $ typeMap s))
a78048ccbdb6256da15e6b0e7e95355e480c2301nd && all (`elem` (Map.keys $ typeMap t))
a78048ccbdb6256da15e6b0e7e95355e480c2301nd && all ((`elem` (Map.keys $ assumps s)) . fst)
4aa603e6448b99f9371397d439795c91a93637eand && all ((`elem` (Map.keys $ assumps t)) . fst)
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmorphismUnion :: Morphism -> Morphism -> Result Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmorphismUnion m1 m2 =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd do s <- merge (msource m1) $ msource m2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd t <- merge (mtarget m1) $ mtarget m2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd tm <- foldr ( \ (i, j) rm ->
a78048ccbdb6256da15e6b0e7e95355e480c2301nd do m <- rm
a78048ccbdb6256da15e6b0e7e95355e480c2301nd case Map.lookup i m of
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Nothing -> return $ Map.insert i j m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Just k -> if j == k then return m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Result [Diag Error
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ("incompatible mapping of type id: " ++
a78048ccbdb6256da15e6b0e7e95355e480c2301nd showId i " to: " ++ showId j " and: "
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ++ showId k "") $ posOfId i] $ Just ()
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (return $ typeIdMap m1) $ Map.toList $ typeIdMap m2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd fm <- foldr ( \ (isc@(i, sc), jsc@(j, sc1)) rm -> do
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let nsc = expand (typeMap t) sc1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd nisc = (i, expand (typeMap s) sc)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd case Map.lookup nisc m of
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Nothing -> return $ Map.insert nisc
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (j, nsc) m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Just ksc@(k, sc2) -> if j == k &&
a78048ccbdb6256da15e6b0e7e95355e480c2301nd nsc == sc2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd then return m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Result [Diag Error
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ("incompatible mapping of op: " ++
a78048ccbdb6256da15e6b0e7e95355e480c2301nd showFun isc " to: " ++ showFun jsc " and: "
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ++ showFun ksc "") $ posOfId i] $ Just ()
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Map.toList (funMap m2))
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return (mkMorphism s t)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd { typeIdMap = tm
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , funMap = fm }
a78048ccbdb6256da15e6b0e7e95355e480c2301ndshowFun :: (Id, TypeScheme) -> ShowS
a78048ccbdb6256da15e6b0e7e95355e480c2301ndshowFun (i, ty) = showId i . (" : " ++) . showPretty ty
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmorphismToSymbMap :: Morphism -> SymbolMap
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmorphismToSymbMap mor =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd src = msource mor
a78048ccbdb6256da15e6b0e7e95355e480c2301nd tar = mtarget mor
a78048ccbdb6256da15e6b0e7e95355e480c2301nd tm = typeIdMap mor
a78048ccbdb6256da15e6b0e7e95355e480c2301nd typeSymMap = Map.foldWithKey ( \ i ti ->
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let j = Map.findWithDefault i i tm
a78048ccbdb6256da15e6b0e7e95355e480c2301nd k = typeKind ti
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in Map.insert (idToTypeSymbol src i k)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd $ idToTypeSymbol tar j k) Map.empty $ typeMap src
a78048ccbdb6256da15e6b0e7e95355e480c2301nd ( \ i (OpInfos l) m ->
a78048ccbdb6256da15e6b0e7e95355e480c2301nd foldr ( \ oi ->
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let ty = opType oi
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (j, t2) = mapFunSym
a78048ccbdb6256da15e6b0e7e95355e480c2301nd tm (funMap mor) (i, ty)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in Map.insert (idToOpSymbol src i ty)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd (idToOpSymbol tar j t2)) m l)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd typeSymMap $ assumps src