18161N/A{- |

18161N/AModule : $Header$

18161N/ACopyright : (c) Christian Maeder and Uni Bremen 2003-2005

18161N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

18161N/A

18161N/AMaintainer : maeder@tzi.de

18161N/AStability : experimental

18161N/APortability : portable

18161N/A

18161N/Amerging parts of local environment

18161N/A-}

18161N/A

18161N/Amodule HasCASL.Merge where

18161N/A

18161N/Aimport Common.Id

18161N/Aimport Common.DocUtils

18161N/Aimport Common.Result

18161N/A

18161N/Aimport HasCASL.As

18161N/Aimport HasCASL.Le

18161N/Aimport HasCASL.AsUtils

18161N/Aimport HasCASL.TypeAna

18161N/Aimport HasCASL.PrintLe()

18161N/Aimport HasCASL.Unify

18161N/Aimport HasCASL.Builtin

18161N/Aimport HasCASL.MapTerm

18161N/Aimport qualified Data.Map as Map

18161N/Aimport qualified Data.Set as Set

18161N/A

18161N/Aimport Control.Monad(foldM)

18161N/Aimport Data.List

18161N/A

18161N/A-- | merge together repeated or extended items

18161N/Aclass Mergeable a where

18161N/A merge :: a -> a -> Result a

18161N/A

18161N/Ainstance (Ord a, PosItem a, Pretty a, Mergeable b)

18161N/A => Mergeable (Map.Map a b) where

18161N/A merge = mergeMap id merge

18161N/A

18161N/AimproveDiag :: (PosItem a, Pretty a) => a -> Diagnosis -> Diagnosis

18161N/AimproveDiag v d = d { diagString = let f:l = lines $ diagString d in

18161N/A unlines $ (f ++ " of '" ++ showDoc v "'") : l

18161N/A , diagPos = getRange v

18161N/A }

18161N/A

18161N/AmergeMap :: (Ord a, PosItem a, Pretty a) =>

18161N/A (b -> b) -> (b -> b -> Result b)

18161N/A -> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)

18161N/AmergeMap e f m1 m2 = foldM ( \ m (k, v) ->

18161N/A case k `Map.lookup` m of

18161N/A Nothing -> return $ Map.insert k (e v) m

18161N/A Just w ->

18161N/A let Result ds mu = f (e v) w

18161N/A ns = map (improveDiag k) ds

18161N/A in case mu of

18161N/A Nothing -> Result ns $ Nothing

18161N/A Just u -> Result ns $ Just $ Map.insert k u m)

18161N/A Map.empty (Map.toList m1 ++ Map.toList m2)

18161N/A

18161N/Ainstance Mergeable a => Mergeable (Maybe a) where

18161N/A merge m1 m2 = case m1 of

18161N/A Nothing -> return m2

18161N/A Just v1 -> case m2 of

18161N/A Nothing -> return m1

18161N/A Just v2 -> do v <- merge v1 v2

18161N/A return $ Just v

18161N/A

18161N/Ainstance Mergeable ClassInfo where

18161N/A merge = mergeA "super classes"

18161N/A

18161N/Ainstance (Pretty a, Eq a) => Mergeable (AnyKind a) where

18161N/A merge = mergeA "super kinds"

18161N/A

18161N/AmergeTypeInfo :: TypeInfo -> TypeInfo -> Result TypeInfo

18161N/AmergeTypeInfo t1 t2 =

18161N/A do k <- merge (typeKind t1) $ typeKind t2

18161N/A o <- merge (otherTypeKinds t1) $ otherTypeKinds t2

18161N/A s <- merge (superTypes t1) $ superTypes t2

18161N/A d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2

18161N/A return $ TypeInfo k o s d

18161N/A

18161N/AmergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn

18161N/AmergeTypeDefn d1 d2 =

18161N/A case (d1, d2) of

18161N/A (_, DatatypeDefn _) -> return d2

18161N/A (PreDatatype, _) -> fail "expected data type definition"

18161N/A (_, PreDatatype) -> return d1

18161N/A (NoTypeDefn, _) -> return d2

18161N/A (_, NoTypeDefn) -> return d1

18161N/A (AliasTypeDefn s1, AliasTypeDefn s2) ->

18161N/A do s <- mergeScheme s1 s2

18161N/A return $ AliasTypeDefn s

18161N/A (_, _) -> mergeA "TypeDefn" d1 d2

18161N/A

18161N/Ainstance Mergeable Vars where

18161N/A merge = mergeA "variables for subtype definition"

18161N/A

18161N/AmergeScheme :: TypeScheme -> TypeScheme -> Result TypeScheme

18161N/AmergeScheme s1@(TypeScheme a1 t1 _)

18161N/A s2@(TypeScheme a2 t2 _) =

18161N/A let v1 = genVarsOf t1

18161N/A v2 = genVarsOf t2

18161N/A mp a v = foldr ( \ i l ->

18161N/A maybe l (:l) $ findIndex ((== i) . getTypeVar) a)

