Morphism.hs revision adee28c3eb7bb0b9bb045d26ee6d35e19cf39053
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannModule : $Header$
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannMaintainer : hets@tzi.de
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannStability : provisional
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannPortability : non-portable (deriving Typeable)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannMorphism on 'Env' (as for CASL)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport qualified Common.Lib.Map as Map
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport qualified Common.Lib.Set as Set
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanndata SymbolType = OpAsItemType TypeScheme
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann | TypeAsItemType Kind
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann | ClassAsItemType Kind
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann deriving (Show, Eq, Ord)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninstance PrettyPrint SymbolType where
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann printText0 ga t = case t of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann OpAsItemType sc -> printText0 ga sc
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann TypeAsItemType k -> printText0 ga k
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ClassAsItemType k -> printText0 ga k
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninstance Ord TypeScheme where
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann sc1 <= sc2 = let (t1, c) = runState (freshInst sc1) 1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann t2 = evalState (freshInst sc2) c
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann v1 = varsOf t1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann v2 = varsOf t2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann in case compare (length v1) $ length v2 of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann EQ -> t1 <= subst (Map.fromList $
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann zipWith (\ v (TypeArg i k _ _) ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (v, TypeName i k 1)) v1 v2) t2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanndata Symbol = Symbol {symName :: Id, symbType :: SymbolType}
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann deriving (Show, Eq, Ord, Typeable)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanndata RawSymbol = ASymbol Symbol | AnID Id | AKindedId SymbKind Id
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann deriving (Show, Eq, Ord, Typeable)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype SymbolMap = Map.Map Symbol Symbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannidToTypeSymbol :: Id -> Kind -> Symbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannidToTypeSymbol idt k = Symbol idt $ TypeAsItemType k
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannidToOpSymbol :: Id -> TypeScheme -> Symbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannidToOpSymbol idt typ = Symbol idt $ OpAsItemType typ
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannidToRaw :: Id -> RawSymbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannidToRaw x = AnID x
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbTypeToKind :: SymbolType -> SymbKind
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbTypeToKind (OpAsItemType _) = SK_op
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbTypeToKind (TypeAsItemType _) = SK_type
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbTypeToKind (ClassAsItemType _) = SK_class
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbolToRaw :: Symbol -> RawSymbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbolToRaw sym = ASymbol sym
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- symbolToRaw (Symbol idt typ) = AKindedId (symbTypeToKind typ) idt
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymOf :: Env -> Set.Set Symbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann let classes = Map.foldWithKey ( \ i ks s ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Set.insert (Symbol i $ ClassAsItemType $
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Intersection (classKinds ks) []) s)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Set.empty $ classMap sigma
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann types = Map.foldWithKey ( \ i ti s ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Set.insert (Symbol i $ TypeAsItemType $
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typeKind ti) s)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann classes $ typeMap sigma
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ops = Map.foldWithKey ( \ i ts s0 ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann foldr ( \ t s1 ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Set.insert (Symbol i $ OpAsItemType $
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann opType t) s1) s0 $ opInfos ts)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann types $ assumps sigma
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannstatSymbMapItems :: [SymbMapItems] -> Result (Map.Map RawSymbol RawSymbol)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannstatSymbMapItems sl = return (Map.fromList $ concat $ map s1 sl)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann s1 (SymbMapItems kind l _ _) = map (symbOrMapToRaw kind) l
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbOrMapToRaw :: SymbKind -> SymbOrMap -> (RawSymbol,RawSymbol)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbOrMapToRaw k (SymbOrMap s mt _) =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (symbToRaw k s,
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann symbToRaw k $ case mt of Nothing -> s
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannstatSymbItems :: [SymbItems] -> Result [RawSymbol]
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannstatSymbItems sl =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return (concat (map s1 sl))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann where s1 (SymbItems kind l _ _) = map (symbToRaw kind) l
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbToRaw :: SymbKind -> Symb -> RawSymbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbToRaw k (Symb idt _ _) = symbKindToRaw k idt
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbKindToRaw :: SymbKind -> Id -> RawSymbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbKindToRaw Implicit idt = AnID idt
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbKindToRaw sk idt = AKindedId sk idt
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmatchSymb :: Symbol -> RawSymbol -> Bool
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmatchSymb x (ASymbol y) = x==y
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmatchSymb (Symbol idt _) (AnID di) = idt==di
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmatchSymb (Symbol idt (TypeAsItemType _)) (AKindedId SK_type di) = idt==di
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmatchSymb (Symbol idt (TypeAsItemType _)) (AKindedId SK_sort di) = idt==di
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmatchSymb (Symbol idt (OpAsItemType _)) (AKindedId SK_op di) = idt==di
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmatchSymb (Symbol idt (OpAsItemType _)) (AKindedId SK_pred di) = idt==di
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmatchSymb _ _ = False
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannrawSymName :: RawSymbol -> Id
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannrawSymName (ASymbol sym) = symName sym
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannrawSymName (AnID i) = i
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannrawSymName (AKindedId _ i) = i
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype IdMap = Map.Map Id Id
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapType :: IdMap -> Type -> Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- include classIdMap later
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapType m t = case t of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann TypeName i k n ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann if n == 0 then
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Just j -> TypeName j k 0
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann TypeAppl t1 t2 ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann TypeAppl (mapType m t1) (mapType m t2)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann TypeToken _ -> t
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann BracketType b l ps ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann BracketType b (map (mapType m) l) ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann KindedType tk k ps ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann KindedType (mapType m tk) k ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann MixfixType l -> MixfixType $ map (mapType m) l
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann LazyType tl ps -> LazyType (mapType m tl) ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ProductType l ps -> ProductType (map (mapType m) l) ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann FunType t1 a t2 ps -> FunType (mapType m t1) a (mapType m t2) ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapTypeScheme :: IdMap -> TypeScheme -> TypeScheme
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- rename clashing type arguments later
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapTypeScheme m (TypeScheme args (q :=> t) ps) =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann TypeScheme args (q :=> mapType m t) ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> Maybe (Id, TypeScheme)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapFunSym tm fm (i, sc) = do
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (newI, _sc1) <- Map.lookup (i, sc) fm
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann let sc2 = mapTypeScheme tm sc
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann -- unify sc2 with sc1 later
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return (newI, sc2)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninstance Mergeable Env where
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann merge e1 e2 =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann do cMap <- merge (classMap e1) $ classMap e2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann let m = max (counter e1) $ counter e2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann tMap <- mergeMap (mergeTypeInfo Map.empty 0)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (typeMap e1) $ typeMap e2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann as <- mergeMap (mergeOpInfos tMap 0)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (assumps e1) $ assumps e2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return initialEnv { classMap = cMap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , typeMap = tMap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , assumps = as }
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanndata Morphism = Morphism { msource :: Env
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , mtarget :: Env
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , classIdMap :: IdMap -- ignore
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , typeIdMap :: IdMap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , funMap :: FunMap }
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann deriving (Eq, Show, Typeable)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmkMorphism :: Env -> Env -> Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannideMor :: Env -> Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannideMor e = (mkMorphism e e)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { typeIdMap = Map.foldWithKey ( \ i _ m ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , funMap = Map.foldWithKey ( \ i ts m ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann foldr ( \ t m2 -> let v = (i, opType t) in
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanncompMor :: Morphism -> Morphism -> Maybe Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanncompMor m1 m2 =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann if mtarget m1 == msource m2 then Just
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (mkMorphism (msource m1) (mtarget m2))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { typeIdMap = Map.map ( \ i -> Map.findWithDefault i i $ typeIdMap m2)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann $ typeIdMap m1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , funMap = Map.foldWithKey ( \ (i1, sc1) (i2, sc2) m ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (Map.findWithDefault (i2, sc2) (i2, sc2) $
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann funMap m2) m) Map.empty $ funMap m1
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannisSubEnv :: Env -> Env -> Bool
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannisSubEnv e1 e2 = diffEnv e1 e2 == initialEnv
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanninclusionMor :: Env -> Env -> Result Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanninclusionMor e1 e2 =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann if isSubEnv e1 e2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann then return (embedMorphism e1 e2)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann else pplain_error (embedMorphism initialEnv initialEnv)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (ptext "Attempt to construct inclusion between non-subsignatures:"
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann $$ ptext "Singature 1:" $$ printText e1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann $$ ptext "Singature 2:" $$ printText e2)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannembedMorphism :: Env -> Env -> Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannembedMorphism a b =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (mkMorphism a b)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { typeIdMap = foldr (\x -> Map.insert x x) Map.empty
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ( \ i (OpInfos ts) m -> foldr
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (\ oi -> let t = opType oi in
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Map.insert (i,t) (i, t)) m ts)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbMapToMorphism :: Env -> Env -> SymbolMap -> Result Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsymbMapToMorphism sigma1 sigma2 smap = do
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann type_map1 <- Map.foldWithKey myIdMap (return Map.empty) $ typeMap sigma1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann fun_map1 <- Map.foldWithKey myAsMap (return Map.empty) $ assumps sigma1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return (mkMorphism sigma1 sigma2)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { typeIdMap = type_map1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , funMap = fun_map1}
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann myIdMap i k m = do
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann sym <- maybeToResult nullPos
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ("symbMapToMorphism - Could not map sort "++showId i "")
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann $ Map.lookup (Symbol { symName = i
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , symbType = TypeAsItemType
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann $ typeKind k}) smap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return (Map.insert i (symName sym) m1)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann myAsMap i (OpInfos ots) m = foldr (insFun i) m ots
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann insFun i ot m = do
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann sym <- maybeToResult nullPos
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ("symbMapToMorphism - Could not map op "++showId i "")
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann $ Map.lookup (Symbol { symName = i
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , symbType = OpAsItemType $ opType ot}) smap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann k <- case symbType sym of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann OpAsItemType sc -> return sc
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann _ -> plain_error (opType ot)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ("symbMapToMorphism - Wrong result symbol type for op"
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ++showId i "") nullPos
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return (Map.insert (i, opType ot) (symName sym,k) m1)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannlegalEnv :: Env -> Bool
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannlegalEnv _ = True -- maybe a closure test?
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannlegalMor :: Morphism -> Bool
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannlegalMor m = let s = msource m
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann t = mtarget m
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ts = typeIdMap m
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann fs = funMap m
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann all (`elem` (Map.keys $ typeMap s))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann && all (`elem` (Map.keys $ typeMap t))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann && all ((`elem` (Map.keys $ assumps s)) . fst)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann && all ((`elem` (Map.keys $ assumps t)) . fst)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmorphismUnion :: Morphism -> Morphism -> Result Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmorphismUnion m1 m2 =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann do s <- merge (msource m1) $ msource m2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann t <- merge (mtarget m1) $ mtarget m2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return (mkMorphism s t)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { typeIdMap = Map.union (typeIdMap m1) $ typeIdMap m2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , funMap = Map.union (funMap m1) $ funMap m2 }
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmorphismToSymbMap :: Morphism -> Map.Map Symbol Symbol
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmorphismToSymbMap mor =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann tm = typeMap $ msource mor
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ( \ s1 s2 m -> let k = typeKind $
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Map.findWithDefault starTypeInfo s1 tm
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann in Map.insert (idToTypeSymbol s1 k) (idToTypeSymbol s2 k) m)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typeIdMap mor
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ( \ (id1,t1) (id2,t2) m ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Map.insert (idToOpSymbol id1 t1)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (idToOpSymbol id2 t2) m)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typeSymMap $ funMap mor
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | Check if two OpTypes are equal except from totality or partiality
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanncompatibleOpTypes :: TypeScheme -> TypeScheme -> Bool
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanncompatibleOpTypes = isUnifiable Map.empty 0
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- Some quick and dirty instances
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninstance PrettyPrint Morphism where
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann printText0 _ga s = text (show s)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninstance PrettyPrint Symbol where
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann printText0 ga s = text (case symbType s of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann OpAsItemType _ -> opS
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann TypeAsItemType _ -> typeS
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ClassAsItemType _ -> classS) <+>
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann printText0 ga (symName s) <+> text colonS <+>
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann printText0 ga (symbType s)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninstance PrettyPrint RawSymbol where
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann printText0 _ga s = text (show s)