{- |
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)
import qualified Control.Monad.Fail as Fail

mergeTypeInfo :: ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
mergeTypeInfo :: ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
mergeTypeInfo cm :: ClassMap
cm t1 :: TypeInfo
t1 t2 :: TypeInfo
t2 = do
    let o :: Set Kind
o = ClassMap -> [Set Kind] -> Set Kind
keepMinKinds ClassMap
cm [TypeInfo -> Set Kind
otherTypeKinds TypeInfo
t1, TypeInfo -> Set Kind
otherTypeKinds TypeInfo
t2]
        s :: Set Id
s = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TypeInfo -> Set Id
superTypes TypeInfo
t1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
t2
    RawKind
k <- String -> RawKind -> RawKind -> Result RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind "type raw kind" (TypeInfo -> RawKind
typeKind TypeInfo
t1) (RawKind -> Result RawKind) -> RawKind -> Result RawKind
forall a b. (a -> b) -> a -> b
$ TypeInfo -> RawKind
typeKind TypeInfo
t2
    TypeDefn
d <- TypeDefn -> TypeDefn -> Result TypeDefn
mergeTypeDefn (TypeInfo -> TypeDefn
typeDefn TypeInfo
t1) (TypeDefn -> Result TypeDefn) -> TypeDefn -> Result TypeDefn
forall a b. (a -> b) -> a -> b
$ TypeInfo -> TypeDefn
typeDefn TypeInfo
t2
    TypeInfo -> Result TypeInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeInfo -> Result TypeInfo) -> TypeInfo -> Result TypeInfo
forall a b. (a -> b) -> a -> b
$ RawKind -> Set Kind -> Set Id -> TypeDefn -> TypeInfo
TypeInfo RawKind
k Set Kind
o Set Id
s TypeDefn
d

mergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
mergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
mergeTypeDefn d1 :: TypeDefn
d1 d2 :: TypeDefn
d2 = case (TypeDefn
d1, TypeDefn
d2) of
    (_, DatatypeDefn _) -> TypeDefn -> Result TypeDefn
forall (m :: * -> *) a. Monad m => a -> m a
return TypeDefn
d2
    (PreDatatype, _) -> String -> Result TypeDefn
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "expected data type definition"
    (_, PreDatatype) -> TypeDefn -> Result TypeDefn
forall (m :: * -> *) a. Monad m => a -> m a
return TypeDefn
d1
    (NoTypeDefn, _) -> TypeDefn -> Result TypeDefn
forall (m :: * -> *) a. Monad m => a -> m a
return TypeDefn
d2
    (_, NoTypeDefn) -> TypeDefn -> Result TypeDefn
forall (m :: * -> *) a. Monad m => a -> m a
return TypeDefn
d1
    (AliasTypeDefn s1 :: Type
s1, AliasTypeDefn s2 :: Type
s2) -> do
        Type
s <- Type -> Type -> Result Type
mergeAlias Type
s1 Type
s2
        TypeDefn -> Result TypeDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeDefn -> Result TypeDefn) -> TypeDefn -> Result TypeDefn
forall a b. (a -> b) -> a -> b
$ Type -> TypeDefn
AliasTypeDefn Type
s
    (_, _) -> String -> TypeDefn -> TypeDefn -> Result TypeDefn
forall a. (Pretty a, Eq a) => String -> a -> a -> Result a
mergeA "TypeDefn" TypeDefn
d1 TypeDefn
d2

mergeAlias :: Type -> Type -> Result Type
mergeAlias :: Type -> Type -> Result Type
mergeAlias s1 :: Type
s1 s2 :: Type
s2 = if Type -> Type -> Bool
eqStrippedType Type
s1 Type
s2 then Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
s1 else
    String -> Result Type
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Type) -> String -> Result Type
forall a b. (a -> b) -> a -> b
$ "wrong type" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> Type -> String
forall a. Pretty a => a -> a -> String
expected Type
s1 Type
s2

mergeOpBrand :: OpBrand -> OpBrand -> OpBrand
mergeOpBrand :: OpBrand -> OpBrand -> OpBrand
mergeOpBrand b1 :: OpBrand
b1 b2 :: OpBrand
b2 = case (OpBrand
b1, OpBrand
b2) of
    (Pred, _) -> OpBrand
Pred
    (_, Pred) -> OpBrand
Pred
    (Op, _) -> OpBrand