18161N/A [] (map fst v)

18161N/A in

18161N/A if t1 == t2 then

18161N/A if null a1 && null a2 || isSingle a1 && isSingle a2 then

18161N/A return s1

18161N/A else if mp a1 v1 == mp a2 v2 then return s1

18161N/A else fail ("differently bound type variables"

18161N/A ++ expected s1 s2)

18161N/A else fail ("wrong type scheme" ++ expected s1 s2)

18161N/A

18161N/Ainstance Mergeable OpAttr where

18161N/A merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =

18161N/A do t <- mergeTerm Warning t1 t2

18161N/A return $ UnitOpAttr t (p1 `appRange` p2)

18161N/A merge a1 a2 = mergeA "attributes" a1 a2

18161N/A

18161N/Ainstance Mergeable OpBrand where

18161N/A merge b1 b2 = return $ case (b1, b2) of

18161N/A (Pred, _) -> Pred

18161N/A (_, Pred) -> Pred

18161N/A (Op, _) -> Op

18161N/A (_, Op) -> Op

18161N/A _ -> Fun

18161N/A

18161N/Ainstance Mergeable OpDefn where

18161N/A merge d1 d2 = case (d1, d2) of

18161N/A (NoOpDefn b1, NoOpDefn b2) -> do

18161N/A b <- merge b1 b2

18161N/A return $ NoOpDefn b

18161N/A (SelectData c1 s, SelectData c2 _) -> do

18161N/A c <- merge c1 c2

18161N/A return $ SelectData c s

18161N/A (Definition b1 e1, Definition b2 e2) -> do

18161N/A d <- mergeTerm Hint e1 e2

18161N/A b <- merge b1 b2

18161N/A return $ Definition b d

18161N/A (NoOpDefn b1, Definition b2 e2) -> do

18161N/A b <- merge b1 b2

18161N/A return $ Definition b e2

18161N/A (Definition b1 e1, NoOpDefn b2) -> do

18161N/A b <- merge b1 b2

18161N/A return $ Definition b e1

18161N/A (ConstructData _, SelectData _ _) ->

18161N/A fail "illegal selector as constructor redefinition"

18161N/A (SelectData _ _, ConstructData _) ->

18161N/A fail "illegal constructor as selector redefinition"

18161N/A (ConstructData _, _) -> return d1

18161N/A (_, ConstructData _) -> return d2

18161N/A (SelectData _ _, _) -> return d1

18161N/A (_, SelectData _ _) -> return d2

18161N/A

18161N/Ainstance Eq a => Mergeable [a] where

18161N/A merge l1 l2 = case l1 of

18161N/A [] -> return l2

18161N/A e : l -> do

18161N/A l3 <- merge l l2

18161N/A return $ if any (e==) l2 then l3 else e : l3

18161N/A

18161N/Ainstance Ord a => Mergeable (Set.Set a) where

18161N/A merge s1 s2 = return $ Set.union s1 s2

18161N/A

18161N/AmergeOpInfos :: TypeMap -> OpInfos -> OpInfos -> Result OpInfos

18161N/AmergeOpInfos tm (OpInfos l1) (OpInfos l2) =

18161N/A do l <- mergeOps (addUnit tm) l1 l2

18161N/A return $ OpInfos l

18161N/A

mergeOps :: TypeMap -> [OpInfo] -> [OpInfo] -> Result [OpInfo]

mergeOps _ [] l = return l

mergeOps tm (o:os) l2 = do

let (es, us) = partition (isUnifiable tm 1

(opType o) . opType) l2

l1 <- mergeOps tm os us

if null es then return (o : l1)

else do r <- mergeOpInfo tm o $ head es

return (r : l1)

mergeOpInfo :: TypeMap -> OpInfo -> OpInfo -> Result OpInfo

mergeOpInfo tm o1 o2 =

do let s1 = opType o1

s2 = opType o2

sc <- if instScheme tm 1 s2 s1 then return s1

else if instScheme tm 1 s1 s2 then return s2

else fail "overlapping but incompatible type schemes"

as <- merge (opAttrs o1) $ opAttrs o2

d <- merge (opDefn o1) $ opDefn o2

return $ OpInfo sc as d

instance Mergeable Env where

merge e1 e2 =

do cMap <- merge (classMap e1) $ classMap e2

tMap <- mergeMap id mergeTypeInfo

(typeMap e1) $ typeMap e2

as <- mergeMap (OpInfos .

map (mapOpInfo (id, expandAlias tMap)) . opInfos)

(mergeOpInfos tMap)

(assumps e1) $ assumps e2

return initialEnv { classMap = cMap

, typeMap = tMap

, assumps = as }

mergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a

mergeA str t1 t2 = if t1 == t2 then return t1 else

fail ("different " ++ str ++ expected t1 t2)

mergeTerm :: DiagKind -> Term -> Term -> Result Term

mergeTerm k t1 t2 = if t1 == t2 then return t1 else

Result [Diag k ("different terms" ++ expected t1 t2)

nullRange] $ Just t2