hets/HasCASL/Merge.hs

	Merge.hs revision e95bbf384f5cbcb7eb23286d5f15dffbd471db17
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule      :  $Header$
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer  :  maeder@tzi.de
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederStability   :  experimental
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPortability :  portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedermerging parts of local environment
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maedermodule HasCASL.Merge where
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.Id
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Common.DocUtils
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Result
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.As
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.Le
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.AsUtils
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport HasCASL.TypeAna
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport HasCASL.PrintLe()
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport HasCASL.Unify
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport HasCASL.Builtin
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport HasCASL.MapTerm
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport qualified Common.Lib.Map as Map
975642b989852fc24119c59cf40bc1af653608ffChristian Maederimport qualified Common.Lib.Set as Set
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport Control.Monad(foldM)
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport Data.List
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder-- | merge together repeated or extended items
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederclass Mergeable a where
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    merge :: a -> a -> Result a
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederinstance (Ord a, PosItem a, Pretty a, Mergeable b)
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder    => Mergeable (Map.Map a b) where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    merge = mergeMap id merge
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederimproveDiag :: (PosItem a, Pretty a) => a -> Diagnosis -> Diagnosis
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederimproveDiag v d = d { diagString = let f:l = lines $ diagString d in
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder                      unlines $ (f ++ " of '" ++ showDoc v "'") : l
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski                    , diagPos = getRange v
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                    }
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeMap :: (Ord a, PosItem a, Pretty a) =>
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            (b -> b) -> (b -> b -> Result b)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder         -> Map.Map a b -> Map.Map a b -> Result  (Map.Map a b)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeMap e f m1 m2 = foldM ( \ m (k, v) ->
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                          case k `Map.lookup` m of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                          Nothing -> return $ Map.insert k (e v) m
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                          Just w ->
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                              let Result ds mu = f (e v) w
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                                  ns = map (improveDiag k) ds
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                              in case mu of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                                 Nothing -> Result ns $ Nothing
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                                 Just u -> Result ns $ Just $ Map.insert k u m)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                  Map.empty (Map.toList m1 ++ Map.toList m2)
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederinstance Mergeable a => Mergeable (Maybe a) where
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    merge m1 m2 = case m1 of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                          Nothing -> return m2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                          Just v1 -> case m2 of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                                             Nothing -> return m1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                                             Just v2 -> do v <- merge v1 v2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                                                           return $ Just v
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederinstance Mergeable ClassInfo where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    merge = mergeA "super classes"
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance (Pretty a, Eq a) => Mergeable (AnyKind a) where
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    merge = mergeA "super kinds"
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeTypeInfo :: TypeInfo -> TypeInfo -> Result TypeInfo
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeTypeInfo t1 t2 =
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder    do k <- merge (typeKind t1) $ typeKind t2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder       o <- merge (otherTypeKinds t1) $ otherTypeKinds t2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder       s <- merge (superTypes t1) $ superTypes t2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder       d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder       return $ TypeInfo k o s d
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeTypeDefn d1 d2 =
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        case (d1, d2) of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            (_, DatatypeDefn _) -> return d2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            (PreDatatype, _) -> fail "expected data type definition"
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            (_, PreDatatype) -> return d1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            (NoTypeDefn, _) -> return d2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            (_, NoTypeDefn) -> return d1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            (AliasTypeDefn s1, AliasTypeDefn s2) ->
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                do s <- mergeScheme s1 s2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                   return $ AliasTypeDefn s
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            (_, _) -> mergeA "TypeDefn" d1 d2
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederinstance Mergeable Vars where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    merge = mergeA "variables for subtype definition"
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeScheme :: TypeScheme -> TypeScheme -> Result TypeScheme
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeScheme s1@(TypeScheme a1 t1 _)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            s2@(TypeScheme a2 t2 _) =
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    let v1 = genVarsOf t1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder        v2 = genVarsOf t2
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder        mp a v = foldr ( \ i l ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder               maybe l (:l) $ findIndex ((== i) . getTypeVar) a)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder                  [] (map fst v)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    in
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    if t1 == t2 then
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder       if null a1 && null a2 || isSingle a1 && isSingle a2 then
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder          return s1
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder       else if mp a1 v1 == mp a2 v2 then return s1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                else fail ("differently bound type variables"
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                         ++ expected s1 s2)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    else fail ("wrong type scheme" ++ expected s1 s2)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maederinstance Mergeable OpAttr where
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder        do t <- mergeTerm Warning t1 t2
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski           return $ UnitOpAttr t (p1 `appRange` p2)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    merge a1 a2 = mergeA "attributes" a1 a2
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maederinstance Mergeable OpBrand where
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    merge b1 b2 = return $ case (b1, b2) of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (Pred, _) -> Pred
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (_, Pred) -> Pred
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (Op, _) -> Op
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (_, Op) -> Op
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      _ -> Fun
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Mergeable OpDefn where
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    merge d1 d2 = case (d1, d2) of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (NoOpDefn b1, NoOpDefn b2) -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        b <- merge b1 b2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        return $ NoOpDefn b
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (SelectData c1 s, SelectData c2 _) -> do
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder        c <- merge c1 c2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        return $ SelectData c s
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (Definition b1 e1, Definition b2 e2) -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        d <- mergeTerm Hint e1 e2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        b <- merge b1 b2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        return $ Definition b d
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (NoOpDefn b1, Definition b2 e2) -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        b <- merge b1 b2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        return $ Definition b e2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (Definition b1 e1, NoOpDefn b2) -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        b <- merge b1 b2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        return $ Definition b e1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (ConstructData _, SelectData _ _) ->
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder          fail "illegal selector as constructor redefinition"
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (SelectData _ _, ConstructData _) ->
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder          fail "illegal constructor as selector redefinition"
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (ConstructData _, _) -> return d1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (_, ConstructData _) -> return d2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (SelectData _ _, _) -> return d1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      (_, SelectData _ _) -> return d2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Eq a => Mergeable [a] where
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    merge l1 l2 = case l1 of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      [] -> return l2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder      e : l -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        l3 <- merge l l2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        return $ if any (e==) l2 then l3 else e : l3
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian Maederinstance Ord a => Mergeable (Set.Set a) where
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder    merge s1 s2 = return $ Set.union s1 s2
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeOpInfos :: TypeMap -> OpInfos -> OpInfos -> Result OpInfos
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeOpInfos tm (OpInfos l1) (OpInfos l2) =
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder    do l <- mergeOps (addUnit tm) l1 l2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder       return $ OpInfos l
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedermergeOps :: TypeMap -> [OpInfo] -> [OpInfo] -> Result [OpInfo]
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedermergeOps _ [] l = return l
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeOps tm (o:os) l2 = do
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder    let (es, us) = partition (isUnifiable tm 1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                              (opType o) . opType) l2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    l1 <- mergeOps tm os us
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder    if null es then return (o : l1)
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder       else do r <- mergeOpInfo tm o $ head es
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder               return (r : l1)
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaedermergeOpInfo ::  TypeMap -> OpInfo -> OpInfo -> Result OpInfo
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeOpInfo tm o1 o2 =
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder        do let s1 = opType o1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder               s2 = opType o2
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder           sc <- if instScheme tm 1 s2 s1 then return s1
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder                    else if instScheme tm 1 s1 s2 then return s2
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder                    else fail "overlapping but incompatible type schemes"
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder           as <- merge (opAttrs o1) $ opAttrs o2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder           d <- merge (opDefn o1) $ opDefn o2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder           return $ OpInfo sc as d
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederinstance Mergeable Env where
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder    merge e1 e2 =
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder        do cMap <- merge (classMap e1) $ classMap e2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder           tMap <- mergeMap id mergeTypeInfo
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                   (typeMap e1) $ typeMap e2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder           as <- mergeMap (OpInfos .
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                           map (mapOpInfo (id, expandAlias tMap)) . opInfos)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                 (mergeOpInfos tMap)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                 (assumps e1) $ assumps e2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder           return initialEnv { classMap = cMap
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                             , typeMap = tMap
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                             , assumps = as }
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeA str t1 t2 = if t1 == t2 then return t1 else
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    fail ("different " ++ str ++ expected t1 t2)
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder
15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaedermergeTerm :: DiagKind -> Term -> Term -> Result Term
15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaedermergeTerm k t1 t2 = if t1 == t2 then return t1 else
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            Result [Diag k ("different terms" ++ expected t1 t2)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski                    nullRange] $ Just t2