{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./NeSyPatterns/Sign.hs
Description :  Signatures for syntax for neural-symbolic patterns
Copyright   :  (c) Till Mossakowski, Uni Magdeburg 2022
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till.mossakowski@ovgu.de
Stability   :  experimental
Portability :  portable

Definition of signatures for neural-symbolic patterns
-}

module NeSyPatterns.Sign
    (Sign (..)                      -- Signatures6
    , ResolvedNode(..)
    , resolved2Node
    , findNodeId
    , nesyIdMap
    , pretty                        -- pretty printing
    , isLegalSignature              -- is a signature ok?
    , addToSig                      -- adds an id to the given Signature
    , addEdgeToSig                  -- adds an edge to the given signature
    , addEdgeToSig'                 -- adds an edge and its nodes to the given signature
    , unite                         -- union of signatures
    , emptySig                      -- empty signature
    , isSubSigOf                    -- is subsignature?
    , sigDiff                       -- Difference of Signatures
    , sigUnion                      -- Union for Logic.Logic
    , nesyIds                       -- extracts the ids of all nodes of a signature
    ) where

import Data.Data
import Data.List as List
import qualified Data.Set as Set
import qualified Data.Relation as Rel
import qualified Data.Map as Map

import Common.Id
import Common.Result
import Common.Doc
import Common.DocUtils
import Common.SetColimit
import Common.IRI
import Common.Keywords

import NeSyPatterns.AS
import NeSyPatterns.Print()

import OWL2.AS
import OWL2.Pretty


