{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./OWL2/Morphism.hs
Description :  OWL Morphisms
Copyright   :  (c) Dominik Luecke, 2008, Felix Gabriel Mance, 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  f.mance@jacobs-university.de
Stability   :  provisional
Portability :  portable

Morphisms for OWL
-}

module OWL2.Morphism where

import Common.IRI
import OWL2.AS
import OWL2.Sign
import OWL2.ManchesterPrint ()
import OWL2.Symbols
import OWL2.Function

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

import Control.Monad

import Data.Data
import Data.List (stripPrefix)
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Control.Monad.Fail as Fail

data OWLMorphism = OWLMorphism
  { OWLMorphism -> Sign
osource :: Sign
  , OWLMorphism -> Sign
otarget :: Sign
  , OWLMorphism -> MorphMap
mmaps :: MorphMap
  , OWLMorphism -> StringMap
pmap :: StringMap
  } deriving (Int -> OWLMorphism -> ShowS
[OWLMorphism] -> ShowS
OWLMorphism -> String
(Int -> OWLMorphism -> ShowS)
-> (OWLMorphism -> String)
-> ([OWLMorphism] -> ShowS)
-> Show OWLMorphism
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OWLMorphism] -> ShowS
$cshowList :: [OWLMorphism] -> ShowS
show :: OWLMorphism -> String
$cshow :: OWLMorphism -> String
showsPrec :: Int -> OWLMorphism -> ShowS
$cshowsPrec :: Int -> OWLMorphism -> ShowS
Show, OWLMorphism -> OWLMorphism -> Bool
(OWLMorphism -> OWLMorphism -> Bool)
-> (OWLMorphism -> OWLMorphism -> Bool) -> Eq OWLMorphism
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OWLMorphism -> OWLMorphism -> Bool
$c/= :: OWLMorphism -> OWLMorphism -> Bool
== :: OWLMorphism -> OWLMorphism -> Bool
$c== :: OWLMorphism -> OWLMorphism -> Bool
Eq, Eq OWLMorphism
Eq OWLMorphism =>
(OWLMorphism -> OWLMorphism -> Ordering)
-> (OWLMorphism -> OWLMorphism -> Bool)
-> (OWLMorphism -> OWLMorphism -> Bool)
-> (OWLMorphism -> OWLMorphism -> Bool)
-> (OWLMorphism -> OWLMorphism -> Bool)
-> (OWLMorphism -> OWLMorphism -> OWLMorphism)
-> (OWLMorphism -> OWLMorphism -> OWLMorphism)
-> Ord OWLMorphism
OWLMorphism -> OWLMorphism -> Bool
OWLMorphism -> OWLMorphism -> Ordering
OWLMorphism -> OWLMorphism -> OWLMorphism
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OWLMorphism -> OWLMorphism -> OWLMorphism
$cmin :: OWLMorphism -> OWLMorphism -> OWLMorphism
max :: OWLMorphism -> OWLMorphism -> OWLMorphism
$cmax :: OWLMorphism -> OWLMorphism -> OWLMorphism
>= :: OWLMorphism -> OWLMorphism -> Bool
$c>= :: OWLMorphism -> OWLMorphism -> Bool
> :: OWLMorphism -> OWLMorphism -> Bool
$c> :: OWLMorphism -> OWLMorphism -> Bool
<= :: OWLMorphism -> OWLMorphism -> Bool
$c<= :: OWLMorphism -> OWLMorphism -> Bool
< :: OWLMorphism -> OWLMorphism -> Bool
$c< :: OWLMorphism -> OWLMorphism -> Bool
compare :: OWLMorphism -> OWLMorphism -> Ordering
$ccompare :: OWLMorphism -> OWLMorphism -> Ordering
$cp1Ord :: Eq OWLMorphism
Ord, Typeable, Typeable OWLMorphism
Constr
DataType
Typeable OWLMorphism =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> OWLMorphism -> c OWLMorphism)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OWLMorphism)
-> (OWLMorphism -> Constr)
-> (OWLMorphism -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OWLMorphism))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c OWLMorphism))
-> ((forall b. Data b => b -> b) -> OWLMorphism -> OWLMorphism)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OWLMorphism -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OWLMorphism -> r)
-> (forall u. (forall d. Data d => d -> u) -> OWLMorphism -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> OWLMorphism -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism)
-> Data OWLMorphism
OWLMorphism -> Constr
OWLMorphism -> DataType
(forall b. Data b => b -> b) -> OWLMorphism -> OWLMorphism
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OWLMorphism -> c OWLMorphism
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OWLMorphism
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> OWLMorphism -> u
forall u. (forall d. Data d => d -> u) -> OWLMorphism -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OWLMorphism -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OWLMorphism -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OWLMorphism
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OWLMorphism -> c OWLMorphism
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OWLMorphism)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OWLMorphism)
$cOWLMorphism :: Constr
$tOWLMorphism :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism
gmapMp :: (forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism
gmapM :: (forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OWLMorphism -> m OWLMorphism
gmapQi :: Int -> (forall d. Data d => d -> u) -> OWLMorphism -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> OWLMorphism -> u
gmapQ :: (forall d. Data d => d -> u) -> OWLMorphism -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OWLMorphism -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OWLMorphism -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OWLMorphism -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OWLMorphism -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OWLMorphism -> r
gmapT :: (forall b. Data b => b -> b) -> OWLMorphism -> OWLMorphism
$cgmapT :: (forall b. Data b => b -> b) -> OWLMorphism -> OWLMorphism
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OWLMorphism)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OWLMorphism)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c OWLMorphism)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OWLMorphism)
dataTypeOf :: OWLMorphism -> DataType
$cdataTypeOf :: OWLMorphism -> DataType
toConstr :: OWLMorphism -> Constr
$ctoConstr :: OWLMorphism -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OWLMorphism
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OWLMorphism
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OWLMorphism -> c OWLMorphism
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OWLMorphism -> c OWLMorphism
$cp1Data :: Typeable OWLMorphism
Data)

