{- |
Module      :  ./OWL2/Theorem.hs
Copyright   :  (c) Felix Gabriel Mance
License     :  GPLv2 or higher, see LICENSE.txt

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

Adds the "implied" annotation - for specifying theorems
-}

module OWL2.Theorem where

import Common.IRI
import qualified OWL2.AS as AS
import OWL2.MS

import Data.List

implied :: AS.Annotation
implied :: Annotation
implied = [Annotation] -> AnnotationProperty -> AnnotationValue -> Annotation
AS.Annotation [] (String -> AnnotationProperty
mkIRI "Implied")
  (AnnotationValue -> Annotation)
-> (AnnotationProperty -> AnnotationValue)
-> AnnotationProperty
-> Annotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> AnnotationValue
AS.AnnValLit (Literal -> AnnotationValue)
-> (AnnotationProperty -> Literal)
-> AnnotationProperty
-> AnnotationValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TypedOrUntyped -> Literal
AS.Literal "true" (TypedOrUntyped -> Literal)
-> (AnnotationProperty -> TypedOrUntyped)
-> AnnotationProperty
-> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnotationProperty -> TypedOrUntyped
AS.Typed (AnnotationProperty -> Annotation)
-> AnnotationProperty -> Annotation
forall a b. (a -> b) -> a -> b
$ String -> AnnotationProperty
mkIRI "string"

rmList :: Annotations -> Annotations
rmList :: [Annotation] -> [Annotation]
rmList = (Annotation -> Bool) -> [Annotation] -> [Annotation]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Annotation -> Bool) -> Annotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annotation -> Bool
prove1)

rmImplied :: AS.Axiom -> AS.Axiom
rmImplied :: Axiom -> Axiom
rmImplied ax :: Axiom
ax = case Axiom
ax of
    AS.Declaration anns :: [Annotation]
anns a :: Entity
a -> [Annotation] -> Entity -> Axiom
AS.Declaration ([Annotation] -> [Annotation]
rmList [Annotation]
anns) Entity
a 
    AS.ClassAxiom cax :: ClassAxiom
cax -> case ClassAxiom
cax of
        AS.SubClassOf anns :: [Annotation]
anns a :: SubClassExpression
a b :: SubClassExpression
b -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SubClassExpression -> SubClassExpression -> ClassAxiom
AS.SubClassOf ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SubClassExpression
a SubClassExpression
b 
        AS.EquivalentClasses anns :: [Annotation]
anns a :: [SubClassExpression]
a -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [SubClassExpression] -> ClassAxiom
AS.EquivalentClasses ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  [SubClassExpression]
a 
        AS.DisjointClasses anns :: [Annotation]
anns a :: [SubClassExpression]
a -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [SubClassExpression] -> ClassAxiom
AS.DisjointClasses ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  [SubClassExpression]
a 
        AS.DisjointUnion anns :: [Annotation]
anns a :: AnnotationProperty
a b :: [SubClassExpression]
b -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> [SubClassExpression] -> ClassAxiom
AS.DisjointUnion ([Annotation] -> [Annotation]
rmList [Annotation]
anns) AnnotationProperty
a [SubClassExpression]
b 
    AS.ObjectPropertyAxiom opax :: ObjectPropertyAxiom
opax -> case ObjectPropertyAxiom
opax of
        AS.SubObjectPropertyOf anns :: [Annotation]
anns a :: SubObjectPropertyExpression
a b :: SuperObjectPropertyExpression
b -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SubObjectPropertyExpression
-> SuperObjectPropertyExpression
-> ObjectPropertyAxiom
AS.SubObjectPropertyOf ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SubObjectPropertyExpression
a SuperObjectPropertyExpression
b 
        AS.EquivalentObjectProperties anns :: [Annotation]
anns a :: [SuperObjectPropertyExpression]
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> [SuperObjectPropertyExpression] -> ObjectPropertyAxiom
AS.EquivalentObjectProperties ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  [SuperObjectPropertyExpression]
a 
        AS.DisjointObjectProperties anns :: [Annotation]
anns a :: [SuperObjectPropertyExpression]
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> [SuperObjectPropertyExpression] -> ObjectPropertyAxiom
AS.DisjointObjectProperties ([Annotation] -> [Annotation]
rmList [Annotation]
anns) [SuperObjectPropertyExpression]
a 
        AS.InverseObjectProperties anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: SuperObjectPropertyExpression