data ResolvedNode = ResolvedNode {
    ResolvedNode -> IRI
resolvedOTerm :: IRI,
    ResolvedNode -> IRI
resolvedNeSyId :: IRI,
    ResolvedNode -> Range
resolvedNodeRange :: Range
  } deriving (Int -> ResolvedNode -> ShowS
[ResolvedNode] -> ShowS
ResolvedNode -> String
(Int -> ResolvedNode -> ShowS)
-> (ResolvedNode -> String)
-> ([ResolvedNode] -> ShowS)
-> Show ResolvedNode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ResolvedNode] -> ShowS
$cshowList :: [ResolvedNode] -> ShowS
show :: ResolvedNode -> String
$cshow :: ResolvedNode -> String
showsPrec :: Int -> ResolvedNode -> ShowS
$cshowsPrec :: Int -> ResolvedNode -> ShowS
Show, ResolvedNode -> ResolvedNode -> Bool
(ResolvedNode -> ResolvedNode -> Bool)
-> (ResolvedNode -> ResolvedNode -> Bool) -> Eq ResolvedNode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ResolvedNode -> ResolvedNode -> Bool
$c/= :: ResolvedNode -> ResolvedNode -> Bool
== :: ResolvedNode -> ResolvedNode -> Bool
$c== :: ResolvedNode -> ResolvedNode -> Bool
Eq, Eq ResolvedNode
Eq ResolvedNode =>
(ResolvedNode -> ResolvedNode -> Ordering)
-> (ResolvedNode -> ResolvedNode -> Bool)
-> (ResolvedNode -> ResolvedNode -> Bool)
-> (ResolvedNode -> ResolvedNode -> Bool)
-> (ResolvedNode -> ResolvedNode -> Bool)
-> (ResolvedNode -> ResolvedNode -> ResolvedNode)
-> (ResolvedNode -> ResolvedNode -> ResolvedNode)
-> Ord ResolvedNode
ResolvedNode -> ResolvedNode -> Bool
ResolvedNode -> ResolvedNode -> Ordering
ResolvedNode -> ResolvedNode -> ResolvedNode
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 :: ResolvedNode -> ResolvedNode -> ResolvedNode
$cmin :: ResolvedNode -> ResolvedNode -> ResolvedNode
max :: ResolvedNode -> ResolvedNode -> ResolvedNode
$cmax :: ResolvedNode -> ResolvedNode -> ResolvedNode
>= :: ResolvedNode -> ResolvedNode -> Bool
$c>= :: ResolvedNode -> ResolvedNode -> Bool
> :: ResolvedNode -> ResolvedNode -> Bool
$c> :: ResolvedNode -> ResolvedNode -> Bool
<= :: ResolvedNode -> ResolvedNode -> Bool
$c<= :: ResolvedNode -> ResolvedNode -> Bool
< :: ResolvedNode -> ResolvedNode -> Bool
$c< :: ResolvedNode -> ResolvedNode -> Bool
compare :: ResolvedNode -> ResolvedNode -> Ordering
$ccompare :: ResolvedNode -> ResolvedNode -> Ordering
$cp1Ord :: Eq ResolvedNode
Ord, Typeable, Typeable ResolvedNode
Constr
DataType
Typeable ResolvedNode =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ResolvedNode -> c ResolvedNode)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ResolvedNode)
-> (ResolvedNode -> Constr)
-> (ResolvedNode -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ResolvedNode))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ResolvedNode))
-> ((forall b. Data b => b -> b) -> ResolvedNode -> ResolvedNode)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ResolvedNode -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ResolvedNode -> r)
-> (forall u. (forall d. Data d => d -> u) -> ResolvedNode -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ResolvedNode -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode)
-> Data ResolvedNode
ResolvedNode -> Constr
ResolvedNode -> DataType
(forall b. Data b => b -> b) -> ResolvedNode -> ResolvedNode
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ResolvedNode -> c ResolvedNode
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ResolvedNode
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) -> ResolvedNode -> u
forall u. (forall d. Data d => d -> u) -> ResolvedNode -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ResolvedNode -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ResolvedNode -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ResolvedNode
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ResolvedNode -> c ResolvedNode
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ResolvedNode)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ResolvedNode)
$cResolvedNode :: Constr
$tResolvedNode :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode
gmapMp :: (forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode
gmapM :: (forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ResolvedNode -> m ResolvedNode
gmapQi :: Int -> (forall d. Data d => d -> u) -> ResolvedNode -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ResolvedNode -> u
gmapQ :: (forall d. Data d => d -> u) -> ResolvedNode -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ResolvedNode -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ResolvedNode -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ResolvedNode -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ResolvedNode -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ResolvedNode -> r
gmapT :: (forall b. Data b => b -> b) -> ResolvedNode -> ResolvedNode
$cgmapT :: (forall b. Data b => b -> b) -> ResolvedNode -> ResolvedNode
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ResolvedNode)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ResolvedNode)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ResolvedNode)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ResolvedNode)
dataTypeOf :: ResolvedNode -> DataType
$cdataTypeOf :: ResolvedNode -> DataType
toConstr :: ResolvedNode -> Constr
$ctoConstr :: ResolvedNode -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ResolvedNode
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ResolvedNode
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ResolvedNode -> c ResolvedNode
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ResolvedNode -> c ResolvedNode
$cp1Data :: Typeable ResolvedNode
Data)

instance SymbolName ResolvedNode where
  addString :: (ResolvedNode, String) -> ResolvedNode
addString (ResolvedNode t1 :: IRI
t1 t2 :: IRI
t2 r :: Range
r, s :: String
s) = IRI -> IRI -> Range -> ResolvedNode
ResolvedNode IRI
t1 (String -> IRI -> IRI
addSuffixToIRI String
s IRI
t2) Range
r

instance Pretty ResolvedNode where
  pretty :: ResolvedNode -> Doc
pretty (ResolvedNode o :: IRI
o i :: IRI
i r :: Range
r) = Node -> Doc
forall a. Pretty a => a -> Doc
pretty (Node -> Doc) -> Node -> Doc
forall a b. (a -> b) -> a -> b
$ IRI -> Maybe IRI -> Range -> Node
Node IRI
o (IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
i) Range
r

instance GetRange ResolvedNode where
  getRange :: ResolvedNode -> Range
