Morphism.hs revision 89054b2b95a3f92e78324dc852f3d34704e2ca49
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)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederdata SymbolType = OpAsItemType TypeScheme
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
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder OpAsItemType sc -> printText0 ga sc
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder TypeAsItemType k -> printText0 ga k
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder ClassAsItemType k -> printText0 ga k
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederinstance Ord TypeScheme where
af621d0066770895fd79562728e93099c8c52060Christian Maeder-- this does not match with Eq TypeScheme!
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sc1 <= sc2 = let (t1, c) = runState (freshInst sc1) 1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder t2 = evalState (freshInst sc2) c
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder v1 = varsOf t1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder v2 = varsOf t2
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder in case compare (length v1) $ length v2 of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder EQ -> t1 <= subst (Map.fromList $
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder zipWith (\ v (TypeArg i k _ _) ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder (v, TypeName i k 1)) v1 v2) t2
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
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToTypeSymbol :: Id -> Kind -> Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToTypeSymbol idt k = Symbol idt $ TypeAsItemType k
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToOpSymbol :: Id -> TypeScheme -> Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToOpSymbol idt typ = Symbol idt $ OpAsItemType typ
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederidToRaw :: Id -> RawSymbol
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederidToRaw x = AnID x
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
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder-- symbolToRaw (Symbol idt typ) = AKindedId (symbTypeToKind typ) idt
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymOf :: Env -> Set.Set Symbol
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 ->
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder Set.insert (Symbol i $ OpAsItemType $
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder opType t) s1) s0 $ opInfos ts)
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder types $ assumps sigma
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbMapItems :: [SymbMapItems] -> Result (Map.Map RawSymbol RawSymbol)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbMapItems sl = return (Map.fromList $ concat $ map s1 sl)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder s1 (SymbMapItems kind l _ _) = map (symbOrMapToRaw kind) l
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbOrMapToRaw :: SymbKind -> SymbOrMap -> (RawSymbol,RawSymbol)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbOrMapToRaw k (SymbOrMap s mt _) =
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder (symbToRaw k s,
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder symbToRaw k $ case mt of Nothing -> s
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbItems :: [SymbItems] -> Result [RawSymbol]
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbItems sl =
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder return (concat (map s1 sl))
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder where s1 (SymbItems kind l _ _) = map (symbToRaw kind) l
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbToRaw :: SymbKind -> Symb -> RawSymbol
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbToRaw k (Symb idt _ _) = symbKindToRaw k idt
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbKindToRaw :: SymbKind -> Id -> RawSymbol
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbKindToRaw Implicit idt = AnID idt
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbKindToRaw sk idt = AKindedId sk idt
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedermatchSymb :: Symbol -> RawSymbol -> Bool
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb x (ASymbol y) = x==y
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt _) (AnID di) = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt (TypeAsItemType _)) (AKindedId SK_type di) = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt (OpAsItemType _)) (AKindedId SK_op di) = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb _ _ = False
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederrawSymName :: RawSymbol -> Id
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederrawSymName (ASymbol sym) = symName sym
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederrawSymName (AnID i) = i
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederrawSymName (AKindedId _ i) = i
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
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maedertype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> Maybe (Id, TypeScheme)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapFunSym tm fm (i, sc) = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder (newI, _sc1) <- Map.lookup (i, sc) fm
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder let sc2 = mapTypeScheme tm sc
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder -- unify sc2 with sc1 later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (newI, sc2)
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maederinstance Mergeable Env where
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder merge 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
967e5f3c25249c779575864692935627004d3f9eChristian MaederideMor :: Env -> Morphism
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederideMor e = (mkMorphism e e)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder { typeIdMap = Map.foldWithKey ( \ i _ m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , funMap = Map.foldWithKey ( \ i ts m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder foldr ( \ t m2 -> let v = (i, opType t) in
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor :: Morphism -> Morphism -> Maybe Morphism
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor m1 m2 =
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder if 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
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederisSubEnv :: Env -> Env -> Bool
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederisSubEnv e1 e2 = diffEnv e1 e2 == initialEnv
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiinclusionMor :: Env -> Env -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinclusionMor e1 e2 =
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder if isSubEnv e1 e2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder then return (embedMorphism e1 e2)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder else pplain_error (embedMorphism initialEnv 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 MaederembedMorphism :: Env -> Env -> Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederembedMorphism a b =
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder (mkMorphism a b)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder { typeIdMap = foldr (\x -> Map.insert x x) Map.empty
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ( \ i (OpInfos ts) m -> foldr
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder (\ oi -> let t = opType oi in
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder Map.insert (i,t) (i, t)) m ts)
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
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sym <- maybeToResult nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Could not map op "++showId i "")
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ Map.lookup (Symbol { symName = i
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , symbType = OpAsItemType $ opType ot}) smap
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder k <- case symbType sym of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder OpAsItemType sc -> return sc
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder _ -> plain_error (opType ot)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Wrong result symbol type for op"
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ++showId i "") nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (Map.insert (i, opType ot) (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)
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaedermergeOpInfos :: TypeMap -> Int -> OpInfos -> OpInfos -> Result OpInfos
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaedermergeOpInfos tm c (OpInfos l1) (OpInfos l2) = fmap OpInfos $
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder foldM ( \ l o ->
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder let (es, us) = partition (isUnifiable tm c (opType o) . opType) l
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder in if null es then return (o:l)
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder else do r <- mergeOpInfo tm c (head es) o
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder return (r : us)) l1 l2
967e5f3c25249c779575864692935627004d3f9eChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermorphismUnion m1 m2 =
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder do s <- merge (msource m1) $ msource m2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder t <- merge (mtarget m1) $ mtarget m2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder return (mkMorphism s t)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder { typeIdMap = Map.union (typeIdMap m1) $ typeIdMap m2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder , funMap = Map.union (funMap m1) $ funMap m2 }
997c56f3bc74a703043010978e5013fdb074d659Christian MaedermorphismToSymbMap :: Morphism -> Map.Map Symbol Symbol
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
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- | Check if two OpTypes are equal except from totality or partiality
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedercompatibleOpTypes :: TypeScheme -> TypeScheme -> Bool
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedercompatibleOpTypes = isUnifiable Map.empty 0
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
af621d0066770895fd79562728e93099c8c52060Christian Maeder SK_class -> classS
af621d0066770895fd79562728e93099c8c52060Christian Maeder _ -> "") <+> printText0 ga i