{-# 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