Merge.hs revision b4fbc96e05117839ca409f5f20f97b3ac872d1ed
{- |
Module : $Header$
Copyright : (c) Christian Maeder and Uni Bremen 2003
Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
Maintainer : maeder@tzi.de
Stability : experimental
Portability : portable
merging parts of local environment
-}
module HasCASL.Merge where
import Common.Id
import Common.PrettyPrint
import Common.Result
import HasCASL.As
import HasCASL.Le
import HasCASL.AsUtils
import HasCASL.PrintLe()
import HasCASL.Unify
import HasCASL.Builtin
import HasCASL.MapTerm
import qualified Common.Lib.Map as Map
import Control.Monad(foldM)
import Data.List
-- | merge together repeated or extended items
class Mergeable a where
merge :: a -> a -> Result a
instance (Ord a, PosItem a, PrettyPrint a, Mergeable b)
=> Mergeable (Map.Map a b) where
merge = mergeMap id merge
improveDiag :: (PosItem a, PrettyPrint a) => a -> Diagnosis -> Diagnosis
improveDiag v d = d { diagString = let f:l = lines $ diagString d in
unlines $ (f ++ " of '" ++ showPretty v "'") : l
, diagPos = get_pos v
}
mergeMap :: (Ord a, PosItem a, PrettyPrint a) =>
(b -> b) -> (b -> b -> Result b)
mergeMap e f m1 m2 = foldM ( \ m (k, v) ->
case k `Map.lookup` m of
Nothing -> return $ Map.insert k (e v) m
Just w ->
let Result ds mu = f (e v) w
ns = map (improveDiag k) ds
in case mu of
Nothing -> Result ns $ Nothing
Just u -> Result ns $ Just $ Map.insert k u m)
instance Mergeable a => Mergeable (Maybe a) where
merge m1 m2 = case m1 of
Nothing -> return m2
Just v1 -> case m2 of
Nothing -> return m1
Just v2 -> do v <- merge v1 v2
return $ Just v
instance Mergeable ClassInfo where
merge = mergeA "super classes"
instance Mergeable Kind where
merge = mergeA "super kinds"
mergeTypeInfo :: TypeInfo -> TypeInfo -> Result TypeInfo
mergeTypeInfo t1 t2 =
do k <- merge (typeKind t1) $ typeKind t2
o <- merge (otherTypeKinds t1) $ otherTypeKinds t2
s <- merge (superTypes t1) $ superTypes t2
d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
return $ TypeInfo k o s d
mergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
mergeTypeDefn d1 d2 =
case (d1, d2) of
(TypeVarDefn 0, TypeVarDefn _) -> return d2
(TypeVarDefn _, TypeVarDefn 0) -> return d1
(TypeVarDefn c1, TypeVarDefn c2) -> do
c <- mergeA "TypeVarDefn" c1 c2
return $ TypeVarDefn c
(TypeVarDefn _, _) -> fail "merge: TypeVarDefn"
(_, TypeVarDefn _) -> fail "merge: TypeVarDefn"
(_, DatatypeDefn _) -> return d2
(PreDatatype, _) -> fail "expected data type definition"
(_, PreDatatype) -> return d1
(NoTypeDefn, _) -> return d2
(_, NoTypeDefn) -> return d1
(AliasTypeDefn s1, AliasTypeDefn s2) ->
do s <- mergeScheme s1 s2
return $ AliasTypeDefn s
(Supertype v1 s1 t1, Supertype v2 s2 t2) ->
do s <- mergeScheme s1 s2
v <- merge v1 v2
t <- mergeTerm Warning t1 t2
return $ Supertype v s t
(_, _) -> mergeA "TypeDefn" d1 d2
instance Mergeable Vars where
merge = mergeA "variables for subtype definition"
mergeScheme :: TypeScheme -> TypeScheme -> Result TypeScheme
mergeScheme s1@(TypeScheme a1 t1 _)
s2@(TypeScheme a2 t2 _) =
let v1 = genVarsOf t1
v2 = genVarsOf t2
mp v = mapArg $ zip v [(1::Int)..]
in
if t1 == t2 then
if null a1 && null a2 || isSingle a1 && isSingle a2 then
return s1
else if map (mp v1) a1 == map (mp v2) a2 then return s1
else fail ("differently bound type variables"
++ expected s1 s2)
else fail ("wrong type scheme" ++ expected s1 s2)
instance Mergeable OpAttr where
merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =
do t <- mergeTerm Warning t1 t2
return $ UnitOpAttr t (p1 ++ p2)
merge a1 a2 = mergeA "attributes" a1 a2
instance Mergeable OpBrand where
merge Pred _ = return Pred
merge _ Pred = return Pred
merge Op _ = return Op
merge _ Op = return Op
merge _ _ = return Fun
instance Mergeable OpDefn where
merge VarDefn VarDefn = return VarDefn
merge VarDefn _ = fail "illegal redeclaration of a variable"
merge _ VarDefn = fail "illegal redeclaration as variable"
merge (NoOpDefn _) d = return d
merge d (NoOpDefn _) = return d
merge (ConstructData d1) (ConstructData _d2) = do
-- d <- mergeA "constructor target type" d1 d2
return $ ConstructData d1
merge (SelectData c1 d1) (SelectData c2 _d2) = do
-- d <- mergeA "selector source type" d1 d2
c <- merge c1 c2
return $ SelectData c d1
merge (Definition b1 d1) (Definition b2 d2) =
do d <- mergeTerm Hint d1 d2
b <- merge b1 b2
return $ Definition b d
merge _d1 _d2 = fail "illegal redefinition"
instance Eq a => Mergeable [a] where
merge [] l2 = return l2
merge (e:l1) l2 = do
l3 <- merge l1 l2
return $ if any (e==) l2 then l3
else e:l3
mergeOpInfos :: TypeMap -> OpInfos -> OpInfos -> Result OpInfos
mergeOpInfos tm (OpInfos l1) (OpInfos l2) =
do l <- mergeOps (addUnit tm) l1 l2
return $ OpInfos l
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 :: (PrettyPrint 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)
[]] $ Just t2