{- |
Module      :  ./HasCASL/SymbolMapAnalysis.hs
Description :  analysis of symbol mappings
Copyright   :  (c) Till Mossakowski, Christian Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

symbol map analysis for the HasCASL logic

-}
module HasCASL.SymbolMapAnalysis
    ( inducedFromMorphism
    , inducedFromToMorphism
    , cogeneratedSign
    , generatedSign
    ) where

import HasCASL.As
import HasCASL.Le
import HasCASL.PrintLe
import HasCASL.AsToLe
import HasCASL.Symbol
import HasCASL.Merge
import HasCASL.Morphism
import HasCASL.VarDecl
import HasCASL.TypeAna

import Common.DocUtils
import Common.Id
import Common.ExtSign
import Common.Result
import Common.Lib.State
import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Monad

inducedFromMorphism :: RawSymbolMap -> Env -> Result Morphism
inducedFromMorphism :: RawSymbolMap -> Env -> Result Morphism
inducedFromMorphism rmap :: RawSymbolMap
rmap sigma :: Env
sigma = do
    let srcTypeMap :: TypeMap
srcTypeMap = Env -> TypeMap
typeMap Env
sigma
        srcClassMap :: ClassMap
srcClassMap = Env -> ClassMap
classMap Env
sigma
        assMap :: Assumps
assMap = Env -> Assumps
assumps Env
sigma
    Map Id Id
myClassIdMap <- ((Id, ClassInfo) -> Result (Map Id Id) -> Result (Map Id Id))
-> Result (Map Id Id) -> [(Id, ClassInfo)] -> Result (Map Id Id)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
              (\ (s :: Id
s, ti :: ClassInfo
ti) m :: Result (Map Id Id)
m ->
               do Id
s' <- Env -> RawSymbolMap -> Id -> RawKind -> Result Id
classFun Env
sigma RawSymbolMap
rmap Id
s (ClassInfo -> RawKind
rawKind ClassInfo
ti)
                  Map Id Id
m1 <- Result (Map Id Id)
m
                  Map Id Id -> Result (Map Id Id)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Id Id -> Result (Map Id Id))
-> Map Id Id -> Result (Map Id Id)
forall a b. (a -> b) -> a -> b
$ if Id
s Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s' then Map Id Id
m1 else Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
s Id
s' Map Id Id
m1)
              (Map Id Id -> Result (Map Id Id)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Id Id
forall k a. Map k a
Map.empty) ([(Id, ClassInfo)] -> Result (Map Id Id))
-> [(Id, ClassInfo)] -> Result (Map Id Id)
forall a b. (a -> b) -> a -> b
$ ClassMap -> [(Id, ClassInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList ClassMap
srcClassMap
    ClassMap
tarClassMap0 <- (ClassMap -> (Id, ClassInfo) -> Result ClassMap)
-> ClassMap -> [(Id, ClassInfo)] -> Result ClassMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ m :: ClassMap
m (i :: Id
i, k :: ClassInfo
k) ->
       let ni :: Id
ni = Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i Map Id Id
myClassIdMap
           nk :: ClassInfo
nk = Map Id Id -> ClassInfo -> ClassInfo
mapClassInfo Map Id Id
myClassIdMap ClassInfo
k
       in case Id -> ClassMap -> Maybe ClassInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
ni ClassMap
m of
         Nothing -> ClassMap -> Result ClassMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassMap -> Result ClassMap) -> ClassMap -> Result ClassMap
forall a b. (a -> b) -> a -> b
$ Id -> ClassInfo -> ClassMap -> ClassMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
ni ClassInfo
nk ClassMap
m
         Just ok :: ClassInfo
ok -> do
           ClassInfo
mk <- ClassInfo -> ClassInfo -> Result ClassInfo
mergeClassInfo ClassInfo
ok ClassInfo
nk
           ClassMap -> Result ClassMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassMap -> Result ClassMap) -> ClassMap -> Result ClassMap
forall a b. (a -> b) -> a -> b
$ Id -> ClassInfo -> ClassMap -> ClassMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
ni ClassInfo
mk ClassMap
m)
       ClassMap