b -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> SuperObjectPropertyExpression
-> ObjectPropertyAxiom
AS.InverseObjectProperties ([Annotation] -> [Annotation]
rmList [Annotation]
anns) SuperObjectPropertyExpression
a SuperObjectPropertyExpression
b 
        AS.ObjectPropertyDomain anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: SubClassExpression
b -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> SubClassExpression
-> ObjectPropertyAxiom
AS.ObjectPropertyDomain ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a SubClassExpression
b 
        AS.ObjectPropertyRange anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: SubClassExpression
b -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> SubClassExpression
-> ObjectPropertyAxiom
AS.ObjectPropertyRange ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a SubClassExpression
b 
        AS.FunctionalObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.FunctionalObjectProperty ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.InverseFunctionalObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.InverseFunctionalObjectProperty ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.ReflexiveObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.ReflexiveObjectProperty ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.IrreflexiveObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.IrreflexiveObjectProperty ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.SymmetricObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.SymmetricObjectProperty ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.AsymmetricObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.AsymmetricObjectProperty ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.TransitiveObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.TransitiveObjectProperty ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a 
    AS.DataPropertyAxiom dpax :: DataPropertyAxiom
dpax -> case DataPropertyAxiom
dpax of
        AS.SubDataPropertyOf anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> DataPropertyAxiom
AS.SubDataPropertyOf ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b 
        AS.EquivalentDataProperties anns :: [Annotation]
anns a :: [AnnotationProperty]
a -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [AnnotationProperty] -> DataPropertyAxiom
AS.EquivalentDataProperties ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  [AnnotationProperty]
a 
        AS.DisjointDataProperties anns :: [Annotation]
anns a :: [AnnotationProperty]
a -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [AnnotationProperty] -> DataPropertyAxiom
AS.DisjointDataProperties ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  [AnnotationProperty]
a 
        AS.DataPropertyDomain anns :: [Annotation]
anns a :: AnnotationProperty
a b :: SubClassExpression
b -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> SubClassExpression -> DataPropertyAxiom
AS.DataPropertyDomain ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a SubClassExpression
b 
        AS.DataPropertyRange anns :: [Annotation]
anns a :: AnnotationProperty
a b :: DataRange
b -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> DataRange -> DataPropertyAxiom
AS.DataPropertyRange ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a DataRange
b 
        AS.FunctionalDataProperty anns :: [Annotation]
anns a :: AnnotationProperty
a -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> AnnotationProperty -> DataPropertyAxiom
AS.FunctionalDataProperty ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a 
    AS.DatatypeDefinition anns :: [Annotation]
anns a :: AnnotationProperty
a b :: DataRange
b -> [Annotation] -> AnnotationProperty -> DataRange -> Axiom
AS.DatatypeDefinition ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a DataRange
b 
    AS.HasKey anns :: [Annotation]
anns a :: SubClassExpression
a b :: [SuperObjectPropertyExpression]
b c :: [AnnotationProperty]
c -> [Annotation]
-> SubClassExpression
-> [SuperObjectPropertyExpression]
-> [AnnotationProperty]
-> Axiom
AS.HasKey ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SubClassExpression
a [SuperObjectPropertyExpression]
b [AnnotationProperty]
c 
    AS.Assertion assertion :: Assertion
assertion -> case Assertion
assertion of
        AS.SameIndividual anns :: [Annotation]
anns a :: [AnnotationProperty]
a -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [AnnotationProperty] -> Assertion
AS.SameIndividual ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  [AnnotationProperty]
a 
        AS.DifferentIndividuals anns :: [Annotation]
anns a :: [AnnotationProperty]
a -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [AnnotationProperty] -> Assertion
AS.DifferentIndividuals ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  [AnnotationProperty]
a 
        AS.ClassAssertion anns :: [Annotation]
anns a :: SubClassExpression
a b :: AnnotationProperty
b -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SubClassExpression -> AnnotationProperty -> Assertion
AS.ClassAssertion ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SubClassExpression
a AnnotationProperty
b 
        AS.ObjectPropertyAssertion anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: AnnotationProperty