inclOWLMorphism :: Sign -> Sign -> OWLMorphism
inclOWLMorphism :: Sign -> Sign -> OWLMorphism
inclOWLMorphism s :: Sign
s t :: Sign
t = OWLMorphism :: Sign -> Sign -> MorphMap -> StringMap -> OWLMorphism
OWLMorphism
 { osource :: Sign
osource = Sign
s
 , otarget :: Sign
otarget = Sign
t
 , pmap :: StringMap
pmap = StringMap
forall k a. Map k a
Map.empty
 , mmaps :: MorphMap
mmaps = MorphMap
forall k a. Map k a
Map.empty }

isOWLInclusion :: OWLMorphism -> Bool
isOWLInclusion :: OWLMorphism -> Bool
isOWLInclusion m :: OWLMorphism
m = StringMap -> Bool
forall k a. Map k a -> Bool
Map.null (OWLMorphism -> StringMap
pmap OWLMorphism
m)
  Bool -> Bool -> Bool
&& MorphMap -> Bool
forall k a. Map k a -> Bool
Map.null (OWLMorphism -> MorphMap
mmaps OWLMorphism
m) Bool -> Bool -> Bool
&& Sign -> Sign -> Bool
isSubSign (OWLMorphism -> Sign
osource OWLMorphism
m) (OWLMorphism -> Sign
otarget OWLMorphism
m)

symMap :: MorphMap -> Map.Map Entity Entity
symMap :: MorphMap -> Map Entity Entity
symMap = (Entity -> IRI -> Entity) -> MorphMap -> Map Entity Entity
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\ (Entity lb :: Maybe String
lb ty :: EntityType
ty _) -> Maybe String -> EntityType -> IRI -> Entity
Entity Maybe String
lb EntityType
ty)

