Morphism.hs revision 83814002b4922114cbe7e9ba728472a0bf44aac5
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$
967e5f3c25249c779575864692935627004d3f9eChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : hets@tzi.de
967e5f3c25249c779575864692935627004d3f9eChristian MaederStability : provisional
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPortability : portable
967e5f3c25249c779575864692935627004d3f9eChristian MaederMorphism on 'Env' (as for CASL)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport qualified Common.Lib.Map as Map
997c56f3bc74a703043010978e5013fdb074d659Christian Maederimport qualified Common.Lib.Set as Set
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport Data.List(partition)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder-- new type to defined a different Eq and Ord instance
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maederdata TySc = TySc TypeScheme deriving Show
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maederinstance Eq TySc where
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder TySc sc1 == TySc sc2 =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder let Result _ ms = mergeScheme Map.empty 0 sc1 sc2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder in maybe False (const True) ms
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maederinstance Ord TySc where
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder-- this does not match with Eq TypeScheme!
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder TySc sc1 <= TySc sc2 =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder TySc sc1 == TySc sc2 ||
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder let (t1, c) = runState (freshInst sc1) 1
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder t2 = evalState (freshInst sc2) c
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder v1 = varsOf t1
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder v2 = varsOf t2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder in case compare (Set.size v1) $ Set.size v2 of
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder EQ -> t1 <= subst (Map.fromAscList $
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder zipWith (\ v (TypeArg i k _ _) ->
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (v, TypeName i k 1))
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maederdata SymbolType = OpAsItemType TySc
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder | TypeAsItemType Kind
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder | ClassAsItemType Kind
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder deriving (Show, Eq, Ord)
997c56f3bc74a703043010978e5013fdb074d659Christian Maederinstance PrettyPrint SymbolType where
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder printText0 ga t = case t of
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder OpAsItemType (TySc sc) -> printText0 ga sc
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder TypeAsItemType k -> printText0 ga k
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder ClassAsItemType k -> printText0 ga k
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederdata Symbol = Symbol {symName :: Id, symbType :: SymbolType}
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder deriving (Show, Eq, Ord)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederdata RawSymbol = ASymbol Symbol | AnID Id | AKindedId SymbKind Id
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder deriving (Show, Eq, Ord)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maedertype SymbolMap = Map.Map Symbol Symbol
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maedertype RawSymbolMap = Map.Map RawSymbol RawSymbol
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maedertype SymbolSet = Set.Set Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToTypeSymbol :: Id -> Kind -> Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToTypeSymbol idt k = Symbol idt $ TypeAsItemType k
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederidToClassSymbol :: Id -> Kind -> Symbol
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederidToClassSymbol idt k = Symbol idt $ ClassAsItemType k
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaederidToOpSymbol :: Id -> TySc -> Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToOpSymbol idt typ = Symbol idt $ OpAsItemType typ
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederidToRaw :: Id -> RawSymbol
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederidToRaw x = AnID x
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederrawSymName :: RawSymbol -> Id
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederrawSymName (ASymbol sym) = symName sym
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederrawSymName (AnID i) = i
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederrawSymName (AKindedId _ i) = i
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbTypeToKind :: SymbolType -> SymbKind
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymbTypeToKind (OpAsItemType _) = SK_op
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymbTypeToKind (TypeAsItemType _) = SK_type
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymbTypeToKind (ClassAsItemType _) = SK_class
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbolToRaw :: Symbol -> RawSymbol
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymbolToRaw sym = ASymbol sym
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedersymOf :: Env -> SymbolSet
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder let classes = Map.foldWithKey ( \ i ks s ->
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder Set.insert (Symbol i $ ClassAsItemType $
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder Intersection (classKinds ks) []) s)
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder Set.empty $ classMap sigma
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder types = Map.foldWithKey ( \ i ti s ->
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder Set.insert (Symbol i $ TypeAsItemType $
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder typeKind ti) s)
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder classes $ typeMap sigma
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder ops = Map.foldWithKey ( \ i ts s0 ->
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder foldr ( \ t s1 ->
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder Set.insert (Symbol i $ OpAsItemType $ TySc $
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder opType t) s1) s0 $ opInfos ts)
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder types $ assumps sigma
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederstatSymbMapItems :: [SymbMapItems] -> Result RawSymbolMap
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederstatSymbMapItems sl = do
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder rs <- mapM ( \ (SymbMapItems kind l _ _)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder -> mapM (symbOrMapToRaw kind) l) sl
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder foldr ( \ (r1, r2) mm -> do
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder if Map.member r1 m then do
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Result [Diag Error ("duplicate mapping for: " ++
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder showPretty r1 "\n ignoring: " ++ showPretty r2 "")
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder $ posOfId $ rawSymName r2] $ Just ()
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder else return $ Map.insert r1 r2 m)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (return Map.empty) $ concat rs
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedersymbOrMapToRaw :: SymbKind -> SymbOrMap -> Result (RawSymbol, RawSymbol)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedersymbOrMapToRaw k (SymbOrMap s mt _) = do
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder s1 <- symbToRaw k s
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder s2 <- symbToRaw k $ case mt of Nothing -> s
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return (s1, s2)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbItems :: [SymbItems] -> Result [RawSymbol]
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederstatSymbItems sl = do rs <- mapM (\ (SymbItems kind l _ _)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder -> mapM (symbToRaw kind) l) sl
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return $ concat rs
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedersymbToRaw :: SymbKind -> Symb -> Result RawSymbol
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedersymbToRaw k (Symb idt mt _) = case mt of
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Nothing -> return $ symbKindToRaw k idt
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just (SymbType sc@(TypeScheme vs (_ :=> t) _)) ->
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder let r = return $ ASymbol $ idToOpSymbol idt (TySc sc)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder rk = if null vs then Nothing else
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder convertTypeToKind t
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder rrk = maybeToResult (getMyPos t)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ("not a kind: " ++ showPretty t "") rk
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder SK_pred -> return $ ASymbol $ idToOpSymbol idt $
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder TySc $ predTypeScheme sc
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder SK_class -> do ck <- rrk
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return $ ASymbol $ idToClassSymbol idt ck
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder _ -> do ck <- rrk
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return $ ASymbol $ idToTypeSymbol idt ck
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederconvertTypeToKind :: Type -> Maybe Kind
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederconvertTypeToKind (FunType t1 FunArr t2 ps) =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder do k1 <- convertTypeToKind t1
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder k2 <- convertTypeToKind t2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ExtKind _ _ _ -> Nothing
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder _ -> Just $ FunKind k1 k2 ps
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederconvertTypeToKind (BracketType Parens [] _) =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederconvertTypeToKind (BracketType Parens [t] _) =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder convertTypeToKind t
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederconvertTypeToKind (BracketType Parens ts ps) =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder do ks <- mapM convertTypeToKind ts
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just $ Intersection ks ps
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederconvertTypeToKind (MixfixType [t1, TypeToken t]) =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder let s = tokStr t
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder v = case s of
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder "-" -> ContraVar
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder InVar -> Nothing
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder _ -> do k1 <- convertTypeToKind t1
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just $ ExtKind k1 v [tokPos t]
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederconvertTypeToKind(TypeToken t) =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder if tokStr t == "Type" then Just $ Universe [tokPos t] else
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder let ci = simpleIdToId t in
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just $ ClassKind ci MissingKind
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederconvertTypeToKind _ = Nothing
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbKindToRaw :: SymbKind -> Id -> RawSymbol
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedersymbKindToRaw Implicit = AnID
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedersymbKindToRaw sk = AKindedId $ case sk of
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder SK_pred -> SK_op
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder SK_fun -> SK_op
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder SK_sort -> SK_type
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedermatchSymb :: Symbol -> RawSymbol -> Bool
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb x (ASymbol y) = x==y
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt _) (AnID di) = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt (OpAsItemType _)) (AKindedId SK_op di) = idt==di
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermatchSymb (Symbol idt (OpAsItemType _)) (AKindedId SK_fun di) = idt==di
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermatchSymb (Symbol idt (OpAsItemType _)) (AKindedId SK_pred di) = idt==di
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermatchSymb (Symbol idt (TypeAsItemType _)) (AKindedId SK_type di) = idt==di
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermatchSymb (Symbol idt (TypeAsItemType _)) (AKindedId SK_sort di) = idt==di
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermatchSymb (Symbol idt (ClassAsItemType _))(AKindedId SK_class di)= idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb _ _ = False
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maedertype IdMap = Map.Map Id Id
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapType :: IdMap -> Type -> Type
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- include classIdMap later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapType m t = case t of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeName i k n ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder if n == 0 then
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder Just j -> TypeName j k 0
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeAppl t1 t2 ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeAppl (mapType m t1) (mapType m t2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeToken _ -> t
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder BracketType b l ps ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder BracketType b (map (mapType m) l) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder KindedType tk k ps ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder KindedType (mapType m tk) k ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder MixfixType l -> MixfixType $ map (mapType m) l
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder LazyType tl ps -> LazyType (mapType m tl) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ProductType l ps -> ProductType (map (mapType m) l) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder FunType t1 a t2 ps -> FunType (mapType m t1) a (mapType m t2) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme :: IdMap -> TypeScheme -> TypeScheme
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- rename clashing type arguments later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme m (TypeScheme args (q :=> t) ps) =
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeScheme args (q :=> mapType m t) ps
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapTySc :: IdMap -> TySc -> TySc
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapTySc m (TySc s1) = TySc (mapTypeScheme m s1)
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maedertype FunMap = Map.Map (Id, TySc) (Id, TySc)
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapFunSym :: IdMap -> FunMap -> (Id, TySc) -> Maybe (Id, TySc)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapFunSym tm fm (i, sc) = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder (newI, _sc1) <- Map.lookup (i, sc) fm
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder let sc2 = mapTySc tm sc
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder -- unify sc2 with sc1 later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (newI, sc2)
09eef8548cd62d787cf3a6535f9eae10592eec89Christian MaedermergeOpInfos :: TypeMap -> Int -> OpInfos -> OpInfos -> Result OpInfos
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermergeOpInfos tm c (OpInfos l1) (OpInfos l2) =
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder do l <- mergeOps tm c l1 l2
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder return $ OpInfos l
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder-- trace (showPretty l1 "\n+ " ++ showPretty l2 "\n 0" ++ showPretty l "") l
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermergeOps :: TypeMap -> Int -> [OpInfo] -> [OpInfo] -> Result [OpInfo]
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermergeOps _ _ [] l = return l
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermergeOps tm c (o:os) l2 = do
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder let (es, us) = partition (isUnifiable tm c (opType o) . opType) l2
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder l1 <- mergeOps tm c os us
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder if null es then return (o : l1)
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder else do r <- mergeOpInfo tm c o $ head es
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder return (r : l1)
09eef8548cd62d787cf3a6535f9eae10592eec89Christian MaedermergeEnv :: Env -> Env -> Result Env
09eef8548cd62d787cf3a6535f9eae10592eec89Christian MaedermergeEnv e1 e2 =
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder do cMap <- merge (classMap e1) $ classMap e2
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder let m = max (counter e1) $ counter e2
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder tMap <- mergeMap (mergeTypeInfo Map.empty 0)
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder (typeMap e1) $ typeMap e2
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder as <- mergeMap (mergeOpInfos tMap m)
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder (assumps e1) $ assumps e2
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder return initialEnv { classMap = cMap
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder , typeMap = tMap
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder , assumps = as }
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maederdata Morphism = Morphism { msource :: Env
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , mtarget :: Env
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , classIdMap :: IdMap -- ignore
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , typeIdMap :: IdMap
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , funMap :: FunMap }
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder deriving (Eq, Show)
967e5f3c25249c779575864692935627004d3f9eChristian MaedermkMorphism :: Env -> Env -> Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederembedMorphism :: Env -> Env -> Morphism
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederembedMorphism a b =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (mkMorphism a b)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder { typeIdMap = foldr (\x -> Map.insert x x) Map.empty
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ( \ i (OpInfos ts) m -> foldr
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (\ oi -> let v = (i, TySc $ opType oi) in
967e5f3c25249c779575864692935627004d3f9eChristian MaederideMor :: Env -> Morphism
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederideMor e = embedMorphism e e
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor :: Morphism -> Morphism -> Maybe Morphism
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor m1 m2 =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder if isSubEnv (mtarget m1) (msource m2) then Just
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (mkMorphism (msource m1) (mtarget m2))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder { typeIdMap = Map.map ( \ i -> Map.findWithDefault i i $ typeIdMap m2)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder $ typeIdMap m1
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , funMap = Map.foldWithKey ( \ (i1, sc1) (i2, sc2) m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (Map.findWithDefault (i2, sc2) (i2, sc2) $
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder funMap m2) m) Map.empty $ funMap m1
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiinclusionMor :: Env -> Env -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinclusionMor e1 e2 =
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder if isSubEnv e1 e2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder then return (embedMorphism e1 e2)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder else pplain_error (ideMor initialEnv)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder (ptext "Attempt to construct inclusion between non-subsignatures:"
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder $$ ptext "Singature 1:" $$ printText e1
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder $$ ptext "Singature 2:" $$ printText e2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedersymbMapToMorphism :: Env -> Env -> SymbolMap -> Result Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedersymbMapToMorphism sigma1 sigma2 smap = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder type_map1 <- Map.foldWithKey myIdMap (return Map.empty) $ typeMap sigma1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder fun_map1 <- Map.foldWithKey myAsMap (return Map.empty) $ assumps sigma1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (mkMorphism sigma1 sigma2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder { typeIdMap = type_map1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , funMap = fun_map1}
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder myIdMap i k m = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sym <- maybeToResult nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Could not map sort "++showId i "")
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ Map.lookup (Symbol { symName = i
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , symbType = TypeAsItemType
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ typeKind k}) smap
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (Map.insert i (symName sym) m1)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder myAsMap i (OpInfos ots) m = foldr (insFun i) m ots
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder insFun i ot m = do
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder let osc = TySc $ opType ot
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sym <- maybeToResult nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Could not map op "++showId i "")
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ Map.lookup (Symbol { symName = i
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder , symbType = OpAsItemType osc}) smap
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder k <- case symbType sym of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder OpAsItemType sc -> return sc
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder _ -> plain_error osc
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Wrong result symbol type for op"
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ++showId i "") nullPos
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder return (Map.insert (i, osc) (symName sym,k) m1)
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv :: Env -> Bool
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv _ = True -- maybe a closure test?
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalMor :: Morphism -> Bool
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederlegalMor m = let s = msource m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder t = mtarget m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder ts = typeIdMap m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder fs = funMap m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder all (`elem` (Map.keys $ typeMap s))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder && all (`elem` (Map.keys $ typeMap t))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder && all ((`elem` (Map.keys $ assumps s)) . fst)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder && all ((`elem` (Map.keys $ assumps t)) . fst)
967e5f3c25249c779575864692935627004d3f9eChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermorphismUnion m1 m2 =
09eef8548cd62d787cf3a6535f9eae10592eec89Christian Maeder do s <- mergeEnv (msource m1) $ msource m2
09eef8548cd62d787cf3a6535f9eae10592eec89Christian Maeder t <- mergeEnv (mtarget m1) $ mtarget m2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder tm <- foldr ( \ (i, j) rm ->
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Nothing -> return $ Map.insert i j m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just k -> if j == k then return m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Result [Diag Error
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ("incompatible mapping of type id: " ++
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder showId i " to: " ++ showId j " and: "
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ++ showId k "") $ posOfId i] $ Just ()
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (return $ typeIdMap m1) $ Map.toList $ typeIdMap m2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder fm <- foldr ( \ (isc@(i, _), jsc@(j, TySc sc1)) rm -> do
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Nothing -> return $ Map.insert isc jsc m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just ksc@(k, TySc sc2) -> if j == k &&
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder isUnifiable (typeMap t) 0 sc1 sc2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder then return m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Result [Diag Error
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ("incompatible mapping of op: " ++
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder showFun isc " to: " ++ showFun jsc " and: "
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ++ showFun ksc "") $ posOfId i] $ Just ()
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (return $ funMap m1) $ Map.toList $ funMap m2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder return (mkMorphism s t)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder { typeIdMap = tm
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , funMap = fm }
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedershowFun :: (Id, TySc) -> ShowS
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedershowFun (i, TySc ty) = showId i . (" : " ++) . showPretty ty
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermorphismToSymbMap mor =
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder tm = typeMap $ msource mor
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder ( \ s1 s2 m -> let k = typeKind $
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder Map.findWithDefault starTypeInfo s1 tm
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder in Map.insert (idToTypeSymbol s1 k) (idToTypeSymbol s2 k) m)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder typeIdMap mor
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder ( \ (id1,t1) (id2,t2) m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder Map.insert (idToOpSymbol id1 t1)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (idToOpSymbol id2 t2) m)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder typeSymMap $ funMap mor
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiinstance PrettyPrint Morphism where
af621d0066770895fd79562728e93099c8c52060Christian Maeder printText0 ga m = braces (printText0 ga (msource m))
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder $$ text mapsTo
af621d0066770895fd79562728e93099c8c52060Christian Maeder <+> braces (printText0 ga (mtarget m))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint Symbol where
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder printText0 ga s = text (case symbType s of
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder OpAsItemType _ -> opS
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder TypeAsItemType _ -> typeS
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder ClassAsItemType _ -> classS) <+>
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder printText0 ga (symName s) <+> text colonS <+>
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder printText0 ga (symbType s)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint RawSymbol where
af621d0066770895fd79562728e93099c8c52060Christian Maeder printText0 ga rs = case rs of
af621d0066770895fd79562728e93099c8c52060Christian Maeder ASymbol s -> printText0 ga s
af621d0066770895fd79562728e93099c8c52060Christian Maeder AnID i -> printText0 ga i
af621d0066770895fd79562728e93099c8c52060Christian Maeder AKindedId k i -> text (case k of
af621d0066770895fd79562728e93099c8c52060Christian Maeder SK_type -> typeS
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder SK_sort -> sortS
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder SK_fun -> funS
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder SK_pred -> predS
af621d0066770895fd79562728e93099c8c52060Christian Maeder SK_class -> classS
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Implicit -> "") <+> printText0 ga i