{- |
Module      :  ./NeSyPatterns/Analysis.hs
Description :  Basic analysis for propositional logic
License     :  GPLv2 or higher, see LICENSE.txt

Stability   :  experimental
Portability :  portable

Basic and static analysis for propositional logic

  Ref.
  <http://en.wikipedia.org/wiki/NeSyPatterns_logic>
-}

module NeSyPatterns.Analysis
    ( basicNeSyPatternsAnalysis
    , mkStatSymbItems
    , mkStatSymbMapItem
    , inducedFromMorphism
    , inducedFromToMorphism
    , signatureColimit
    , subClassRelation
    )
    where


import Data.Maybe (fromMaybe)
import Data.Foldable (foldrM, foldlM)
import Data.List (stripPrefix)
import Data.Bifunctor (bimap, Bifunctor (second))

import Control.Applicative
import Common.ExtSign
import Common.IRI
import Common.Lib.Graph
import Common.Result (resultToMaybe)
import Common.SetColimit
import Common.Utils

import NeSyPatterns.Sign as Sign

import qualified Common.AS_Annotation as AS_Anno
import qualified Common.GlobalAnnotations as GlobalAnnos
import qualified Common.Id as Id
import qualified Common.Result as Result
import qualified Data.Graph.Inductive.Graph as Gr
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.Relation as Rel
import qualified NeSyPatterns.AS as AS
import qualified NeSyPatterns.Morphism as Morphism
import qualified NeSyPatterns.Symbol as Symbol
import qualified OWL2.AS as OWL2

-- | Retrieves the signature out of a basic spec
makeSig ::
    AS.BASIC_SPEC                         -- Input SPEC
    -> Sign.Sign                          -- Input Signature
    -> Result.Result Sign.Sign                   -- Output Signature
makeSig :: BASIC_SPEC -> Sign -> Result Sign
makeSig bs :: BASIC_SPEC
bs sig :: Sign
sig = let spec' :: [BASIC_ITEM]
spec' = BASIC_SPEC -> [BASIC_ITEM]
genIds BASIC_SPEC
bs in
  (BASIC_ITEM -> Sign -> Result Sign)
-> Sign -> [BASIC_ITEM] -> Result Sign
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM BASIC_ITEM -> Sign -> Result Sign
retrieveBasicItem Sign
sig [BASIC_ITEM]
spec'

addNodeToIdMap :: AS.Node -> Map.Map IRI IRI -> Map.Map IRI IRI
addNodeToIdMap :: Node -> Map IRI IRI -> Map IRI IRI
addNodeToIdMap (AS.Node o :: IRI
o mi :: Maybe IRI
mi _) m :: Map IRI IRI
m = case Maybe IRI
mi of
  Just i :: IRI
i -> IRI -> IRI -> Map IRI IRI -> Map IRI IRI
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
i IRI
o Map IRI IRI
m
  Nothing -> Map IRI IRI
m

addPathToIdMap :: AS.BASIC_ITEM -> Map.Map IRI IRI -> Map.Map IRI IRI
addPathToIdMap :: BASIC_ITEM -> Map IRI IRI -> Map IRI IRI
addPathToIdMap (AS.Path ns :: [Node]
ns) m :: Map IRI IRI
m = (Node -> Map IRI IRI -> Map IRI IRI)
-> Map IRI IRI -> [Node] -> Map IRI IRI
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Node -> Map IRI IRI -> Map IRI IRI
addNodeToIdMap Map IRI IRI
m [Node]
ns

extractIdMap :: AS.BASIC_SPEC -> Map.Map IRI IRI
extractIdMap :: BASIC_SPEC -> Map IRI IRI
extractIdMap (AS.Basic_spec spec :: [Annoted BASIC_ITEM]
spec) = (BASIC_ITEM -> Map IRI IRI -> Map IRI IRI)
-> Map IRI IRI -> [BASIC_ITEM] -> Map IRI IRI
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr BASIC_ITEM -> Map IRI IRI -> Map IRI IRI
addPathToIdMap Map IRI IRI
forall k a. Map k a
Map.empty (Annoted BASIC_ITEM -> BASIC_ITEM
forall a. Annoted a -> a
AS_Anno.item (Annoted BASIC_ITEM -> BASIC_ITEM)
-> [Annoted BASIC_ITEM] -> [BASIC_ITEM]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Annoted BASIC_ITEM]
spec)

genIds :: AS.BASIC_SPEC -> [AS.BASIC_ITEM]
genIds :: BASIC_SPEC -> [BASIC_ITEM]
genIds (AS.Basic_spec paths :: [Annoted BASIC_ITEM]
paths) = (Int, [BASIC_ITEM]) -> [BASIC_ITEM]
forall a b. (a, b) -> b
snd ((Int, [BASIC_ITEM]) -> [BASIC_ITEM])
-> (Int, [BASIC_ITEM]) -> [BASIC_ITEM]
forall a b. (a -> b) -> a -> b
$ (BASIC_ITEM -> (Int, [BASIC_ITEM]) -> (Int, [BASIC_ITEM]))
-> (Int, [BASIC_ITEM]) -> [BASIC_ITEM] -> (Int, [BASIC_ITEM])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr BASIC_ITEM -> (Int, [BASIC_ITEM]) -> (Int, [BASIC_ITEM])
genIdsPath (0, []) ([BASIC_ITEM] -> (Int, [BASIC_ITEM]))
-> [BASIC_ITEM] -> (Int, [BASIC_ITEM])
forall a b. (a -> b) -> a -> b
$ Annoted BASIC_ITEM -> BASIC_ITEM
forall a. Annoted a -> a
AS_Anno.item (Annoted BASIC_ITEM -> BASIC_ITEM)
-> [Annoted BASIC_ITEM] -> [BASIC_ITEM]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Annoted BASIC_ITEM]
paths