inducedElems :: MorphMap -> [Entity]
inducedElems :: MorphMap -> [Entity]
inducedElems = Map Entity Entity -> [Entity]
forall k a. Map k a -> [a]
Map.elems (Map Entity Entity -> [Entity])
-> (MorphMap -> Map Entity Entity) -> MorphMap -> [Entity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MorphMap -> Map Entity Entity
symMap

inducedSign :: MorphMap -> StringMap -> Sign -> Sign
inducedSign :: MorphMap -> StringMap -> Sign -> Sign
inducedSign m :: MorphMap
m t :: StringMap
t s :: Sign
s =
    let new :: Sign
new = State Sign () -> Sign -> Sign
forall s a. State s a -> s -> s
execState (do
            (Entity -> State Sign ()) -> [Entity] -> State Sign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((IRI -> Set IRI -> Set IRI) -> Entity -> State Sign ()
modEntity IRI -> Set IRI -> Set IRI
forall a. Ord a => a -> Set a -> Set a
Set.delete) ([Entity] -> State Sign ()) -> [Entity] -> State Sign ()
forall a b. (a -> b) -> a -> b
$ MorphMap -> [Entity]
forall k a. Map k a -> [k]
Map.keys MorphMap
m
            (Entity -> State Sign ()) -> [Entity] -> State Sign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((IRI -> Set IRI -> Set IRI) -> Entity -> State Sign ()
modEntity IRI -> Set IRI -> Set IRI
forall a. Ord a => a -> Set a -> Set a
Set.insert) ([Entity] -> State Sign ()) -> [Entity] -> State Sign ()
forall a b. (a -> b) -> a -> b
$ MorphMap -> [Entity]
inducedElems MorphMap
m) Sign
s
    in Action -> AMap -> Sign -> Sign
forall a. Function a => Action -> AMap -> a -> a
function Action
Rename (StringMap -> AMap
StringMap StringMap
t) Sign
new

inducedPref :: String -> String -> Sign -> (MorphMap, StringMap)
    -> Result (MorphMap, StringMap)
inducedPref :: String
-> String
-> Sign
-> (MorphMap, StringMap)
-> Result (MorphMap, StringMap)
inducedPref v :: String
v u :: String
u sig :: Sign
sig (m :: MorphMap
m, t :: StringMap
t) =
    let pm :: StringMap
pm = Sign -> StringMap
prefixMap Sign
sig
    in if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
v (Set String -> Bool) -> Set String -> Bool
forall a b. (a -> b) -> a -> b
$ StringMap -> Set String
forall k a. Map k a -> Set k
Map.keysSet StringMap
pm
         then if String
u String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v then (MorphMap, StringMap) -> Result (MorphMap, StringMap)
forall (m :: * -> *) a. Monad m => a -> m a
return (MorphMap
m, StringMap
t) else (MorphMap, StringMap) -> Result (MorphMap, StringMap)
forall (m :: * -> *) a. Monad m => a -> m a
return (MorphMap
m, String -> String -> StringMap -> StringMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
v String
u StringMap
t)
        else
          (MorphMap, StringMap)
-> String -> Range -> Result (MorphMap, StringMap)
forall a. a -> String -> Range -> Result a
plain_error (MorphMap
forall k a. Map k a
Map.empty, StringMap
forall k a. Map k a
Map.empty) ("unknown symbol: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS
forall a. Pretty a => a -> ShowS
showDoc String
v "\nin signature:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sign -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Sign
sig "") Range
nullRange

 
inducedFromMor :: Map.Map RawSymb RawSymb -> Sign -> Result OWLMorphism
inducedFromMor :: Map RawSymb RawSymb -> Sign -> Result OWLMorphism
inducedFromMor rm :: Map RawSymb RawSymb
rm sig :: Sign
sig = do
  let syms :: Set Entity
syms = Sign -> Set Entity
symOf Sign
sig
  (mm :: MorphMap
mm, tm :: StringMap
tm) <- ((MorphMap, StringMap)
 -> (RawSymb, RawSymb) -> Result (MorphMap, StringMap))
-> (MorphMap, StringMap)
-> [(RawSymb, RawSymb)]
-> Result (MorphMap, StringMap)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (m :: MorphMap
m, t :: StringMap
t) p :: (RawSymb, RawSymb)
p -> case (RawSymb, RawSymb)
p of
        (ASymbol s :: Entity
s@(Entity _ _ v :: IRI
v), ASymbol (Entity _ _ u :: IRI
u)) ->
            if Entity -> Set Entity -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Entity
s Set Entity
syms
            then (MorphMap, StringMap) -> Result (MorphMap, StringMap)
forall (m :: * -> *) a. Monad m => a -> m a
return ((MorphMap, StringMap) -> Result (MorphMap, StringMap))
-> (MorphMap, StringMap) -> Result (MorphMap, StringMap)
forall a b. (a -> b) -> a -> b
$ if IRI
u IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
v then (MorphMap
m, StringMap
t) else (Entity -> IRI -> MorphMap -> MorphMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Entity
s IRI
u MorphMap
m, StringMap
t)
            else String -> Result (MorphMap, StringMap)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (MorphMap, StringMap))
-> String -> Result (MorphMap, StringMap)
forall a b. (a -> b) -> a -> b
$ "unknown symbol: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Entity -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Entity
s "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sign -> ShowS
forall a. Show a => a -> ShowS
shows Sign
sig ""
        (AnUri v :: IRI
v, AnUri u :: IRI
u) -> case (Entity -> Bool) -> [Entity] -> [Entity]
forall a. (a -> Bool) -> [a] -> [a]
filter (Entity -> Set Entity -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Entity
syms)
          ([Entity] -> [Entity]) -> [Entity] -> [Entity]
forall a b. (a -> b) -> a -> b
$ (EntityType -> Entity) -> [EntityType] -> [Entity]
forall a b. (a -> b) -> [a] -> [b]
map (EntityType -> IRI -> Entity
`mkEntity` IRI
v) [EntityType]
entityTypes of
          [] -> let v2 :: String
v2 = IRI -> String
showIRICompact IRI
v
                    u2 :: String
u2 = IRI -> String
showIRICompact IRI
u
                in String
-> String
-> Sign
-> (MorphMap, StringMap)
-> Result (MorphMap, StringMap)
inducedPref String
v2 String
u2 Sign
sig (MorphMap
m, StringMap
t)
          l :: [Entity]
l -> (MorphMap, StringMap) -> Result (MorphMap, StringMap)
forall (m :: * -> *) a. Monad m => a -> m a
return ((MorphMap, StringMap) -> Result (MorphMap, StringMap))
-> (MorphMap, StringMap) -> Result (MorphMap, StringMap)
forall a b. (a -> b) -> a -> b
$ if IRI
u IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
v then (MorphMap
m, StringMap
t) else
                            ((Entity -> MorphMap -> MorphMap)
-> MorphMap -> [Entity] -> MorphMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Entity -> IRI -> MorphMap -> MorphMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
`Map.insert` IRI
u) MorphMap
m [Entity]
l, StringMap
t)
        (APrefix v :: String
v, APrefix u :: String
u) -> String
-> String
-> Sign
-> (MorphMap, StringMap)
-> Result (MorphMap, StringMap)
inducedPref String
v String
u Sign
sig (MorphMap
m, StringMap
t)
        _ -> String -> Result (MorphMap, StringMap)