forall k a. Map k a
Map.empty ([(Id, ClassInfo)] -> Result ClassMap)
-> [(Id, ClassInfo)] -> Result ClassMap
forall a b. (a -> b) -> a -> b
$ ClassMap -> [(Id, ClassInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList ClassMap
srcClassMap
    let tarClassMap :: ClassMap
tarClassMap = ClassMap -> ClassMap
minimizeClassMap ClassMap
tarClassMap0
  -- compute the type map (as a Map)
    Map Id Id
myTypeIdMap <- ((Id, TypeInfo) -> Result (Map Id Id) -> Result (Map Id Id))
-> Result (Map Id Id) -> [(Id, TypeInfo)] -> Result (Map Id Id)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
              (\ (s :: Id
s, ti :: TypeInfo
ti) m :: Result (Map Id Id)
m ->
               do Id
s' <- Env -> RawSymbolMap -> Id -> RawKind -> Result Id
typeFun Env
sigma RawSymbolMap
rmap Id
s (TypeInfo -> RawKind
typeKind TypeInfo
ti)
                  Map Id Id
m1 <- Result (Map Id Id)
m
                  Map Id Id -> Result (Map Id Id)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Id Id -> Result (Map Id Id))
-> Map Id Id -> Result (Map Id Id)
forall a b. (a -> b) -> a -> b
$ if Id
s Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s' then Map Id Id
m1 else Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
s Id
s' Map Id Id
m1)
              (Map Id Id -> Result (Map Id Id)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Id Id
forall k a. Map k a
Map.empty) ([(Id, TypeInfo)] -> Result (Map Id Id))
-> [(Id, TypeInfo)] -> Result (Map Id Id)
forall a b. (a -> b) -> a -> b
$ TypeMap -> [(Id, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList TypeMap
srcTypeMap
    TypeMap
tarTypeMap0 <- (TypeMap -> (Id, TypeInfo) -> Result TypeMap)
-> TypeMap -> [(Id, TypeInfo)] -> Result TypeMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ m :: TypeMap
m (i :: Id
i, k :: TypeInfo
k) ->
       let ni :: Id
ni = Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i Map Id Id
myTypeIdMap
           nk :: TypeInfo
nk = Map Id Id -> Map Id Id -> TypeInfo -> TypeInfo
mapTypeInfo Map Id Id
myClassIdMap Map Id Id
myTypeIdMap TypeInfo
k
       in case Id -> TypeMap -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
ni TypeMap
m of
         Nothing -> TypeMap -> Result TypeMap
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeMap -> Result TypeMap) -> TypeMap -> Result TypeMap
forall a b. (a -> b) -> a -> b
$ Id -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
ni TypeInfo
nk TypeMap
m
         Just ok :: TypeInfo
ok -> do
           TypeInfo
mk <- ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
mergeTypeInfo ClassMap
tarClassMap TypeInfo
ok TypeInfo
nk
           TypeMap -> Result TypeMap
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeMap -> Result TypeMap) -> TypeMap -> Result TypeMap
forall a b. (a -> b) -> a -> b
$ Id -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
ni TypeInfo
mk TypeMap
m)
       TypeMap