genIdsPath :: AS.BASIC_ITEM -> (Int, [AS.BASIC_ITEM]) -> (Int, [AS.BASIC_ITEM])
genIdsPath :: BASIC_ITEM -> (Int, [BASIC_ITEM]) -> (Int, [BASIC_ITEM])
genIdsPath (AS.Path ns :: [Node]
ns) (genId :: Int
genId, agg :: [BASIC_ITEM]
agg) = (BASIC_ITEM -> [BASIC_ITEM] -> [BASIC_ITEM]
forall a. a -> [a] -> [a]
: [BASIC_ITEM]
agg) (BASIC_ITEM -> [BASIC_ITEM])
-> ([Node] -> BASIC_ITEM) -> [Node] -> [BASIC_ITEM]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Node] -> BASIC_ITEM
AS.Path ([Node] -> [BASIC_ITEM]) -> (Int, [Node]) -> (Int, [BASIC_ITEM])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Node -> (Int, [Node]) -> (Int, [Node]))
-> (Int, [Node]) -> [Node] -> (Int, [Node])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Node -> (Int, [Node]) -> (Int, [Node])
genIdsNode (Int
genId, []) [Node]
ns

genIdsNode :: AS.Node -> (Int, [AS.Node]) -> (Int, [AS.Node])
genIdsNode :: Node -> (Int, [Node]) -> (Int, [Node])
genIdsNode node :: Node
node (genId :: Int
genId, agg :: [Node]
agg) = (Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
agg) (Node -> [Node]) -> (Int, Node) -> (Int, [Node])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Node -> (Int, Node)
genIdNode Int
genId Node
node

genIdNode :: Int -> AS.Node -> (Int, AS.Node)
genIdNode :: Int -> Node -> (Int, Node)
genIdNode genId :: Int
genId node :: Node
node = case Node -> Maybe IRI
AS.nesyId Node
node of
  Nothing -> (Int
genId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, Node
node { nesyId :: Maybe IRI
AS.nesyId = IRI -> Maybe IRI
forall a. a -> Maybe a
Just (IRI -> Maybe IRI) -> ([Token] -> IRI) -> [Token] -> Maybe IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> IRI
idToIRI (Id -> IRI) -> ([Token] -> Id) -> [Token] -> IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Id
Id.mkId ([Token] -> Maybe IRI) -> [Token] -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ [ String -> Int -> Token
Id.genNumVar "nesy" Int
genId ] })
  Just _ -> (Int
genId, Node
node)


-- Helper for makeSig
retrieveBasicItem ::
    AS.BASIC_ITEM              -- Input Item
    -> Sign                                          -- Input Signature
    -> Result.Result Sign                                -- Output Signature
retrieveBasicItem :: BASIC_ITEM -> Sign -> Result Sign
retrieveBasicItem x :: BASIC_ITEM
x sig :: Sign
sig = let sigM :: Maybe Sign
sigM = Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
sig in case BASIC_ITEM
x of
      AS.Path [] -> Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return Sign
sig
      AS.Path ns :: [Node]
ns -> do
        let n0 :: Node
n0 = [Node] -> Node
forall a. [a] -> a
last [Node]
ns
        ResolvedNode
n0' <- Maybe Sign -> Node -> Result ResolvedNode
resolveNode Maybe Sign
sigM Node
n0
        let sig' :: Sign
sig' = Sign -> ResolvedNode -> Sign
addToSig Sign
sig ResolvedNode
n0'
        (_, sig'' :: Sign
sig'') <- (Node -> (ResolvedNode, Sign) -> Result (ResolvedNode, Sign))
-> (ResolvedNode, Sign) -> [Node] -> Result (ResolvedNode, Sign)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\f :: Node
f (t :: ResolvedNode
t, s :: Sign
s) -> do
            ResolvedNode
resolvedFrom <- Maybe Sign -> Node -> Result ResolvedNode
resolveNode Maybe Sign
sigM Node
f
            (ResolvedNode, Sign) -> Result (ResolvedNode, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedNode
resolvedFrom, Sign -> (ResolvedNode, ResolvedNode) -> Sign
addEdgeToSig' Sign
s (ResolvedNode
resolvedFrom, ResolvedNode
t))
          ) (ResolvedNode
n0', Sign
sig') ([Node] -> [Node]
forall a. [a] -> [a]
init [Node]
ns)
        Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return Sign
sig''


{- | @resolveNode sm n@ converts @n@ to a @ResolvedNode@ if it's ontology term
  is declared in the data ontology @owlClasses s@. If @n@ does not contain an id,
  @findId@ is used to try to match it.
   -}
resolveNode :: Maybe Sign -- ^ 
  -> AS.Node -- ^ 
  -> Result.Result ResolvedNode
resolveNode :: Maybe Sign -> Node -> Result ResolvedNode
resolveNode sigM :: Maybe Sign
sigM n :: Node
n@(AS.Node o :: IRI
o mi :: Maybe IRI
mi r :: Range
r) = case Maybe IRI
mi of
    Just i :: IRI
i -> case Maybe Sign
sigM of
      Just sig :: Sign
sig -> if IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
o (Sign -> Set IRI
owlClasses Sign
sig) then
          ResolvedNode -> Result ResolvedNode
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedNode -> Result ResolvedNode)
-> ResolvedNode -> Result ResolvedNode
forall a b. (a -> b) -> a -> b
$ IRI -> IRI -> Range -> ResolvedNode
ResolvedNode IRI
o IRI
i Range
r
        else
          String -> Node -> Result ResolvedNode
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
Result.mkError "Undefined class" Node
n

      Nothing -> ResolvedNode -> Result ResolvedNode
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedNode -> Result ResolvedNode)
-> ResolvedNode -> Result ResolvedNode
forall a b. (a -> b) -> a -> b
$ IRI -> IRI -> Range -> ResolvedNode
ResolvedNode IRI
o IRI
i Range
r
    Nothing -> case Maybe Sign
sigM of
      Just sig :: Sign
sig -> case IRI -> Set ResolvedNode -> Maybe IRI
forall (t :: * -> *).
Foldable t =>
IRI -> t ResolvedNode -> Maybe IRI
findId IRI
o (Set ResolvedNode -> Maybe IRI) -> Set ResolvedNode -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ Sign -> Set ResolvedNode
nodes Sign
sig of
        Just i :: IRI
i -> ResolvedNode -> Result ResolvedNode
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedNode -> Result ResolvedNode)
-> ResolvedNode -> Result ResolvedNode
forall a b. (a -> b) -> a -> b
$ IRI -> IRI -> Range -> ResolvedNode
ResolvedNode IRI
o IRI
i Range
r
        Nothing -> String -> Node -> Result ResolvedNode
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
Result.mkError "Cannot uniquely resolve unset nesyid." Node
n
      Nothing -> String -> Node -> Result ResolvedNode
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
Result.mkError "Unset nesyid." Node
n

{- | @findId o f@ finds a the id used to refer to @o@ in @f@ if there is exactly
  one id used in @f@ to refer to @o@ -}
findId :: Foldable t => IRI -- ^ Ontology term which id should be found
  -> t ResolvedNode -- ^ List of nodes in which @o@ should be searched
  -> Maybe IRI
findId :: IRI -> t ResolvedNode -> Maybe IRI
findId o :: IRI
o = (ResolvedNode -> Maybe IRI -> Maybe IRI)
-> Maybe IRI -> t ResolvedNode -> Maybe IRI
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\n' :: ResolvedNode
n' r :: Maybe IRI
r -> case (Maybe IRI
r, ResolvedNode -> IRI
resolvedOTerm ResolvedNode
n' IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
o) of
          (Nothing, True)  -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just (IRI -> Maybe IRI) -> IRI -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ ResolvedNode -> IRI
resolvedNeSyId ResolvedNode
n'
          (Just i :: IRI
i, True) | IRI
i IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
/= ResolvedNode -> IRI
resolvedNeSyId ResolvedNode
n' -> Maybe IRI
forall a. Maybe a
Nothing
          _ -> Maybe IRI
r) Maybe IRI
forall a. Maybe a
Nothing

-- | Basic analysis 
basicNeSyPatternsAnalysis
  :: (AS.BASIC_SPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
  -> Result.Result (AS.BASIC_SPEC,
                    ExtSign Sign.Sign Symbol.Symbol,
                    [AS_Anno.Named ()])
basicNeSyPatternsAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named ()])
basicNeSyPatternsAnalysis (spec :: BASIC_SPEC
spec, sig :: Sign
sig, _) = do
  let idm :: Map IRI IRI
idm = BASIC_SPEC -> Map IRI IRI
extractIdMap BASIC_SPEC
spec
  Sign
sign <- BASIC_SPEC -> Sign -> Result Sign
makeSig BASIC_SPEC
spec Sign
sig { idMap :: Map IRI IRI
idMap = Map IRI IRI
idm }
  (BASIC_SPEC, ExtSign Sign Symbol, [Named ()])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named ()])
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_SPEC
spec, Sign -> Set Symbol -> ExtSign Sign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign
sign ((ResolvedNode -> Symbol) -> Set ResolvedNode -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ResolvedNode -> Symbol
Symbol.Symbol (Set ResolvedNode -> Set Symbol) -> Set ResolvedNode -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set ResolvedNode
Sign.nodes Sign
sign), [])

-- | Static analysis for symbol maps
mkStatSymbMapItem :: Sign -> Maybe Sign -> [AS.SYMB_MAP_ITEMS]
                  -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
mkStatSymbMapItem :: Sign
-> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (Map Symbol Symbol)
mkStatSymbMapItem sig :: Sign
sig sigM :: Maybe Sign
sigM = Map Symbol Symbol -> Result (Map Symbol Symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Symbol Symbol -> Result (Map Symbol Symbol))
-> ([SYMB_MAP_ITEMS] -> Map Symbol Symbol)
-> [SYMB_MAP_ITEMS]
-> Result (Map Symbol Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SYMB_MAP_ITEMS -> Map Symbol Symbol -> Map Symbol Symbol)
-> Map Symbol Symbol -> [SYMB_MAP_ITEMS] -> Map Symbol Symbol
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr 
  (\(AS.Symb_map_items sitem :: [SYMB_OR_MAP]
sitem _) -> Map Symbol Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map Symbol Symbol -> Map Symbol Symbol -> Map Symbol Symbol)
-> Map Symbol Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Maybe Sign -> [SYMB_OR_MAP] -> Map Symbol Symbol
statSymbMapItem Sign
sig Maybe Sign
sigM [SYMB_OR_MAP]
sitem)
  Map Symbol Symbol
forall k a. Map k a
Map.empty

statSymbMapItem :: Sign.Sign -> Maybe Sign -> [AS.SYMB_OR_MAP]
                 -> Map.Map Symbol.Symbol Symbol.Symbol
statSymbMapItem :: Sign -> Maybe Sign -> [SYMB_OR_MAP] -> Map Symbol Symbol
statSymbMapItem sig :: Sign
sig sigM :: Maybe Sign
sigM = let s :: Sign
s = Sign -> Maybe Sign -> Sign
forall a. a -> Maybe a -> a
fromMaybe Sign
sig Maybe Sign
sigM in (SYMB_OR_MAP -> Map Symbol Symbol -> Map Symbol Symbol)
-> Map Symbol Symbol -> [SYMB_OR_MAP] -> Map Symbol Symbol
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\x :: SYMB_OR_MAP
x mmap :: Map Symbol Symbol
mmap ->
         case SYMB_OR_MAP
x of
           AS.Symb sym :: SYMB
sym -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Sign -> SYMB -> Symbol
symbToSymbol Sign
sig SYMB
sym) (Sign -> SYMB -> Symbol
symbToSymbol Sign
sig SYMB
sym) Map Symbol Symbol
mmap
           AS.Symb_map s1 :: SYMB
s1 s2 :: SYMB
s2 _ ->
               Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Sign -> SYMB -> Symbol
symbToSymbol Sign
sig SYMB
s1) (Sign -> SYMB -> Symbol
symbToSymbol Sign
s SYMB
s2) Map Symbol Symbol
mmap
    ) Map Symbol Symbol
forall k a. Map k a
Map.empty

-- | Retrieve raw symbols
mkStatSymbItems :: Sign.Sign -> [AS.SYMB_ITEMS] -> Result.Result [Symbol.Symbol]
mkStatSymbItems :: Sign -> [SYMB_ITEMS] -> Result [Symbol]
mkStatSymbItems sig :: Sign
sig a :: [SYMB_ITEMS]
a = do
    [ResolvedNode]
resolvedSymbols <- (Node -> Result ResolvedNode) -> [Node] -> Result [ResolvedNode]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Sign -> Node -> Result ResolvedNode
resolveNode (Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
sig)) [Node
t | (AS.Symb_items r :: [SYMB]
r _) <- [SYMB_ITEMS]
a, (AS.Symb_id t :: Node
t) <- [SYMB]
r]
    [Symbol] -> Result [Symbol]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Symbol] -> Result [Symbol]) -> [Symbol] -> Result [Symbol]
forall a b. (a -> b) -> a -> b
$ ResolvedNode -> Symbol
Symbol.Symbol (ResolvedNode -> Symbol) -> [ResolvedNode] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ResolvedNode]
resolvedSymbols

symbToSymbol :: Sign.Sign -> AS.SYMB -> Symbol.Symbol
symbToSymbol :: Sign -> SYMB -> Symbol
symbToSymbol sig :: Sign
sig (AS.Symb_id node :: Node
node) = let
    resolved :: Result ResolvedNode
resolved = Maybe Sign -> Node -> Result ResolvedNode
resolveNode (Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
sig) Node
node
    nextId :: Int
nextId = Sign -> Int
nextGenId Sign
sig
    (_, newId :: Node
newId) = Int -> Node -> (Int, Node)
genIdNode Int
nextId Node
node
    nodeM :: Maybe ResolvedNode
nodeM = Result ResolvedNode -> Maybe ResolvedNode
forall a. Result a -> Maybe a
resultToMaybe (Result ResolvedNode -> Maybe ResolvedNode)
-> Result ResolvedNode -> Maybe ResolvedNode
forall a b. (a -> b) -> a -> b
$ Result ResolvedNode
resolved Result ResolvedNode -> Result ResolvedNode -> Result ResolvedNode
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Sign -> Node -> Result ResolvedNode
resolveNode (Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
sig) Node
newId
  in case Maybe ResolvedNode
nodeM of
  Just n :: ResolvedNode
n -> ResolvedNode -> Symbol
Symbol.Symbol ResolvedNode
n
  Nothing -> String -> Symbol
forall a. HasCallStack => String -> a
error "NeSyPatterns.Analysis.symbToSymbol: Cannot convert symbol"



makePMapR :: Map.Map Symbol.Symbol Symbol.Symbol
  -> Map.Map ResolvedNode ResolvedNode
makePMapR :: Map Symbol Symbol -> Map ResolvedNode ResolvedNode
makePMapR = [(ResolvedNode, ResolvedNode)] -> Map ResolvedNode ResolvedNode
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(ResolvedNode, ResolvedNode)] -> Map ResolvedNode ResolvedNode)
-> (Map Symbol Symbol -> [(ResolvedNode, ResolvedNode)])
-> Map Symbol Symbol
-> Map ResolvedNode ResolvedNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, Symbol) -> (ResolvedNode, ResolvedNode))
-> [(Symbol, Symbol)] -> [(ResolvedNode, ResolvedNode)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Symbol -> ResolvedNode)
-> (Symbol -> ResolvedNode)
-> (Symbol, Symbol)
-> (ResolvedNode, ResolvedNode)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Symbol -> ResolvedNode
Symbol.node Symbol -> ResolvedNode
Symbol.node) ([(Symbol, Symbol)] -> [(ResolvedNode, ResolvedNode)])
-> (Map Symbol Symbol -> [(Symbol, Symbol)])
-> Map Symbol Symbol
-> [(ResolvedNode, ResolvedNode)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Symbol Symbol -> [(Symbol, Symbol)]
forall k a. Map k a -> [(k, a)]
Map.toList

-- | Induce a signature morphism from a source signature and a raw symbol map
inducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                    -> Sign.Sign
                    -> Result.Result Morphism.Morphism
inducedFromMorphism :: Map Symbol Symbol -> Sign -> Result Morphism
inducedFromMorphism imap :: Map Symbol Symbol
imap sig :: Sign
sig = let pMap :: Map ResolvedNode ResolvedNode
pMap = Map Symbol Symbol -> Map ResolvedNode ResolvedNode
makePMapR Map Symbol Symbol
imap in
              Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return
              Morphism :: Sign
-> Sign -> Map IRI IRI -> Map ResolvedNode ResolvedNode -> Morphism
Morphism.Morphism
                          { source :: Sign
Morphism.source = Sign
sig
                          , owlMap :: Map IRI IRI
Morphism.owlMap = Map IRI IRI
forall k a. Map k a
Map.empty
                          , nodeMap :: Map ResolvedNode ResolvedNode
Morphism.nodeMap = Map ResolvedNode ResolvedNode
pMap
                          , target :: Sign
Morphism.target = Sign
Sign.emptySig
                            { nodes :: Set ResolvedNode
Sign.nodes = (ResolvedNode -> ResolvedNode)
-> Set ResolvedNode -> Set ResolvedNode
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map ResolvedNode ResolvedNode -> ResolvedNode -> ResolvedNode
Morphism.applyMap Map ResolvedNode ResolvedNode
pMap)
                              (Set ResolvedNode -> Set ResolvedNode)
-> Set ResolvedNode -> Set ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign -> Set ResolvedNode
Sign.nodes Sign
sig }
                          }

-- | Induce a signature morphism from a source signature and a raw symbol map
inducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                    -> ExtSign Sign.Sign Symbol.Symbol
                    -> ExtSign Sign.Sign Symbol.Symbol
                    -> Result.Result Morphism.Morphism
inducedFromToMorphism :: Map Symbol Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism imap :: Map Symbol Symbol
imap (ExtSign sig :: Sign
sig _) (ExtSign tSig :: Sign
tSig _) =
              let
                  targetSig :: Sign
targetSig = Sign :: Set IRI
-> Relation IRI IRI
-> Set ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Map IRI IRI
-> Sign
Sign.Sign {
                    owlClasses :: Set IRI
Sign.owlClasses = Set IRI
forall a. Set a
Set.empty, --TODO
                    owlTaxonomy :: Relation IRI IRI
Sign.owlTaxonomy = Relation IRI IRI
forall a b. Relation a b
Rel.empty, -- TODO
                    nodes :: Set ResolvedNode
Sign.nodes = Set ResolvedNode
forall a. Set a
Set.empty, -- Set.map (Morphism.applyMap pMap) $ Sign.nodes sig,
                    edges :: Relation ResolvedNode ResolvedNode
Sign.edges = Relation ResolvedNode ResolvedNode
forall a b. Relation a b
Rel.empty,
                    idMap :: Map IRI IRI
Sign.idMap = Map IRI IRI
forall k a. Map k a
Map.empty } -- TODO: IMPLEMENT
                  isSub :: Bool
isSub = Sign -> Set ResolvedNode
Sign.nodes Sign
targetSig Set ResolvedNode -> Set ResolvedNode -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Sign -> Set ResolvedNode
Sign.nodes Sign
tSig
              in if Bool
isSub then Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism :: Sign
-> Sign -> Map IRI IRI -> Map ResolvedNode ResolvedNode -> Morphism
Morphism.Morphism
                     { source :: Sign
Morphism.source = Sign
sig
                     , nodeMap :: Map ResolvedNode ResolvedNode
Morphism.nodeMap = Map Symbol Symbol -> Map ResolvedNode ResolvedNode
makePMapR Map Symbol Symbol
imap
                     , owlMap :: Map IRI IRI
Morphism.owlMap = Map IRI IRI
forall k a. Map k a
Map.empty -- TODO
                     , target :: Sign
Morphism.target = Sign
tSig
                     }
                     else String -> Result Morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Incompatible mapping"

-- | Retrieves a relation of simple classes from a set of axioms. If (a SubClassOf b) then (a ~ b)
subClassRelation :: [OWL2.Axiom] -> Rel.Relation IRI IRI
subClassRelation :: [Axiom] -> Relation IRI IRI
subClassRelation axs :: [Axiom]
axs = [(IRI, IRI)] -> Relation IRI IRI
forall a b. (Ord a, Ord b) => [(a, b)] -> Relation a b
Rel.fromList [ (IRI
cl1, IRI
cl2) | OWL2.ClassAxiom (OWL2.SubClassOf _ (OWL2.Expression cl1 :: IRI
cl1) (OWL2.Expression cl2 :: IRI
cl2)) <- [Axiom]
axs]

computeGLB :: (Ord a, Show a) => Rel.Relation a a -> Set.Set a -> Maybe a
computeGLB :: Relation a a -> Set a -> Maybe a
computeGLB r :: Relation a a
r s :: Set a
s =
 let getAllBounds :: Set a -> Set a
getAllBounds aSet :: Set a
aSet =
      let aBounds :: Set a
aBounds = [Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set a] -> Set a) -> [Set a] -> Set a
forall a b. (a -> b) -> a -> b
$ (a -> Set a) -> [a] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Relation a a -> Set a
forall b a. Ord b => b -> Relation a b -> Set a
`Rel.lookupRan` Relation a a
r) ([a] -> [Set a]) -> [a] -> [Set a]
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
aSet
      in if Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set a
aBounds Set a
aSet
            then Set a
aSet
            else Set a -> Set a
getAllBounds (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
aBounds Set a
aSet
     bounds :: [Set a]
bounds = (a -> Set a) -> [a] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map (Set a -> Set a
getAllBounds (Set a -> Set a) -> (a -> Set a) -> a -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\x :: a
x -> Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union (a -> Set a
forall a. a -> Set a
Set.singleton a
x) (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ a -> Relation a a -> Set a
forall b a. Ord b => b -> Relation a b -> Set a
Rel.lookupRan a
x Relation a a
r)) (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s)
 in case [Set a]
bounds of
      [] -> Maybe a
forall a. Maybe a
Nothing
      aSet :: Set a
aSet : sets :: [Set a]
sets ->
        let intBounds :: Set a
intBounds = (Set a -> Set a -> Set a) -> Set a -> [Set a] -> Set a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set a
aSet [Set a]
sets
        in if Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set a
intBounds then Maybe a
forall a. Maybe a
Nothing
           else let isLB :: a -> Bool
isLB y :: a
y = let notR :: Set a
notR = (a -> Bool) -> Set a -> Set a
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\x :: a
x -> a -> a -> Relation a a -> Bool
forall a b. (Ord a, Ord b) => a -> b -> Relation a b -> Bool
Rel.notMember a
x a
y Relation a a
r Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y ) Set a
intBounds
                              in Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
notR
                    gbs :: Set a
gbs = (a -> Bool) -> Set a -> Set a
forall a. (a -> Bool) -> Set a -> Set a
Set.filter a -> Bool
isLB Set a
intBounds
                in case Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
gbs of
                    [x :: a
x] -> a -> Maybe a
forall a. a -> Maybe a
Just a
x
                    _ -> Maybe a
forall a. Maybe a
Nothing

allLabels :: [(Int, Set.Set ResolvedNode)] -- the graph nodes
          -> Map.Map Int (Map.Map IRI IRI) -- the structural morphisms f of the colimit on nodeIds
          -> IRI -- the nodeId N in the colimit 
          -> Set.Set ResolvedNode
          -- all resolved nodes in the graph whose nodeId is mapped to N 
          -- along the corresponding morphism in f
allLabels :: [(Int, Set ResolvedNode)]
-> Map Int (Map IRI IRI) -> IRI -> Set ResolvedNode
allLabels nSets :: [(Int, Set ResolvedNode)]
nSets tMaps :: Map Int (Map IRI IRI)
tMaps cId :: IRI
cId =
  (Set ResolvedNode
 -> (Map IRI IRI, Set ResolvedNode) -> Set ResolvedNode)
-> Set ResolvedNode
-> [(Map IRI IRI, Set ResolvedNode)]
-> Set ResolvedNode
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\aSet :: Set ResolvedNode
aSet (iMap :: Map IRI IRI
iMap, s :: Set ResolvedNode
s) -> Set ResolvedNode -> Set ResolvedNode -> Set ResolvedNode
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ResolvedNode
aSet (Set ResolvedNode -> Set ResolvedNode)
-> Set ResolvedNode -> Set ResolvedNode
forall a b. (a -> b) -> a -> b
$
                            (ResolvedNode -> Bool) -> Set ResolvedNode -> Set ResolvedNode
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(ResolvedNode _ nId :: IRI
nId _) -> IRI
cId IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI -> IRI -> Map IRI IRI -> IRI
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault IRI
nId IRI
nId Map IRI IRI
iMap) Set ResolvedNode
s)
        Set ResolvedNode
forall a. Set a
Set.empty ([(Map IRI IRI, Set ResolvedNode)] -> Set ResolvedNode)
-> [(Map IRI IRI, Set ResolvedNode)] -> Set ResolvedNode
forall a b. (a -> b) -> a -> b
$ ((Int, Set ResolvedNode) -> (Map IRI IRI, Set ResolvedNode))
-> [(Int, Set ResolvedNode)] -> [(Map IRI IRI, Set ResolvedNode)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i :: Int
i, s :: Set ResolvedNode
s) -> (Map IRI IRI -> Int -> Map Int (Map IRI IRI) -> Map IRI IRI
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map IRI IRI
forall a. HasCallStack => String -> a
error "missing index") Int
i Map Int (Map IRI IRI)
tMaps, Set ResolvedNode
s))[(Int, Set ResolvedNode)]
nSets

signatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
                 -> Result.Result (Sign.Sign, Map.Map Int Morphism.Morphism)
signatureColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signatureColimit graph :: Gr Sign (Int, Morphism)
graph = do
  let owlGraph :: Gr (Set IRI) (Int, Map IRI IRI)
owlGraph = (Sign -> Set IRI)
-> Gr Sign (Int, Map IRI IRI) -> Gr (Set IRI) (Int, Map IRI IRI)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
Gr.nmap Sign -> Set IRI
Sign.owlClasses (Gr Sign (Int, Map IRI IRI) -> Gr (Set IRI) (Int, Map IRI IRI))
-> Gr Sign (Int, Map IRI IRI) -> Gr (Set IRI) (Int, Map IRI IRI)
forall a b. (a -> b) -> a -> b
$
                 ((Int, Morphism) -> (Int, Map IRI IRI))
-> Gr Sign (Int, Morphism) -> Gr Sign (Int, Map IRI IRI)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
Gr.emap ((Morphism -> Map IRI IRI) -> (Int, Morphism) -> (Int, Map IRI IRI)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
Data.Bifunctor.second Morphism -> Map IRI IRI
Morphism.owlMap) Gr Sign (Int, Morphism)
graph
      (owlC :: Set IRI
owlC, owlMors :: Map Int (Map IRI IRI)
owlMors) = (Set (IRI, Int), Map Int (Map IRI (IRI, Int)))
-> (Set IRI, Map Int (Map IRI IRI))
forall a.
SymbolName a =>
(Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a))
addIntToSymbols ((Set (IRI, Int), Map Int (Map IRI (IRI, Int)))
 -> (Set IRI, Map Int (Map IRI IRI)))
-> (Set (IRI, Int), Map Int (Map IRI (IRI, Int)))
-> (Set IRI, Map Int (Map IRI IRI))
forall a b. (a -> b) -> a -> b
$ Gr (Set IRI) (Int, Map IRI IRI)
-> (Set (IRI, Int), Map Int (Map IRI (IRI, Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
computeColimitSet Gr (Set IRI) (Int, Map IRI IRI)
owlGraph
      owlR :: Relation IRI IRI
owlR = [(Int, Relation IRI IRI)]
-> Map Int (Map IRI IRI) -> Relation IRI IRI
forall a.
Ord a =>
[(Int, Relation a a)] -> Map Int (Map a a) -> Relation a a
colimitRel ( ((Int, Sign) -> (Int, Relation IRI IRI))
-> [(Int, Sign)] -> [(Int, Relation IRI IRI)]
forall a b. (a -> b) -> [a] -> [b]
map((Sign -> Relation IRI IRI)
-> (Int, Sign) -> (Int, Relation IRI IRI)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Sign -> Relation IRI IRI
owlTaxonomy) ([(Int, Sign)] -> [(Int, Relation IRI IRI)])
-> [(Int, Sign)] -> [(Int, Relation IRI IRI)]
forall a b. (a -> b) -> a -> b
$ Gr Sign (Int, Morphism) -> [(Int, Sign)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
Gr.labNodes Gr Sign (Int, Morphism)
graph) Map Int (Map IRI IRI)
owlMors
      graph1 :: Gr (Set IRI) (Int, Map IRI IRI)
graph1 = (Sign -> Set IRI)
-> Gr Sign (Int, Map IRI IRI) -> Gr (Set IRI) (Int, Map IRI IRI)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
Gr.nmap ((ResolvedNode -> IRI) -> Set ResolvedNode -> Set IRI
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ResolvedNode -> IRI
Sign.resolvedNeSyId (Set ResolvedNode -> Set IRI)
-> (Sign -> Set ResolvedNode) -> Sign -> Set IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set ResolvedNode
Sign.nodes) (Gr Sign (Int, Map IRI IRI) -> Gr (Set IRI) (Int, Map IRI IRI))
-> Gr Sign (Int, Map IRI IRI) -> Gr (Set IRI) (Int, Map IRI IRI)
forall a b. (a -> b) -> a -> b
$
               ((Int, Morphism) -> (Int, Map IRI IRI))
-> Gr Sign (Int, Morphism) -> Gr Sign (Int, Map IRI IRI)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
Gr.emap ((Morphism -> Map IRI IRI) -> (Int, Morphism) -> (Int, Map IRI IRI)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Morphism -> Map IRI IRI
Morphism.morphism2TokenMap) Gr Sign (Int, Morphism)
graph
      (nodeSet :: Set IRI
nodeSet, maps :: Map Int (Map IRI IRI)
maps) = (Set (IRI, Int), Map Int (Map IRI (IRI, Int)))
-> (Set IRI, Map Int (Map IRI IRI))
forall a.
SymbolName a =>
(Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a))
addIntToSymbols ((Set (IRI, Int), Map Int (Map IRI (IRI, Int)))
 -> (Set IRI, Map Int (Map IRI IRI)))
-> (Set (IRI, Int), Map Int (Map IRI (IRI, Int)))
-> (Set IRI, Map Int (Map IRI IRI))
forall a b. (a -> b) -> a -> b
$ Gr (Set IRI) (Int, Map IRI IRI)
-> (Set (IRI, Int), Map Int (Map IRI (IRI, Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
computeColimitSet Gr (Set IRI) (Int, Map IRI IRI)
graph1
  Set ResolvedNode
resSet <- (Set ResolvedNode -> IRI -> Result (Set ResolvedNode))
-> Set ResolvedNode -> Set IRI -> Result (Set ResolvedNode)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\aSet :: Set ResolvedNode
aSet aNode :: IRI
aNode -> do
                        let labSet :: Set IRI
labSet = (ResolvedNode -> IRI) -> Set ResolvedNode -> Set IRI
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ResolvedNode -> IRI
Sign.resolvedOTerm (Set ResolvedNode -> Set IRI) -> Set ResolvedNode -> Set IRI
forall a b. (a -> b) -> a -> b
$
                                     [(Int, Set ResolvedNode)]
-> Map Int (Map IRI IRI) -> IRI -> Set ResolvedNode
allLabels (((Int, Sign) -> (Int, Set ResolvedNode))
-> [(Int, Sign)] -> [(Int, Set ResolvedNode)]
forall a b. (a -> b) -> [a] -> [b]
map ((Sign -> Set ResolvedNode)
-> (Int, Sign) -> (Int, Set ResolvedNode)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Sign -> Set ResolvedNode
nodes) ([(Int, Sign)] -> [(Int, Set ResolvedNode)])
-> [(Int, Sign)] -> [(Int, Set ResolvedNode)]
forall a b. (a -> b) -> a -> b
$ Gr Sign (Int, Morphism) -> [(Int, Sign)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
Gr.labNodes Gr Sign (Int, Morphism)
graph) Map Int (Map IRI IRI)
maps IRI
aNode
                        case Relation IRI IRI -> Set IRI -> Maybe IRI
forall a. (Ord a, Show a) => Relation a a -> Set a -> Maybe a
computeGLB Relation IRI IRI
owlR Set IRI
labSet of
                          Nothing -> String -> Result (Set ResolvedNode)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "couldn't compute greatest lower bound"
                          Just glb :: IRI
glb -> Set ResolvedNode -> Result (Set ResolvedNode)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set ResolvedNode -> Result (Set ResolvedNode))
-> Set ResolvedNode -> Result (Set ResolvedNode)
forall a b. (a -> b) -> a -> b
$ ResolvedNode -> Set ResolvedNode -> Set ResolvedNode
forall a. Ord a => a -> Set a -> Set a
Set.insert (IRI -> IRI -> Range -> ResolvedNode
ResolvedNode IRI
glb IRI
aNode Range
Id.nullRange) Set ResolvedNode
aSet
                     ) Set ResolvedNode
forall a. Set a
Set.empty Set IRI
nodeSet
  Map Int (Map ResolvedNode ResolvedNode)
nMaps <- (Map Int (Map ResolvedNode ResolvedNode)
 -> (Int, Sign) -> Result (Map Int (Map ResolvedNode ResolvedNode)))
-> Map Int (Map ResolvedNode ResolvedNode)
-> [(Int, Sign)]
-> Result (Map Int (Map ResolvedNode ResolvedNode))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\f :: Map Int (Map ResolvedNode ResolvedNode)
f (i :: Int
i, sig :: Sign
sig) -> do
                    let fi :: Map IRI IRI
fi = Map IRI IRI -> Int -> Map Int (Map IRI IRI) -> Map IRI IRI
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map IRI IRI
forall a. HasCallStack => String -> a
error "missing morphism") Int
i Map Int (Map IRI IRI)
maps
                    Map ResolvedNode ResolvedNode
gi <- Set ResolvedNode
-> Set ResolvedNode
-> Map IRI IRI
-> Result (Map ResolvedNode ResolvedNode)
Morphism.tokenMap2NodeMap (Sign -> Set ResolvedNode
Sign.nodes Sign
sig) Set ResolvedNode
resSet Map IRI IRI
fi
                    Map Int (Map ResolvedNode ResolvedNode)
-> Result (Map Int (Map ResolvedNode ResolvedNode))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int (Map ResolvedNode ResolvedNode)
 -> Result (Map Int (Map ResolvedNode ResolvedNode)))
-> Map Int (Map ResolvedNode ResolvedNode)
-> Result (Map Int (Map ResolvedNode ResolvedNode))
forall a b. (a -> b) -> a -> b
$ Int
-> Map ResolvedNode ResolvedNode
-> Map Int (Map ResolvedNode ResolvedNode)
-> Map Int (Map ResolvedNode ResolvedNode)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
i Map ResolvedNode ResolvedNode
gi Map Int (Map ResolvedNode ResolvedNode)
f
                  )
           Map Int (Map ResolvedNode ResolvedNode)
forall k a. Map k a
Map.empty ([(Int, Sign)] -> Result (Map Int (Map ResolvedNode ResolvedNode)))
-> [(Int, Sign)]
-> Result (Map Int (Map ResolvedNode ResolvedNode))
forall a b. (a -> b) -> a -> b
$ Gr Sign (Int, Morphism) -> [(Int, Sign)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
Gr.labNodes Gr Sign (Int, Morphism)
graph
  let edgesC :: Relation ResolvedNode ResolvedNode
edgesC = [(Int, Relation ResolvedNode ResolvedNode)]
-> Map Int (Map ResolvedNode ResolvedNode)
-> Relation ResolvedNode ResolvedNode
forall a.
Ord a =>
[(Int, Relation a a)] -> Map Int (Map a a) -> Relation a a
colimitRel ( ((Int, Sign) -> (Int, Relation ResolvedNode ResolvedNode))
-> [(Int, Sign)] -> [(Int, Relation ResolvedNode ResolvedNode)]
forall a b. (a -> b) -> [a] -> [b]
map((Sign -> Relation ResolvedNode ResolvedNode)
-> (Int, Sign) -> (Int, Relation ResolvedNode ResolvedNode)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Sign -> Relation ResolvedNode ResolvedNode
edges) ([(Int, Sign)] -> [(Int, Relation ResolvedNode ResolvedNode)])
-> [(Int, Sign)] -> [(Int, Relation ResolvedNode ResolvedNode)]
forall a b. (a -> b) -> a -> b
$ Gr Sign (Int, Morphism) -> [(Int, Sign)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
Gr.labNodes Gr Sign (Int, Morphism)
graph) Map Int (Map ResolvedNode ResolvedNode)
nMaps
      colimSig :: Sign
colimSig = Sign :: Set IRI
-> Relation IRI IRI
-> Set ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Map IRI IRI
-> Sign
Sign{ owlClasses :: Set IRI
owlClasses = Set IRI
owlC
                     , owlTaxonomy :: Relation IRI IRI
owlTaxonomy = Relation IRI IRI
owlR
                     , nodes :: Set ResolvedNode
nodes = Set ResolvedNode
resSet
                     , edges :: Relation ResolvedNode ResolvedNode
edges = Relation ResolvedNode ResolvedNode
edgesC
                     , idMap :: Map IRI IRI
idMap = Set ResolvedNode -> Map IRI IRI
nesyIdMap Set ResolvedNode
resSet}
      colimMors :: Map Int Morphism
colimMors = [(Int, Morphism)] -> Map Int Morphism
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Morphism)] -> Map Int Morphism)
-> [(Int, Morphism)] -> Map Int Morphism
forall a b. (a -> b) -> a -> b
$
                  ((Int, Sign) -> (Int, Morphism))
-> [(Int, Sign)] -> [(Int, Morphism)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i :: Int
i, sig :: Sign
sig) -> let oi :: Map IRI IRI
oi = Map IRI IRI -> Int -> Map Int (Map IRI IRI) -> Map IRI IRI
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map IRI IRI
forall a. HasCallStack => String -> a
error "owl map") Int
i Map Int (Map IRI IRI)
owlMors
                                        ni :: Map ResolvedNode ResolvedNode