forall a. HasCallStack => String -> a
error "OWL2.Morphism.inducedFromMor") (MorphMap
forall k a. Map k a
Map.empty, StringMap
forall k a. Map k a
Map.empty)
                        ([(RawSymb, RawSymb)] -> Result (MorphMap, StringMap))
-> [(RawSymb, RawSymb)] -> Result (MorphMap, StringMap)
forall a b. (a -> b) -> a -> b
$ Map RawSymb RawSymb -> [(RawSymb, RawSymb)]
forall k a. Map k a -> [(k, a)]
Map.toList Map RawSymb RawSymb
rm
  OWLMorphism -> Result OWLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return OWLMorphism :: Sign -> Sign -> MorphMap -> StringMap -> OWLMorphism
OWLMorphism 
    { osource :: Sign
osource = Sign
sig
    , otarget :: Sign
otarget = MorphMap -> StringMap -> Sign -> Sign
inducedSign MorphMap
mm StringMap
tm Sign
sig
    , pmap :: StringMap
pmap = StringMap
tm
    , mmaps :: MorphMap
mmaps = MorphMap
mm }

symMapOf :: OWLMorphism -> Map.Map Entity Entity
symMapOf :: OWLMorphism -> Map Entity Entity
symMapOf mor :: OWLMorphism
mor = Map Entity Entity -> Map Entity Entity -> Map Entity Entity
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (MorphMap -> Map Entity Entity
symMap (MorphMap -> Map Entity Entity) -> MorphMap -> Map Entity Entity
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> MorphMap
mmaps OWLMorphism
mor) (Map Entity Entity -> Map Entity Entity)
-> Map Entity Entity -> Map Entity Entity
forall a b. (a -> b) -> a -> b
$ Set Entity -> Map Entity Entity
forall a. Ord a => Set a -> Map a a
setToMap (Set Entity -> Map Entity Entity)
-> Set Entity -> Map Entity Entity
forall a b. (a -> b) -> a -> b
$ Sign -> Set Entity
symOf (Sign -> Set Entity) -> Sign -> Set Entity
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
mor

instance Pretty OWLMorphism where
  pretty :: OWLMorphism -> Doc
pretty m :: OWLMorphism
m = let
    s :: Sign
s = OWLMorphism -> Sign
osource OWLMorphism
m
    srcD :: Doc
srcD = Doc -> Doc
specBraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Sign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign
s
    t :: Sign
t = OWLMorphism -> Sign
otarget OWLMorphism
m
    in [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ if OWLMorphism -> Bool
isOWLInclusion OWLMorphism
m then
           if Sign -> Sign -> Bool
isSubSign Sign
t Sign
s then
              [String -> Doc
text "identity morphism over", Doc
srcD]
           else
             [ String -> Doc
text "inclusion morphism of"
             , Doc
srcD
             , String -> Doc
text "extended with"
             , Set Entity -> Doc
forall a. Pretty a => a -> Doc
pretty (Set Entity -> Doc) -> Set Entity -> Doc
forall a b. (a -> b) -> a -> b
$ Set Entity -> Set Entity -> Set Entity
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Entity
symOf Sign
t) (Set Entity -> Set Entity) -> Set Entity -> Set Entity
forall a b. (a -> b) -> a -> b
$ Sign -> Set Entity
symOf Sign
s ]
       else
         [ MorphMap -> Doc
forall a. Pretty a => a -> Doc
pretty (MorphMap -> Doc) -> MorphMap -> Doc
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> MorphMap
mmaps OWLMorphism
m
         , StringMap -> Doc
forall a. Pretty a => a -> Doc
pretty (StringMap -> Doc) -> StringMap -> Doc
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> StringMap
pmap OWLMorphism
m
         , Doc
colon Doc -> Doc -> Doc
<+> Doc
srcD, Doc
mapsto Doc -> Doc -> Doc
<+> Doc -> Doc
specBraces (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Sign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign
t) ]