Op
    (_, Op) -> OpBrand
Op
    _ -> OpBrand
Fun

mergeOpDefn :: OpDefn -> OpDefn -> Result OpDefn
mergeOpDefn :: OpDefn -> OpDefn -> Result OpDefn
mergeOpDefn d1 :: OpDefn
d1 d2 :: OpDefn
d2 = case (OpDefn
d1, OpDefn
d2) of
    (NoOpDefn b1 :: OpBrand
b1, NoOpDefn b2 :: OpBrand
b2) -> do
        let b :: OpBrand
b = OpBrand -> OpBrand -> OpBrand
mergeOpBrand OpBrand
b1 OpBrand
b2
        OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (OpDefn -> Result OpDefn) -> OpDefn -> Result OpDefn
forall a b. (a -> b) -> a -> b
$ OpBrand -> OpDefn
NoOpDefn OpBrand
b
    (SelectData c1 :: Set ConstrInfo
c1 s :: Id
s, SelectData c2 :: Set ConstrInfo
c2 _) -> do
        let c :: Set ConstrInfo
c = Set ConstrInfo -> Set ConstrInfo -> Set ConstrInfo
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ConstrInfo
c1 Set ConstrInfo
c2
        OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (OpDefn -> Result OpDefn) -> OpDefn -> Result OpDefn
forall a b. (a -> b) -> a -> b
$ Set ConstrInfo -> Id -> OpDefn
SelectData Set ConstrInfo
c Id
s
    (Definition b1 :: OpBrand
b1 e1 :: Term
e1, Definition b2 :: OpBrand
b2 e2 :: Term
e2) -> do
        Term
d <- DiagKind -> Term -> Term -> Result Term
mergeTerm DiagKind
Hint Term
e1 Term
e2
        let b :: OpBrand
b = OpBrand -> OpBrand -> OpBrand
mergeOpBrand OpBrand
b1 OpBrand
b2
        OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (OpDefn -> Result OpDefn) -> OpDefn -> Result OpDefn
forall a b. (a -> b) -> a -> b
$ OpBrand -> Term -> OpDefn
Definition OpBrand
b Term
d
    (NoOpDefn b1 :: OpBrand
b1, Definition b2 :: OpBrand
b2 e2 :: Term
e2) -> do
        let b :: OpBrand
b = OpBrand -> OpBrand -> OpBrand
mergeOpBrand OpBrand
b1 OpBrand
b2
        OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (OpDefn -> Result OpDefn) -> OpDefn -> Result OpDefn
forall a b. (a -> b) -> a -> b
$ OpBrand -> Term -> OpDefn
Definition OpBrand
b Term
e2
    (Definition b1 :: OpBrand
b1 e1 :: Term
e1, NoOpDefn b2 :: OpBrand
b2) -> do
        let b :: OpBrand
b = OpBrand -> OpBrand -> OpBrand
mergeOpBrand OpBrand
b1 OpBrand
b2
        OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (OpDefn -> Result OpDefn) -> OpDefn -> Result OpDefn
forall a b. (a -> b) -> a -> b
$ OpBrand -> Term -> OpDefn
Definition OpBrand
b Term
e1
    (ConstructData _, SelectData _ _) ->
        String -> Result OpDefn
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal selector as constructor redefinition"
    (SelectData _ _, ConstructData _) ->
        String -> Result OpDefn
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal constructor as selector redefinition"
    (ConstructData _, _) -> OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return OpDefn
d1
    (_, ConstructData _) -> OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return OpDefn
d2
    (SelectData _ _, _) -> OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return OpDefn
d1
    (_, SelectData _ _) -> OpDefn -> Result OpDefn
forall (m :: * -> *) a. Monad m => a -> m a
return OpDefn
d2

addUnit :: ClassMap -> TypeMap -> TypeMap
addUnit :: ClassMap -> TypeMap -> TypeMap
addUnit cm :: ClassMap
cm = TypeMap -> Maybe TypeMap -> TypeMap
forall a. a -> Maybe a -> a
fromMaybe (String -> TypeMap
forall a. HasCallStack => String -> a
error "addUnit") (Maybe TypeMap -> TypeMap)
-> (TypeMap -> Maybe TypeMap) -> TypeMap -> TypeMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result TypeMap -> Maybe TypeMap
forall a. Result a -> Maybe a
maybeResult (Result TypeMap -> Maybe TypeMap)
-> (TypeMap -> Result TypeMap) -> TypeMap -> Maybe TypeMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassMap -> TypeMap -> TypeMap -> Result TypeMap
mergeTypeMap ClassMap
cm TypeMap
bTypes

mergeOpInfos :: Set.Set OpInfo -> Set.Set OpInfo -> Result (Set.Set OpInfo)
mergeOpInfos :: Set OpInfo -> Set OpInfo -> Result (Set OpInfo)
mergeOpInfos s1 :: Set OpInfo
s1 s2 :: Set OpInfo
s2 = if Set OpInfo -> Bool
forall a. Set a -> Bool
Set.null Set OpInfo
s1 then Set OpInfo -> Result (Set OpInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return Set OpInfo
s2 else do
    let (o :: OpInfo
o, os :: Set OpInfo
os) = Set OpInfo -> (OpInfo, Set OpInfo)
forall a. Set a -> (a, Set a)
Set.deleteFindMin Set OpInfo
s1
        (es :: Set OpInfo
es, us :: Set OpInfo
us) = (OpInfo -> Bool) -> Set OpInfo -> (Set OpInfo, Set OpInfo)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition ((OpInfo -> TypeScheme
opType OpInfo
o TypeScheme -> TypeScheme -> Bool
forall a. Eq a => a -> a -> Bool
==) (TypeScheme -> Bool) -> (OpInfo -> TypeScheme) -> OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
opType) Set OpInfo
s2
    Set OpInfo
s <- Set OpInfo -> Set OpInfo -> Result (Set OpInfo)
mergeOpInfos Set OpInfo
os Set OpInfo
us
    OpInfo
r <- (OpInfo -> OpInfo -> Result OpInfo)
-> OpInfo -> [OpInfo] -> Result OpInfo
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM OpInfo -> OpInfo -> Result OpInfo
mergeOpInfo OpInfo
o ([OpInfo] -> Result OpInfo) -> [OpInfo] -> Result OpInfo
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
es
    Set OpInfo -> Result (Set OpInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set OpInfo -> Result (Set OpInfo))
-> Set OpInfo -> Result (Set OpInfo)
forall a b. (a -> b) -> a -> b
$ OpInfo -> Set OpInfo -> Set OpInfo
forall a. Ord a => a -> Set a -> Set a
Set.insert OpInfo
r Set OpInfo
s

mergeOpInfo :: OpInfo -> OpInfo -> Result OpInfo
mergeOpInfo :: OpInfo -> OpInfo -> Result OpInfo
mergeOpInfo o1 :: OpInfo
o1 o2 :: OpInfo
o2 = do
    let as :: Set OpAttr
as = Set OpAttr -> Set OpAttr -> Set OpAttr
forall a. Ord a => Set a -> Set a -> Set a
Set.union (OpInfo -> Set OpAttr
opAttrs OpInfo
o1) (Set OpAttr -> Set OpAttr) -> Set OpAttr -> Set OpAttr
forall a b. (a -> b) -> a -> b
$ OpInfo -> Set OpAttr
opAttrs OpInfo
o2
    OpDefn
d <- OpDefn -> OpDefn -> Result OpDefn
mergeOpDefn (OpInfo -> OpDefn
opDefn OpInfo
o1) (OpDefn -> Result OpDefn) -> OpDefn -> Result OpDefn
forall a b. (a -> b) -> a -> b
$ OpInfo -> OpDefn
opDefn OpInfo
o2
    OpInfo -> Result OpInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (OpInfo -> Result OpInfo) -> OpInfo -> Result OpInfo
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo (OpInfo -> TypeScheme
opType OpInfo
o1) Set OpAttr
as OpDefn
d

mergeTypeMap :: ClassMap -> TypeMap -> TypeMap -> Result TypeMap
mergeTypeMap :: ClassMap -> TypeMap -> TypeMap -> Result TypeMap
mergeTypeMap = (TypeInfo -> TypeInfo -> Result TypeInfo)
-> TypeMap -> TypeMap -> Result TypeMap
forall a b.
(Ord a, GetRange a, Pretty a) =>
(b -> b -> Result b) -> Map a b -> Map a b -> Result (Map a b)
mergeMap ((TypeInfo -> TypeInfo -> Result TypeInfo)
 -> TypeMap -> TypeMap -> Result TypeMap)
-> (ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo)
-> ClassMap
-> TypeMap
-> TypeMap
-> Result TypeMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
mergeTypeInfo

merge :: Env -> Env -> Result Env
merge :: Env -> Env -> Result Env
merge e1 :: Env
e1 e2 :: Env
e2 = do
    ClassMap
clMap <- ClassMap -> ClassMap -> Result ClassMap
mergeClassMap (Env -> ClassMap
classMap Env
e1) (ClassMap -> Result ClassMap) -> ClassMap -> Result ClassMap
forall a b. (a -> b) -> a -> b
$ Env -> ClassMap
classMap Env
e2
    TypeMap
tMap <- ClassMap -> TypeMap -> TypeMap -> Result TypeMap
mergeTypeMap ClassMap
clMap (Env -> TypeMap
typeMap Env
e1) (TypeMap -> Result TypeMap) -> TypeMap -> Result TypeMap
forall a b. (a -> b) -> a -> b
$ Env -> TypeMap
typeMap Env
e2
    let tAs :: TypeMap
tAs = TypeMap -> TypeMap
filterAliases TypeMap
tMap
    Map Id (Set OpInfo)
as <- (Set OpInfo -> Set OpInfo -> Result (Set OpInfo))
-> Map Id (Set OpInfo)
-> Map Id (Set OpInfo)
-> Result (Map Id (Set OpInfo))
forall a b.
(Ord a, GetRange a, Pretty a) =>
(b -> b -> Result b) -> Map a b -> Map a b -> Result (Map a b)
mergeMap Set OpInfo -> Set OpInfo -> Result (Set OpInfo)
mergeOpInfos (Env -> Map Id (Set OpInfo)
assumps Env
e1) (Map Id (Set OpInfo) -> Result (Map Id (Set OpInfo)))
-> Map Id (Set OpInfo) -> Result (Map Id (Set OpInfo))
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e2
    Map Id Id
bs <- (Id -> Id -> Result Id)
-> Map Id Id -> Map Id Id -> Result (Map Id Id)
forall a b.
(Ord a, GetRange a, Pretty a) =>
(b -> b -> Result b) -> Map a b -> Map a b -> Result (Map a b)
mergeMap (\ i1 :: Id
i1 i2 :: Id
i2 -> if Id
i1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
i2 then Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
i1 else
                    String -> Result Id
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "conflicting operation for binder syntax")
         (Env -> Map Id Id
binders Env
e1) (Map Id Id -> Result (Map Id Id))
-> Map Id Id -> Result (Map Id Id)
forall a b. (a -> b) -> a -> b
$ Env -> Map Id Id
binders Env
e2
    Env -> Result Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
initialEnv
      { classMap :: ClassMap
classMap = ClassMap
clMap
      , typeMap :: TypeMap
typeMap = TypeMap
tMap
      , assumps :: Map Id (Set OpInfo)
assumps = (Set OpInfo -> Set OpInfo)
-> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((OpInfo -> OpInfo) -> Set OpInfo -> Set OpInfo
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((OpInfo -> OpInfo) -> Set OpInfo -> Set OpInfo)
-> (OpInfo -> OpInfo) -> Set OpInfo -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ Rename -> OpInfo -> OpInfo
mapOpInfo ((Id, TypeScheme) -> (Id, TypeScheme)
forall a. a -> a
id, TypeMap -> Type -> Type
expandAliases TypeMap
tAs)) Map Id (Set OpInfo)
as
      , binders :: Map Id Id
binders = Map Id Id
bs }

mergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
mergeA :: String -> a -> a -> Result a
mergeA str :: String
str t1 :: a
t1 t2 :: a
t2 = if a
t1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
t2 then a -> Result a
forall (m :: * -> *) a. Monad m => a -> m a
return a
t1 else
    String -> Result a
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("different " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> a -> String
forall a. Pretty a => a -> a -> String
expected a
t1 a
t2)

mergeTerm :: DiagKind -> Term -> Term -> Result Term
mergeTerm :: DiagKind -> Term -> Term -> Result Term
mergeTerm k :: DiagKind
k t1 :: Term
t1 t2 :: Term
t2 = if Term
t1 Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
t2 then Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t1 else
  [Diagnosis] -> Maybe Term -> Result Term
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
k ("different terms" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> Term -> String
forall a. Pretty a => a -> a -> String
expected Term
t1 Term
t2) (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t2] (Maybe Term -> Result Term) -> Maybe Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just Term
t2