getRange = Range -> ResolvedNode -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: ResolvedNode -> [Pos]
rangeSpan x :: ResolvedNode
x = case ResolvedNode
x of
    ResolvedNode a :: IRI
a b :: IRI
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [IRI -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan IRI
a, IRI -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan IRI
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

{- | Datatype for propositional Signatures
Signatures are graphs over nodes from the abstract syntax -}
data Sign = Sign { Sign -> Set IRI
owlClasses :: Set.Set IRI,
                   Sign -> Relation IRI IRI
owlTaxonomy :: Rel.Relation IRI IRI,
                   Sign -> Set ResolvedNode
nodes :: Set.Set ResolvedNode,
                   Sign -> Relation ResolvedNode ResolvedNode
edges :: Rel.Relation ResolvedNode ResolvedNode,
                   Sign -> Map IRI IRI
idMap :: Map.Map IRI IRI }
  deriving (Int -> Sign -> ShowS
[Sign] -> ShowS
Sign -> String
(Int -> Sign -> ShowS)
-> (Sign -> String) -> ([Sign] -> ShowS) -> Show Sign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sign] -> ShowS
$cshowList :: [Sign] -> ShowS
show :: Sign -> String
$cshow :: Sign -> String
showsPrec :: Int -> Sign -> ShowS
$cshowsPrec :: Int -> Sign -> ShowS
Show, Sign -> Sign -> Bool
(Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sign -> Sign -> Bool
$c/= :: Sign -> Sign -> Bool
== :: Sign -> Sign -> Bool
$c== :: Sign -> Sign -> Bool
Eq, Eq Sign
Eq Sign =>
(Sign -> Sign -> Ordering)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Sign)
-> (Sign -> Sign -> Sign)
-> Ord Sign
Sign -> Sign -> Bool
Sign -> Sign -> Ordering
Sign -> Sign -> Sign
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 :: Sign -> Sign -> Sign
$cmin :: Sign -> Sign -> Sign
max :: Sign -> Sign -> Sign
$cmax :: Sign -> Sign -> Sign
>= :: Sign -> Sign -> Bool
$c>= :: Sign -> Sign -> Bool
> :: Sign -> Sign -> Bool
$c> :: Sign -> Sign -> Bool
<= :: Sign -> Sign -> Bool
$c<= :: Sign -> Sign -> Bool
< :: Sign -> Sign -> Bool
$c< :: Sign -> Sign -> Bool
compare :: Sign -> Sign -> Ordering
$ccompare :: Sign -> Sign -> Ordering
$cp1Ord :: Eq Sign
Ord, Typeable)

instance Pretty Sign where
    pretty :: Sign -> Doc
pretty = Sign -> Doc
printSign

findNodeId :: IRI -> Set.Set ResolvedNode -> Set.Set ResolvedNode
findNodeId :: IRI -> Set ResolvedNode -> Set ResolvedNode
findNodeId t :: IRI
t = (ResolvedNode -> Bool) -> Set ResolvedNode -> Set ResolvedNode
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(ResolvedNode _ t1 :: IRI
t1 _) -> IRI
t IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
t1 )

nesyIds :: Sign -> Set.Set IRI
nesyIds :: Sign -> Set IRI
nesyIds = (ResolvedNode -> IRI) -> Set ResolvedNode -> Set IRI
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ResolvedNode -> IRI
resolvedNeSyId (Set ResolvedNode -> Set IRI)
-> (Sign -> Set ResolvedNode) -> Sign -> Set IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set ResolvedNode
nodes

nesyIdMap :: Set.Set ResolvedNode -> Map.Map IRI IRI
nesyIdMap :: Set ResolvedNode -> Map IRI IRI
nesyIdMap ns :: Set ResolvedNode
ns = [(IRI, IRI)] -> Map IRI IRI
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(IRI
i, IRI
o) | ResolvedNode o :: IRI
o i :: IRI
i _ <- Set ResolvedNode -> [ResolvedNode]
forall a. Set a -> [a]
Set.toList Set ResolvedNode
ns]

