Merge.hs revision f42bcc750a9a02cb4f753b70679f9aacf1b338d7
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederModule : $Header$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederDescription : union of signature parts
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : Christian.Maeder@dfki.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : experimental
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedermerging parts of local environment
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , mergeTypeDefn
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , mergeOpInfo
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport qualified Data.Map as Map
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport qualified Data.Set as Set
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedermergeTypeInfo :: ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
53310804002cd9e3c9c5844db3b984abcf001788Christian MaedermergeTypeInfo cm t1 t2 = do
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder let o = keepMinKinds cm [otherTypeKinds t1, otherTypeKinds t2]
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder s = Set.union (superTypes t1) $ superTypes t2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder k <- minRawKind "type raw kind" (typeKind t1) $ typeKind t2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder return $ TypeInfo k o s d
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimergeTypeDefn d1 d2 = case (d1, d2) of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (_, DatatypeDefn _) -> return d2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (PreDatatype, _) -> fail "expected data type definition"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (_, PreDatatype) -> return d1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (NoTypeDefn, _) -> return d2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (_, NoTypeDefn) -> return d1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (AliasTypeDefn s1, AliasTypeDefn s2) -> do
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski s <- mergeAlias s1 s2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return $ AliasTypeDefn s
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu (_, _) -> mergeA "TypeDefn" d1 d2
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescumergeAlias :: Type -> Type -> Result Type
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescumergeAlias s1 s2 = if eqStrippedType s1 s2 then return s1 else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fail $ "wrong type" ++ expected s1 s2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskimergeOpBrand :: OpBrand -> OpBrand -> OpBrand
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskimergeOpBrand b1 b2 = case (b1, b2) of
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski (Pred, _) -> Pred
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski (_, Pred) -> Pred
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski (Op, _) -> Op
bba825b39570777866d560bfde3807731131097eKlaus Luettich (_, Op) -> Op
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimergeOpDefn :: OpDefn -> OpDefn -> Result OpDefn
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedermergeOpDefn d1 d2 = case (d1, d2) of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (NoOpDefn b1, NoOpDefn b2) -> do
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski let b = mergeOpBrand b1 b2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder return $ NoOpDefn b
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder (SelectData c1 s, SelectData c2 _) -> do
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return $ SelectData c s
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Definition b1 e1, Definition b2 e2) -> do
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski d <- mergeTerm Hint e1 e2
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder let b = mergeOpBrand b1 b2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu return $ Definition b d
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu (NoOpDefn b1, Definition b2 e2) -> do
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu let b = mergeOpBrand b1 b2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu return $ Definition b e2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu (Definition b1 e1, NoOpDefn b2) -> do
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu let b = mergeOpBrand b1 b2
da955132262baab309a50fdffe228c9efe68251dCui Jian return $ Definition b e1
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (ConstructData _, SelectData _ _) ->
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu fail "illegal selector as constructor redefinition"
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (SelectData _ _, ConstructData _) ->
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu fail "illegal constructor as selector redefinition"
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (ConstructData _, _) -> return d1
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (_, ConstructData _) -> return d2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski (SelectData _ _, _) -> return d1
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski (_, SelectData _ _) -> return d2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichaddUnit :: ClassMap -> TypeMap -> TypeMap
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichaddUnit cm = maybe (error "addUnit") id . maybeResult . mergeTypeMap cm bTypes
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimergeOpInfos :: Set.Set OpInfo -> Set.Set OpInfo -> Result (Set.Set OpInfo)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermergeOpInfos s1 s2 = if Set.null s1 then return s2 else do
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (es, us) = Set.partition ((opType o ==) . opType) s2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder s <- mergeOpInfos os us
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder r <- foldM mergeOpInfo o $ Set.toList es
da955132262baab309a50fdffe228c9efe68251dCui JianmergeOpInfo :: OpInfo -> OpInfo -> Result OpInfo
bba825b39570777866d560bfde3807731131097eKlaus LuettichmergeOpInfo o1 o2 = do
da955132262baab309a50fdffe228c9efe68251dCui Jian let as = Set.union (opAttrs o1) $ opAttrs o2
bba825b39570777866d560bfde3807731131097eKlaus Luettich d <- mergeOpDefn (opDefn o1) $ opDefn o2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder return $ OpInfo (opType o1) as d
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermergeTypeMap :: ClassMap -> TypeMap -> TypeMap -> Result TypeMap
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermergeTypeMap cm = mergeMap $ mergeTypeInfo cm
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermerge :: Env -> Env -> Result Env
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermerge e1 e2 = do
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder cMap <- mergeMap mergeClassInfo (classMap e1) $ classMap e2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder let clMap = Map.map (\ ci -> ci { classKinds =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder keepMinKinds cMap [classKinds ci] }) cMap
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder tMap <- mergeTypeMap clMap (typeMap e1) $ typeMap e2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let tAs = filterAliases tMap
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder as <- mergeMap mergeOpInfos (assumps e1) $ assumps e2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder bs <- mergeMap (\ i1 i2 -> if i1 == i2 then return i1 else
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fail "conflicting operation for binder syntax")
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (binders e1) $ binders e2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder return initialEnv
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder { classMap = clMap
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder , typeMap = tMap
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder , assumps = Map.map (Set.map $ mapOpInfo (id, expandAliases tAs)) $ as
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder , binders = bs }
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermergeA str t1 t2 = if t1 == t2 then return t1 else
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fail ("different " ++ str ++ expected t1 t2)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermergeTerm :: DiagKind -> Term -> Term -> Result Term
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermergeTerm k t1 t2 = if t1 == t2 then return t1 else
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Result [Diag k ("different terms" ++ expected t1 t2) $ getRange t2] $ Just t2