legalMor :: OWLMorphism -> Result ()
legalMor :: OWLMorphism -> Result ()
legalMor m :: OWLMorphism
m = let mm :: MorphMap
mm = OWLMorphism -> MorphMap
mmaps OWLMorphism
m in Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
  (Set Entity -> Set Entity -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (MorphMap -> Set Entity
forall k a. Map k a -> Set k
Map.keysSet MorphMap
mm) (Sign -> Set Entity
symOf (Sign -> Set Entity) -> Sign -> Set Entity
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
m)
  Bool -> Bool -> Bool
&& Set Entity -> Set Entity -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf ([Entity] -> Set Entity
forall a. Ord a => [a] -> Set a
Set.fromList ([Entity] -> Set Entity) -> [Entity] -> Set Entity
forall a b. (a -> b) -> a -> b
$ MorphMap -> [Entity]
inducedElems MorphMap
mm) (Sign -> Set Entity
symOf (Sign -> Set Entity) -> Sign -> Set Entity
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
otarget OWLMorphism
m))
        (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal OWL2 morphism"

composeMor :: OWLMorphism -> OWLMorphism -> Result OWLMorphism
composeMor :: OWLMorphism -> OWLMorphism -> Result OWLMorphism
composeMor m1 :: OWLMorphism
m1 m2 :: OWLMorphism
m2 =
  let nm :: MorphMap
nm = (Entity -> MorphMap -> MorphMap)
-> MorphMap -> Set Entity -> MorphMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ s :: Entity
s@(Entity _ ty :: EntityType
ty u :: IRI
u) -> let
            t :: IRI
t = EntityType -> IRI -> MorphMap -> IRI
getIri EntityType
ty IRI
u (MorphMap -> IRI) -> MorphMap -> IRI
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> MorphMap
mmaps OWLMorphism
m1
            r :: IRI
r = EntityType -> IRI -> MorphMap -> IRI
getIri EntityType
ty IRI
t (MorphMap -> IRI) -> MorphMap -> IRI
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> MorphMap
mmaps OWLMorphism
m2
            in if IRI
r IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
u then MorphMap -> MorphMap
forall a. a -> a
id else Entity -> IRI -> MorphMap -> MorphMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Entity
s IRI
r) MorphMap
forall k a. Map k a
Map.empty
           (Set Entity -> MorphMap)
-> (Sign -> Set Entity) -> Sign -> MorphMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Entity
symOf (Sign -> MorphMap) -> Sign -> MorphMap
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
m1
  in OWLMorphism -> Result OWLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return OWLMorphism
m1
     { otarget :: Sign
otarget = OWLMorphism -> Sign
otarget OWLMorphism
m2
     , pmap :: StringMap
pmap = StringMap -> StringMap -> StringMap -> StringMap
forall a b. Ord a => Map a b -> Map a a -> Map a a -> Map a a
composeMap (Sign -> StringMap
prefixMap (Sign -> StringMap) -> Sign -> StringMap
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
m1) (OWLMorphism -> StringMap
pmap OWLMorphism
m1) (StringMap -> StringMap) -> StringMap -> StringMap
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> StringMap
pmap OWLMorphism
m2
     , mmaps :: MorphMap
mmaps = MorphMap
nm }

cogeneratedSign :: Set.Set Entity -> Sign -> Result OWLMorphism
cogeneratedSign :: Set Entity -> Sign -> Result OWLMorphism
cogeneratedSign s :: Set Entity
s sign :: Sign
sign =
  let sig2 :: Sign
sig2 = State Sign () -> Sign -> Sign
forall s a. State s a -> s -> s
execState ((Entity -> State Sign ()) -> [Entity] -> State Sign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((IRI -> Set IRI -> Set IRI) -> Entity -> State Sign ()
modEntity IRI -> Set IRI -> Set IRI
forall a. Ord a => a -> Set a -> Set a
Set.delete) ([Entity] -> State Sign ()) -> [Entity] -> State Sign ()
forall a b. (a -> b) -> a -> b
$ Set Entity -> [Entity]
forall a. Set a -> [a]
Set.toList Set Entity
s) Sign
sign
  in if Sign -> Sign -> Bool
isSubSign Sign
sig2 Sign
sign then OWLMorphism -> Result OWLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (OWLMorphism -> Result OWLMorphism)
-> OWLMorphism -> Result OWLMorphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> OWLMorphism
inclOWLMorphism Sign
sig2 Sign
sign else
         String -> Result OWLMorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "non OWL2 subsignatures for (co)generatedSign"

generatedSign :: Set.Set Entity -> Sign -> Result OWLMorphism
generatedSign :: Set Entity -> Sign -> Result OWLMorphism
generatedSign s :: Set Entity
s sign :: Sign
sign = Set Entity -> Sign -> Result OWLMorphism
cogeneratedSign (Set Entity -> Set Entity -> Set Entity
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Entity
symOf Sign
sign) Set Entity
s) Sign
sign

matchesSym :: Entity -> RawSymb -> Bool
matchesSym :: Entity -> RawSymb -> Bool
matchesSym e :: Entity
e@(Entity _ _ u :: IRI
u) r :: RawSymb
r = case RawSymb
r of
       ASymbol s :: Entity
s -> Entity
s Entity -> Entity -> Bool
forall a. Eq a => a -> a -> Bool
== Entity
e
       AnUri s :: IRI
s -> IRI
s IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
u  -- expandedIRI s == expandedIRI u 
                Bool -> Bool -> Bool
|| case
         String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix (ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show (Id -> String) -> Id -> String
forall a b. (a -> b) -> a -> b
$ IRI -> Id
iriPath IRI
s) (ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show (Id -> String) -> Id -> String
forall a b. (a -> b) -> a -> b
$ IRI -> Id
iriPath IRI
u) of
           Just (c :: Char
c : _) | String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (IRI -> String
prefixName IRI
s) -> Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "/#"
           _ -> Bool
False
       APrefix p :: String
p -> String
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== IRI -> String
prefixName IRI
u