forall k a. Map k a
Map.empty ([(Id, TypeInfo)] -> Result TypeMap)
-> [(Id, TypeInfo)] -> Result TypeMap
forall a b. (a -> b) -> a -> b
$ TypeMap -> [(Id, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList TypeMap
srcTypeMap
    let tarTypeMap :: TypeMap
tarTypeMap = ClassMap -> TypeMap -> TypeMap
addUnit (ClassMap -> ClassMap
addCpoMap ClassMap
srcClassMap) TypeMap
tarTypeMap0
        tarAliases :: TypeMap
tarAliases = TypeMap -> TypeMap
filterAliases TypeMap
tarTypeMap
  -- compute the op map (as a Map)
    FunMap
op_Map <- (Id -> Set OpInfo -> Result FunMap -> Result FunMap)
-> Result FunMap -> Assumps -> Result FunMap
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
      (RawSymbolMap
-> Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> Set OpInfo
-> Result FunMap
-> Result FunMap
opFun RawSymbolMap
rmap Env
sigma Map Id Id
myClassIdMap TypeMap
tarAliases Map Id Id
myTypeIdMap)
      (FunMap -> Result FunMap
forall (m :: * -> *) a. Monad m => a -> m a
return FunMap
forall k a. Map k a
Map.empty) Assumps
assMap
  -- compute target signature
    let tarTypeMap2 :: TypeMap
tarTypeMap2 = (TypeInfo -> TypeInfo) -> TypeMap -> TypeMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
          (Map Id Id -> TypeMap -> Map Id Id -> FunMap -> TypeInfo -> TypeInfo
mapRestTypeInfo Map Id Id
myClassIdMap TypeMap
tarAliases Map Id Id
myTypeIdMap FunMap
op_Map)
                        TypeMap
tarTypeMap
        sigma' :: Env
sigma' = (Id -> Set OpInfo -> Env -> Env) -> Env -> Assumps -> Env
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
          (Map Id Id
-> TypeMap -> Map Id Id -> FunMap -> Id -> Set OpInfo -> Env -> Env
mapOps Map Id Id
myClassIdMap TypeMap
tarAliases Map Id Id
myTypeIdMap FunMap
op_Map) Env
sigma
                   { typeMap :: TypeMap
typeMap = TypeMap
tarTypeMap2
                   , classMap :: ClassMap
classMap = ClassMap
tarClassMap
                   , assumps :: Assumps
assumps = Assumps
forall k a. Map k a
Map.empty }
                   Assumps
assMap
    TypeMap -> ClassMap -> Result ()
forall a (m :: * -> *) b c.
(Ord a, Pretty a, MonadFail m) =>
Map a b -> Map a c -> m ()
disjointKeys TypeMap
tarTypeMap2 ClassMap
tarClassMap
  -- return assembled morphism
    [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result (Env -> [Diagnosis]
envDiags Env
sigma') (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
    Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ (Env -> Env -> Morphism
mkMorphism Env
sigma (Env -> Morphism) -> Env -> Morphism
forall a b. (a -> b) -> a -> b
$ Env -> Env
cleanEnv Env
sigma')
                 { typeIdMap :: Map Id Id
typeIdMap = Map Id Id
myTypeIdMap
                 , classIdMap :: Map Id Id
classIdMap = Map Id Id
myClassIdMap
                 , funMap :: FunMap
funMap = FunMap
op_Map }

mapRestTypeInfo :: IdMap -> TypeMap -> IdMap -> FunMap -> TypeInfo -> TypeInfo
mapRestTypeInfo :: Map Id Id -> TypeMap -> Map Id Id -> FunMap -> TypeInfo -> TypeInfo
mapRestTypeInfo jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im fm :: FunMap
fm ti :: TypeInfo
ti = TypeInfo
ti
    { typeDefn :: TypeDefn
typeDefn = Map Id Id -> TypeMap -> Map Id Id -> FunMap -> TypeDefn -> TypeDefn
mapRestTypeDefn Map Id Id
jm TypeMap
tm Map Id Id
im FunMap
fm (TypeDefn -> TypeDefn) -> TypeDefn -> TypeDefn
forall a b. (a -> b) -> a -> b
$ TypeInfo -> TypeDefn
typeDefn TypeInfo
ti }

mapRestTypeDefn :: IdMap -> TypeMap -> IdMap -> FunMap -> TypeDefn -> TypeDefn
mapRestTypeDefn :: Map Id Id -> TypeMap -> Map Id Id -> FunMap -> TypeDefn -> TypeDefn
mapRestTypeDefn jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im fm :: FunMap
fm td :: TypeDefn
td = case TypeDefn
td of
    DatatypeDefn de :: DataEntry
de -> DataEntry -> TypeDefn
DatatypeDefn (DataEntry -> TypeDefn) -> DataEntry -> TypeDefn
forall a b. (a -> b) -> a -> b
$ Map Id Id
-> TypeMap -> Map Id Id -> FunMap -> DataEntry -> DataEntry
mapDataEntry Map Id Id
jm TypeMap
tm Map Id Id
im FunMap
fm DataEntry
de
    AliasTypeDefn t :: Type
t -> Type -> TypeDefn
AliasTypeDefn (Type -> TypeDefn) -> Type -> TypeDefn
forall a b. (a -> b) -> a -> b
$ Map Id Id -> TypeMap -> Map Id Id -> Type -> Type
mapTypeE Map Id Id
jm TypeMap
tm Map Id Id
im Type
t
    _ -> TypeDefn
td

mapClassInfo :: IdMap -> ClassInfo -> ClassInfo
mapClassInfo :: Map Id Id -> ClassInfo -> ClassInfo
mapClassInfo im :: Map Id Id
im ti :: ClassInfo
ti =
    ClassInfo
ti { classKinds :: Set Kind
classKinds = (Kind -> Kind) -> Set Kind -> Set Kind
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Kind -> Kind
mapKindI Map Id Id
im) (Set Kind -> Set Kind) -> Set Kind -> Set Kind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> Set Kind
classKinds ClassInfo
ti }

mapTypeInfo :: IdMap -> IdMap -> TypeInfo -> TypeInfo
mapTypeInfo :: Map Id Id -> Map Id Id -> TypeInfo -> TypeInfo
mapTypeInfo jm :: Map Id Id
jm im :: Map Id Id
im ti :: TypeInfo
ti =
    TypeInfo
ti { superTypes :: Set Id
superTypes = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ( \ i :: Id
i -> Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i Map Id Id
im)
                      (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
ti
       , otherTypeKinds :: Set Kind
otherTypeKinds = (Kind -> Kind) -> Set Kind -> Set Kind
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Kind -> Kind
mapKindI Map Id Id
jm) (Set Kind -> Set Kind) -> Set Kind -> Set Kind
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Kind
otherTypeKinds TypeInfo
ti
       , typeDefn :: TypeDefn
typeDefn = Map Id Id -> TypeDefn -> TypeDefn
mapTypeDefn Map Id Id
im (TypeDefn -> TypeDefn) -> TypeDefn -> TypeDefn
forall a b. (a -> b) -> a -> b
$ TypeInfo -> TypeDefn
typeDefn TypeInfo
ti }

mapTypeDefn :: IdMap -> TypeDefn -> TypeDefn
mapTypeDefn :: Map Id Id -> TypeDefn -> TypeDefn
mapTypeDefn im :: Map Id Id
im td :: TypeDefn
td = case TypeDefn
td of
    DatatypeDefn (DataEntry dm :: Map Id Id
dm i :: Id
i k :: GenKind
k args :: [TypeArg]
args rk :: RawKind
rk alts :: Set AltDefn
alts) ->
        DataEntry -> TypeDefn
DatatypeDefn (DataEntry -> TypeDefn) -> DataEntry -> TypeDefn
forall a b. (a -> b) -> a -> b
$ Map Id Id
-> Id
-> GenKind
-> [TypeArg]
-> RawKind
-> Set AltDefn
-> DataEntry
DataEntry
           ((Id -> Id) -> Map Id Id -> Map Id Id
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ a :: Id
a -> Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
a Id
a Map Id Id
im) Map Id Id
dm)
           Id
i GenKind
k [TypeArg]
args RawKind
rk Set AltDefn
alts
    AliasTypeDefn sc :: Type
sc -> Type -> TypeDefn
AliasTypeDefn (Type -> TypeDefn) -> Type -> TypeDefn
forall a b. (a -> b) -> a -> b
$ Map Id Id -> Type -> Type
mapType Map Id Id
im Type
sc
    _ -> TypeDefn
td

-- | compute class mapping
classFun :: Env -> RawSymbolMap -> Id -> RawKind -> Result Id
classFun :: Env -> RawSymbolMap -> Id -> RawKind -> Result Id
classFun _e :: Env
_e rmap :: RawSymbolMap
rmap s :: Id
s k :: RawKind
k = do
    let rsys :: Set RawSymbol
rsys = [Set RawSymbol] -> Set RawSymbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set RawSymbol] -> Set RawSymbol)
-> [Set RawSymbol] -> Set RawSymbol
forall a b. (a -> b) -> a -> b
$ (RawSymbol -> Set RawSymbol) -> [RawSymbol] -> [Set RawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map ( \ x :: RawSymbol
x -> case RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup RawSymbol
x RawSymbolMap
rmap of
                 Nothing -> Set RawSymbol
forall a. Set a
Set.empty
                 Just r :: RawSymbol
r -> RawSymbol -> Set RawSymbol
forall a. a -> Set a
Set.singleton RawSymbol
r)
               [Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Symbol
idToClassSymbol Id
s RawKind
k, Id -> RawSymbol
AnID Id
s, SymbKind -> Id -> RawSymbol
AKindedId SymbKind
SyKclass Id
s]
    -- rsys contains the raw symbols to which s is mapped to
    if Set RawSymbol -> Bool
forall a. Set a -> Bool
Set.null Set RawSymbol
rsys then Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
s -- use default = identity mapping
       else if Set RawSymbol -> Bool
forall a. Set a -> Bool
Set.null (Set RawSymbol -> Bool) -> Set RawSymbol -> Bool
forall a b. (a -> b) -> a -> b
$ Set RawSymbol -> Set RawSymbol
forall a. Set a -> Set a
Set.deleteMin Set RawSymbol
rsys then
            Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> Result Id) -> Id -> Result Id
forall a b. (a -> b) -> a -> b
$ RawSymbol -> Id
rawSymName (RawSymbol -> Id) -> RawSymbol -> Id
forall a b. (a -> b) -> a -> b
$ Set RawSymbol -> RawSymbol
forall a. Set a -> a
Set.findMin Set RawSymbol
rsys
            else [Diagnosis] -> Maybe Id -> Result Id
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Set RawSymbol -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error ("class: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Id
s
                       " mapped ambiguously") Set RawSymbol
rsys] Maybe Id
forall a. Maybe a
Nothing