b c :: AnnotationProperty
c -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> AnnotationProperty
-> AnnotationProperty
-> Assertion
AS.ObjectPropertyAssertion ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a AnnotationProperty
b AnnotationProperty
c 
        AS.NegativeObjectPropertyAssertion anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: AnnotationProperty
b c :: AnnotationProperty
c -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> AnnotationProperty
-> AnnotationProperty
-> Assertion
AS.NegativeObjectPropertyAssertion ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  SuperObjectPropertyExpression
a AnnotationProperty
b AnnotationProperty
c 
        AS.DataPropertyAssertion anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b c :: Literal
c -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> Literal -> Assertion
AS.DataPropertyAssertion ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b Literal
c 
        AS.NegativeDataPropertyAssertion anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b c :: Literal
c -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> Literal -> Assertion
AS.NegativeDataPropertyAssertion ([Annotation] -> [Annotation]
rmList [Annotation]
anns) AnnotationProperty
a AnnotationProperty
b Literal
c 
    AS.AnnotationAxiom annax :: AnnotationAxiom
annax -> case AnnotationAxiom
annax of
        AS.AnnotationAssertion anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationSubject
b c :: AnnotationValue
c -> AnnotationAxiom -> Axiom
AS.AnnotationAxiom (AnnotationAxiom -> Axiom) -> AnnotationAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty
-> AnnotationSubject
-> AnnotationValue
-> AnnotationAxiom
AS.AnnotationAssertion ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a AnnotationSubject
b AnnotationValue
c 
        AS.SubAnnotationPropertyOf anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b -> AnnotationAxiom -> Axiom
AS.AnnotationAxiom (AnnotationAxiom -> Axiom) -> AnnotationAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> AnnotationAxiom
AS.SubAnnotationPropertyOf ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b 
        AS.AnnotationPropertyDomain anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b -> AnnotationAxiom -> Axiom
AS.AnnotationAxiom (AnnotationAxiom -> Axiom) -> AnnotationAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> AnnotationAxiom
AS.AnnotationPropertyDomain ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b 
        AS.AnnotationPropertyRange anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b -> AnnotationAxiom -> Axiom