statSymbItems :: Sign -> [SymbItems] -> [RawSymb]
statSymbItems :: Sign -> [SymbItems] -> [RawSymb]
statSymbItems sig :: Sign
sig = (RawSymb -> RawSymb) -> [RawSymb] -> [RawSymb]
forall a b. (a -> b) -> [a] -> [b]
map (Action -> AMap -> RawSymb -> RawSymb
forall a. Function a => Action -> AMap -> a -> a
function Action
Expand (AMap -> RawSymb -> RawSymb)
-> (StringMap -> AMap) -> StringMap -> RawSymb -> RawSymb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StringMap -> AMap
StringMap (StringMap -> RawSymb -> RawSymb)
-> StringMap -> RawSymb -> RawSymb
forall a b. (a -> b) -> a -> b
$ Sign -> StringMap
prefixMap Sign
sig)
  ([RawSymb] -> [RawSymb])
-> ([SymbItems] -> [RawSymb]) -> [SymbItems] -> [RawSymb]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymbItems -> [RawSymb]) -> [SymbItems] -> [RawSymb]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
  (\ (SymbItems m :: ExtEntityType
m us :: [IRI]
us) -> case ExtEntityType
m of
               AnyEntity -> (IRI -> RawSymb) -> [IRI] -> [RawSymb]
forall a b. (a -> b) -> [a] -> [b]
map IRI -> RawSymb
AnUri [IRI]
us
               EntityType ty :: EntityType
ty -> (IRI -> RawSymb) -> [IRI] -> [RawSymb]
forall a b. (a -> b) -> [a] -> [b]
map (Entity -> RawSymb
ASymbol (Entity -> RawSymb) -> (IRI -> Entity) -> IRI -> RawSymb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> IRI -> Entity
mkEntity EntityType
ty) [IRI]
us
               PrefixO -> (IRI -> RawSymb) -> [IRI] -> [RawSymb]
forall a b. (a -> b) -> [a] -> [b]
map (String -> RawSymb
APrefix (String -> RawSymb) -> (IRI -> String) -> IRI -> RawSymb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> String
showIRI) [IRI]
us)

statSymbMapItems :: Sign -> Maybe Sign -> [SymbMapItems]
  -> Result (Map.Map RawSymb RawSymb)
statSymbMapItems :: Sign
-> Maybe Sign -> [SymbMapItems] -> Result (Map RawSymb RawSymb)
statSymbMapItems sig :: Sign
sig mtsig :: Maybe Sign
mtsig =
  (Map RawSymb RawSymb -> Map RawSymb RawSymb)
-> Result (Map RawSymb RawSymb) -> Result (Map RawSymb RawSymb)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(RawSymb, RawSymb)] -> Map RawSymb RawSymb
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(RawSymb, RawSymb)] -> Map RawSymb RawSymb)
-> (Map RawSymb RawSymb -> [(RawSymb, RawSymb)])
-> Map RawSymb RawSymb
-> Map RawSymb RawSymb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((RawSymb, RawSymb) -> (RawSymb, RawSymb))
-> [(RawSymb, RawSymb)] -> [(RawSymb, RawSymb)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (r1 :: RawSymb
r1, r2 :: RawSymb
r2) ->
        let f :: Sign -> RawSymb -> RawSymb
f = Action -> AMap -> RawSymb -> RawSymb
forall a. Function a => Action -> AMap -> a -> a
function Action
Expand (AMap -> RawSymb -> RawSymb)
-> (Sign -> AMap) -> Sign -> RawSymb -> RawSymb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StringMap -> AMap
StringMap (StringMap -> AMap) -> (Sign -> StringMap) -> Sign -> AMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> StringMap
prefixMap
            f1 :: RawSymb -> RawSymb
f1 = Sign -> RawSymb -> RawSymb
f Sign
sig
            f2 :: RawSymb -> RawSymb
f2 = Sign -> RawSymb -> RawSymb
f (Sign -> RawSymb -> RawSymb) -> Sign -> RawSymb -> RawSymb
forall a b. (a -> b) -> a -> b
$ Sign -> Maybe Sign -> Sign
forall a. a -> Maybe a -> a
fromMaybe Sign
sig Maybe Sign
mtsig
        in (RawSymb -> RawSymb
f1 RawSymb
r1, RawSymb -> RawSymb
f2 RawSymb
r2)) ([(RawSymb, RawSymb)] -> [(RawSymb, RawSymb)])
-> (Map RawSymb RawSymb -> [(RawSymb, RawSymb)])
-> Map RawSymb RawSymb
-> [(RawSymb, RawSymb)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map RawSymb RawSymb -> [(RawSymb, RawSymb)]
forall k a. Map k a -> [(k, a)]
Map.toList)
  (Result (Map RawSymb RawSymb) -> Result (Map RawSymb RawSymb))
-> ([SymbMapItems] -> Result (Map RawSymb RawSymb))
-> [SymbMapItems]
-> Result (Map RawSymb RawSymb)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map RawSymb RawSymb
 -> (RawSymb, RawSymb) -> Result (Map RawSymb RawSymb))
-> Map RawSymb RawSymb
-> [(RawSymb, RawSymb)]
-> Result (Map RawSymb RawSymb)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ m :: Map RawSymb RawSymb
m (s :: RawSymb
s, t :: RawSymb
t) -> case RawSymb -> Map RawSymb RawSymb -> Maybe RawSymb
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup RawSymb
s Map RawSymb RawSymb
m of
    Nothing -> Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map RawSymb RawSymb -> Result (Map RawSymb RawSymb))
-> Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall a b. (a -> b) -> a -> b
$ RawSymb -> RawSymb -> Map RawSymb RawSymb -> Map RawSymb RawSymb
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert RawSymb
s RawSymb
t Map RawSymb RawSymb
m
    Just u :: RawSymb
u -> case (RawSymb
u, RawSymb
t) of
      (AnUri su :: IRI
su, ASymbol (Entity _ _ tu :: IRI
tu)) | IRI
su IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
tu ->
        Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map RawSymb RawSymb -> Result (Map RawSymb RawSymb))
-> Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall a b. (a -> b) -> a -> b
$ RawSymb -> RawSymb -> Map RawSymb RawSymb -> Map RawSymb RawSymb
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert RawSymb
s RawSymb
t Map RawSymb RawSymb
m
      (ASymbol (Entity _ _ su :: IRI
su), AnUri tu :: IRI
tu) | IRI
su IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
tu -> Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall (m :: * -> *) a. Monad m => a -> m a
return Map RawSymb RawSymb
m
      (AnUri su :: IRI
su, APrefix tu :: String
tu) | IRI -> String
showIRICompact IRI
su String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
tu ->
        Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map RawSymb RawSymb -> Result (Map RawSymb RawSymb))
-> Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall a b. (a -> b) -> a -> b
$ RawSymb -> RawSymb -> Map RawSymb RawSymb -> Map RawSymb RawSymb
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert RawSymb
s RawSymb
t Map RawSymb RawSymb
m
      (APrefix su :: String
su, AnUri tu :: IRI
tu) | String
su String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== IRI -> String
showIRICompact IRI
tu -> Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall (m :: * -> *) a. Monad m => a -> m a
return Map RawSymb RawSymb
m
      _ -> if RawSymb
u RawSymb -> RawSymb -> Bool
forall a. Eq a => a -> a -> Bool
== RawSymb
t then Map RawSymb RawSymb -> Result (Map RawSymb RawSymb)
forall (m :: * -> *) a. Monad m => a -> m a
return Map RawSymb RawSymb
m else
        String -> Result (Map RawSymb RawSymb)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Map RawSymb RawSymb))
-> String -> Result (Map RawSymb RawSymb)
forall a b. (a -> b) -> a -> b
$ "differently mapped symbol: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RawSymb -> ShowS
forall a. Pretty a => a -> ShowS
showDoc RawSymb
s "\nmapped to "
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ RawSymb -> ShowS
forall a. Pretty a => a -> ShowS
showDoc RawSymb
u " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RawSymb -> ShowS
forall a. Pretty a => a -> ShowS
showDoc RawSymb
t "")
  Map RawSymb RawSymb
forall k a. Map k a
Map.empty
  ([(RawSymb, RawSymb)] -> Result (Map RawSymb RawSymb))
-> ([SymbMapItems] -> [(RawSymb, RawSymb)])
-> [SymbMapItems]
-> Result (Map RawSymb RawSymb)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymbMapItems -> [(RawSymb, RawSymb)])
-> [SymbMapItems] -> [(RawSymb, RawSymb)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (SymbMapItems m :: ExtEntityType
m us :: [(IRI, Maybe IRI)]
us) ->
      let ps :: [(IRI, IRI)]
ps = ((IRI, Maybe IRI) -> (IRI, IRI))
-> [(IRI, Maybe IRI)] -> [(IRI, IRI)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (u :: IRI
u, v :: Maybe IRI
v) -> (IRI
u, IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe IRI
u Maybe IRI
v)) [(IRI, Maybe IRI)]
us in
      case ExtEntityType
m of
        AnyEntity -> ((IRI, IRI) -> (RawSymb, RawSymb))
-> [(IRI, IRI)] -> [(RawSymb, RawSymb)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: IRI
s, t :: IRI
t) -> (IRI -> RawSymb
AnUri IRI
s, IRI -> RawSymb
AnUri IRI
t)) [(IRI, IRI)]
ps
        EntityType ty :: EntityType
ty ->
            let mS :: IRI -> RawSymb
mS = Entity -> RawSymb
ASymbol (Entity -> RawSymb) -> (IRI -> Entity) -> IRI -> RawSymb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> IRI -> Entity
mkEntity EntityType
ty
            in ((IRI, IRI) -> (RawSymb, RawSymb))
-> [(IRI, IRI)] -> [(RawSymb, RawSymb)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: IRI
s, t :: IRI
t) -> (IRI -> RawSymb
mS IRI
s, IRI -> RawSymb
mS IRI
t)) [(IRI, IRI)]
ps
        PrefixO ->
            ((IRI, IRI) -> (RawSymb, RawSymb))
-> [(IRI, IRI)] -> [(RawSymb, RawSymb)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: IRI
s, t :: IRI
t) -> (String -> RawSymb
APrefix (IRI -> String
showIRICompact IRI
s), String -> RawSymb
APrefix (String -> RawSymb) -> String -> RawSymb
forall a b. (a -> b) -> a -> b
$ IRI -> String
showIRICompact IRI
t)) [(IRI, IRI)]
ps)

mapSen :: OWLMorphism -> Axiom -> Result Axiom
mapSen :: OWLMorphism -> Axiom -> Result Axiom
mapSen m :: OWLMorphism
m a :: Axiom
a = do
    let new :: Axiom
new = Action -> AMap -> Axiom -> Axiom
forall a. Function a => Action -> AMap -> a -> a
function Action
Rename (MorphMap -> AMap
MorphMap (MorphMap -> AMap) -> MorphMap -> AMap
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> MorphMap
mmaps OWLMorphism
m) Axiom
a
    Axiom -> Result Axiom
forall (m :: * -> *) a. Monad m => a -> m a
return (Axiom -> Result Axiom) -> Axiom -> Result Axiom
forall a b. (a -> b) -> a -> b
$ Action -> AMap -> Axiom -> Axiom
forall a. Function a => Action -> AMap -> a -> a
function Action
Rename (StringMap -> AMap
StringMap (StringMap -> AMap) -> StringMap -> AMap
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> StringMap
pmap OWLMorphism
m) Axiom
new

morphismUnion :: OWLMorphism -> OWLMorphism -> Result OWLMorphism
morphismUnion :: OWLMorphism -> OWLMorphism -> Result OWLMorphism
morphismUnion mor1 :: OWLMorphism
mor1 mor2 :: OWLMorphism
mor2 = do
 let ssig1 :: Sign
ssig1 = OWLMorphism -> Sign
osource OWLMorphism
mor1
     tsig1 :: Sign
tsig1 = OWLMorphism -> Sign
otarget OWLMorphism
mor1
     ssig2 :: Sign
ssig2 = OWLMorphism -> Sign
osource OWLMorphism
mor2
     tsig2 :: Sign
tsig2 = OWLMorphism -> Sign
otarget OWLMorphism
mor2
     ssig :: Sign
ssig = Sign -> Sign -> Sign
addSign Sign
ssig1 Sign
ssig2
     tsig :: Sign
tsig = Sign -> Sign -> Sign
addSign Sign
tsig1 Sign
tsig2
     m1 :: MorphMap
m1 = OWLMorphism -> MorphMap
mmaps OWLMorphism
mor1
     m2 :: MorphMap
m2 = OWLMorphism -> MorphMap
mmaps OWLMorphism
mor2
     intM :: MorphMap
intM = MorphMap -> MorphMap -> MorphMap
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection MorphMap
m1 MorphMap
m2
     pairs :: [(IRI, IRI)]
pairs = ((IRI, IRI) -> Bool) -> [(IRI, IRI)] -> [(IRI, IRI)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a :: IRI
a,b :: IRI
b) -> IRI
a IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
/= IRI
b)
             ([(IRI, IRI)] -> [(IRI, IRI)]) -> [(IRI, IRI)] -> [(IRI, IRI)]
forall a b. (a -> b) -> a -> b
$ (Entity -> (IRI, IRI)) -> [Entity] -> [(IRI, IRI)]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: Entity
x -> (IRI -> Entity -> MorphMap -> IRI
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> IRI
forall a. HasCallStack => String -> a
error "1") Entity
x MorphMap
m1, 
                           IRI -> Entity -> MorphMap -> IRI
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> IRI
forall a. HasCallStack => String -> a
error "2") Entity
x MorphMap
m2)) 
             ([Entity] -> [(IRI, IRI)]) -> [Entity] -> [(IRI, IRI)]
forall a b. (a -> b) -> a -> b
$ MorphMap -> [Entity]
forall k a. Map k a -> [k]
Map.keys MorphMap
intM
 case [(IRI, IRI)]
pairs of 
  [] -> 
    OWLMorphism -> Result OWLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (OWLMorphism -> Result OWLMorphism)
-> OWLMorphism -> Result OWLMorphism
forall a b. (a -> b) -> a -> b
$  OWLMorphism :: Sign -> Sign -> MorphMap -> StringMap -> OWLMorphism
OWLMorphism {
                 osource :: Sign
osource = Sign
ssig,
                 otarget :: Sign
otarget = Sign
tsig,
                 mmaps :: MorphMap
mmaps = MorphMap -> MorphMap -> MorphMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union MorphMap
m1 MorphMap
m2,
                 pmap :: StringMap
pmap = StringMap -> StringMap -> StringMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (OWLMorphism -> StringMap
pmap OWLMorphism
mor1) (StringMap -> StringMap) -> StringMap -> StringMap
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> StringMap
pmap OWLMorphism
mor2}
  _ -> String -> Result OWLMorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result OWLMorphism) -> String -> Result OWLMorphism
forall a b. (a -> b) -> a -> b
$ "can't unite morphisms:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(IRI, IRI)] -> String
forall a. Show a => a -> String
show [(IRI, IRI)]
pairs