-- | compute type mapping
typeFun :: Env -> RawSymbolMap -> Id -> RawKind -> Result Id
typeFun :: Env -> RawSymbolMap -> Id -> RawKind -> Result Id
typeFun _e :: Env
_e rmap :: RawSymbolMap
rmap s :: Id
s k :: RawKind
k = do
    let rsys :: Set RawSymbol
rsys = [Set RawSymbol] -> Set RawSymbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set RawSymbol] -> Set RawSymbol)
-> [Set RawSymbol] -> Set RawSymbol
forall a b. (a -> b) -> a -> b
$ (RawSymbol -> Set RawSymbol) -> [RawSymbol] -> [Set RawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map ( \ x :: RawSymbol
x -> case RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup RawSymbol
x RawSymbolMap
rmap of
                 Nothing -> Set RawSymbol
forall a. Set a
Set.empty
                 Just r :: RawSymbol
r -> RawSymbol -> Set RawSymbol
forall a. a -> Set a
Set.singleton RawSymbol
r)
               [Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Symbol
idToTypeSymbol Id
s RawKind
k, Id -> RawSymbol
AnID Id
s, SymbKind -> Id -> RawSymbol
AKindedId SymbKind
SyKtype Id
s]
    -- rsys contains the raw symbols to which s is mapped to
    if Set RawSymbol -> Bool
forall a. Set a -> Bool
Set.null Set RawSymbol
rsys then Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
s -- use default = identity mapping
       else if Set RawSymbol -> Bool
forall a. Set a -> Bool
Set.null (Set RawSymbol -> Bool) -> Set RawSymbol -> Bool
forall a b. (a -> b) -> a -> b
$ Set RawSymbol -> Set RawSymbol
forall a. Set a -> Set a
Set.deleteMin Set RawSymbol
rsys then
            Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> Result Id) -> Id -> Result Id
forall a b. (a -> b) -> a -> b
$ RawSymbol -> Id
rawSymName (RawSymbol -> Id) -> RawSymbol -> Id
forall a b. (a -> b) -> a -> b
$ Set RawSymbol -> RawSymbol
forall a. Set a -> a
Set.findMin Set RawSymbol
rsys
            else [Diagnosis] -> Maybe Id -> Result Id
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Set RawSymbol -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error ("type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Id
s
                       " mapped ambiguously") Set RawSymbol
rsys] Maybe Id
forall a. Maybe a
Nothing

-- | compute mapping of functions
opFun :: RawSymbolMap -> Env -> IdMap -> TypeMap -> IdMap -> Id
      -> Set.Set OpInfo -> Result FunMap -> Result FunMap
opFun :: RawSymbolMap
-> Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> Set OpInfo
-> Result FunMap
-> Result FunMap
opFun rmap :: RawSymbolMap
rmap e :: Env
e jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im i :: Id
i ots :: Set OpInfo
ots m :: Result FunMap
m =
    -- first consider all directly mapped profiles
    let (ots1 :: Set TypeScheme
ots1, m1 :: Result FunMap
m1) = (OpInfo
 -> (Set TypeScheme, Result FunMap)
 -> (Set TypeScheme, Result FunMap))
