89390a303afa9ca380fc9b878cffdd88667fdd25Christian Maeder{- |

89390a303afa9ca380fc9b878cffdd88667fdd25Christian MaederModule : ./HasCASL/Merge.hs

89390a303afa9ca380fc9b878cffdd88667fdd25Christian MaederDescription : union of signature parts

89390a303afa9ca380fc9b878cffdd88667fdd25Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

89390a303afa9ca380fc9b878cffdd88667fdd25Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

89390a303afa9ca380fc9b878cffdd88667fdd25Christian Maeder

89390a303afa9ca380fc9b878cffdd88667fdd25Christian MaederMaintainer : 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 :: Set.Set OpInfo -> Set.Set OpInfo -> Result (Set.Set OpInfo)

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

, assumps = Map.map (Set.map $ mapOpInfo (id, expandAliases tAs)) as

, 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