ni = Map ResolvedNode ResolvedNode
-> Int
-> Map Int (Map ResolvedNode ResolvedNode)
-> Map ResolvedNode ResolvedNode
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map ResolvedNode ResolvedNode
forall a. HasCallStack => String -> a
error "node map") Int
i Map Int (Map ResolvedNode ResolvedNode)
nMaps
                                   in (Int
i, Sign
-> Sign -> Map IRI IRI -> Map ResolvedNode ResolvedNode -> Morphism
Morphism.Morphism Sign
sig Sign
colimSig Map IRI IRI
oi Map ResolvedNode ResolvedNode
ni) ) ([(Int, Sign)] -> [(Int, Morphism)])
-> [(Int, Sign)] -> [(Int, Morphism)]
forall a b. (a -> b) -> a -> b
$ Gr Sign (Int, Morphism) -> [(Int, Sign)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
Gr.labNodes Gr Sign (Int, Morphism)
graph
  (Sign, Map Int Morphism) -> Result (Sign, Map Int Morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
colimSig, Map Int Morphism
colimMors)

nextGenId :: Sign.Sign -> Int
nextGenId :: Sign -> Int
nextGenId sig :: Sign
sig = (ResolvedNode -> Int -> Int) -> Int -> Set ResolvedNode -> Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\n :: ResolvedNode
n genId :: Int
genId -> Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
genId (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ do
      Int
genId' <- ResolvedNode -> Maybe Int
genIdFromNode ResolvedNode
n
      Int -> Maybe Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ if Int
genId' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
genId then Int
genId' else Int
genId
    ) 0 (Sign -> Set ResolvedNode
Sign.nodes Sign
sig) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
  where
    genIdFromNode :: Sign.ResolvedNode -> Maybe Int
    genIdFromNode :: ResolvedNode -> Maybe Int
genIdFromNode n :: ResolvedNode
n = do
      String
num <- String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix (String
Id.genNamePrefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ "nesy") (String -> Maybe String)
-> (ResolvedNode -> String) -> ResolvedNode -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> String
iFragment (IRI -> String) -> (ResolvedNode -> IRI) -> ResolvedNode -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResolvedNode -> IRI
Sign.resolvedNeSyId (ResolvedNode -> Maybe String) -> ResolvedNode -> Maybe String
forall a b. (a -> b) -> a -> b
$ ResolvedNode
n
      String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
num