-> (Set TypeScheme, Result FunMap)
-> Set OpInfo
-> (Set TypeScheme, Result FunMap)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (RawSymbolMap
-> Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> OpInfo
-> (Set TypeScheme, Result FunMap)
-> (Set TypeScheme, Result FunMap)
directOpMap RawSymbolMap
rmap Env
e Map Id Id
jm TypeMap
tm Map Id Id
im Id
i)
                    (Set TypeScheme
forall a. Set a
Set.empty, Result FunMap
m) Set OpInfo
ots
    -- now try the remaining ones with (un)kinded raw symbol
    in case (RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SymbKind -> Id -> RawSymbol
AKindedId SymbKind
SyKop Id
i) RawSymbolMap
rmap, RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id -> RawSymbol
AnID Id
i) RawSymbolMap
rmap) of
       (Just rsy1 :: RawSymbol
rsy1, Just rsy2 :: RawSymbol
rsy2) ->
             [Diagnosis] -> Maybe FunMap -> Result FunMap
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> (RawSymbol, RawSymbol) -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error ("Operation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
i " is mapped twice")
                     (RawSymbol
rsy1, RawSymbol
rsy2)] Maybe FunMap
forall a. Maybe a
Nothing
       (Just rsy :: RawSymbol
rsy, Nothing) ->
          (TypeScheme -> Result FunMap -> Result FunMap)
-> Result FunMap -> Set TypeScheme -> Result FunMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> RawSymbol
-> TypeScheme
-> Result FunMap
-> Result FunMap
insertmapOpSym Env
e Map Id Id
jm TypeMap
tm Map Id Id
im Id
i RawSymbol
rsy) Result FunMap
m1 Set TypeScheme
ots1
       (Nothing, Just rsy :: RawSymbol
rsy) ->
          (TypeScheme -> Result FunMap -> Result FunMap)
-> Result FunMap -> Set TypeScheme -> Result FunMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> RawSymbol
-> TypeScheme
-> Result FunMap
-> Result FunMap
insertmapOpSym Env
e Map Id Id
jm TypeMap
tm Map Id Id
im Id
i RawSymbol
rsy) Result FunMap
m1 Set TypeScheme
ots1
       -- Anything not mapped explicitly is left unchanged
       (Nothing, Nothing) -> Result FunMap
m1

    {- try to map an operation symbol directly and
    collect all opTypes that cannot be mapped directly -}
directOpMap :: RawSymbolMap -> Env -> IdMap -> TypeMap -> IdMap -> Id -> OpInfo
            -> (Set.Set TypeScheme, Result FunMap)
            -> (Set.Set TypeScheme, Result FunMap)
directOpMap :: RawSymbolMap
-> Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> OpInfo
-> (Set TypeScheme, Result FunMap)
-> (Set TypeScheme, Result FunMap)
directOpMap rmap :: RawSymbolMap
rmap e :: Env
e jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im i :: Id
i oi :: OpInfo
oi (ots :: Set TypeScheme
ots, m :: Result FunMap
m) = let ot :: TypeScheme
ot = OpInfo -> TypeScheme
opType OpInfo
oi in
    case RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> TypeScheme -> Symbol
idToOpSymbol Id
i TypeScheme
ot) RawSymbolMap
rmap of
        Just rsy :: RawSymbol
rsy -> (Set TypeScheme
ots, Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> RawSymbol
-> TypeScheme
-> Result FunMap
-> Result FunMap
insertmapOpSym Env
e Map Id Id
jm TypeMap
tm Map Id Id
im Id
i RawSymbol
rsy TypeScheme
ot Result FunMap
m)
        Nothing -> (TypeScheme -> Set TypeScheme -> Set TypeScheme
forall a. Ord a => a -> Set a -> Set a
Set.insert TypeScheme
ot Set TypeScheme
ots, Result FunMap
m)

    -- map op symbol (id,ot) to raw symbol rsy
mapOpSym :: Env -> IdMap -> TypeMap -> IdMap -> Id -> TypeScheme -> RawSymbol
         -> Result (Id, TypeScheme)
mapOpSym :: Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> TypeScheme
-> RawSymbol
-> Result (Id, TypeScheme)
mapOpSym _e :: Env
_e jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im i :: Id
i ot :: TypeScheme
ot rsy :: RawSymbol
rsy =
    let sc :: TypeScheme
sc = Map Id Id -> TypeMap -> Map Id Id -> TypeScheme -> TypeScheme
mapTypeScheme Map Id Id
jm TypeMap
tm Map Id Id
im TypeScheme
ot
        err :: String -> Result a
err d :: String
d = [Diagnosis] -> Maybe a -> Result a
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> RawSymbol -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error ("Operation symbol " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                             Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (Id -> TypeScheme -> Symbol
idToOpSymbol Id
i TypeScheme
sc)
                             "\nis mapped to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d) RawSymbol
rsy] Maybe a
forall a. Maybe a
Nothing in
      case RawSymbol
rsy of
      AnID id' :: Id
id' -> (Id, TypeScheme) -> Result (Id, TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
id', TypeScheme
sc)
      AKindedId k :: SymbKind
k id' :: Id
id' -> case SymbKind
k of
          SyKop -> (Id, TypeScheme) -> Result (Id, TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
id', TypeScheme
sc)
          _ -> String -> Result (Id, TypeScheme)
forall a. String -> Result a
err "wrongly kinded raw symbol"
      ASymbol sy :: Symbol
sy -> case Symbol -> SymbolType
symType Symbol
sy of
          OpAsItemType ot2 :: TypeScheme
ot2
            | TypeScheme
ot2 TypeScheme -> TypeScheme -> Bool
forall a. Eq a => a -> a -> Bool
== TypeScheme
sc -> (Id, TypeScheme) -> Result (Id, TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
j, TypeScheme
sc)
            | String
ots String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
scs -> (Id, TypeScheme) -> String -> Range -> Result (Id, TypeScheme)
forall a. a -> String -> Range -> Result a
hint (Id
j, TypeScheme
sc) String
msg Range
rgn
            | Bool
otherwise ->
                (Id, TypeScheme) -> String -> Range -> Result (Id, TypeScheme)
forall a. a -> String -> Range -> Result a
warning (Id
j, TypeScheme
sc) (String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nversus: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ots) Range
rgn
            where
              j :: Id
j = Symbol -> Id
symName Symbol
sy
              ots :: String
ots = TypeScheme -> String -> String
forall a. Pretty a => a -> String -> String
showDoc TypeScheme
ot2 ""
              scs :: String
scs = TypeScheme -> String -> String
forall a. Pretty a => a -> String -> String
showDoc TypeScheme
sc ""
              msg :: String
msg = "ignoring different target symbol type for '"
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Symbol
sy "'"
              rgn :: Range
rgn = TypeScheme -> Range
forall a. GetRange a => a -> Range
getRange TypeScheme
ot2
          _ -> String -> Result (Id, TypeScheme)
forall a. String -> Result a
err "wrongly kinded symbol"

    -- insert mapping of op symbol (id, ot) to raw symbol rsy into m
insertmapOpSym :: Env -> IdMap -> TypeMap -> IdMap -> Id -> RawSymbol
               -> TypeScheme -> Result FunMap -> Result FunMap
insertmapOpSym :: Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> RawSymbol
-> TypeScheme
-> Result FunMap
-> Result FunMap
insertmapOpSym e :: Env
e jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im i :: Id
i rsy :: RawSymbol
rsy ot :: TypeScheme
ot m :: Result FunMap
m = do
      FunMap
m1 <- Result FunMap
m
      (Id, TypeScheme)
q <- Env
-> Map Id Id
-> TypeMap
-> Map Id Id
-> Id
-> TypeScheme
-> RawSymbol
-> Result (Id, TypeScheme)
mapOpSym Env
e Map Id Id
jm TypeMap
tm Map Id Id
im Id
i TypeScheme
ot RawSymbol
rsy
      let p :: (Id, TypeScheme)
p = (Id
i, Map Id Id -> TypeMap -> Map Id Id -> TypeScheme -> TypeScheme
mapTypeScheme Map Id Id
jm TypeMap
tm Map Id Id
im TypeScheme
ot)
      FunMap -> Result FunMap
forall (m :: * -> *) a. Monad m => a -> m a
return (FunMap -> Result FunMap) -> FunMap -> Result FunMap
forall a b. (a -> b) -> a -> b
$ if (Id, TypeScheme)
p (Id, TypeScheme) -> (Id, TypeScheme) -> Bool
forall a. Eq a => a -> a -> Bool
== (Id, TypeScheme)
q then FunMap
m1 else (Id, TypeScheme) -> (Id, TypeScheme) -> FunMap -> FunMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id
i, TypeScheme
ot) (Id, TypeScheme)
q FunMap
m1
    -- insert mapping of op symbol (i, ot) into m

  -- map the ops in the source signature
mapOps :: IdMap -> TypeMap -> IdMap -> FunMap -> Id -> Set.Set OpInfo -> Env
       -> Env
mapOps :: Map Id Id
-> TypeMap -> Map Id Id -> FunMap -> Id -> Set OpInfo -> Env -> Env
mapOps jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im fm :: FunMap
fm i :: Id
i ots :: Set OpInfo
ots e :: Env
e =
    (OpInfo -> Env -> Env) -> Env -> Set OpInfo -> Env
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ ot :: OpInfo
ot e' :: Env
e' ->
        let osc :: TypeScheme
osc = OpInfo -> TypeScheme
opType OpInfo
ot
            sc :: TypeScheme
sc = Map Id Id -> TypeMap -> Map Id Id -> TypeScheme -> TypeScheme
mapTypeScheme Map Id Id
jm TypeMap
tm Map Id Id
im TypeScheme
osc
            (id' :: Id
id', sc' :: TypeScheme
sc') = (Id, TypeScheme) -> (Id, TypeScheme) -> FunMap -> (Id, TypeScheme)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Id
i, TypeScheme
sc)
                         (Id
i, TypeScheme
osc) FunMap
fm
            in State Env Bool -> Env -> Env