resolved2Node :: ResolvedNode -> Node
resolved2Node :: ResolvedNode -> Node
resolved2Node (ResolvedNode t :: IRI
t i :: IRI
i r :: Range
r) = IRI -> Maybe IRI -> Range -> Node
Node IRI
t (IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
i) Range
r

-- | Builds the owl2 ontology from a signature
getOntology :: Sign -> OntologyDocument
getOntology :: Sign -> OntologyDocument
getOntology s :: Sign
s = let
    decls :: [Axiom]
decls = AxiomAnnotations -> Entity -> Axiom
Declaration [] (Entity -> Axiom) -> (IRI -> Entity) -> IRI -> Axiom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> IRI -> Entity
mkEntity EntityType
Class (IRI -> Axiom) -> [IRI] -> [Axiom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set IRI -> [IRI]
forall a. Set a -> [a]
Set.toList (Sign -> Set IRI
owlClasses Sign
s)
    subClasses :: [ClassAxiom]
subClasses = ((IRI, IRI) -> ClassAxiom) -> [(IRI, IRI)] -> [ClassAxiom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a :: IRI
a,b :: IRI
b) -> AxiomAnnotations
-> SubClassExpression -> SubClassExpression -> ClassAxiom
SubClassOf [] (IRI -> SubClassExpression
Expression IRI
a) (IRI -> SubClassExpression
Expression IRI
b)) ([(IRI, IRI)] -> [ClassAxiom]) -> [(IRI, IRI)] -> [ClassAxiom]
forall a b. (a -> b) -> a -> b
$ Relation IRI IRI -> [(IRI, IRI)]
forall a b. Relation a b -> [(a, b)]
Rel.toList (Sign -> Relation IRI IRI
owlTaxonomy Sign
s)
    subClassAxs :: [Axiom]
subClassAxs = ClassAxiom -> Axiom
ClassAxiom (ClassAxiom -> Axiom) -> [ClassAxiom] -> [Axiom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ClassAxiom]
subClasses
    axs :: [Axiom]
axs = [Axiom]
decls [Axiom] -> [Axiom] -> [Axiom]
forall a. [a] -> [a] -> [a]
++ [Axiom]
subClassAxs
  in OntologyDocument
emptyOntologyDoc { ontology :: Ontology
ontology = Ontology
emptyOntology { axioms :: [Axiom]
axioms = [Axiom]
axs}}

{- | determines whether a signature is vaild -}
isLegalSignature :: Sign -> Bool
isLegalSignature :: Sign -> Bool
isLegalSignature s :: Sign
s =
  Relation ResolvedNode ResolvedNode -> Set ResolvedNode
forall a b. Relation a b -> Set a
Rel.dom (Sign -> Relation ResolvedNode ResolvedNode
edges Sign
s) Set ResolvedNode -> Set ResolvedNode -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Sign -> Set ResolvedNode
nodes Sign
s
  Bool -> Bool -> Bool
&& Relation ResolvedNode ResolvedNode -> Set ResolvedNode
forall a b. Relation a b -> Set b
Rel.ran (Sign -> Relation ResolvedNode ResolvedNode
edges Sign
s) Set ResolvedNode -> Set ResolvedNode -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Sign -> Set ResolvedNode
nodes Sign
s

-- | pretty printin for edge e.g. tuple (ResolvedNode, ResolvedNode)
printEdge :: (ResolvedNode, ResolvedNode) -> Doc
printEdge :: (ResolvedNode, ResolvedNode) -> Doc
printEdge (node1 :: ResolvedNode
node1, node2 :: ResolvedNode
node2) = ResolvedNode -> Doc
forall a. Pretty a => a -> Doc
pretty ResolvedNode
node1 Doc -> Doc -> Doc
<+> String -> Doc
text "->" Doc -> Doc -> Doc
<+> ResolvedNode -> Doc
forall a. Pretty a => a -> Doc
pretty ResolvedNode
node2 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
semi
  -- (fsep . punctuate (text " ->") $ map pretty [node1, node2]) <> semi

