Merge.hs revision 72b9099aeec0762bae4546db3bc4b48721027bf4
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder{- |
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederModule : $Header$
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederDescription : union of signature parts
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederMaintainer : Christian.Maeder@dfki.de
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederStability : experimental
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederPortability : portable
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedermerging parts of local environment
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-}
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedermodule HasCASL.Merge
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ( merge
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , mergeTypeInfo
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , mergeTypeDefn
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , mergeOpInfo
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder , addUnit
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , minimizeClassMap
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ) where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Common.Id
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Common.DocUtils
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Common.Result
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HasCASL.As
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HasCASL.Le
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HasCASL.AsUtils
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HasCASL.PrintLe
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HasCASL.ClassAna
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HasCASL.TypeAna
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HasCASL.Builtin
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HasCASL.MapTerm
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport qualified Data.Map as Map
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport qualified Data.Set as Set
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Data.Maybe
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Control.Monad(foldM)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeTypeInfo :: ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeTypeInfo cm t1 t2 = do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let o = keepMinKinds cm [otherTypeKinds t1, otherTypeKinds t2]
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder s = Set.union (superTypes t1) $ superTypes t2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder k <- minRawKind "type raw kind" (typeKind t1) $ typeKind t2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ TypeInfo k o s d
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeTypeDefn d1 d2 = case (d1, d2) of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (_, DatatypeDefn _) -> return d2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (PreDatatype, _) -> fail "expected data type definition"
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (_, PreDatatype) -> return d1
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (NoTypeDefn, _) -> return d2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (_, NoTypeDefn) -> return d1
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (AliasTypeDefn s1, AliasTypeDefn s2) -> do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder s <- mergeAlias s1 s2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ AliasTypeDefn s
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (_, _) -> mergeA "TypeDefn" d1 d2
fe883661c9d1a5a8b42ac4e8673ec133d9dad354Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeAlias :: Type -> Type -> Result Type
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeAlias s1 s2 = if eqStrippedType s1 s2 then return s1 else
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder fail $ "wrong type" ++ expected s1 s2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeOpBrand :: OpBrand -> OpBrand -> OpBrand
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeOpBrand b1 b2 = case (b1, b2) of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (Pred, _) -> Pred
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (_, Pred) -> Pred
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (Op, _) -> Op
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (_, Op) -> Op
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder _ -> Fun
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeOpDefn :: OpDefn -> OpDefn -> Result OpDefn
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeOpDefn d1 d2 = case (d1, d2) of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (NoOpDefn b1, NoOpDefn b2) -> do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let b = mergeOpBrand b1 b2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ NoOpDefn b
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (SelectData c1 s, SelectData c2 _) -> do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let c = Set.union c1 c2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ SelectData c s
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (Definition b1 e1, Definition b2 e2) -> do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder d <- mergeTerm Hint e1 e2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let b = mergeOpBrand b1 b2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ Definition b d
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (NoOpDefn b1, Definition b2 e2) -> do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let b = mergeOpBrand b1 b2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ Definition b e2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (Definition b1 e1, NoOpDefn b2) -> do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let b = mergeOpBrand b1 b2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ Definition b e1
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (ConstructData _, SelectData _ _) ->
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder fail "illegal selector as constructor redefinition"
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (SelectData _ _, ConstructData _) ->
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder fail "illegal constructor as selector redefinition"
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (ConstructData _, _) -> return d1
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (_, ConstructData _) -> return d2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (SelectData _ _, _) -> return d1
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (_, SelectData _ _) -> return d2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederaddUnit :: ClassMap -> TypeMap -> TypeMap
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederaddUnit cm = fromMaybe (error "addUnit") . maybeResult . mergeTypeMap cm bTypes
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeOpInfos :: Set.Set OpInfo -> Set.Set OpInfo -> Result (Set.Set OpInfo)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeOpInfos s1 s2 = if Set.null s1 then return s2 else do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let (o, os) = Set.deleteFindMin s1
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (es, us) = Set.partition ((opType o ==) . opType) s2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder s <- mergeOpInfos os us
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder r <- foldM mergeOpInfo o $ Set.toList es
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ Set.insert r s
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeOpInfo :: OpInfo -> OpInfo -> Result OpInfo
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeOpInfo o1 o2 = do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let as = Set.union (opAttrs o1) $ opAttrs o2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder d <- mergeOpDefn (opDefn o1) $ opDefn o2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ OpInfo (opType o1) as d
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeTypeMap :: ClassMap -> TypeMap -> TypeMap -> Result TypeMap
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeTypeMap = mergeMap . mergeTypeInfo
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederminimizeClassMap :: ClassMap -> ClassMap
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederminimizeClassMap cm = Map.map (\ ci -> ci { classKinds =
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder keepMinKinds cm [classKinds ci] }) cm
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
e05956d1da3c97e4d808926f97c6841c4a561991Christian Maedermerge :: Env -> Env -> Result Env
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedermerge e1 e2 = do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder cMap <- mergeMap mergeClassInfo (classMap e1) $ classMap e2
e05956d1da3c97e4d808926f97c6841c4a561991Christian Maeder let clMap = minimizeClassMap cMap
e05956d1da3c97e4d808926f97c6841c4a561991Christian Maeder tMap <- mergeTypeMap clMap (typeMap e1) $ typeMap e2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder let tAs = filterAliases tMap
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder as <- mergeMap mergeOpInfos (assumps e1) $ assumps e2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder bs <- mergeMap (\ i1 i2 -> if i1 == i2 then return i1 else
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder fail "conflicting operation for binder syntax")
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (binders e1) $ binders e2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return initialEnv
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder { classMap = clMap
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , typeMap = tMap
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , assumps = Map.map (Set.map $ mapOpInfo (id, expandAliases tAs)) as
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , binders = bs }
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeA str t1 t2 = if t1 == t2 then return t1 else
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder fail ("different " ++ str ++ expected t1 t2)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeTerm :: DiagKind -> Term -> Term -> Result Term
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermergeTerm k t1 t2 = if t1 == t2 then return t1 else
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Result [Diag k ("different terms" ++ expected t1 t2) $ getRange t2] $ Just t2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder