```{- |
Module      :  ./HasCASL/Morphism.hs
Description :  morphisms implementation
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

mapping entities of morphisms

-}

module HasCASL.Morphism where

import HasCASL.As
import HasCASL.AsToLe
import HasCASL.AsUtils
import HasCASL.FoldType
import HasCASL.Le
import HasCASL.MapTerm
import HasCASL.Merge
import HasCASL.PrintLe
import HasCASL.TypeAna

import Common.DocUtils
import Common.Doc
import Common.Id
import Common.Result
import Common.Utils (composeMap)
import Common.Lib.MapSet (setToMap)

import Control.Monad
import qualified Control.Monad.Fail as Fail

import qualified Data.Set as Set
import qualified Data.Map as Map

disjointKeys :: (Ord a, Pretty a, Fail.MonadFail m) => Map.Map a b -> Map.Map a c
-> m ()
disjointKeys :: Map a b -> Map a c -> m ()
disjointKeys m1 :: Map a b
m1 m2 :: Map a c
m2 = let d :: Set a
d = Map a b -> Set a
forall k a. Map k a -> Set k
Map.keysSet (Map a b -> Set a) -> Map a b -> Set a
forall a b. (a -> b) -> a -> b
\$ Map a b -> Map a c -> Map a b
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection Map a b
m1 Map a c
m2 in
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
d) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
\$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
\$ Doc -> String
forall a. Show a => a -> String
show
([Doc] -> Doc
sep [ String -> Doc
text "overlapping identifiers for types and classes:"
, Set a -> Doc
forall a. Pretty a => a -> Doc
pretty Set a
d])

-- | map a kind along an identifier map
mapKindI :: IdMap -> Kind -> Kind
mapKindI :: IdMap -> Kind -> Kind
mapKindI jm :: IdMap
jm = (Id -> Id) -> Kind -> Kind
forall a b. (a -> b) -> AnyKind a -> AnyKind b
mapKind (\ a :: Id
a -> Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
a Id
a IdMap
jm)

-- | map a kind along a signature morphism (variance is preserved)
mapKinds :: Morphism -> Kind -> Kind
mapKinds :: Morphism -> Kind -> Kind
mapKinds = IdMap -> Kind -> Kind
mapKindI (IdMap -> Kind -> Kind)
-> (Morphism -> IdMap) -> Morphism -> Kind -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> IdMap
classIdMap

-- | only rename the kinds in a type
mapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
mapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
mapKindsOfType jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im = FoldTypeRec Type -> Type -> Type
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec Type
mapTypeRec
{ foldTypeAbs :: Type -> TypeArg -> Type -> Range -> Type
foldTypeAbs = \ _ -> TypeArg -> Type -> Range -> Type
TypeAbs (TypeArg -> Type -> Range -> Type)
-> (TypeArg -> TypeArg) -> TypeArg -> Type -> Range -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
mapTypeArg IdMap
jm TypeMap
tm IdMap
im
, foldKindedType :: Type -> Type -> Set Kind -> Range -> Type
foldKindedType = \ _ t :: Type
t -> Type -> Set Kind -> Range -> Type
KindedType Type
t (Set Kind -> Range -> Type)
-> (Set Kind -> Set Kind) -> Set Kind -> Range -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Kind) -> Set Kind -> Set Kind
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IdMap -> Kind -> Kind
mapKindI IdMap
jm) }

-- | map type, expand it, and also adjust the kinds
mapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
mapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
mapTypeE jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im =
IdMap -> TypeMap -> IdMap -> Type -> Type
mapKindsOfType IdMap
jm TypeMap
tm IdMap
im (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeMap -> Type -> Type
expandAliases TypeMap
tm (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdMap -> Type -> Type
mapType IdMap
im

-- | map a kind along a signature morphism (variance is preserved)
mapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
mapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
mapVarKind jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im vk :: VarKind
vk = case VarKind
vk of
VarKind k :: Kind
k -> Kind -> VarKind
VarKind (Kind -> VarKind) -> Kind -> VarKind
forall a b. (a -> b) -> a -> b
\$ IdMap -> Kind -> Kind
mapKindI IdMap
jm Kind
k
Downset ty :: Type
ty -> Type -> VarKind
Downset (Type -> VarKind) -> Type -> VarKind
forall a b. (a -> b) -> a -> b
\$ IdMap -> TypeMap -> IdMap -> Type -> Type
mapTypeE IdMap
jm TypeMap
tm IdMap
im Type
ty
_ -> VarKind
vk

mapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
mapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
mapTypeArg jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im (TypeArg i :: Id
i v :: Variance
v vk :: VarKind
vk rk :: RawKind
rk c :: Int
c s :: SeparatorKind
s r :: Range
r) =
Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v (IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
mapVarKind IdMap
jm TypeMap
tm IdMap
im VarKind
vk) RawKind
rk Int
c SeparatorKind
s Range
r

mapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
mapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
mapTypeScheme jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im (TypeScheme args :: [TypeArg]
args ty :: Type
ty ps :: Range
ps) =
[TypeArg] -> Type -> Range -> TypeScheme
TypeScheme ((TypeArg -> TypeArg) -> [TypeArg] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
mapTypeArg IdMap
jm TypeMap
tm IdMap
im) [TypeArg]
args) (IdMap -> TypeMap -> IdMap -> Type -> Type
mapTypeE IdMap
jm TypeMap
tm IdMap
im Type
ty) Range
ps

mapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
mapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
mapSen jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im fm :: FunMap
fm = Rename -> Term -> Term
mapTerm (IdMap
-> TypeMap
-> IdMap
-> FunMap
-> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym IdMap
jm TypeMap
tm IdMap
im FunMap
fm, IdMap -> TypeMap -> IdMap -> Type -> Type
mapTypeE IdMap
jm TypeMap
tm IdMap
im)

getDatatypeIds :: DataEntry -> Set.Set Id
getDatatypeIds :: DataEntry -> Set Id
getDatatypeIds (DataEntry _ i :: Id
i _ _ _ alts :: Set AltDefn
alts) =
let getAltIds :: AltDefn -> Set Id
getAltIds (Construct _ tys :: [Type]
tys _ sels :: [[Selector]]
sels) = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union
([Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
\$ (Type -> Set Id) -> [Type] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Set Id
getTypeIds [Type]
tys)
(Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
\$ [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
\$ ([Selector] -> [Set Id]) -> [[Selector]] -> [Set Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Selector -> Set Id) -> [Selector] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map Selector -> Set Id
getSelIds) [[Selector]]
sels
getSelIds :: Selector -> Set Id
getSelIds (Select _ ty :: Type
ty _) = Type -> Set Id
getTypeIds Type
ty
getTypeIds :: Type -> Set Id
getTypeIds = (Int -> Bool) -> Type -> Set Id
idsOf (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0)
in Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
i (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
\$ [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
\$ (AltDefn -> Set Id) -> [AltDefn] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map AltDefn -> Set Id
getAltIds ([AltDefn] -> [Set Id]) -> [AltDefn] -> [Set Id]
forall a b. (a -> b) -> a -> b
\$ Set AltDefn -> [AltDefn]
forall a. Set a -> [a]
Set.toList Set AltDefn
alts

mapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
mapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
mapDataEntry jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im fm :: FunMap
fm (DataEntry dm :: IdMap
dm i :: Id
i k :: GenKind
k args :: [TypeArg]
args rk :: RawKind
rk alts :: Set AltDefn
alts) =
let nDm :: IdMap
nDm = (Id -> Id) -> IdMap -> IdMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ a :: Id
a -> Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
a Id
a IdMap
im) IdMap
dm
newargs :: [TypeArg]
newargs = (TypeArg -> TypeArg) -> [TypeArg] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
mapTypeArg IdMap
jm TypeMap
tm IdMap
im) [TypeArg]
args
nIm :: IdMap
nIm = IdMap -> IdMap -> IdMap
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference IdMap
im IdMap
dm
in IdMap
-> Id
-> GenKind
-> [TypeArg]
-> RawKind
-> Set AltDefn
-> DataEntry
DataEntry IdMap
nDm Id
i GenKind
k [TypeArg]
newargs RawKind
rk (Set AltDefn -> DataEntry) -> Set AltDefn -> DataEntry
forall a b. (a -> b) -> a -> b
\$ (AltDefn -> AltDefn) -> Set AltDefn -> Set AltDefn
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map
(IdMap
-> TypeMap
-> IdMap
-> FunMap
-> IdMap
-> [TypeArg]
-> Type
-> AltDefn
-> AltDefn
mapAlt IdMap
jm TypeMap
tm IdMap
im FunMap
fm IdMap
nIm [TypeArg]
newargs
(Type -> AltDefn -> AltDefn) -> Type -> AltDefn -> AltDefn
forall a b. (a -> b) -> a -> b
\$ Id -> [TypeArg] -> RawKind -> Type
patToType (Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i IdMap
dm) [TypeArg]
newargs RawKind
rk) Set AltDefn
alts

mapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
-> AltDefn -> AltDefn
mapAlt :: IdMap
-> TypeMap
-> IdMap
-> FunMap
-> IdMap
-> [TypeArg]
-> Type
-> AltDefn
-> AltDefn
mapAlt jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im fm :: FunMap
fm nIm :: IdMap
nIm args :: [TypeArg]
args dt :: Type
dt (Construct mi :: Maybe Id
mi ts :: [Type]
ts p :: Partiality
p sels :: [[Selector]]
sels) =
let newTs :: [Type]
newTs = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> TypeMap -> IdMap -> Type -> Type
mapTypeE IdMap
jm TypeMap
tm IdMap
nIm) [Type]
ts
newSels :: [[Selector]]
newSels = ([Selector] -> [Selector]) -> [[Selector]] -> [[Selector]]
forall a b. (a -> b) -> [a] -> [b]
map ((Selector -> Selector) -> [Selector] -> [Selector]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap
-> TypeMap
-> IdMap
-> FunMap
-> IdMap
-> [TypeArg]
-> Type
-> Selector
-> Selector
mapSel IdMap
jm TypeMap
tm IdMap
im FunMap
fm IdMap
nIm [TypeArg]
args Type
dt)) [[Selector]]
sels
in case Maybe Id
mi of
Just i :: Id
i -> let
sc :: TypeScheme
sc = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
args (Type -> Partiality -> [Type] -> Type
getFunType Type
dt Partiality
p [Type]
ts) Range
nullRange
(j :: Id
j, TypeScheme _ ty :: Type
ty _) = IdMap
-> TypeMap
-> IdMap
-> FunMap
-> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym IdMap
jm TypeMap
tm IdMap
im FunMap
fm (Id
i, TypeScheme
sc)
in Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
j) [Type]
newTs ([Type] -> Type -> Partiality
forall a. [a] -> Type -> Partiality
getPartiality [Type]
newTs Type
ty) [[Selector]]
newSels
Nothing -> Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct Maybe Id
mi [Type]
newTs Partiality
p [[Selector]]
newSels

mapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
-> Selector -> Selector
mapSel :: IdMap
-> TypeMap
-> IdMap
-> FunMap
-> IdMap
-> [TypeArg]
-> Type
-> Selector
-> Selector
mapSel jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im fm :: FunMap
fm nIm :: IdMap
nIm args :: [TypeArg]
args dt :: Type
dt (Select mid :: Maybe Id
mid t :: Type
t p :: Partiality
p) =
let newT :: Type
newT = IdMap -> TypeMap -> IdMap -> Type -> Type
mapTypeE IdMap
jm TypeMap
tm IdMap
nIm Type
t
in case Maybe Id
mid of
Nothing -> Maybe Id -> Type -> Partiality -> Selector
Select Maybe Id
mid Type
newT Partiality
p
Just i :: Id
i -> let
sc :: TypeScheme
sc = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
args (Type -> Partiality -> Type -> Type
getSelType Type
dt Partiality
p Type
t) Range
nullRange
(j :: Id
j, TypeScheme _ ty :: Type
ty _) = IdMap
-> TypeMap
-> IdMap
-> FunMap
-> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym IdMap
jm TypeMap
tm IdMap
im FunMap
fm (Id
i, TypeScheme
sc)
in Maybe Id -> Type -> Partiality -> Selector
Select (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
j) Type
newT (Partiality -> Selector) -> Partiality -> Selector
forall a b. (a -> b) -> a -> b
\$ [Type] -> Type -> Partiality
forall a. [a] -> Type -> Partiality
getPartiality [Type
dt] Type
ty

{- | get the partiality from a constructor type
with a given number of curried arguments. -}
getPartiality :: [a] -> Type -> Partiality
getPartiality :: [a] -> Type -> Partiality
getPartiality args :: [a]
args t :: Type
t = case Type -> (Type, [Type])
getTypeAppl Type
t of
(TypeName i :: Id
i _ _, [_, res :: Type
res]) | Id -> Bool
isArrow Id
i -> case [a]
args of
[] -> Partiality
Total
[_] -> if Id -> Bool
isPartialArrow Id
i then Partiality
Partial else Partiality
Total
_ : rs :: [a]
rs -> [a] -> Type -> Partiality
forall a. [a] -> Type -> Partiality
getPartiality [a]
rs Type
res
(TypeName i :: Id
i _ _, [_]) | Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
args then Partiality
Partial else String -> Partiality
forall a. HasCallStack => String -> a
error "getPartiality"
_ -> Partiality
Total

mapSentence :: Morphism -> Sentence -> Result Sentence
mapSentence :: Morphism -> Sentence -> Result Sentence
mapSentence m :: Morphism
m s :: Sentence
s = let
tm :: TypeMap
tm = TypeMap -> TypeMap
filterAliases (TypeMap -> TypeMap) -> (Env -> TypeMap) -> Env -> TypeMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TypeMap
typeMap (Env -> TypeMap) -> Env -> TypeMap
forall a b. (a -> b) -> a -> b
\$ Morphism -> Env
mtarget Morphism
m
im :: IdMap
im = Morphism -> IdMap
typeIdMap Morphism
m
jm :: IdMap
jm = Morphism -> IdMap
classIdMap Morphism
m
fm :: FunMap
fm = Morphism -> FunMap
funMap Morphism
m
f :: (Id, TypeScheme) -> (Id, TypeScheme)
f = IdMap
-> TypeMap
-> IdMap
-> FunMap
-> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym IdMap
jm TypeMap
tm IdMap
im FunMap
fm
in Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence) -> Sentence -> Result Sentence
forall a b. (a -> b) -> a -> b
\$ case Sentence
s of
Formula t :: Term
t -> Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
\$ IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
mapSen IdMap
jm TypeMap
tm IdMap
im FunMap
fm Term
t
DatatypeSen td :: [DataEntry]
td -> [DataEntry] -> Sentence
DatatypeSen ([DataEntry] -> Sentence) -> [DataEntry] -> Sentence
forall a b. (a -> b) -> a -> b
\$ (DataEntry -> DataEntry) -> [DataEntry] -> [DataEntry]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
mapDataEntry IdMap
jm TypeMap
tm IdMap
im FunMap
fm) [DataEntry]
td
ProgEqSen i :: Id
i sc :: TypeScheme
sc pe :: ProgEq
pe ->
let (ni :: Id
ni, nsc :: TypeScheme
nsc) = (Id, TypeScheme) -> (Id, TypeScheme)
f (Id
i, TypeScheme
sc)
in Id -> TypeScheme -> ProgEq -> Sentence
ProgEqSen Id
ni TypeScheme
nsc (ProgEq -> Sentence) -> ProgEq -> Sentence
forall a b. (a -> b) -> a -> b
\$ Rename -> ProgEq -> ProgEq
mapEq ((Id, TypeScheme) -> (Id, TypeScheme)
f, IdMap -> TypeMap -> IdMap -> Type -> Type
mapTypeE IdMap
jm TypeMap
tm IdMap
im) ProgEq
pe

mapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym :: IdMap
-> TypeMap
-> IdMap
-> FunMap
-> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym jm :: IdMap
jm tm :: TypeMap
tm im :: IdMap
im fm :: FunMap
fm (i :: Id
i, sc :: TypeScheme
sc) =
let msc :: TypeScheme
msc = IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
mapTypeScheme IdMap
jm TypeMap
tm IdMap
im TypeScheme
sc
in (Id, TypeScheme) -> (Id, TypeScheme) -> FunMap -> (Id, TypeScheme)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Id
i, TypeScheme
msc) (Id
i, TypeScheme
sc) FunMap
fm

ideMor :: Env -> Morphism
ideMor :: Env -> Morphism
ideMor e :: Env
e = Env -> Env -> Morphism
mkMorphism Env
e Env
e

compMor :: Morphism -> Morphism -> Result Morphism
compMor :: Morphism -> Morphism -> Result Morphism
compMor m1 :: Morphism
m1 m2 :: Morphism
m2 = let
tm1 :: IdMap
tm1 = Morphism -> IdMap
typeIdMap Morphism
m1
tm2 :: IdMap
tm2 = Morphism -> IdMap
typeIdMap Morphism
m2
ctm :: IdMap
ctm = TypeMap -> IdMap -> IdMap -> IdMap
forall a b. Ord a => Map a b -> Map a a -> Map a a -> Map a a
composeMap (Env -> TypeMap
typeMap Env
src) IdMap
tm1 IdMap
tm2
cm1 :: IdMap
cm1 = Morphism -> IdMap
classIdMap Morphism
m1
cm2 :: IdMap
cm2 = Morphism -> IdMap
classIdMap Morphism
m2
ccm :: IdMap
ccm = Map Id ClassInfo -> IdMap -> IdMap -> IdMap
forall a b. Ord a => Map a b -> Map a a -> Map a a -> Map a a
composeMap (Env -> Map Id ClassInfo
classMap Env
src) IdMap
cm1 IdMap
cm2
fm2 :: FunMap
fm2 = Morphism -> FunMap
funMap Morphism
m2
fm1 :: FunMap
fm1 = Morphism -> FunMap
funMap Morphism
m1
tar :: Env
tar = Morphism -> Env
mtarget Morphism
m2
src :: Env
src = Morphism -> Env
msource Morphism
m1
tm :: TypeMap
tm = TypeMap -> TypeMap
filterAliases (TypeMap -> TypeMap) -> TypeMap -> TypeMap
forall a b. (a -> b) -> a -> b
\$ Env -> TypeMap
typeMap Env
tar
emb :: Morphism
emb = Env -> Env -> Morphism
mkMorphism Env
src Env
tar
in if Morphism -> Bool
isInclMor Morphism
m1 Bool -> Bool -> Bool
&& Morphism -> Bool
isInclMor Morphism
m2 then Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism
emb else do
IdMap -> IdMap -> Result ()
forall a (m :: * -> *) b c.
(Ord a, Pretty a, MonadFail m) =>
Map a b -> Map a c -> m ()
disjointKeys IdMap
ctm IdMap
ccm
Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism
emb
{ typeIdMap :: IdMap
typeIdMap = IdMap
ctm
, classIdMap :: IdMap
classIdMap = IdMap
ccm
, funMap :: FunMap
funMap = FunMap -> Map (Id, TypeScheme) () -> FunMap
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection
(((Id, TypeScheme) -> (Id, TypeScheme) -> FunMap -> FunMap)
-> FunMap -> FunMap -> FunMap
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ p1 :: (Id, TypeScheme)
p1@(i :: Id
i, sc :: TypeScheme
sc) p2 :: (Id, TypeScheme)
p2 ->
let p3 :: (Id, TypeScheme)
p3 = IdMap
-> TypeMap
-> IdMap
-> FunMap
-> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym IdMap
ccm TypeMap
tm IdMap
tm2 FunMap
fm2 (Id, TypeScheme)
p2
nSc :: TypeScheme
nSc = IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
mapTypeScheme IdMap
ccm TypeMap
tm IdMap
ctm TypeScheme
sc
in if (Id
i, TypeScheme
nSc) (Id, TypeScheme) -> (Id, TypeScheme) -> Bool
forall a. Eq a => a -> a -> Bool
== (Id, TypeScheme)
p3 then (Id, TypeScheme) -> FunMap -> FunMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (Id, TypeScheme)
p1 else
(Id, TypeScheme) -> (Id, TypeScheme) -> FunMap -> FunMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id, TypeScheme)
p1 (Id, TypeScheme)
p3)
FunMap
fm2 FunMap
fm1) (Map (Id, TypeScheme) () -> FunMap)
-> Map (Id, TypeScheme) () -> FunMap
forall a b. (a -> b) -> a -> b
\$ [((Id, TypeScheme), ())] -> Map (Id, TypeScheme) ()
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((Id, TypeScheme), ())] -> Map (Id, TypeScheme) ())
-> [((Id, TypeScheme), ())] -> Map (Id, TypeScheme) ()
forall a b. (a -> b) -> a -> b
\$
((Id, Set OpInfo) -> [((Id, TypeScheme), ())])
-> [(Id, Set OpInfo)] -> [((Id, TypeScheme), ())]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ( \ (k :: Id
k, os :: Set OpInfo
os) ->
(OpInfo -> ((Id, TypeScheme), ()))
-> [OpInfo] -> [((Id, TypeScheme), ())]
forall a b. (a -> b) -> [a] -> [b]
map ( \ o :: OpInfo
o -> ((Id
k, OpInfo -> TypeScheme
opType OpInfo
o), ())) ([OpInfo] -> [((Id, TypeScheme), ())])
-> [OpInfo] -> [((Id, TypeScheme), ())]
forall a b. (a -> b) -> a -> b
\$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
os)
([(Id, Set OpInfo)] -> [((Id, TypeScheme), ())])
-> [(Id, Set OpInfo)] -> [((Id, TypeScheme), ())]
forall a b. (a -> b) -> a -> b
\$ Map Id (Set OpInfo) -> [(Id, Set OpInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Id (Set OpInfo) -> [(Id, Set OpInfo)])
-> Map Id (Set OpInfo) -> [(Id, Set OpInfo)]
forall a b. (a -> b) -> a -> b
\$ Env -> Map Id (Set OpInfo)
assumps Env
src }

showEnvDiff :: Env -> Env -> String
showEnvDiff :: Env -> Env -> String
showEnvDiff e1 :: Env
e1 e2 :: Env
e2 =
"Signature 1:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Env -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Env
e1 "\nSignature 2:\n"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Env -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Env
e2 "\nDifference\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Env -> String -> String
forall a. Pretty a => a -> String -> String
showDoc
(Env -> Env -> Env
diffEnv Env
e1 Env
e2) ""

legalMor :: Morphism -> Result ()
legalMor :: Morphism -> Result ()
legalMor m :: Morphism
m = let
s :: Env
s = Morphism -> Env
msource Morphism
m
t :: Env
t = Morphism -> Env
mtarget Morphism
m
ts :: IdMap
ts = Morphism -> IdMap
typeIdMap Morphism
m
cs :: IdMap
cs = Morphism -> IdMap
classIdMap Morphism
m
fs :: FunMap
fs = Morphism -> FunMap
funMap Morphism
m in
Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TypeMap -> [Id]
forall k a. Map k a -> [k]
Map.keys (Env -> TypeMap
typeMap Env
s)) (IdMap -> [Id]
forall k a. Map k a -> [k]
Map.keys IdMap
ts)
Bool -> Bool -> Bool
&& (Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TypeMap -> [Id]
forall k a. Map k a -> [k]
Map.keys (Env -> TypeMap
typeMap Env
t)) (IdMap -> [Id]
forall k a. Map k a -> [a]
Map.elems IdMap
ts)
Bool -> Bool -> Bool
&& (Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Id ClassInfo -> [Id]
forall k a. Map k a -> [k]
Map.keys (Env -> Map Id ClassInfo
classMap Env
s)) (IdMap -> [Id]
forall k a. Map k a -> [k]
Map.keys IdMap
cs)
Bool -> Bool -> Bool
&& (Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Id ClassInfo -> [Id]
forall k a. Map k a -> [k]
Map.keys (Env -> Map Id ClassInfo
classMap Env
t)) (IdMap -> [Id]
forall k a. Map k a -> [a]
Map.elems IdMap
cs)
Bool -> Bool -> Bool
&& ((Id, TypeScheme) -> Bool) -> [(Id, TypeScheme)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Id (Set OpInfo) -> [Id]
forall k a. Map k a -> [k]
Map.keys (Env -> Map Id (Set OpInfo)
assumps Env
s)) (Id -> Bool)
-> ((Id, TypeScheme) -> Id) -> (Id, TypeScheme) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst) (FunMap -> [(Id, TypeScheme)]
forall k a. Map k a -> [k]
Map.keys FunMap
fs)
Bool -> Bool -> Bool
&& ((Id, TypeScheme) -> Bool) -> [(Id, TypeScheme)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Id (Set OpInfo) -> [Id]
forall k a. Map k a -> [k]
Map.keys (Env -> Map Id (Set OpInfo)
assumps Env
t)) (Id -> Bool)
-> ((Id, TypeScheme) -> Id) -> (Id, TypeScheme) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst) (FunMap -> [(Id, TypeScheme)]
forall k a. Map k a -> [a]
Map.elems FunMap
fs))
(String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal HasCASL morphism")

morphismUnion :: Morphism -> Morphism -> Result Morphism
morphismUnion :: Morphism -> Morphism -> Result Morphism
morphismUnion m1 :: Morphism
m1 m2 :: Morphism
m2 = do
let s1 :: Env
s1 = Morphism -> Env
msource Morphism
m1
s2 :: Env
s2 = Morphism -> Env
msource Morphism
m2
Env
s <- Env -> Env -> Result Env
merge Env
s1 Env
s2
Env
t <- Env -> Env -> Result Env
merge (Morphism -> Env
mtarget Morphism
m1) (Env -> Result Env) -> Env -> Result Env
forall a b. (a -> b) -> a -> b
\$ Morphism -> Env
mtarget Morphism
m2
let tm1 :: TypeMap
tm1 = Env -> TypeMap
typeMap Env
s1
tm2 :: TypeMap
tm2 = Env -> TypeMap
typeMap Env
s2
im1 :: IdMap
im1 = Morphism -> IdMap
typeIdMap Morphism
m1
im2 :: IdMap
im2 = Morphism -> IdMap
typeIdMap Morphism
m2
-- unchanged types
ut1 :: Set Id
ut1 = TypeMap -> Set Id
forall k a. Map k a -> Set k
Map.keysSet TypeMap
tm1 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ IdMap -> Set Id
forall k a. Map k a -> Set k
Map.keysSet IdMap
im1
ut2 :: Set Id
ut2 = TypeMap -> Set Id
forall k a. Map k a -> Set k
Map.keysSet TypeMap
tm2 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ IdMap -> Set Id
forall k a. Map k a -> Set k
Map.keysSet IdMap
im2
ima1 :: IdMap
ima1 = IdMap -> IdMap -> IdMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union IdMap
im1 (IdMap -> IdMap) -> IdMap -> IdMap
forall a b. (a -> b) -> a -> b
\$ Set Id -> IdMap
forall a. Ord a => Set a -> Map a a
setToMap Set Id
ut1
ima2 :: IdMap
ima2 = IdMap -> IdMap -> IdMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union IdMap
im2 (IdMap -> IdMap) -> IdMap -> IdMap
forall a b. (a -> b) -> a -> b
\$ Set Id -> IdMap
forall a. Ord a => Set a -> Map a a
setToMap Set Id
ut2
sAs :: TypeMap
sAs = TypeMap -> TypeMap
filterAliases (TypeMap -> TypeMap) -> TypeMap -> TypeMap
forall a b. (a -> b) -> a -> b
\$ Env -> TypeMap
typeMap Env
s
tAs :: TypeMap
tAs = TypeMap -> TypeMap
filterAliases (TypeMap -> TypeMap) -> TypeMap -> TypeMap
forall a b. (a -> b) -> a -> b
\$ Env -> TypeMap
typeMap Env
t
cm1 :: Map Id ClassInfo
cm1 = Env -> Map Id ClassInfo
classMap Env
s1
cm2 :: Map Id ClassInfo
cm2 = Env -> Map Id ClassInfo
classMap Env
s2
jm1 :: IdMap
jm1 = Morphism -> IdMap
classIdMap Morphism
m1
jm2 :: IdMap
jm2 = Morphism -> IdMap
classIdMap Morphism
m2
-- unchanged classes
cut1 :: Set Id
cut1 = Map Id ClassInfo -> Set Id
forall k a. Map k a -> Set k
Map.keysSet Map Id ClassInfo
cm1 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ IdMap -> Set Id
forall k a. Map k a -> Set k
Map.keysSet IdMap
jm1
cut2 :: Set Id
cut2 = Map Id ClassInfo -> Set Id
forall k a. Map k a -> Set k
Map.keysSet Map Id ClassInfo
cm2 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ IdMap -> Set Id
forall k a. Map k a -> Set k
Map.keysSet IdMap
jm2
cima1 :: IdMap
cima1 = IdMap -> IdMap -> IdMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union IdMap
jm1 (IdMap -> IdMap) -> IdMap -> IdMap
forall a b. (a -> b) -> a -> b
\$ Set Id -> IdMap
forall a. Ord a => Set a -> Map a a
setToMap Set Id
cut1
cima2 :: IdMap
cima2 = IdMap -> IdMap -> IdMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union IdMap
jm2 (IdMap -> IdMap) -> IdMap -> IdMap
forall a b. (a -> b) -> a -> b
\$ Set Id -> IdMap
forall a. Ord a => Set a -> Map a a
setToMap Set Id
cut2
expP :: Map (Id, TypeScheme) (a, TypeScheme)
-> Map (Id, TypeScheme) (a, TypeScheme)
expP = [((Id, TypeScheme), (a, TypeScheme))]
-> Map (Id, TypeScheme) (a, TypeScheme)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((Id, TypeScheme), (a, TypeScheme))]
-> Map (Id, TypeScheme) (a, TypeScheme))
-> (Map (Id, TypeScheme) (a, TypeScheme)
-> [((Id, TypeScheme), (a, TypeScheme))])
-> Map (Id, TypeScheme) (a, TypeScheme)
-> Map (Id, TypeScheme) (a, TypeScheme)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Id, TypeScheme), (a, TypeScheme))
-> ((Id, TypeScheme), (a, TypeScheme)))
-> [((Id, TypeScheme), (a, TypeScheme))]
-> [((Id, TypeScheme), (a, TypeScheme))]
forall a b. (a -> b) -> [a] -> [b]
map ( \ ((i :: Id
i, o :: TypeScheme
o), (j :: a
j, p :: TypeScheme
p)) ->
((Id
i, TypeMap -> TypeScheme -> TypeScheme
expand TypeMap
tAs TypeScheme
o), (a
j, TypeMap -> TypeScheme -> TypeScheme
expand TypeMap
tAs TypeScheme
p)))
([((Id, TypeScheme), (a, TypeScheme))]
-> [((Id, TypeScheme), (a, TypeScheme))])
-> (Map (Id, TypeScheme) (a, TypeScheme)
-> [((Id, TypeScheme), (a, TypeScheme))])
-> Map (Id, TypeScheme) (a, TypeScheme)
-> [((Id, TypeScheme), (a, TypeScheme))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Id, TypeScheme) (a, TypeScheme)
-> [((Id, TypeScheme), (a, TypeScheme))]
forall k a. Map k a -> [(k, a)]
Map.toList
fm1 :: FunMap
fm1 = FunMap -> FunMap
forall a.
Map (Id, TypeScheme) (a, TypeScheme)
-> Map (Id, TypeScheme) (a, TypeScheme)
expP (FunMap -> FunMap) -> FunMap -> FunMap
forall a b. (a -> b) -> a -> b
\$ Morphism -> FunMap
funMap Morphism
m1
fm2 :: FunMap
fm2 = FunMap -> FunMap
forall a.
Map (Id, TypeScheme) (a, TypeScheme)
-> Map (Id, TypeScheme) (a, TypeScheme)
expP (FunMap -> FunMap) -> FunMap -> FunMap
forall a b. (a -> b) -> a -> b
\$ Morphism -> FunMap
funMap Morphism
m2
af :: IdMap -> IdMap -> Map a (Set OpInfo) -> Set (a, TypeScheme)
af jm :: IdMap
jm im :: IdMap
im = [Set (a, TypeScheme)] -> Set (a, TypeScheme)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (a, TypeScheme)] -> Set (a, TypeScheme))
-> (Map a (Set OpInfo) -> [Set (a, TypeScheme)])
-> Map a (Set OpInfo)
-> Set (a, TypeScheme)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Set OpInfo) -> Set (a, TypeScheme))
-> [(a, Set OpInfo)] -> [Set (a, TypeScheme)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: a
i, os :: Set OpInfo
os) ->
(OpInfo -> (a, TypeScheme)) -> Set OpInfo -> Set (a, TypeScheme)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ( \ o :: OpInfo
o -> (a
i, IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
mapTypeScheme IdMap
jm TypeMap
tAs IdMap
im
(TypeScheme -> TypeScheme) -> TypeScheme -> TypeScheme
forall a b. (a -> b) -> a -> b
\$ TypeMap -> TypeScheme -> TypeScheme
expand TypeMap
sAs (TypeScheme -> TypeScheme) -> TypeScheme -> TypeScheme
forall a b. (a -> b) -> a -> b
\$ OpInfo -> TypeScheme
opType OpInfo
o)) Set OpInfo
os)
([(a, Set OpInfo)] -> [Set (a, TypeScheme)])
-> (Map a (Set OpInfo) -> [(a, Set OpInfo)])
-> Map a (Set OpInfo)
-> [Set (a, TypeScheme)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a (Set OpInfo) -> [(a, Set OpInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList
-- unchanged functions
uf1 :: Set (Id, TypeScheme)
uf1 = IdMap -> IdMap -> Map Id (Set OpInfo) -> Set (Id, TypeScheme)
forall a.
Ord a =>
IdMap -> IdMap -> Map a (Set OpInfo) -> Set (a, TypeScheme)
af IdMap
jm1 IdMap
im1 (Env -> Map Id (Set OpInfo)
assumps Env
s1) Set (Id, TypeScheme)
-> Set (Id, TypeScheme) -> Set (Id, TypeScheme)
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ FunMap -> Set (Id, TypeScheme)
forall k a. Map k a -> Set k
Map.keysSet FunMap
fm1
uf2 :: Set (Id, TypeScheme)
uf2 = IdMap -> IdMap -> Map Id (Set OpInfo) -> Set (Id, TypeScheme)
forall a.
Ord a =>
IdMap -> IdMap -> Map a (Set OpInfo) -> Set (a, TypeScheme)
af IdMap
jm2 IdMap
im2 (Env -> Map Id (Set OpInfo)
assumps Env
s2) Set (Id, TypeScheme)
-> Set (Id, TypeScheme) -> Set (Id, TypeScheme)
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ FunMap -> Set (Id, TypeScheme)
forall k a. Map k a -> Set k
Map.keysSet FunMap
fm2
fma1 :: FunMap
fma1 = FunMap -> FunMap -> FunMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union FunMap
fm1 (FunMap -> FunMap) -> FunMap -> FunMap
forall a b. (a -> b) -> a -> b
\$ Set (Id, TypeScheme) -> FunMap
forall a. Ord a => Set a -> Map a a
setToMap Set (Id, TypeScheme)
uf1
fma2 :: FunMap
fma2 = FunMap -> FunMap -> FunMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union FunMap
fm2 (FunMap -> FunMap) -> FunMap -> FunMap
forall a b. (a -> b) -> a -> b
\$ Set (Id, TypeScheme) -> FunMap
forall a. Ord a => Set a -> Map a a
setToMap Set (Id, TypeScheme)
uf2
showFun :: (Id, a) -> String -> String
showFun (i :: Id
i, ty :: a
ty) = Id -> String -> String
showId Id
i (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String -> String
forall a. Pretty a => a -> String -> String
showDoc a
ty
IdMap
tma <- (Id -> Id -> Result Id) -> IdMap -> IdMap -> Result IdMap
forall a b.
(Ord a, GetRange a, Pretty a) =>
(b -> b -> Result b) -> Map a b -> Map a b -> Result (Map a b)
mergeMap ( \ t1 :: Id
t1 t2 :: Id
t2 -> if Id
t1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
t2 then Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
t1 else
String -> Result Id
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Id) -> String -> Result Id
forall a b. (a -> b) -> a -> b
\$ "incompatible type mapping to `"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
t1 "' and '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
t2 "'") IdMap
ima1 IdMap
ima2
IdMap
cma <- (Id -> Id -> Result Id) -> IdMap -> IdMap -> Result IdMap
forall a b.
(Ord a, GetRange a, Pretty a) =>
(b -> b -> Result b) -> Map a b -> Map a b -> Result (Map a b)
mergeMap ( \ t1 :: Id
t1 t2 :: Id
t2 -> if Id
t1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
t2 then Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
t1 else
String -> Result Id
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Id) -> String -> Result Id
forall a b. (a -> b) -> a -> b
\$ "incompatible class mapping to `"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
t1 "' and '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
t2 "'") IdMap
cima1 IdMap
cima2
FunMap
fma <- ((Id, TypeScheme) -> (Id, TypeScheme) -> Result (Id, TypeScheme))
-> FunMap -> FunMap -> Result FunMap
forall a b.
(Ord a, GetRange a, Pretty a) =>
(b -> b -> Result b) -> Map a b -> Map a b -> Result (Map a b)
mergeMap ( \ o1 :: (Id, TypeScheme)
o1 o2 :: (Id, TypeScheme)
o2 -> if (Id, TypeScheme)
o1 (Id, TypeScheme) -> (Id, TypeScheme) -> Bool
forall a. Eq a => a -> a -> Bool
== (Id, TypeScheme)
o2 then (Id, TypeScheme) -> Result (Id, TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id, TypeScheme)
o1 else
String -> Result (Id, TypeScheme)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Id, TypeScheme))
-> String -> Result (Id, TypeScheme)
forall a b. (a -> b) -> a -> b
\$ "incompatible mapping to '"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Id, TypeScheme) -> String -> String
forall a. Pretty a => (Id, a) -> String -> String
showFun (Id, TypeScheme)
o1 "' and '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Id, TypeScheme) -> String -> String
forall a. Pretty a => (Id, a) -> String -> String
showFun (Id, TypeScheme)
o2 "'") FunMap
fma1 FunMap
fma2
IdMap -> IdMap -> Result ()
forall a (m :: * -> *) b c.
(Ord a, Pretty a, MonadFail m) =>
Map a b -> Map a c -> m ()
disjointKeys IdMap
tma IdMap
cma
Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Env -> Morphism
mkMorphism Env
s Env
t)
{ typeIdMap :: IdMap
typeIdMap = IdMap
tma
, classIdMap :: IdMap
classIdMap = IdMap
cma
, funMap :: FunMap
funMap = FunMap
fma }