-- | pretty printing for Signatures
printSign :: Sign -> Doc
printSign :: Sign -> Doc
printSign s :: Sign
s = String -> Doc
keyword String
dataS Doc -> Doc -> Doc
<+> (Doc -> Doc
specBraces (Doc -> Doc) -> (Sign -> Doc) -> Sign -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OntologyDocument -> Doc
toDocAsMS (OntologyDocument -> Doc)
-> (Sign -> OntologyDocument) -> Sign -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> OntologyDocument
getOntology (Sign -> Doc) -> Sign -> Doc
forall a b. (a -> b) -> a -> b
$ Sign
s) Doc -> Doc -> Doc
$+$
    ([Doc] -> Doc
vcat ([Doc] -> Doc) -> (Sign -> [Doc]) -> Sign -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ResolvedNode, ResolvedNode) -> Doc)
-> [(ResolvedNode, ResolvedNode)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ResolvedNode, ResolvedNode) -> Doc
printEdge ([(ResolvedNode, ResolvedNode)] -> [Doc])
-> (Sign -> [(ResolvedNode, ResolvedNode)]) -> Sign -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relation ResolvedNode ResolvedNode
-> [(ResolvedNode, ResolvedNode)]
forall a b. Relation a b -> [(a, b)]
Rel.toList (Relation ResolvedNode ResolvedNode
 -> [(ResolvedNode, ResolvedNode)])
-> (Sign -> Relation ResolvedNode ResolvedNode)
-> Sign
-> [(ResolvedNode, ResolvedNode)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Relation ResolvedNode ResolvedNode
edges (Sign -> Doc) -> Sign -> Doc
forall a b. (a -> b) -> a -> b
$ Sign
s) Doc -> Doc -> Doc
$+$
    ([Doc] -> Doc
vcat ([Doc] -> Doc)
-> (Set ResolvedNode -> [Doc]) -> Set ResolvedNode -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ResolvedNode -> Doc) -> [ResolvedNode] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
semi) (Doc -> Doc) -> (ResolvedNode -> Doc) -> ResolvedNode -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResolvedNode -> Doc
forall a. Pretty a => a -> Doc
pretty) ([ResolvedNode] -> [Doc])
-> (Set ResolvedNode -> [ResolvedNode])
-> Set ResolvedNode
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ResolvedNode -> [ResolvedNode]
forall a. Set a -> [a]
Set.toList (Set ResolvedNode -> Doc) -> Set ResolvedNode -> Doc
forall a b. (a -> b) -> a -> b
$ (Sign -> Set ResolvedNode
nodes Sign
s Set ResolvedNode -> Set ResolvedNode -> Set ResolvedNode
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set ResolvedNode -> Set ResolvedNode -> Set ResolvedNode
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Relation ResolvedNode ResolvedNode -> Set ResolvedNode
forall a b. Relation a b -> Set a
Rel.dom (Relation ResolvedNode ResolvedNode -> Set ResolvedNode)
-> (Sign -> Relation ResolvedNode ResolvedNode)
-> Sign
-> Set ResolvedNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Relation ResolvedNode ResolvedNode
edges (Sign -> Set ResolvedNode) -> Sign -> Set ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign
s) (Relation ResolvedNode ResolvedNode -> Set ResolvedNode
forall a b. Relation a b -> Set b
Rel.ran (Relation ResolvedNode ResolvedNode -> Set ResolvedNode)
-> (Sign -> Relation ResolvedNode ResolvedNode)
-> Sign
-> Set ResolvedNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Relation ResolvedNode ResolvedNode
edges (Sign -> Set ResolvedNode) -> Sign -> Set ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign
s)))

