{- |
Module : ./HasCASL/Merge.hs
Description : union of signature parts
Copyright : (c) Christian Maeder and Uni Bremen 2003-2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : experimental
Portability : portable
merging parts of local environment
-}
module HasCASL.Merge
( merge
, mergeTypeInfo
, mergeTypeDefn
, mergeOpInfo
, addUnit
) where
import Common.Id
import Common.DocUtils
import Common.Result
import HasCASL.As
import HasCASL.Le
import HasCASL.AsUtils
import HasCASL.PrintLe
import HasCASL.ClassAna
import HasCASL.TypeAna
import HasCASL.Builtin
import HasCASL.MapTerm
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Control.Monad (foldM)
mergeTypeInfo :: ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
mergeTypeInfo cm t1 t2 = do
let o = keepMinKinds cm [otherTypeKinds t1, otherTypeKinds t2]
s = Set.union (superTypes t1) $ superTypes t2
k <- minRawKind "type raw kind" (typeKind t1) $ typeKind 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
(_, DatatypeDefn _) -> return d2
(PreDatatype, _) -> fail "expected data type definition"
(_, PreDatatype) -> return d1
(NoTypeDefn, _) -> return d2
(_, NoTypeDefn) -> return d1
(AliasTypeDefn s1, AliasTypeDefn s2) -> do
s <- mergeAlias s1 s2
return $ AliasTypeDefn s
(_, _) -> mergeA "TypeDefn" d1 d2
mergeAlias :: Type -> Type -> Result Type
mergeAlias s1 s2 = if eqStrippedType s1 s2 then return s1 else
fail $ "wrong type" ++ expected s1 s2
mergeOpBrand :: OpBrand -> OpBrand -> OpBrand
mergeOpBrand b1 b2 = case (b1, b2) of
(Pred, _) -> Pred
(_, Pred) -> Pred
(Op, _) -> Op
(_, Op) -> Op
_ -> Fun
mergeOpDefn :: OpDefn -> OpDefn -> Result OpDefn
mergeOpDefn d1 d2 = case (d1, d2) of
(NoOpDefn b1, NoOpDefn b2) -> do
let b = mergeOpBrand b1 b2
return $ NoOpDefn b
(SelectData c1 s, SelectData c2 _) -> do
let c = Set.union c1 c2
return $ SelectData c s
(Definition b1 e1, Definition b2 e2) -> do
d <- mergeTerm Hint e1 e2
let b = mergeOpBrand b1 b2
return $ Definition b d
(NoOpDefn b1, Definition b2 e2) -> do
let b = mergeOpBrand b1 b2
return $ Definition b e2
(Definition b1 e1, NoOpDefn b2) -> do
let b = mergeOpBrand b1 b2
return $ Definition b e1
(ConstructData _, SelectData _ _) ->
fail "illegal selector as constructor redefinition"
(SelectData _ _, ConstructData _) ->
fail "illegal constructor as selector redefinition"
(ConstructData _, _) -> return d1
(_, ConstructData _) -> return d2
(SelectData _ _, _) -> return d1
(_, SelectData _ _) -> return d2
addUnit :: ClassMap -> TypeMap -> TypeMap
addUnit cm = fromMaybe (error "addUnit") . maybeResult . mergeTypeMap cm bTypes
mergeOpInfos s1 s2 = if Set.null s1 then return s2 else do
let (o, os) = Set.deleteFindMin s1
(es, us) = Set.partition ((opType o ==) . opType) s2
s <- mergeOpInfos os us
r <- foldM mergeOpInfo o $ Set.toList es
return $ Set.insert r s
mergeOpInfo :: OpInfo -> OpInfo -> Result OpInfo
mergeOpInfo o1 o2 = do
let as = Set.union (opAttrs o1) $ opAttrs o2
d <- mergeOpDefn (opDefn o1) $ opDefn o2
return $ OpInfo (opType o1) as d
mergeTypeMap :: ClassMap -> TypeMap -> TypeMap -> Result TypeMap
mergeTypeMap = mergeMap . mergeTypeInfo
merge :: Env -> Env -> Result Env
merge e1 e2 = do
clMap <- mergeClassMap (classMap e1) $ classMap e2
tMap <- mergeTypeMap clMap (typeMap e1) $ typeMap e2
let tAs = filterAliases tMap
as <- mergeMap mergeOpInfos (assumps e1) $ assumps e2
bs <- mergeMap (\ i1 i2 -> if i1 == i2 then return i1 else
fail "conflicting operation for binder syntax")
(binders e1) $ binders e2
return initialEnv
{ classMap = clMap
, typeMap = tMap
, binders = bs }
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) $ getRange t2] $ Just t2