forall s a. State s a -> s -> s
execState (Id -> TypeScheme -> Set OpAttr -> OpDefn -> State Env Bool
addOpId Id
id' TypeScheme
sc' ((OpAttr -> OpAttr) -> Set OpAttr -> Set OpAttr
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> TypeMap -> Map Id Id -> FunMap -> OpAttr -> OpAttr
mapOpAttr Map Id Id
jm TypeMap
tm Map Id Id
im FunMap
fm)
                                          (Set OpAttr -> Set OpAttr) -> Set OpAttr -> Set OpAttr
forall a b. (a -> b) -> a -> b
$ OpInfo -> Set OpAttr
opAttrs OpInfo
ot)
                          (Map Id Id -> TypeMap -> Map Id Id -> FunMap -> OpDefn -> OpDefn
mapOpDefn Map Id Id
jm TypeMap
tm Map Id Id
im FunMap
fm (OpDefn -> OpDefn) -> OpDefn -> OpDefn
forall a b. (a -> b) -> a -> b
$ OpInfo -> OpDefn
opDefn OpInfo
ot)) Env
e')
    Env
e Set OpInfo
ots

mapOpAttr :: IdMap -> TypeMap -> IdMap -> FunMap -> OpAttr -> OpAttr
mapOpAttr :: Map Id Id -> TypeMap -> Map Id Id -> FunMap -> OpAttr -> OpAttr
mapOpAttr jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im fm :: FunMap
fm oa :: OpAttr
oa = case OpAttr
oa of
    UnitOpAttr t :: Term
t ps :: Range
ps -> Term -> Range -> OpAttr
UnitOpAttr (Map Id Id -> TypeMap -> Map Id Id -> FunMap -> Term -> Term
mapSen Map Id Id
jm TypeMap
tm Map Id Id
im FunMap
fm Term
t) Range
ps
    _ -> OpAttr
oa

mapOpDefn :: IdMap -> TypeMap -> IdMap -> FunMap -> OpDefn -> OpDefn
mapOpDefn :: Map Id Id -> TypeMap -> Map Id Id -> FunMap -> OpDefn -> OpDefn
mapOpDefn jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im fm :: FunMap
fm d :: OpDefn
d = case OpDefn
d of
   ConstructData i :: Id
i -> Id -> OpDefn
ConstructData (Id -> OpDefn) -> Id -> OpDefn
forall a b. (a -> b) -> a -> b
$ Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i Map Id Id
im
   SelectData cs :: Set ConstrInfo
cs i :: Id
i -> Set ConstrInfo -> Id -> OpDefn
SelectData ((ConstrInfo -> ConstrInfo) -> Set ConstrInfo -> Set ConstrInfo
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id
-> TypeMap -> Map Id Id -> FunMap -> ConstrInfo -> ConstrInfo
mapConstrInfo Map Id Id
jm TypeMap
tm Map Id Id
im FunMap
fm) Set ConstrInfo
cs)
                      (Id -> OpDefn) -> Id -> OpDefn
forall a b. (a -> b) -> a -> b
$ Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i Map Id Id
im
   Definition b :: OpBrand
b t :: Term
t -> OpBrand -> Term -> OpDefn
Definition OpBrand
b (Term -> OpDefn) -> Term -> OpDefn
forall a b. (a -> b) -> a -> b
$ Map Id Id -> TypeMap -> Map Id Id -> FunMap -> Term -> Term
mapSen Map Id Id
jm TypeMap
tm Map Id Id
im FunMap
fm Term
t
   _ -> OpDefn
d

mapConstrInfo :: IdMap -> TypeMap -> IdMap -> FunMap -> ConstrInfo
              -> ConstrInfo
mapConstrInfo :: Map Id Id
-> TypeMap -> Map Id Id -> FunMap -> ConstrInfo -> ConstrInfo
mapConstrInfo jm :: Map Id Id
jm tm :: TypeMap
tm im :: Map Id Id
im fm :: FunMap
fm (ConstrInfo i :: Id
i sc :: TypeScheme
sc) =
    let (j :: Id
j, nSc :: TypeScheme
nSc) = Map Id Id
-> TypeMap
-> Map Id Id
-> FunMap
-> (Id, TypeScheme)
-> (Id, TypeScheme)
mapFunSym Map Id Id
jm TypeMap
tm Map Id Id
im FunMap
fm (Id
i, TypeScheme
sc) in Id -> TypeScheme -> ConstrInfo
ConstrInfo Id
j TypeScheme
nSc

-- | basically test if the renamed source signature is in the target signature
inducedFromToMorphism :: RawSymbolMap -> ExtSign Env Symbol
                      -> ExtSign Env Symbol -> Result Morphism
inducedFromToMorphism :: RawSymbolMap
-> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism
inducedFromToMorphism rmap1 :: RawSymbolMap
rmap1 e1 :: ExtSign Env Symbol
e1@(ExtSign sigma1 :: Env
sigma1 sy1 :: Set Symbol
sy1) (ExtSign sigma2 :: Env
sigma2 sy2 :: Set Symbol
sy2) = do
  Morphism
mor1 <- RawSymbolMap -> Env -> Result Morphism
inducedFromMorphism RawSymbolMap
rmap1 Env
sigma1
  if Env -> Env -> Bool
isSubEnv (Morphism -> Env
mtarget Morphism
mor1) Env
sigma2
    -- yes => we are done
    then Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism
mor1 { mtarget :: Env
mtarget = Env
sigma2 }
    -- no => OK, we've to take a harder way
    else do
        let ft :: Set Symbol -> Set Symbol
ft = (Symbol -> Bool) -> Set Symbol -> Set Symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ( \ (Symbol _ t :: SymbolType
t) -> case SymbolType
t of
                        TypeAsItemType _ -> Bool
True
                        _ -> Bool
False)
            s1 :: Set Symbol
s1 = Set Symbol -> Set Symbol
ft Set Symbol
sy1
            s2 :: Set Symbol
s2 = Set Symbol -> Set Symbol
ft Set Symbol
sy2
            err :: Morphism -> Result a
err mor :: Morphism
mor = [Diagnosis] -> Maybe a -> Result a
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error ("No symbol mapping found for:\n"
                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String -> String
forall a. Show a => a -> String -> String
shows (RawSymbolMap -> Doc
forall a b. (Pretty a, Ord a, Pretty b) => Map a b -> Doc
printMap1 RawSymbolMap
rmap1) "\nOriginal Signature 1:\n"
                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ExtSign Env Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ExtSign Env Symbol
e1 "\nInduced "
                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ Env -> Env -> String
showEnvDiff (Morphism -> Env
mtarget Morphism
mor) Env
sigma2
                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nMor fun-Map\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String -> String
forall a. Show a => a -> String -> String
shows (FunMap -> Doc
forall a b. (Pretty a, Ord a, Pretty b) => Map a b -> Doc
printMap1 (FunMap -> Doc) -> FunMap -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> FunMap
funMap Morphism
mor) "\n"
                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\ndeclared Symbols of Signature 2:\n"
                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set Symbol
sy2 "") Range
nullRange] Maybe a
forall a. Maybe a
Nothing
        if Set Symbol -> Int
forall a. Set a -> Int
Set.size Set Symbol
s1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Bool -> Bool -> Bool
&& Set Symbol -> Int
forall a. Set a -> Int
Set.size Set Symbol
s2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then do
          let Symbol n1 :: Id
n1 _ = Set Symbol -> Symbol
forall a. Set a -> a
Set.findMin Set Symbol
s1
              Symbol n2 :: Id
n2 _ = Set Symbol -> Symbol
forall a. Set a -> a
Set.findMin Set Symbol
s2
          Morphism
mor2 <- RawSymbolMap -> Env -> Result Morphism
inducedFromMorphism (RawSymbol -> RawSymbol -> RawSymbolMap -> RawSymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SymbKind -> Id -> RawSymbol
AKindedId SymbKind
SyKtype Id
n1)
                                       (SymbKind -> Id -> RawSymbol
AKindedId SymbKind
SyKtype Id
n2) RawSymbolMap
rmap1) Env
sigma1
          if Env -> Env -> Bool
isSubEnv (Morphism -> Env
mtarget Morphism
mor2) Env
sigma2
            then Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism
mor2 { mtarget :: Env
mtarget = Env
sigma2 }
            else Morphism -> Result Morphism
forall a. Morphism -> Result a
err Morphism
mor2
          else Morphism -> Result Morphism
forall a. Morphism -> Result a
err Morphism
mor1

-- | reveal the symbols in the set
generatedSign :: SymbolSet -> Env -> Result Morphism
generatedSign :: Set Symbol -> Env -> Result Morphism
generatedSign syms :: Set Symbol
syms sigma :: Env
sigma =
    let signSyms :: Set Symbol
signSyms = [Set Symbol] -> Set Symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Symbol] -> Set Symbol) -> [Set Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Env -> [Set Symbol]
symOf Env
sigma
        closedSyms :: Set Symbol
closedSyms = Set Symbol -> Set Symbol
closeSymbSet Set Symbol
syms
        subSigma :: Env
subSigma = Set Symbol -> Env -> Env
plainHide (Set Symbol
signSyms Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Symbol
closedSyms) Env
sigma
    in Set Symbol -> Set Symbol -> Result Morphism -> Result Morphism
forall a. Set Symbol -> Set Symbol -> Result a -> Result a
checkSymbols Set Symbol
closedSyms Set Symbol
signSyms (Result Morphism -> Result Morphism)
-> Result Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$
       Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Env -> Env -> Morphism
mkMorphism Env
subSigma Env
sigma

-- | hide the symbols in the set
cogeneratedSign :: SymbolSet -> Env -> Result Morphism
cogeneratedSign :: Set Symbol -> Env -> Result Morphism
cogeneratedSign syms :: Set Symbol
syms sigma :: Env
sigma =
    let signSyms :: Set Symbol
signSyms = [Set Symbol] -> Set Symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Symbol] -> Set Symbol) -> [Set Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Env -> [Set Symbol]
symOf Env
sigma
        subSigma :: Env
subSigma = (Symbol -> Env -> Env) -> Env -> Set Symbol -> Env
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Symbol -> Env -> Env
hideRelSymbol Env
sigma Set Symbol
syms
        in Set Symbol -> Set Symbol -> Result Morphism -> Result Morphism
forall a. Set Symbol -> Set Symbol -> Result a -> Result a
checkSymbols Set Symbol
syms Set Symbol
signSyms (Result Morphism -> Result Morphism)
-> Result Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$
           Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Env -> Env -> Morphism
mkMorphism Env
subSigma Env
sigma