-- | Adds a node to the signature
addToSig :: Sign -> ResolvedNode -> Sign
addToSig :: Sign -> ResolvedNode -> Sign
addToSig sig :: Sign
sig node :: ResolvedNode
node = Sign
sig {nodes :: Set ResolvedNode
nodes = ResolvedNode -> Set ResolvedNode -> Set ResolvedNode
forall a. Ord a => a -> Set a -> Set a
Set.insert ResolvedNode
node (Set ResolvedNode -> Set ResolvedNode)
-> Set ResolvedNode -> Set ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign -> Set ResolvedNode
nodes Sign
sig}

-- | Adds an edge to the signature. Nodes are not added. See addEdgeToSig' 
addEdgeToSig :: Sign -> (ResolvedNode, ResolvedNode) -> Sign
addEdgeToSig :: Sign -> (ResolvedNode, ResolvedNode) -> Sign
addEdgeToSig sig :: Sign
sig (f :: ResolvedNode
f, t :: ResolvedNode
t) = Sign
sig {edges :: Relation ResolvedNode ResolvedNode
edges = ResolvedNode
-> ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
forall a b.
(Ord a, Ord b) =>
a -> b -> Relation a b -> Relation a b
Rel.insert ResolvedNode
f ResolvedNode
t (Relation ResolvedNode ResolvedNode
 -> Relation ResolvedNode ResolvedNode)
-> Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign -> Relation ResolvedNode ResolvedNode
edges Sign
sig}

-- | Adds an edge with its nodes to the signature
addEdgeToSig' :: Sign -> (ResolvedNode, ResolvedNode) -> Sign
addEdgeToSig' :: Sign -> (ResolvedNode, ResolvedNode) -> Sign
addEdgeToSig' sig :: Sign
sig (f :: ResolvedNode
f, t :: ResolvedNode
t) = Sign -> ResolvedNode -> Sign
addToSig (Sign -> ResolvedNode -> Sign
addToSig (Sign
sig {edges :: Relation ResolvedNode ResolvedNode
edges = ResolvedNode
-> ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
forall a b.
(Ord a, Ord b) =>
a -> b -> Relation a b -> Relation a b
Rel.insert ResolvedNode
f ResolvedNode
t (Relation ResolvedNode ResolvedNode
 -> Relation ResolvedNode ResolvedNode)
-> Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign -> Relation ResolvedNode ResolvedNode
edges Sign
sig}) ResolvedNode
f) ResolvedNode
t

-- | Union of signatures
unite :: Sign -> Sign -> Sign
unite :: Sign -> Sign -> Sign
unite sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Sign :: Set IRI
-> Relation IRI IRI
-> Set ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Map IRI IRI
-> Sign
Sign {owlClasses :: Set IRI
owlClasses = Set IRI -> Set IRI -> Set IRI
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign -> Set IRI
owlClasses Sign
sig1) (Set IRI -> Set IRI) -> Set IRI -> Set IRI
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
owlClasses Sign
sig2,
                        owlTaxonomy :: Relation IRI IRI
owlTaxonomy = Relation IRI IRI -> Relation IRI IRI -> Relation IRI IRI
forall a b.
(Ord a, Ord b) =>
Relation a b -> Relation a b -> Relation a b
Rel.union (Sign -> Relation IRI IRI
owlTaxonomy Sign
sig1) (Relation IRI IRI -> Relation IRI IRI)
-> Relation IRI IRI -> Relation IRI IRI
forall a b. (a -> b) -> a -> b
$ Sign -> Relation IRI IRI
owlTaxonomy Sign
sig2,
                        nodes :: Set ResolvedNode
nodes = Set ResolvedNode -> Set ResolvedNode -> Set ResolvedNode
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign -> Set ResolvedNode
nodes Sign
sig1) (Set ResolvedNode -> Set ResolvedNode)
-> Set ResolvedNode -> Set ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign -> Set ResolvedNode
nodes Sign
sig2,
                        idMap :: Map IRI IRI
