Merge.hs revision c797f343be2f3619bb1f5569753166ec49d27bdb
{- |
Module : $Header$
Copyright : (c) Christian Maeder and Uni Bremen 2003
Licence : All rights reserved.
Maintainer : hets@tzi.de
Stability : experimental
Portability : portable
merging parts of local environment
-}
module HasCASL.Merge where
import Common.Id
import Common.PrettyPrint
import HasCASL.As
import HasCASL.Le
import HasCASL.AsUtils
import HasCASL.Unify
import qualified Common.Lib.Map as Map
import Data.List
import Control.Monad
import Common.Result
-- for Logic.signature_union
instance Mergeable Env where
merge e1 e2 =
do cMap <- merge (classMap e1) $ classMap e2
tMap <- merge (typeMap e1) $ typeMap e2
let m = max (counter e1) $ counter e2
as <- mergeAssumps tMap m
(assumps e1) $ assumps e2
return $ Env cMap tMap as (sentences e1 ++ sentences e2)
(envDiags e1 ++ envDiags e2) m
instance (Ord a, PosItem a, PrettyPrint a, Mergeable b)
=> Mergeable (Map.Map a b) where
merge = mergeMap 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 = getMyPos v
, diagKind = case diagKind d of
FatalError -> Error
w -> w
}
mergeMap :: (Ord a, PosItem a, PrettyPrint a) => (b -> b -> Result b)
-> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)
mergeMap f m1 m2 = foldM ( \ m (k, v) ->
case k `Map.lookup` m of
Nothing -> return $ Map.insert k v m
Just w ->
let Result ds mu = f 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)
m1 (Map.toList m2)
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 c1 c2 = do k <- merge (classKind c1) (classKind c2)
d <- merge (classDefn c1) (classDefn c2)
let s1 = superClasses c1
s2 = superClasses c2
if s1 == s2 then
return $ ClassInfo s1 k d
else fail "merge: non-equal super classes"
instance Mergeable Kind where
merge k1 k2 = if k1 == k2 then return k1
else fail "merge: non-equal kinds"
instance Mergeable Class where
merge c1@(Downset t1) (Downset t2) =
if t1 == t2 then return c1
else fail "merge: non-equal downset"
merge c1@(Intersection i1 _) (Intersection i2 _) =
if i1 == i2 then return c1
else fail "merge: non-equal intersection class"
merge _ _ = fail "merge: class"
mergeList :: Eq a => [a] -> [a] -> Result [a]
mergeList l1 l2 = return $ nub (l1 ++ l2)
instance Mergeable TypeInfo where
merge t1 t2 = do k <- merge (typeKind t1) $ typeKind t2
o <- mergeList (otherTypeKinds t1) $ otherTypeKinds t2
s <- mergeList (superTypes t1) $ superTypes t2
d <- merge (typeDefn t1) $ typeDefn t2
return $ TypeInfo k o s d
instance Mergeable TypeDefn where
merge d1 d2 =
case (d1, d2) of
(TypeVarDefn, TypeVarDefn) -> return d1
(TypeVarDefn, _) -> fail "merge: TypeVarDefn"
(_, TypeVarDefn) -> fail "merge: TypeVarDefn"
(NoTypeDefn, AliasTypeDefn _) -> fail "merge: AliasTypeDefn"
(AliasTypeDefn _, NoTypeDefn) -> fail "merge: AliasTypeDefn"
(NoTypeDefn, _) -> return d2
(_, NoTypeDefn) -> return d1
(_, _) -> if d1 == d2 then return d1 else
fail "merge: TypeDefn"
mergeAssumps :: TypeMap -> Int -> Assumps -> Assumps -> Result Assumps
mergeAssumps tm c = mergeMap (mergeOpInfos tm c)
mergeOpInfos :: TypeMap -> Int -> OpInfos -> OpInfos -> Result OpInfos
mergeOpInfos tm c (OpInfos l1) (OpInfos l2) = fmap OpInfos $
foldM ( \ l o ->
let (es, us) = partition (isUnifiable tm c (opType o) . opType) l
in if null es then return (o:l)
else do r <- merge o $ head es
return (r : us)) l1 l2
instance Mergeable OpInfo where
merge o1 o2 =
do sc <- merge (opType o1) $ opType o2
as <- mergeAttrs (opAttrs o1) $ opAttrs o2
d <- merge (opDefn o1) $ opDefn o2
return $ OpInfo sc as d
expected :: PrettyPrint a => a -> a -> String
expected a b =
"\n expected: " ++ showPretty a
"\n found: " ++ showPretty b "\n"
instance Mergeable TypeScheme where
merge s1 s2 = if s1 == s2 then return s1
else fail ("wrong type scheme"
++ expected s1 s2)
-- instance Mergeable [OpAttr] where
mergeAttrs :: [OpAttr] -> [OpAttr] -> Result [OpAttr]
mergeAttrs l1 l2 =
let binAttr a = case a of BinOpAttr _ _ -> True
_ -> False
(l1b, l1u) = partition binAttr l1
(l2b, l2u) = partition binAttr l2
lb = nubBy ( \ (BinOpAttr b1 _) (BinOpAttr b2 _) -> b1 == b2)
(l1b ++ l2b)
in if null l1u || null l2u then
return (l1u ++ l2u ++ lb)
else do u <- merge (head l1u) (head l2u)
return (u : lb)
instance Mergeable OpAttr where
merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =
if t1 == t2 then return $ UnitOpAttr t1 (p1 ++ p2)
else fail "unequal unit elements"
merge _ _ = fail "merge: OpAttr"
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 d@(ConstructData d1) (ConstructData d2) =
if d1 == d2 then return d else
fail ("wrong constructor target type" ++
expected d1 d2)
merge (SelectData c1 d1) (SelectData c2 d2) =
if d1 == d2 then
do c <- mergeConstrInfos c1 c2
return $ SelectData c d1
else fail ("wrong selector's source type" ++
expected d1 d2)
merge (Definition d1) (Definition d2) =
do d <- merge d1 d2
return $ Definition d
merge _d1 _d2 = fail "illegal redefinition"
mergeConstrInfos :: [ConstrInfo] -> [ConstrInfo] -> Result [ConstrInfo]
mergeConstrInfos [] c2 = return c2
mergeConstrInfos (c : r) c2 =
do c3 <- mergeConstrInfos r c2
let cs = filter (==c) c2
if null cs then
return (c : c3)
else return c3
instance Mergeable Term where
merge t1 t2 = if t1 == t2 then return t1
else fail ("different terms\n\t"
++ showPretty t1 "\n\t"
++ showPretty t2 "\n\t")