morphismToSymbMap :: Morphism -> SymbolMap
morphismToSymbMap :: Morphism -> SymbolMap
morphismToSymbMap mor :: Morphism
mor = let
src :: Env
src = Morphism -> Env
msource Morphism
mor
tar :: Env
tar = Morphism -> Env
mtarget Morphism
mor
im :: IdMap
im = Morphism -> IdMap
typeIdMap Morphism
mor
jm :: IdMap
jm = Morphism -> IdMap
classIdMap Morphism
mor
tm :: TypeMap
tm = TypeMap -> TypeMap
filterAliases (TypeMap -> TypeMap) -> TypeMap -> TypeMap
forall a b. (a -> b) -> a -> b
\$ Env -> TypeMap
typeMap Env
tar
classSymMap :: SymbolMap
classSymMap = (Id -> ClassInfo -> SymbolMap -> SymbolMap)
-> SymbolMap -> Map Id ClassInfo -> SymbolMap
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i ti :: ClassInfo
ti ->
let j :: Id
j = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i IdMap
jm
k :: RawKind
k = ClassInfo -> RawKind
rawKind ClassInfo
ti
in Symbol -> Symbol -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> RawKind -> Symbol
idToClassSymbol Id
i RawKind
k)
(Symbol -> SymbolMap -> SymbolMap)
-> Symbol -> SymbolMap -> SymbolMap
forall a b. (a -> b) -> a -> b
\$ Id -> RawKind -> Symbol
idToClassSymbol Id
j RawKind
k) SymbolMap
forall k a. Map k a
Map.empty (Map Id ClassInfo -> SymbolMap) -> Map Id ClassInfo -> SymbolMap
forall a b. (a -> b) -> a -> b
\$ Env -> Map Id ClassInfo
classMap Env
src
typeSymMap :: SymbolMap
typeSymMap = (Id -> TypeInfo -> SymbolMap -> SymbolMap)
-> SymbolMap -> TypeMap -> SymbolMap
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i ti :: TypeInfo
ti ->
let j :: Id
j = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i IdMap
im
k :: RawKind
k = TypeInfo -> RawKind
typeKind TypeInfo
ti
in Symbol -> Symbol -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> RawKind -> Symbol
idToTypeSymbol Id
i RawKind
k)
(Symbol -> SymbolMap -> SymbolMap)
-> Symbol -> SymbolMap -> SymbolMap
forall a b. (a -> b) -> a -> b
\$ Id -> RawKind -> Symbol
idToTypeSymbol Id
j RawKind
k) SymbolMap
classSymMap (TypeMap -> SymbolMap) -> TypeMap -> SymbolMap
forall a b. (a -> b) -> a -> b
\$ Env -> TypeMap
typeMap Env
src
in (Id -> Set OpInfo -> SymbolMap -> SymbolMap)
-> SymbolMap -> Map Id (Set OpInfo) -> SymbolMap
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
( \ i :: Id
i s :: Set OpInfo
s m :: SymbolMap
m ->
(OpInfo -> SymbolMap -> SymbolMap)
-> SymbolMap -> Set OpInfo -> SymbolMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ oi :: OpInfo
oi ->
let ty :: TypeScheme
ty = OpInfo -> TypeScheme
opType OpInfo
oi
(j :: Id
j, t2 :: TypeScheme
t2) = IdMap
-> TypeMap
-> IdMap
-> FunMap
-> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym IdMap
jm TypeMap
tm IdMap
im (Morphism -> FunMap
funMap Morphism
mor) (Id
i, TypeScheme
ty)
in Symbol -> Symbol -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> TypeScheme -> Symbol
idToOpSymbol Id
i TypeScheme
ty)
(Id -> TypeScheme -> Symbol
idToOpSymbol Id
j TypeScheme
t2)) SymbolMap
m Set OpInfo
s)
SymbolMap
typeSymMap (Map Id (Set OpInfo) -> SymbolMap)
-> Map Id (Set OpInfo) -> SymbolMap
forall a b. (a -> b) -> a -> b
\$ Env -> Map Id (Set OpInfo)
assumps Env
src
```