idMap = Map IRI IRI -> Map IRI IRI -> Map IRI IRI
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Sign -> Map IRI IRI
idMap Sign
sig1) (Map IRI IRI -> Map IRI IRI) -> Map IRI IRI -> Map IRI IRI
forall a b. (a -> b) -> a -> b
$ Sign -> Map IRI IRI
idMap Sign
sig2,
                        edges :: Relation ResolvedNode ResolvedNode
edges = Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
forall a b.
(Ord a, Ord b) =>
Relation a b -> Relation a b -> Relation a b
Rel.union (Sign -> Relation ResolvedNode ResolvedNode
edges Sign
sig1) (Relation ResolvedNode ResolvedNode
 -> Relation ResolvedNode ResolvedNode)
-> Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign -> Relation ResolvedNode ResolvedNode
edges Sign
sig2}

-- | The empty signature
emptySig :: Sign
emptySig :: Sign
emptySig = Sign :: Set IRI
-> Relation IRI IRI
-> Set ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Map IRI IRI
-> Sign
Sign { owlClasses :: Set IRI
owlClasses = Set IRI
forall a. Set a
Set.empty
                , owlTaxonomy :: Relation IRI IRI
owlTaxonomy = Relation IRI IRI
forall a b. Relation a b
Rel.empty
                , nodes :: Set ResolvedNode
nodes = Set ResolvedNode
forall a. Set a
Set.empty
                , edges :: Relation ResolvedNode ResolvedNode
edges = Relation ResolvedNode ResolvedNode
forall a b. Relation a b
Rel.empty
                , idMap :: Map IRI IRI
idMap = Map IRI IRI
forall k a. Map k a
Map.empty}

relToSet :: (Ord a, Ord b) => Rel.Relation a b -> Set.Set (a,b)
relToSet :: Relation a b -> Set (a, b)
relToSet r :: Relation a b
r = [(a, b)] -> Set (a, b)
forall a. Ord a => [a] -> Set a
Set.fromList ([(a, b)] -> Set (a, b)) -> [(a, b)] -> Set (a, b)
forall a b. (a -> b) -> a -> b
$ Relation a b -> [(a, b)]
forall a b. Relation a b -> [(a, b)]
Rel.toList Relation a b
r

-- | Determines if sig1 is subsignature of sig2
isSubSigOf :: Sign -> Sign -> Bool
isSubSigOf :: Sign -> Sign -> Bool
isSubSigOf sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
     Sign -> Set IRI
owlClasses Sign
sig1 Set IRI -> Set IRI -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Sign -> Set IRI
owlClasses Sign
sig2
  Bool -> Bool -> Bool
&& Sign -> Set ResolvedNode
nodes Sign
sig1 Set ResolvedNode -> Set ResolvedNode -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Sign -> Set ResolvedNode
nodes Sign
sig2
  Bool -> Bool -> Bool
&& Relation ResolvedNode ResolvedNode
-> Set (ResolvedNode, ResolvedNode)
forall a b. (Ord a, Ord b) => Relation a b -> Set (a, b)
relToSet (Sign -> Relation ResolvedNode ResolvedNode
edges Sign
sig1) Set (ResolvedNode, ResolvedNode)
-> Set (ResolvedNode, ResolvedNode) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Relation ResolvedNode ResolvedNode
-> Set (ResolvedNode, ResolvedNode)
forall a b. (Ord a, Ord b) => Relation a b -> Set (a, b)
relToSet (Sign -> Relation ResolvedNode ResolvedNode
edges Sign
sig2)
  Bool -> Bool -> Bool
&& Relation IRI IRI -> Set (IRI, IRI)
forall a b. (Ord a, Ord b) => Relation a b -> Set (a, b)
relToSet (Sign -> Relation IRI IRI
owlTaxonomy Sign
sig1) Set (IRI, IRI) -> Set (IRI, IRI) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Relation IRI IRI -> Set (IRI, IRI)
forall a b. (Ord a, Ord b) => Relation a b -> Set (a, b)
relToSet (Sign -> Relation IRI IRI
owlTaxonomy Sign
sig2)