AS.AnnotationAxiom (AnnotationAxiom -> Axiom) -> AnnotationAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> AnnotationAxiom
AS.AnnotationPropertyRange ([Annotation] -> [Annotation]
rmList [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b 
    AS.Rule rule :: Rule
rule -> case Rule
rule of
        AS.DLSafeRule anns :: [Annotation]
anns a :: Body
a b :: Body
b -> Rule -> Axiom
AS.Rule (Rule -> Axiom) -> Rule -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> Body -> Body -> Rule
AS.DLSafeRule ([Annotation] -> [Annotation]
rmList [Annotation]
anns) Body
a Body
b
        AS.DGRule anns :: [Annotation]
anns a :: DGBody
a b :: DGBody
b -> Rule -> Axiom
AS.Rule (Rule -> Axiom) -> Rule -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> DGBody -> DGBody -> Rule
AS.DGRule ([Annotation] -> [Annotation]
rmList [Annotation]
anns) DGBody
a DGBody
b 
    AS.DGAxiom anns :: [Annotation]
anns a :: AnnotationProperty
a b :: DGNodes
b c :: DGEdges
c d :: [AnnotationProperty]
d -> [Annotation]
-> AnnotationProperty
-> DGNodes
-> DGEdges
-> [AnnotationProperty]
-> Axiom
AS.DGAxiom ([Annotation] -> [Annotation]
rmList [Annotation]
anns) AnnotationProperty
a DGNodes
b DGEdges
c [AnnotationProperty]
d 

addImplied :: AS.Axiom -> AS.Axiom
addImplied :: Axiom -> Axiom
addImplied ax :: Axiom
ax = case Axiom
ax of
    AS.Declaration anns :: [Annotation]
anns a :: Entity
a -> [Annotation] -> Entity -> Axiom
AS.Declaration (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns) Entity
a 
    AS.ClassAxiom cax :: ClassAxiom
cax -> case ClassAxiom
cax of
        AS.SubClassOf anns :: [Annotation]
anns a :: SubClassExpression
a b :: SubClassExpression
b -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SubClassExpression -> SubClassExpression -> ClassAxiom
AS.SubClassOf (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SubClassExpression
a SubClassExpression
b 
        AS.EquivalentClasses anns :: [Annotation]
anns a :: [SubClassExpression]
a -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [SubClassExpression] -> ClassAxiom
AS.EquivalentClasses (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  [SubClassExpression]
a 
        AS.DisjointClasses anns :: [Annotation]
anns a :: [SubClassExpression]
a -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [SubClassExpression] -> ClassAxiom
AS.DisjointClasses (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  [SubClassExpression]
a 
        AS.DisjointUnion anns :: [Annotation]
anns a :: AnnotationProperty
a b :: [SubClassExpression]
b -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> [SubClassExpression] -> ClassAxiom
AS.DisjointUnion (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns) AnnotationProperty
a [SubClassExpression]
b 
    AS.ObjectPropertyAxiom opax :: ObjectPropertyAxiom
opax -> case ObjectPropertyAxiom
opax of
        AS.SubObjectPropertyOf anns :: [Annotation]
anns a :: SubObjectPropertyExpression
a b :: SuperObjectPropertyExpression
b -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SubObjectPropertyExpression
-> SuperObjectPropertyExpression
-> ObjectPropertyAxiom
AS.SubObjectPropertyOf (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SubObjectPropertyExpression
a SuperObjectPropertyExpression
b 
        AS.EquivalentObjectProperties anns :: [Annotation]
anns a :: [SuperObjectPropertyExpression]
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> [SuperObjectPropertyExpression] -> ObjectPropertyAxiom
AS.EquivalentObjectProperties (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  [SuperObjectPropertyExpression]
a 
        AS.DisjointObjectProperties anns :: [Annotation]
anns a :: [SuperObjectPropertyExpression]
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> [SuperObjectPropertyExpression] -> ObjectPropertyAxiom
AS.DisjointObjectProperties (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns) [SuperObjectPropertyExpression]
a 
        AS.InverseObjectProperties anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: SuperObjectPropertyExpression
b -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> SuperObjectPropertyExpression
-> ObjectPropertyAxiom
AS.InverseObjectProperties (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns) SuperObjectPropertyExpression
a SuperObjectPropertyExpression
b 
        AS.ObjectPropertyDomain anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: SubClassExpression
b -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> SubClassExpression
-> ObjectPropertyAxiom
AS.ObjectPropertyDomain (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a SubClassExpression
b 
        AS.ObjectPropertyRange anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: SubClassExpression
b -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> SubClassExpression
-> ObjectPropertyAxiom
AS.ObjectPropertyRange (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a SubClassExpression
b 
        AS.FunctionalObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.FunctionalObjectProperty (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.InverseFunctionalObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.InverseFunctionalObjectProperty (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.ReflexiveObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.ReflexiveObjectProperty (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.IrreflexiveObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.IrreflexiveObjectProperty (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.SymmetricObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.SymmetricObjectProperty (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.AsymmetricObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.AsymmetricObjectProperty (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a 
        AS.TransitiveObjectProperty anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression -> ObjectPropertyAxiom
AS.TransitiveObjectProperty (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a 
    AS.DataPropertyAxiom dpax :: DataPropertyAxiom
dpax -> case DataPropertyAxiom
dpax of
        AS.SubDataPropertyOf anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> DataPropertyAxiom
AS.SubDataPropertyOf (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b 
        AS.EquivalentDataProperties anns :: [Annotation]
anns a :: [AnnotationProperty]
a -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [AnnotationProperty] -> DataPropertyAxiom
AS.EquivalentDataProperties (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  [AnnotationProperty]
a 
        AS.DisjointDataProperties anns :: [Annotation]
anns a :: [AnnotationProperty]
a -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [AnnotationProperty] -> DataPropertyAxiom
AS.DisjointDataProperties (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  [AnnotationProperty]
a 
        AS.DataPropertyDomain anns :: [Annotation]
anns a :: AnnotationProperty
a b :: SubClassExpression
b -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> SubClassExpression -> DataPropertyAxiom
AS.DataPropertyDomain (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a SubClassExpression
b 
        AS.DataPropertyRange anns :: [Annotation]
anns a :: AnnotationProperty
a b :: DataRange
b -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> DataRange -> DataPropertyAxiom
AS.DataPropertyRange (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a DataRange
b 
        AS.FunctionalDataProperty anns :: [Annotation]
anns a :: AnnotationProperty
a -> DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> AnnotationProperty -> DataPropertyAxiom
AS.FunctionalDataProperty (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a 
    AS.DatatypeDefinition anns :: [Annotation]
anns a :: AnnotationProperty
a b :: DataRange
b -> [Annotation] -> AnnotationProperty -> DataRange -> Axiom
AS.DatatypeDefinition (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a DataRange
b 
    AS.HasKey anns :: [Annotation]
anns a :: SubClassExpression
a b :: [SuperObjectPropertyExpression]
b c :: [AnnotationProperty]
c -> [Annotation]
-> SubClassExpression
-> [SuperObjectPropertyExpression]
-> [AnnotationProperty]
-> Axiom
AS.HasKey (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SubClassExpression
a [SuperObjectPropertyExpression]
b [AnnotationProperty]
c 
    AS.Assertion assertion :: Assertion
assertion -> case Assertion
assertion of
        AS.SameIndividual anns :: [Annotation]
anns a :: [AnnotationProperty]
a -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [AnnotationProperty] -> Assertion
AS.SameIndividual (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  [AnnotationProperty]
a 
        AS.DifferentIndividuals anns :: [Annotation]
anns a :: [AnnotationProperty]
a -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [AnnotationProperty] -> Assertion
AS.DifferentIndividuals (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  [AnnotationProperty]
a 
        AS.ClassAssertion anns :: [Annotation]
anns a :: SubClassExpression
a b :: AnnotationProperty
b -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SubClassExpression -> AnnotationProperty -> Assertion
AS.ClassAssertion (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SubClassExpression
a AnnotationProperty
b 
        AS.ObjectPropertyAssertion anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: AnnotationProperty
b c :: AnnotationProperty
c -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> AnnotationProperty
-> AnnotationProperty
-> Assertion
AS.ObjectPropertyAssertion (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a AnnotationProperty
b AnnotationProperty
c 
        AS.NegativeObjectPropertyAssertion anns :: [Annotation]
anns a :: SuperObjectPropertyExpression
a b :: AnnotationProperty
b c :: AnnotationProperty
c -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> SuperObjectPropertyExpression
-> AnnotationProperty
-> AnnotationProperty
-> Assertion
AS.NegativeObjectPropertyAssertion (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  SuperObjectPropertyExpression
a AnnotationProperty
b AnnotationProperty
c 
        AS.DataPropertyAssertion anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b c :: Literal
c -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> Literal -> Assertion
AS.DataPropertyAssertion (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b Literal
c 
        AS.NegativeDataPropertyAssertion anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b c :: Literal
c -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> Literal -> Assertion
AS.NegativeDataPropertyAssertion (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns) AnnotationProperty
a AnnotationProperty
b Literal
c 
    AS.AnnotationAxiom anax :: AnnotationAxiom
anax -> case AnnotationAxiom
anax of
        AS.AnnotationAssertion anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationSubject
b c :: AnnotationValue
c -> AnnotationAxiom -> Axiom
AS.AnnotationAxiom (AnnotationAxiom -> Axiom) -> AnnotationAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty
-> AnnotationSubject
-> AnnotationValue
-> AnnotationAxiom
AS.AnnotationAssertion (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a AnnotationSubject
b AnnotationValue
c 
        AS.SubAnnotationPropertyOf anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b -> AnnotationAxiom -> Axiom
AS.AnnotationAxiom (AnnotationAxiom -> Axiom) -> AnnotationAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> AnnotationAxiom
AS.SubAnnotationPropertyOf (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b 
        AS.AnnotationPropertyDomain anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b -> AnnotationAxiom -> Axiom
AS.AnnotationAxiom (AnnotationAxiom -> Axiom) -> AnnotationAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> AnnotationAxiom
AS.AnnotationPropertyDomain (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b 
        AS.AnnotationPropertyRange anns :: [Annotation]
anns a :: AnnotationProperty
a b :: AnnotationProperty
b -> AnnotationAxiom -> Axiom
AS.AnnotationAxiom (AnnotationAxiom -> Axiom) -> AnnotationAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> AnnotationProperty -> AnnotationProperty -> AnnotationAxiom
AS.AnnotationPropertyRange (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns)  AnnotationProperty
a AnnotationProperty
b
    AS.Rule rule :: Rule
rule -> case Rule
rule of
        AS.DLSafeRule anns :: [Annotation]
anns a :: Body
a b :: Body
b -> Rule -> Axiom
AS.Rule (Rule -> Axiom) -> Rule -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> Body -> Body -> Rule
AS.DLSafeRule (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns) Body
a Body
b
        AS.DGRule anns :: [Annotation]
anns a :: DGBody
a b :: DGBody
b -> Rule -> Axiom
AS.Rule (Rule -> Axiom) -> Rule -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> DGBody -> DGBody -> Rule
AS.DGRule (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns) DGBody
a DGBody
b
    AS.DGAxiom anns :: [Annotation]
anns a :: AnnotationProperty
a b :: DGNodes
b c :: DGEdges
c d :: [AnnotationProperty]
d -> [Annotation]
-> AnnotationProperty
-> DGNodes
-> DGEdges
-> [AnnotationProperty]
-> Axiom
AS.DGAxiom (Annotation
implied Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
anns) AnnotationProperty
a DGNodes
b DGEdges
c [AnnotationProperty]
d 

prove1 :: AS.Annotation -> Bool
prove1 :: Annotation -> Bool
prove1 anno :: Annotation
anno = case Annotation
anno of
      AS.Annotation _ aIRI :: AnnotationProperty
aIRI (AS.AnnValLit (AS.Literal value :: String
value (AS.Typed _))) ->
          AnnotationProperty -> String
iFragment AnnotationProperty
aIRI String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "Implied" Bool -> Bool -> Bool
&& String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "true" String
value
      _ -> Bool
False

proveAnnos :: [AS.Annotation] -> Bool
proveAnnos :: [Annotation] -> Bool
proveAnnos = (Annotation -> Bool) -> [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Annotation -> Bool
prove1

prove :: AS.Axiom -> Bool
prove :: Axiom -> Bool
prove ax :: Axiom
ax = case Axiom
ax of
    AS.Declaration anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.ClassAxiom cax :: ClassAxiom
cax -> case ClassAxiom
cax of
        AS.SubClassOf anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.EquivalentClasses anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DisjointClasses anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DisjointUnion anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.ObjectPropertyAxiom opax :: ObjectPropertyAxiom
opax -> case ObjectPropertyAxiom
opax of
        AS.SubObjectPropertyOf anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.EquivalentObjectProperties anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DisjointObjectProperties anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.InverseObjectProperties anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.ObjectPropertyDomain anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.ObjectPropertyRange anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.FunctionalObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.InverseFunctionalObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.ReflexiveObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.IrreflexiveObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.SymmetricObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.AsymmetricObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.TransitiveObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.DataPropertyAxiom a :: DataPropertyAxiom
a -> case DataPropertyAxiom
a of
        AS.SubDataPropertyOf anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.EquivalentDataProperties anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DisjointDataProperties anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DataPropertyDomain anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DataPropertyRange anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.FunctionalDataProperty anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.DatatypeDefinition anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.HasKey anns :: [Annotation]
anns _ _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.Assertion a :: Assertion
a -> case Assertion
a of
        AS.SameIndividual anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DifferentIndividuals anns :: [Annotation]
anns _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.ClassAssertion anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.ObjectPropertyAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.NegativeObjectPropertyAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DataPropertyAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.NegativeDataPropertyAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.AnnotationAxiom a :: AnnotationAxiom
a -> case AnnotationAxiom
a of
        AS.AnnotationAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.SubAnnotationPropertyOf anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.AnnotationPropertyDomain anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.AnnotationPropertyRange anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.Rule rule :: Rule
rule -> case Rule
rule of 
        AS.DLSafeRule anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
        AS.DGRule anns :: [Annotation]
anns _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns
    AS.DGAxiom anns :: [Annotation]
anns _ _ _ _ -> [Annotation] -> Bool
proveAnnos [Annotation]
anns