relDiff :: (Ord a, Ord b) => Rel.Relation a b -> Rel.Relation a b -> Rel.Relation a b
relDiff :: Relation a b -> Relation a b -> Relation a b
relDiff r1 :: Relation a b
r1 r2 :: Relation a b
r2 = [(a, b)] -> Relation a b
forall a b. (Ord a, Ord b) => [(a, b)] -> Relation a b
Rel.fromList ([(a, b)]
l1 [(a, b)] -> [(a, b)] -> [(a, b)]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [(a, b)]
l2)
   where l1 :: [(a, b)]
l1 = Relation a b -> [(a, b)]
forall a b. Relation a b -> [(a, b)]
Rel.toList Relation a b
r1
         l2 :: [(a, b)]
l2 = Relation a b -> [(a, b)]
forall a b. Relation a b -> [(a, b)]
Rel.toList Relation a b
r2

-- | difference of Signatures
sigDiff :: Sign -> Sign -> Sign
sigDiff :: Sign -> Sign -> Sign
sigDiff sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Sign :: Set IRI
-> Relation IRI IRI
-> Set ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Map IRI IRI
-> Sign
Sign
  {owlClasses :: Set IRI
owlClasses = Set IRI -> Set IRI -> Set IRI
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set IRI
owlClasses Sign
sig1) (Set IRI -> Set IRI) -> Set IRI -> Set IRI
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
owlClasses Sign
sig2,
   owlTaxonomy :: Relation IRI IRI
owlTaxonomy = Relation IRI IRI -> Relation IRI IRI -> Relation IRI IRI
forall a b.
(Ord a, Ord b) =>
Relation a b -> Relation a b -> Relation a b
relDiff (Sign -> Relation IRI IRI
owlTaxonomy Sign
sig1) (Relation IRI IRI -> Relation IRI IRI)
-> Relation IRI IRI -> Relation IRI IRI
forall a b. (a -> b) -> a -> b
$ Sign -> Relation IRI IRI
owlTaxonomy Sign
sig2,
   nodes :: Set ResolvedNode
nodes = Set ResolvedNode -> Set ResolvedNode -> Set ResolvedNode
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set ResolvedNode
nodes Sign
sig1) (Set ResolvedNode -> Set ResolvedNode)
-> Set ResolvedNode -> Set ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign -> Set ResolvedNode
nodes Sign
sig2,
   idMap :: Map IRI IRI
idMap = Map IRI IRI -> Map IRI IRI -> Map IRI IRI
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference (Sign -> Map IRI IRI
idMap Sign
sig1) (Map IRI IRI -> Map IRI IRI) -> Map IRI IRI -> Map IRI IRI
forall a b. (a -> b) -> a -> b
$ Sign -> Map IRI IRI
idMap Sign
sig2,
   edges :: Relation ResolvedNode ResolvedNode
edges = Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
forall a b.
(Ord a, Ord b) =>
Relation a b -> Relation a b -> Relation a b
relDiff (Sign -> Relation ResolvedNode ResolvedNode
edges Sign
sig1) (Relation ResolvedNode ResolvedNode
 -> Relation ResolvedNode ResolvedNode)
-> Relation ResolvedNode ResolvedNode
-> Relation ResolvedNode ResolvedNode
forall a b. (a -> b) -> a -> b
$ Sign -> Relation ResolvedNode ResolvedNode
edges Sign
sig2}

{- | union of Signatures, using Result -}
sigUnion :: Sign -> Sign -> Result Sign
sigUnion :: Sign -> Sign -> Result Sign
sigUnion s1 :: Sign
s1 s2 :: Sign
s2 = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Sign
unite Sign
s1 Sign
s2