{-# OPTIONS --safe --cubical #-}
module OWL2.Corpus.Rejected.Raw where
open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab
open import OWL2.Raw
rawClassIri : RawIRI
rawClassIri =
rawIRI "http://example.test/Class"
rawClassAxiom : RawAnnotated RawAxiom
rawClassAxiom =
rawAnnotated [] (rawDeclaration (rawEntity rawClass rawClassIri))
importedRawIri : RawIRI
importedRawIri =
rawIRI "http://example.test/imported"
importedRawDocument : RawOntology
importedRawDocument =
rawOntology
anonymousSource
absent
absent
(importedRawIri ∷ [])
[]
[]
emptyImportResult : ElaborationResult
emptyImportResult =
elaborateEmptyKernelStrict importedRawDocument
emptyImportDiagnostics :
diagnostics emptyImportResult ≡
singleDiagnostic unsupportedImportDiagnostic
emptyImportDiagnostics =
refl
emptyImportRejected :
Clean emptyImportResult → ⊥
emptyImportRejected clean =
clean
emptyImportEvidenceAbsent :
evidence? emptyImportResult ≡ absent
emptyImportEvidenceAbsent =
refl
declarationImportResult : ElaborationResult
declarationImportResult =
elaborateDeclarationsKernelStrict importedRawDocument
declarationImportDiagnostics :
diagnostics declarationImportResult ≡
singleDiagnostic unsupportedDeclarationImportDiagnostic
declarationImportDiagnostics =
refl
declarationImportRejected :
Clean declarationImportResult → ⊥
declarationImportRejected clean =
clean
declarationImportEvidenceAbsent :
evidence? declarationImportResult ≡ absent
declarationImportEvidenceAbsent =
refl
structuralImportResult : ElaborationResult
structuralImportResult =
elaborateStructuralKernelStrict importedRawDocument
structuralImportDiagnostics :
diagnostics structuralImportResult ≡
singleDiagnostic structuralUnsupportedImportDiagnostic
structuralImportDiagnostics =
refl
structuralImportRejected :
Clean structuralImportResult → ⊥
structuralImportRejected clean =
clean
structuralImportEvidenceAbsent :
evidence? structuralImportResult ≡ absent
structuralImportEvidenceAbsent =
refl
nonEmptyRawDocument : RawOntology
nonEmptyRawDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷ [])
nonEmptyRawDocumentResult : ElaborationResult
nonEmptyRawDocumentResult =
elaborateEmptyKernelStrict nonEmptyRawDocument
nonEmptyRawDocumentDiagnostics :
diagnostics nonEmptyRawDocumentResult ≡
singleDiagnostic unsupportedAxiomDiagnostic
nonEmptyRawDocumentDiagnostics =
refl
nonEmptyRawDocumentRejected :
Clean nonEmptyRawDocumentResult → ⊥
nonEmptyRawDocumentRejected clean =
clean
nonEmptyRawDocumentEvidenceAbsent :
evidence? nonEmptyRawDocumentResult ≡ absent
nonEmptyRawDocumentEvidenceAbsent =
refl
nonEmptyRawDocumentEvidenceUnavailable :
EvidenceUnavailable nonEmptyRawDocumentResult
nonEmptyRawDocumentEvidenceUnavailable =
evidenceUnavailable
nonEmptyRawDocumentResult
nonEmptyRawDocumentEvidenceAbsent
rawOntologyIri : RawIRI
rawOntologyIri =
rawIRI "http://example.test/ontology"
emptyOntologyIRIDocument : RawOntology
emptyOntologyIRIDocument =
rawOntology
anonymousSource
(present rawOntologyIri)
absent
[]
[]
[]
emptyOntologyIRIResult : ElaborationResult
emptyOntologyIRIResult =
elaborateEmptyKernelStrict emptyOntologyIRIDocument
emptyOntologyIRIDiagnostics :
diagnostics emptyOntologyIRIResult ≡
singleDiagnostic unsupportedOntologyIRIDiagnostic
emptyOntologyIRIDiagnostics =
refl
emptyOntologyIRIRejected :
Clean emptyOntologyIRIResult → ⊥
emptyOntologyIRIRejected clean =
clean
unknownKindIri : RawIRI
unknownKindIri =
rawIRI "http://example.test/Unknown"
unknownKindAxiom : RawAnnotated RawAxiom
unknownKindAxiom =
rawAnnotated []
(rawDeclaration (rawEntity rawUnknownEntityKind unknownKindIri))
unknownKindDocument : RawOntology
unknownKindDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(unknownKindAxiom ∷ [])
unknownKindResult : ElaborationResult
unknownKindResult =
elaborateDeclarationsKernelStrict unknownKindDocument
unknownKindDiagnostics :
diagnostics unknownKindResult ≡
singleDiagnostic unknownEntityKindDiagnostic
unknownKindDiagnostics =
refl
unknownKindRejected : Clean unknownKindResult → ⊥
unknownKindRejected clean =
clean
punnedEntityIri : RawIRI
punnedEntityIri =
rawIRI "http://example.test/PunnedEntity"
punnedClassAxiom : RawAnnotated RawAxiom
punnedClassAxiom =
rawAnnotated []
(rawDeclaration (rawEntity rawClass punnedEntityIri))
punnedObjectPropertyAxiom : RawAnnotated RawAxiom
punnedObjectPropertyAxiom =
rawAnnotated []
(rawDeclaration (rawEntity rawObjectProperty punnedEntityIri))
punnedDeclarationsDocument : RawOntology
punnedDeclarationsDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(punnedClassAxiom ∷ punnedObjectPropertyAxiom ∷ [])
punnedDeclarationsResult : ElaborationResult
punnedDeclarationsResult =
elaborateDeclarationsKernelStrict punnedDeclarationsDocument
punnedDeclarationsDiagnostics :
diagnostics punnedDeclarationsResult ≡
singleDiagnostic (punningDeclarationDiagnostic punnedEntityIri)
punnedDeclarationsDiagnostics =
refl
punnedDeclarationsRejected : Clean punnedDeclarationsResult → ⊥
punnedDeclarationsRejected clean =
clean
punnedDeclarationsEvidenceAbsent :
evidence? punnedDeclarationsResult ≡ absent
punnedDeclarationsEvidenceAbsent =
refl
punnedDeclarationsEvidenceUnavailable :
EvidenceUnavailable punnedDeclarationsResult
punnedDeclarationsEvidenceUnavailable =
evidenceUnavailable
punnedDeclarationsResult
punnedDeclarationsEvidenceAbsent
punnedStructuralResult : ElaborationResult
punnedStructuralResult =
elaborateStructuralKernelStrict punnedDeclarationsDocument
punnedStructuralDiagnostics :
diagnostics punnedStructuralResult ≡
singleDiagnostic (punningDeclarationDiagnostic punnedEntityIri)
punnedStructuralDiagnostics =
refl
punnedStructuralRejected : Clean punnedStructuralResult → ⊥
punnedStructuralRejected clean =
clean
punnedStructuralEvidenceAbsent :
evidence? punnedStructuralResult ≡ absent
punnedStructuralEvidenceAbsent =
refl
punnedStructuralEvidenceUnavailable :
EvidenceUnavailable punnedStructuralResult
punnedStructuralEvidenceUnavailable =
evidenceUnavailable
punnedStructuralResult
punnedStructuralEvidenceAbsent
unsupportedSubClassDocument : RawOntology
unsupportedSubClassDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawNamedClass rawClassIri))
∷ [])
unsupportedSubClassResult : ElaborationResult
unsupportedSubClassResult =
elaborateDeclarationsKernelStrict unsupportedSubClassDocument
unsupportedSubClassDiagnostics :
diagnostics unsupportedSubClassResult ≡
singleDiagnostic unsupportedDeclarationAxiomDiagnostic
unsupportedSubClassDiagnostics =
refl
unsupportedSubClassRejected :
Clean unsupportedSubClassResult → ⊥
unsupportedSubClassRejected clean =
clean
declarationAnnotationIri : RawIRI
declarationAnnotationIri =
rawIRI "http://example.test/declarationLabel"
declarationAnnotation : RawAnnotation
declarationAnnotation =
rawAnnotation []
declarationAnnotationIri
(rawAnnotationValueIRI rawClassIri)
emptyAnnotationOnlyDocument : RawOntology
emptyAnnotationOnlyDocument =
rawOntology
anonymousSource
absent
absent
[]
(declarationAnnotation ∷ [])
[]
emptyAnnotationOnlyResult : ElaborationResult
emptyAnnotationOnlyResult =
elaborateEmptyKernelStrict emptyAnnotationOnlyDocument
emptyAnnotationOnlyDiagnostics :
diagnostics emptyAnnotationOnlyResult ≡
singleDiagnostic unsupportedOntologyAnnotationDiagnostic
emptyAnnotationOnlyDiagnostics =
refl
emptyAnnotationOnlyRejected :
Clean emptyAnnotationOnlyResult → ⊥
emptyAnnotationOnlyRejected clean =
clean
annotatedDeclarationOnlyDocument : RawOntology
annotatedDeclarationOnlyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated (declarationAnnotation ∷ [])
(rawDeclaration (rawEntity rawClass rawClassIri))
∷ [])
annotatedDeclarationOnlyResult : ElaborationResult
annotatedDeclarationOnlyResult =
elaborateDeclarationsKernelStrict annotatedDeclarationOnlyDocument
annotatedDeclarationOnlyDiagnostics :
diagnostics annotatedDeclarationOnlyResult ≡
singleDiagnostic unsupportedDeclarationAxiomAnnotationDiagnostic
annotatedDeclarationOnlyDiagnostics =
refl
annotatedDeclarationOnlyRejected :
Clean annotatedDeclarationOnlyResult → ⊥
annotatedDeclarationOnlyRejected clean =
clean
annotatedDeclarationOntologyDocument : RawOntology
annotatedDeclarationOntologyDocument =
rawOntology
anonymousSource
absent
absent
[]
(declarationAnnotation ∷ [])
(rawClassAxiom ∷ [])
annotatedDeclarationOntologyResult : ElaborationResult
annotatedDeclarationOntologyResult =
elaborateDeclarationsKernelStrict annotatedDeclarationOntologyDocument
annotatedDeclarationOntologyDiagnostics :
diagnostics annotatedDeclarationOntologyResult ≡
singleDiagnostic unsupportedDeclarationOntologyAnnotationDiagnostic
annotatedDeclarationOntologyDiagnostics =
refl
annotatedDeclarationOntologyRejected :
Clean annotatedDeclarationOntologyResult → ⊥
annotatedDeclarationOntologyRejected clean =
clean
declarationOntologyIRIDocument : RawOntology
declarationOntologyIRIDocument =
rawOntology
anonymousSource
(present rawOntologyIri)
absent
[]
[]
(rawClassAxiom ∷ [])
declarationOntologyIRIResult : ElaborationResult
declarationOntologyIRIResult =
elaborateDeclarationsKernelStrict declarationOntologyIRIDocument
declarationOntologyIRIDiagnosticsExpected :
diagnostics declarationOntologyIRIResult ≡
singleDiagnostic unsupportedDeclarationOntologyIRIDiagnostic
declarationOntologyIRIDiagnosticsExpected =
refl
declarationOntologyIRIRejected :
Clean declarationOntologyIRIResult → ⊥
declarationOntologyIRIRejected clean =
clean
structuralOntologyIRIDocument : RawOntology
structuralOntologyIRIDocument =
rawOntology
anonymousSource
(present rawOntologyIri)
absent
[]
[]
(rawClassAxiom ∷ [])
structuralOntologyIRIResult : ElaborationResult
structuralOntologyIRIResult =
elaborateStructuralKernelStrict structuralOntologyIRIDocument
structuralOntologyIRIDiagnosticsExpected :
diagnostics structuralOntologyIRIResult ≡
singleDiagnostic structuralUnsupportedOntologyIRIDiagnostic
structuralOntologyIRIDiagnosticsExpected =
refl
structuralOntologyIRIRejected :
Clean structuralOntologyIRIResult → ⊥
structuralOntologyIRIRejected clean =
clean
missingClassIri : RawIRI
missingClassIri =
rawIRI "http://example.test/MissingClass"
undeclaredSubClassDocument : RawOntology
undeclaredSubClassDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawNamedClass missingClassIri))
∷ [])
undeclaredSubClassResult : ElaborationResult
undeclaredSubClassResult =
elaborateStructuralKernelStrict undeclaredSubClassDocument
undeclaredSubClassDiagnostics :
diagnostics undeclaredSubClassResult ≡
singleDiagnostic (undeclaredClassDiagnostic missingClassIri)
undeclaredSubClassDiagnostics =
refl
undeclaredSubClassRejected :
Clean undeclaredSubClassResult → ⊥
undeclaredSubClassRejected clean =
clean
missingObjectPropertyIri : RawIRI
missingObjectPropertyIri =
rawIRI "http://example.test/missingRelation"
undeclaredObjectPropertyDocument : RawOntology
undeclaredObjectPropertyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawDeclaration (rawEntity rawClass missingClassIri))
∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectSomeValuesFrom
(rawObjectProperty missingObjectPropertyIri)
(rawNamedClass missingClassIri)))
∷ [])
undeclaredObjectPropertyResult : ElaborationResult
undeclaredObjectPropertyResult =
elaborateStructuralKernelStrict undeclaredObjectPropertyDocument
undeclaredObjectPropertyDiagnostics :
diagnostics undeclaredObjectPropertyResult ≡
singleDiagnostic
(undeclaredObjectPropertyDiagnostic missingObjectPropertyIri)
undeclaredObjectPropertyDiagnostics =
refl
undeclaredObjectPropertyRejected :
Clean undeclaredObjectPropertyResult → ⊥
undeclaredObjectPropertyRejected clean =
clean
emptyIntersectionDocument : RawOntology
emptyIntersectionDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectIntersectionOf []))
∷ [])
emptyIntersectionResult : ElaborationResult
emptyIntersectionResult =
elaborateStructuralKernelStrict emptyIntersectionDocument
emptyIntersectionDiagnostics :
diagnostics emptyIntersectionResult ≡
singleDiagnostic emptyClassExpressionListDiagnostic
emptyIntersectionDiagnostics =
refl
emptyIntersectionRejected : Clean emptyIntersectionResult → ⊥
emptyIntersectionRejected clean =
clean
emptyUnionDocument : RawOntology
emptyUnionDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectUnionOf []))
∷ [])
emptyUnionResult : ElaborationResult
emptyUnionResult =
elaborateStructuralKernelStrict emptyUnionDocument
emptyUnionDiagnostics :
diagnostics emptyUnionResult ≡
singleDiagnostic emptyClassExpressionListDiagnostic
emptyUnionDiagnostics =
refl
emptyUnionRejected : Clean emptyUnionResult → ⊥
emptyUnionRejected clean =
clean
emptyEquivalentClassesDocument : RawOntology
emptyEquivalentClassesDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated [] (rawEquivalentClasses []) ∷ [])
emptyEquivalentClassesResult : ElaborationResult
emptyEquivalentClassesResult =
elaborateStructuralKernelStrict emptyEquivalentClassesDocument
emptyEquivalentClassesDiagnostics :
diagnostics emptyEquivalentClassesResult ≡
singleDiagnostic tooFewClassExpressionsDiagnostic
emptyEquivalentClassesDiagnostics =
refl
emptyEquivalentClassesRejected :
Clean emptyEquivalentClassesResult → ⊥
emptyEquivalentClassesRejected clean =
clean
singletonEquivalentClassesDocument : RawOntology
singletonEquivalentClassesDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawEquivalentClasses (rawNamedClass rawClassIri ∷ []))
∷ [])
singletonEquivalentClassesResult : ElaborationResult
singletonEquivalentClassesResult =
elaborateStructuralKernelStrict singletonEquivalentClassesDocument
singletonEquivalentClassesDiagnostics :
diagnostics singletonEquivalentClassesResult ≡
singleDiagnostic tooFewClassExpressionsDiagnostic
singletonEquivalentClassesDiagnostics =
refl
singletonEquivalentClassesRejected :
Clean singletonEquivalentClassesResult → ⊥
singletonEquivalentClassesRejected clean =
clean
emptyDisjointClassesDocument : RawOntology
emptyDisjointClassesDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated [] (rawDisjointClasses []) ∷ [])
emptyDisjointClassesResult : ElaborationResult
emptyDisjointClassesResult =
elaborateStructuralKernelStrict emptyDisjointClassesDocument
emptyDisjointClassesDiagnostics :
diagnostics emptyDisjointClassesResult ≡
singleDiagnostic tooFewClassExpressionsDiagnostic
emptyDisjointClassesDiagnostics =
refl
emptyDisjointClassesRejected :
Clean emptyDisjointClassesResult → ⊥
emptyDisjointClassesRejected clean =
clean
singletonDisjointClassesDocument : RawOntology
singletonDisjointClassesDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawDisjointClasses (rawNamedClass rawClassIri ∷ []))
∷ [])
singletonDisjointClassesResult : ElaborationResult
singletonDisjointClassesResult =
elaborateStructuralKernelStrict singletonDisjointClassesDocument
singletonDisjointClassesDiagnostics :
diagnostics singletonDisjointClassesResult ≡
singleDiagnostic tooFewClassExpressionsDiagnostic
singletonDisjointClassesDiagnostics =
refl
singletonDisjointClassesRejected :
Clean singletonDisjointClassesResult → ⊥
singletonDisjointClassesRejected clean =
clean
nestedMissingClassDocument : RawOntology
nestedMissingClassDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectUnionOf
(rawObjectComplementOf
(rawObjectIntersectionOf
(rawNamedClass missingClassIri ∷ []))
∷ [])))
∷ [])
nestedMissingClassResult : ElaborationResult
nestedMissingClassResult =
elaborateStructuralKernelStrict nestedMissingClassDocument
nestedMissingClassDiagnostics :
diagnostics nestedMissingClassResult ≡
singleDiagnostic (undeclaredClassDiagnostic missingClassIri)
nestedMissingClassDiagnostics =
refl
nestedMissingClassRejected : Clean nestedMissingClassResult → ⊥
nestedMissingClassRejected clean =
clean
equivalentMissingClassDocument : RawOntology
equivalentMissingClassDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawEquivalentClasses
(rawNamedClass rawClassIri ∷
rawNamedClass missingClassIri ∷ []))
∷ [])
equivalentMissingClassResult : ElaborationResult
equivalentMissingClassResult =
elaborateStructuralKernelStrict equivalentMissingClassDocument
equivalentMissingClassDiagnostics :
diagnostics equivalentMissingClassResult ≡
singleDiagnostic (undeclaredClassDiagnostic missingClassIri)
equivalentMissingClassDiagnostics =
refl
equivalentMissingClassRejected :
Clean equivalentMissingClassResult → ⊥
equivalentMissingClassRejected clean =
clean
disjointMissingClassDocument : RawOntology
disjointMissingClassDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawDisjointClasses
(rawNamedClass rawClassIri ∷
rawNamedClass missingClassIri ∷ []))
∷ [])
disjointMissingClassResult : ElaborationResult
disjointMissingClassResult =
elaborateStructuralKernelStrict disjointMissingClassDocument
disjointMissingClassDiagnostics :
diagnostics disjointMissingClassResult ≡
singleDiagnostic (undeclaredClassDiagnostic missingClassIri)
disjointMissingClassDiagnostics =
refl
disjointMissingClassRejected :
Clean disjointMissingClassResult → ⊥
disjointMissingClassRejected clean =
clean
missingDataPropertyIri : RawIRI
missingDataPropertyIri =
rawIRI "http://example.test/missingDataProperty"
undeclaredDataPropertyDomainDocument : RawOntology
undeclaredDataPropertyDomainDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawDataPropertyDomain
(rawDataProperty missingDataPropertyIri)
(rawNamedClass rawClassIri))
∷ [])
undeclaredDataPropertyDomainResult : ElaborationResult
undeclaredDataPropertyDomainResult =
elaborateStructuralKernelStrict undeclaredDataPropertyDomainDocument
undeclaredDataPropertyDomainDiagnostics :
diagnostics undeclaredDataPropertyDomainResult ≡
singleDiagnostic (undeclaredDataPropertyDiagnostic missingDataPropertyIri)
undeclaredDataPropertyDomainDiagnostics =
refl
undeclaredDataPropertyDomainRejected :
Clean undeclaredDataPropertyDomainResult → ⊥
undeclaredDataPropertyDomainRejected clean =
clean
unsupportedPropertyChainDocument : RawOntology
unsupportedPropertyChainDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated []
(rawSubObjectPropertyOf
(rawSubObjectPropertyChain [])
rawTopObjectProperty)
∷ [])
unsupportedPropertyChainResult : ElaborationResult
unsupportedPropertyChainResult =
elaborateStructuralKernelStrict unsupportedPropertyChainDocument
unsupportedPropertyChainDiagnostics :
diagnostics unsupportedPropertyChainResult ≡
singleDiagnostic tooFewObjectPropertyExpressionsDiagnostic
unsupportedPropertyChainDiagnostics =
refl
unsupportedPropertyChainRejected :
Clean unsupportedPropertyChainResult → ⊥
unsupportedPropertyChainRejected clean =
clean
uncertifiedChainPropertyIri : RawIRI
uncertifiedChainPropertyIri =
rawIRI "http://example.test/uncertifiedChainProperty"
uncertifiedChainPropertyAxiom : RawAnnotated RawAxiom
uncertifiedChainPropertyAxiom =
rawAnnotated []
(rawDeclaration
(rawEntity rawObjectProperty uncertifiedChainPropertyIri))
uncertifiedPropertyChainDocument : RawOntology
uncertifiedPropertyChainDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(uncertifiedChainPropertyAxiom ∷
rawAnnotated []
(rawSubObjectPropertyOf
(rawSubObjectPropertyChain
(rawObjectProperty uncertifiedChainPropertyIri ∷
rawObjectProperty uncertifiedChainPropertyIri ∷ []))
(rawObjectProperty uncertifiedChainPropertyIri))
∷ [])
uncertifiedPropertyChainResult : ElaborationResult
uncertifiedPropertyChainResult =
elaborateStructuralKernelStrict uncertifiedPropertyChainDocument
uncertifiedPropertyChainDiagnostics :
diagnostics uncertifiedPropertyChainResult ≡
singleDiagnostic unsupportedPropertyChainRegularityDiagnostic
uncertifiedPropertyChainDiagnostics =
refl
uncertifiedPropertyChainRejected :
Clean uncertifiedPropertyChainResult → ⊥
uncertifiedPropertyChainRejected clean =
clean
uncertifiedPropertyChainEvidenceAbsent :
evidence? uncertifiedPropertyChainResult ≡ absent
uncertifiedPropertyChainEvidenceAbsent =
refl
uncertifiedPropertyChainEvidenceUnavailable :
EvidenceUnavailable uncertifiedPropertyChainResult
uncertifiedPropertyChainEvidenceUnavailable =
evidenceUnavailable
uncertifiedPropertyChainResult
uncertifiedPropertyChainEvidenceAbsent
missingIndividualIri : RawIRI
missingIndividualIri =
rawIRI "http://example.test/MissingIndividual"
undeclaredIndividualAssertionDocument : RawOntology
undeclaredIndividualAssertionDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawClassAssertion
(rawNamedClass rawClassIri)
(rawNamedIndividual missingIndividualIri))
∷ [])
undeclaredIndividualAssertionResult : ElaborationResult
undeclaredIndividualAssertionResult =
elaborateStructuralKernelStrict undeclaredIndividualAssertionDocument
undeclaredIndividualAssertionDiagnostics :
diagnostics undeclaredIndividualAssertionResult ≡
singleDiagnostic (undeclaredIndividualDiagnostic missingIndividualIri)
undeclaredIndividualAssertionDiagnostics =
refl
undeclaredIndividualAssertionRejected :
Clean undeclaredIndividualAssertionResult → ⊥
undeclaredIndividualAssertionRejected clean =
clean
anonymousIndividualAssertionDocument : RawOntology
anonymousIndividualAssertionDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawClassAssertion
(rawNamedClass rawClassIri)
(rawAnonymousIndividual "anon"))
∷ [])
anonymousIndividualAssertionResult : ElaborationResult
anonymousIndividualAssertionResult =
elaborateStructuralKernelStrict anonymousIndividualAssertionDocument
anonymousIndividualAssertionDiagnostics :
diagnostics anonymousIndividualAssertionResult ≡
singleDiagnostic (unsupportedAnonymousIndividualDiagnostic "anon")
anonymousIndividualAssertionDiagnostics =
refl
anonymousIndividualAssertionRejected :
Clean anonymousIndividualAssertionResult → ⊥
anonymousIndividualAssertionRejected clean =
clean
emptyObjectOneOfDocument : RawOntology
emptyObjectOneOfDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectOneOf []))
∷ [])
emptyObjectOneOfResult : ElaborationResult
emptyObjectOneOfResult =
elaborateStructuralKernelStrict emptyObjectOneOfDocument
emptyObjectOneOfDiagnostics :
diagnostics emptyObjectOneOfResult ≡
singleDiagnostic emptyIndividualListDiagnostic
emptyObjectOneOfDiagnostics =
refl
emptyObjectOneOfRejected :
Clean emptyObjectOneOfResult → ⊥
emptyObjectOneOfRejected clean =
clean
rejectedObjectPropertyIri : RawIRI
rejectedObjectPropertyIri =
rawIRI "http://example.test/rejectedObjectProperty"
rejectedObjectPropertyAxiom : RawAnnotated RawAxiom
rejectedObjectPropertyAxiom =
rawAnnotated []
(rawDeclaration (rawEntity rawObjectProperty rejectedObjectPropertyIri))
objectHasValueMissingIndividualDocument : RawOntology
objectHasValueMissingIndividualDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rejectedObjectPropertyAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectHasValue
(rawObjectProperty rejectedObjectPropertyIri)
(rawNamedIndividual missingIndividualIri)))
∷ [])
objectHasValueMissingIndividualResult : ElaborationResult
objectHasValueMissingIndividualResult =
elaborateStructuralKernelStrict objectHasValueMissingIndividualDocument
objectHasValueMissingIndividualDiagnostics :
diagnostics objectHasValueMissingIndividualResult ≡
singleDiagnostic (undeclaredIndividualDiagnostic missingIndividualIri)
objectHasValueMissingIndividualDiagnostics =
refl
objectHasValueMissingIndividualRejected :
Clean objectHasValueMissingIndividualResult → ⊥
objectHasValueMissingIndividualRejected clean =
clean
objectCardinalityMissingPropertyDocument : RawOntology
objectCardinalityMissingPropertyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectMinCardinality
1
(rawObjectProperty missingObjectPropertyIri)
absent))
∷ [])
objectCardinalityMissingPropertyResult : ElaborationResult
objectCardinalityMissingPropertyResult =
elaborateStructuralKernelStrict objectCardinalityMissingPropertyDocument
objectCardinalityMissingPropertyDiagnostics :
diagnostics objectCardinalityMissingPropertyResult ≡
singleDiagnostic (undeclaredObjectPropertyDiagnostic missingObjectPropertyIri)
objectCardinalityMissingPropertyDiagnostics =
refl
objectCardinalityMissingPropertyRejected :
Clean objectCardinalityMissingPropertyResult → ⊥
objectCardinalityMissingPropertyRejected clean =
clean
objectCardinalityMissingQualifierDocument : RawOntology
objectCardinalityMissingQualifierDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rejectedObjectPropertyAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectMinCardinality
1
(rawObjectProperty rejectedObjectPropertyIri)
(present (rawNamedClass missingClassIri))))
∷ [])
objectCardinalityMissingQualifierResult : ElaborationResult
objectCardinalityMissingQualifierResult =
elaborateStructuralKernelStrict objectCardinalityMissingQualifierDocument
objectCardinalityMissingQualifierDiagnostics :
diagnostics objectCardinalityMissingQualifierResult ≡
singleDiagnostic (undeclaredClassDiagnostic missingClassIri)
objectCardinalityMissingQualifierDiagnostics =
refl
objectCardinalityMissingQualifierRejected :
Clean objectCardinalityMissingQualifierResult → ⊥
objectCardinalityMissingQualifierRejected clean =
clean
objectCardinalityInversePropertyDocument : RawOntology
objectCardinalityInversePropertyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rejectedObjectPropertyAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectMaxCardinality
1
(rawObjectInverseOf
(rawObjectProperty rejectedObjectPropertyIri))
absent))
∷ [])
objectCardinalityInversePropertyResult : ElaborationResult
objectCardinalityInversePropertyResult =
elaborateStructuralKernelStrict objectCardinalityInversePropertyDocument
objectCardinalityInversePropertyDiagnostics :
diagnostics objectCardinalityInversePropertyResult ≡
singleDiagnostic unsupportedSimpleObjectPropertyExpressionDiagnostic
objectCardinalityInversePropertyDiagnostics =
refl
objectCardinalityInversePropertyRejected :
Clean objectCardinalityInversePropertyResult → ⊥
objectCardinalityInversePropertyRejected clean =
clean
emptyEquivalentObjectPropertiesDocument : RawOntology
emptyEquivalentObjectPropertiesDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated [] (rawEquivalentObjectProperties []) ∷ [])
emptyEquivalentObjectPropertiesResult : ElaborationResult
emptyEquivalentObjectPropertiesResult =
elaborateStructuralKernelStrict emptyEquivalentObjectPropertiesDocument
emptyEquivalentObjectPropertiesDiagnostics :
diagnostics emptyEquivalentObjectPropertiesResult ≡
singleDiagnostic tooFewObjectPropertyExpressionsDiagnostic
emptyEquivalentObjectPropertiesDiagnostics =
refl
emptyEquivalentObjectPropertiesRejected :
Clean emptyEquivalentObjectPropertiesResult → ⊥
emptyEquivalentObjectPropertiesRejected clean =
clean
singletonDisjointObjectPropertiesDocument : RawOntology
singletonDisjointObjectPropertiesDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedObjectPropertyAxiom ∷
rawAnnotated []
(rawDisjointObjectProperties
(rawObjectProperty rejectedObjectPropertyIri ∷ []))
∷ [])
singletonDisjointObjectPropertiesResult : ElaborationResult
singletonDisjointObjectPropertiesResult =
elaborateStructuralKernelStrict singletonDisjointObjectPropertiesDocument
singletonDisjointObjectPropertiesDiagnostics :
diagnostics singletonDisjointObjectPropertiesResult ≡
singleDiagnostic tooFewSimpleObjectPropertyExpressionsDiagnostic
singletonDisjointObjectPropertiesDiagnostics =
refl
singletonDisjointObjectPropertiesRejected :
Clean singletonDisjointObjectPropertiesResult → ⊥
singletonDisjointObjectPropertiesRejected clean =
clean
functionalObjectPropertyMissingDocument : RawOntology
functionalObjectPropertyMissingDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated []
(rawFunctionalObjectProperty
(rawObjectProperty missingObjectPropertyIri))
∷ [])
functionalObjectPropertyMissingResult : ElaborationResult
functionalObjectPropertyMissingResult =
elaborateStructuralKernelStrict functionalObjectPropertyMissingDocument
functionalObjectPropertyMissingDiagnostics :
diagnostics functionalObjectPropertyMissingResult ≡
singleDiagnostic
(undeclaredObjectPropertyDiagnostic missingObjectPropertyIri)
functionalObjectPropertyMissingDiagnostics =
refl
functionalObjectPropertyMissingRejected :
Clean functionalObjectPropertyMissingResult → ⊥
functionalObjectPropertyMissingRejected clean =
clean
asymmetricObjectPropertyInverseDocument : RawOntology
asymmetricObjectPropertyInverseDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedObjectPropertyAxiom ∷
rawAnnotated []
(rawAsymmetricObjectProperty
(rawObjectInverseOf
(rawObjectProperty rejectedObjectPropertyIri)))
∷ [])
asymmetricObjectPropertyInverseResult : ElaborationResult
asymmetricObjectPropertyInverseResult =
elaborateStructuralKernelStrict asymmetricObjectPropertyInverseDocument
asymmetricObjectPropertyInverseDiagnostics :
diagnostics asymmetricObjectPropertyInverseResult ≡
singleDiagnostic unsupportedSimpleObjectPropertyExpressionDiagnostic
asymmetricObjectPropertyInverseDiagnostics =
refl
asymmetricObjectPropertyInverseRejected :
Clean asymmetricObjectPropertyInverseResult → ⊥
asymmetricObjectPropertyInverseRejected clean =
clean
nonSimpleObjectPropertyIri : RawIRI
nonSimpleObjectPropertyIri =
rawIRI "http://example.test/nonSimpleObjectProperty"
nonSimpleObjectPropertyAxiom : RawAnnotated RawAxiom
nonSimpleObjectPropertyAxiom =
rawAnnotated []
(rawDeclaration
(rawEntity rawObjectProperty nonSimpleObjectPropertyIri))
nonSimpleFunctionalObjectPropertyDocument : RawOntology
nonSimpleFunctionalObjectPropertyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(nonSimpleObjectPropertyAxiom ∷
rawAnnotated []
(rawTransitiveObjectProperty
(rawObjectProperty nonSimpleObjectPropertyIri))
∷
rawAnnotated []
(rawFunctionalObjectProperty
(rawObjectProperty nonSimpleObjectPropertyIri))
∷ [])
nonSimpleFunctionalObjectPropertyResult : ElaborationResult
nonSimpleFunctionalObjectPropertyResult =
elaborateStructuralKernelStrict nonSimpleFunctionalObjectPropertyDocument
nonSimpleFunctionalObjectPropertyDiagnostics :
diagnostics nonSimpleFunctionalObjectPropertyResult ≡
singleDiagnostic
(nonSimpleObjectPropertyDiagnostic nonSimpleObjectPropertyIri)
nonSimpleFunctionalObjectPropertyDiagnostics =
refl
nonSimpleFunctionalObjectPropertyRejected :
Clean nonSimpleFunctionalObjectPropertyResult → ⊥
nonSimpleFunctionalObjectPropertyRejected clean =
clean
nonSimpleFunctionalObjectPropertyEvidenceAbsent :
evidence? nonSimpleFunctionalObjectPropertyResult ≡ absent
nonSimpleFunctionalObjectPropertyEvidenceAbsent =
refl
nonSimpleFunctionalObjectPropertyEvidenceUnavailable :
EvidenceUnavailable nonSimpleFunctionalObjectPropertyResult
nonSimpleFunctionalObjectPropertyEvidenceUnavailable =
evidenceUnavailable
nonSimpleFunctionalObjectPropertyResult
nonSimpleFunctionalObjectPropertyEvidenceAbsent
nonSimpleSubObjectPropertyIri : RawIRI
nonSimpleSubObjectPropertyIri =
rawIRI "http://example.test/nonSimpleSubObjectProperty"
nonSimpleSuperObjectPropertyIri : RawIRI
nonSimpleSuperObjectPropertyIri =
rawIRI "http://example.test/nonSimpleSuperObjectProperty"
nonSimpleSubObjectPropertyAxiom : RawAnnotated RawAxiom
nonSimpleSubObjectPropertyAxiom =
rawAnnotated []
(rawDeclaration
(rawEntity rawObjectProperty nonSimpleSubObjectPropertyIri))
nonSimpleSuperObjectPropertyAxiom : RawAnnotated RawAxiom
nonSimpleSuperObjectPropertyAxiom =
rawAnnotated []
(rawDeclaration
(rawEntity rawObjectProperty nonSimpleSuperObjectPropertyIri))
nonSimpleHierarchyFunctionalObjectPropertyDocument : RawOntology
nonSimpleHierarchyFunctionalObjectPropertyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(nonSimpleSubObjectPropertyAxiom ∷
nonSimpleSuperObjectPropertyAxiom ∷
rawAnnotated []
(rawTransitiveObjectProperty
(rawObjectProperty nonSimpleSubObjectPropertyIri))
∷
rawAnnotated []
(rawSubObjectPropertyOf
(rawSubObjectProperty
(rawObjectProperty nonSimpleSubObjectPropertyIri))
(rawObjectProperty nonSimpleSuperObjectPropertyIri))
∷
rawAnnotated []
(rawFunctionalObjectProperty
(rawObjectProperty nonSimpleSuperObjectPropertyIri))
∷ [])
nonSimpleHierarchyFunctionalObjectPropertyResult : ElaborationResult
nonSimpleHierarchyFunctionalObjectPropertyResult =
elaborateStructuralKernelStrict
nonSimpleHierarchyFunctionalObjectPropertyDocument
nonSimpleHierarchyFunctionalObjectPropertyDiagnostics :
diagnostics nonSimpleHierarchyFunctionalObjectPropertyResult ≡
singleDiagnostic
(nonSimpleObjectPropertyDiagnostic nonSimpleSuperObjectPropertyIri)
nonSimpleHierarchyFunctionalObjectPropertyDiagnostics =
refl
nonSimpleHierarchyFunctionalObjectPropertyRejected :
Clean nonSimpleHierarchyFunctionalObjectPropertyResult → ⊥
nonSimpleHierarchyFunctionalObjectPropertyRejected clean =
clean
nonSimpleHierarchyFunctionalObjectPropertyEvidenceAbsent :
evidence? nonSimpleHierarchyFunctionalObjectPropertyResult ≡ absent
nonSimpleHierarchyFunctionalObjectPropertyEvidenceAbsent =
refl
nonSimpleHierarchyFunctionalObjectPropertyEvidenceUnavailable :
EvidenceUnavailable nonSimpleHierarchyFunctionalObjectPropertyResult
nonSimpleHierarchyFunctionalObjectPropertyEvidenceUnavailable =
evidenceUnavailable
nonSimpleHierarchyFunctionalObjectPropertyResult
nonSimpleHierarchyFunctionalObjectPropertyEvidenceAbsent
nonSimpleChainLeftPropertyIri : RawIRI
nonSimpleChainLeftPropertyIri =
rawIRI "http://example.test/nonSimpleChainLeftProperty"
nonSimpleChainRightPropertyIri : RawIRI
nonSimpleChainRightPropertyIri =
rawIRI "http://example.test/nonSimpleChainRightProperty"
nonSimpleChainSuperPropertyIri : RawIRI
nonSimpleChainSuperPropertyIri =
rawIRI "http://example.test/nonSimpleChainSuperProperty"
nonSimpleChainLeftPropertyAxiom : RawAnnotated RawAxiom
nonSimpleChainLeftPropertyAxiom =
rawAnnotated []
(rawDeclaration
(rawEntity rawObjectProperty nonSimpleChainLeftPropertyIri))
nonSimpleChainRightPropertyAxiom : RawAnnotated RawAxiom
nonSimpleChainRightPropertyAxiom =
rawAnnotated []
(rawDeclaration
(rawEntity rawObjectProperty nonSimpleChainRightPropertyIri))
nonSimpleChainSuperPropertyAxiom : RawAnnotated RawAxiom
nonSimpleChainSuperPropertyAxiom =
rawAnnotated []
(rawDeclaration
(rawEntity rawObjectProperty nonSimpleChainSuperPropertyIri))
nonSimpleChainCardinalityDocument : RawOntology
nonSimpleChainCardinalityDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
nonSimpleChainLeftPropertyAxiom ∷
nonSimpleChainRightPropertyAxiom ∷
nonSimpleChainSuperPropertyAxiom ∷
rawAnnotated []
(rawSubObjectPropertyOf
(rawSubObjectPropertyChain
(rawObjectProperty nonSimpleChainLeftPropertyIri ∷
rawObjectProperty nonSimpleChainRightPropertyIri ∷ []))
(rawObjectProperty nonSimpleChainSuperPropertyIri))
∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawObjectMinCardinality
1
(rawObjectProperty nonSimpleChainSuperPropertyIri)
absent))
∷ [])
nonSimpleChainCardinalityResult : ElaborationResult
nonSimpleChainCardinalityResult =
elaborateStructuralKernelStrict nonSimpleChainCardinalityDocument
nonSimpleChainCardinalityDiagnostics :
diagnostics nonSimpleChainCardinalityResult ≡
unsupportedPropertyChainRegularityDiagnostic ∷
nonSimpleObjectPropertyDiagnostic nonSimpleChainSuperPropertyIri ∷
[]
nonSimpleChainCardinalityDiagnostics =
refl
nonSimpleChainCardinalityRejected :
Clean nonSimpleChainCardinalityResult → ⊥
nonSimpleChainCardinalityRejected clean =
clean
nonSimpleChainCardinalityEvidenceAbsent :
evidence? nonSimpleChainCardinalityResult ≡ absent
nonSimpleChainCardinalityEvidenceAbsent =
refl
nonSimpleChainCardinalityEvidenceUnavailable :
EvidenceUnavailable nonSimpleChainCardinalityResult
nonSimpleChainCardinalityEvidenceUnavailable =
evidenceUnavailable
nonSimpleChainCardinalityResult
nonSimpleChainCardinalityEvidenceAbsent
rejectedDataPropertyIri : RawIRI
rejectedDataPropertyIri =
rawIRI "http://example.test/rejectedDataProperty"
rejectedDataPropertyAxiom : RawAnnotated RawAxiom
rejectedDataPropertyAxiom =
rawAnnotated []
(rawDeclaration (rawEntity rawDataProperty rejectedDataPropertyIri))
emptyEquivalentDataPropertiesDocument : RawOntology
emptyEquivalentDataPropertiesDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated [] (rawEquivalentDataProperties []) ∷ [])
emptyEquivalentDataPropertiesResult : ElaborationResult
emptyEquivalentDataPropertiesResult =
elaborateStructuralKernelStrict emptyEquivalentDataPropertiesDocument
emptyEquivalentDataPropertiesDiagnostics :
diagnostics emptyEquivalentDataPropertiesResult ≡
singleDiagnostic tooFewDataPropertyExpressionsDiagnostic
emptyEquivalentDataPropertiesDiagnostics =
refl
emptyEquivalentDataPropertiesRejected :
Clean emptyEquivalentDataPropertiesResult → ⊥
emptyEquivalentDataPropertiesRejected clean =
clean
singletonDisjointDataPropertiesDocument : RawOntology
singletonDisjointDataPropertiesDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rawAnnotated []
(rawDisjointDataProperties
(rawDataProperty rejectedDataPropertyIri ∷ []))
∷ [])
singletonDisjointDataPropertiesResult : ElaborationResult
singletonDisjointDataPropertiesResult =
elaborateStructuralKernelStrict singletonDisjointDataPropertiesDocument
singletonDisjointDataPropertiesDiagnostics :
diagnostics singletonDisjointDataPropertiesResult ≡
singleDiagnostic tooFewDataPropertyExpressionsDiagnostic
singletonDisjointDataPropertiesDiagnostics =
refl
singletonDisjointDataPropertiesRejected :
Clean singletonDisjointDataPropertiesResult → ⊥
singletonDisjointDataPropertiesRejected clean =
clean
functionalDataPropertyMissingDocument : RawOntology
functionalDataPropertyMissingDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated []
(rawFunctionalDataProperty
(rawDataProperty missingDataPropertyIri))
∷ [])
functionalDataPropertyMissingResult : ElaborationResult
functionalDataPropertyMissingResult =
elaborateStructuralKernelStrict functionalDataPropertyMissingDocument
functionalDataPropertyMissingDiagnostics :
diagnostics functionalDataPropertyMissingResult ≡
singleDiagnostic (undeclaredDataPropertyDiagnostic missingDataPropertyIri)
functionalDataPropertyMissingDiagnostics =
refl
functionalDataPropertyMissingRejected :
Clean functionalDataPropertyMissingResult → ⊥
functionalDataPropertyMissingRejected clean =
clean
rejectedIndividualIri : RawIRI
rejectedIndividualIri =
rawIRI "http://example.test/RejectedIndividual"
rejectedIndividualAxiom : RawAnnotated RawAxiom
rejectedIndividualAxiom =
rawAnnotated []
(rawDeclaration (rawEntity rawIndividual rejectedIndividualIri))
rejectedDatatypeIri : RawIRI
rejectedDatatypeIri =
rawIRI "http://example.test/RejectedDatatype"
rejectedDatatypeAxiom : RawAnnotated RawAxiom
rejectedDatatypeAxiom =
rawAnnotated []
(rawDeclaration (rawEntity rawDatatype rejectedDatatypeIri))
singletonSameIndividualDocument : RawOntology
singletonSameIndividualDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedIndividualAxiom ∷
rawAnnotated []
(rawSameIndividual
(rawNamedIndividual rejectedIndividualIri ∷ []))
∷ [])
singletonSameIndividualResult : ElaborationResult
singletonSameIndividualResult =
elaborateStructuralKernelStrict singletonSameIndividualDocument
singletonSameIndividualDiagnostics :
diagnostics singletonSameIndividualResult ≡
singleDiagnostic tooFewIndividualsDiagnostic
singletonSameIndividualDiagnostics =
refl
singletonSameIndividualRejected :
Clean singletonSameIndividualResult → ⊥
singletonSameIndividualRejected clean =
clean
sameIndividualMissingIndividualDocument : RawOntology
sameIndividualMissingIndividualDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedIndividualAxiom ∷
rawAnnotated []
(rawSameIndividual
(rawNamedIndividual missingIndividualIri ∷
rawNamedIndividual rejectedIndividualIri ∷ []))
∷ [])
sameIndividualMissingIndividualResult : ElaborationResult
sameIndividualMissingIndividualResult =
elaborateStructuralKernelStrict sameIndividualMissingIndividualDocument
sameIndividualMissingIndividualDiagnostics :
diagnostics sameIndividualMissingIndividualResult ≡
singleDiagnostic (undeclaredIndividualDiagnostic missingIndividualIri)
sameIndividualMissingIndividualDiagnostics =
refl
sameIndividualMissingIndividualRejected :
Clean sameIndividualMissingIndividualResult → ⊥
sameIndividualMissingIndividualRejected clean =
clean
negativeObjectAssertionMissingIndividualDocument : RawOntology
negativeObjectAssertionMissingIndividualDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedObjectPropertyAxiom ∷
rejectedIndividualAxiom ∷
rawAnnotated []
(rawNegativeObjectPropertyAssertion
(rawObjectProperty rejectedObjectPropertyIri)
(rawNamedIndividual missingIndividualIri)
(rawNamedIndividual rejectedIndividualIri))
∷ [])
negativeObjectAssertionMissingIndividualResult : ElaborationResult
negativeObjectAssertionMissingIndividualResult =
elaborateStructuralKernelStrict
negativeObjectAssertionMissingIndividualDocument
negativeObjectAssertionMissingIndividualDiagnostics :
diagnostics negativeObjectAssertionMissingIndividualResult ≡
singleDiagnostic (undeclaredIndividualDiagnostic missingIndividualIri)
negativeObjectAssertionMissingIndividualDiagnostics =
refl
negativeObjectAssertionMissingIndividualRejected :
Clean negativeObjectAssertionMissingIndividualResult → ⊥
negativeObjectAssertionMissingIndividualRejected clean =
clean
negativeDataAssertionMissingLiteralDatatypeDocument : RawOntology
negativeDataAssertionMissingLiteralDatatypeDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rejectedIndividualAxiom ∷
rawAnnotated []
(rawNegativeDataPropertyAssertion
(rawDataProperty rejectedDataPropertyIri)
(rawNamedIndividual rejectedIndividualIri)
(rawLiteral "hello" absent absent))
∷ [])
negativeDataAssertionMissingLiteralDatatypeResult : ElaborationResult
negativeDataAssertionMissingLiteralDatatypeResult =
elaborateStructuralKernelStrict
negativeDataAssertionMissingLiteralDatatypeDocument
negativeDataAssertionMissingLiteralDatatypeDiagnostics :
diagnostics negativeDataAssertionMissingLiteralDatatypeResult ≡
singleDiagnostic missingLiteralDatatypeDiagnostic
negativeDataAssertionMissingLiteralDatatypeDiagnostics =
refl
negativeDataAssertionMissingLiteralDatatypeRejected :
Clean negativeDataAssertionMissingLiteralDatatypeResult → ⊥
negativeDataAssertionMissingLiteralDatatypeRejected clean =
clean
dataRangeMissingDatatypeIri : RawIRI
dataRangeMissingDatatypeIri =
rawIRI "http://example.test/MissingDataRangeDatatype"
disjointUnionMissingHeadDocument : RawOntology
disjointUnionMissingHeadDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawDisjointUnion
missingClassIri
(rawNamedClass rawClassIri ∷
rawOwlThing ∷ []))
∷ [])
disjointUnionMissingHeadResult : ElaborationResult
disjointUnionMissingHeadResult =
elaborateStructuralKernelStrict disjointUnionMissingHeadDocument
disjointUnionMissingHeadDiagnostics :
diagnostics disjointUnionMissingHeadResult ≡
singleDiagnostic (undeclaredClassDiagnostic missingClassIri)
disjointUnionMissingHeadDiagnostics =
refl
disjointUnionMissingHeadRejected :
Clean disjointUnionMissingHeadResult → ⊥
disjointUnionMissingHeadRejected clean =
clean
singletonDisjointUnionDocument : RawOntology
singletonDisjointUnionDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawDisjointUnion
rawClassIri
(rawNamedClass rawClassIri ∷ []))
∷ [])
singletonDisjointUnionResult : ElaborationResult
singletonDisjointUnionResult =
elaborateStructuralKernelStrict singletonDisjointUnionDocument
singletonDisjointUnionDiagnostics :
diagnostics singletonDisjointUnionResult ≡
singleDiagnostic tooFewClassExpressionsDiagnostic
singletonDisjointUnionDiagnostics =
refl
singletonDisjointUnionRejected :
Clean singletonDisjointUnionResult → ⊥
singletonDisjointUnionRejected clean =
clean
datatypeDefinitionMissingDatatypeDocument : RawOntology
datatypeDefinitionMissingDatatypeDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated []
(rawDatatypeDefinition dataRangeMissingDatatypeIri rawDataTop)
∷ [])
datatypeDefinitionMissingDatatypeResult : ElaborationResult
datatypeDefinitionMissingDatatypeResult =
elaborateStructuralKernelStrict datatypeDefinitionMissingDatatypeDocument
datatypeDefinitionMissingDatatypeDiagnostics :
diagnostics datatypeDefinitionMissingDatatypeResult ≡
singleDiagnostic (undeclaredDatatypeDiagnostic dataRangeMissingDatatypeIri)
datatypeDefinitionMissingDatatypeDiagnostics =
refl
datatypeDefinitionMissingDatatypeRejected :
Clean datatypeDefinitionMissingDatatypeResult → ⊥
datatypeDefinitionMissingDatatypeRejected clean =
clean
hasKeyMissingObjectPropertyDocument : RawOntology
hasKeyMissingObjectPropertyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rawAnnotated []
(rawHasKey
(rawNamedClass rawClassIri)
(rawObjectProperty missingObjectPropertyIri ∷ [])
[])
∷ [])
hasKeyMissingObjectPropertyResult : ElaborationResult
hasKeyMissingObjectPropertyResult =
elaborateStructuralKernelStrict hasKeyMissingObjectPropertyDocument
hasKeyMissingObjectPropertyDiagnostics :
diagnostics hasKeyMissingObjectPropertyResult ≡
singleDiagnostic
(undeclaredObjectPropertyDiagnostic missingObjectPropertyIri)
hasKeyMissingObjectPropertyDiagnostics =
refl
hasKeyMissingObjectPropertyRejected :
Clean hasKeyMissingObjectPropertyResult → ⊥
hasKeyMissingObjectPropertyRejected clean =
clean
hasKeyNonSimpleObjectPropertyDocument : RawOntology
hasKeyNonSimpleObjectPropertyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
nonSimpleObjectPropertyAxiom ∷
rawAnnotated []
(rawTransitiveObjectProperty
(rawObjectProperty nonSimpleObjectPropertyIri))
∷
rawAnnotated []
(rawHasKey
(rawNamedClass rawClassIri)
(rawObjectProperty nonSimpleObjectPropertyIri ∷ [])
[])
∷ [])
hasKeyNonSimpleObjectPropertyResult : ElaborationResult
hasKeyNonSimpleObjectPropertyResult =
elaborateStructuralKernelStrict hasKeyNonSimpleObjectPropertyDocument
hasKeyNonSimpleObjectPropertyDiagnostics :
diagnostics hasKeyNonSimpleObjectPropertyResult ≡
singleDiagnostic
(nonSimpleObjectPropertyDiagnostic nonSimpleObjectPropertyIri)
hasKeyNonSimpleObjectPropertyDiagnostics =
refl
hasKeyNonSimpleObjectPropertyRejected :
Clean hasKeyNonSimpleObjectPropertyResult → ⊥
hasKeyNonSimpleObjectPropertyRejected clean =
clean
hasKeyNonSimpleObjectPropertyEvidenceAbsent :
evidence? hasKeyNonSimpleObjectPropertyResult ≡ absent
hasKeyNonSimpleObjectPropertyEvidenceAbsent =
refl
hasKeyNonSimpleObjectPropertyEvidenceUnavailable :
EvidenceUnavailable hasKeyNonSimpleObjectPropertyResult
hasKeyNonSimpleObjectPropertyEvidenceUnavailable =
evidenceUnavailable
hasKeyNonSimpleObjectPropertyResult
hasKeyNonSimpleObjectPropertyEvidenceAbsent
emptyDataIntersectionDocument : RawOntology
emptyDataIntersectionDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rawAnnotated []
(rawDataPropertyRange
(rawDataProperty rejectedDataPropertyIri)
(rawDataIntersectionOf []))
∷ [])
emptyDataIntersectionResult : ElaborationResult
emptyDataIntersectionResult =
elaborateStructuralKernelStrict emptyDataIntersectionDocument
emptyDataIntersectionDiagnostics :
diagnostics emptyDataIntersectionResult ≡
singleDiagnostic emptyDataRangeListDiagnostic
emptyDataIntersectionDiagnostics =
refl
emptyDataIntersectionRejected :
Clean emptyDataIntersectionResult → ⊥
emptyDataIntersectionRejected clean =
clean
emptyDataOneOfDocument : RawOntology
emptyDataOneOfDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rawAnnotated []
(rawDataPropertyRange
(rawDataProperty rejectedDataPropertyIri)
(rawDataOneOf []))
∷ [])
emptyDataOneOfResult : ElaborationResult
emptyDataOneOfResult =
elaborateStructuralKernelStrict emptyDataOneOfDocument
emptyDataOneOfDiagnostics :
diagnostics emptyDataOneOfResult ≡
singleDiagnostic emptyLiteralListDiagnostic
emptyDataOneOfDiagnostics =
refl
emptyDataOneOfRejected :
Clean emptyDataOneOfResult → ⊥
emptyDataOneOfRejected clean =
clean
nestedDataRangeMissingDatatypeDocument : RawOntology
nestedDataRangeMissingDatatypeDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rawAnnotated []
(rawDataPropertyRange
(rawDataProperty rejectedDataPropertyIri)
(rawDataComplementOf
(rawDatatype dataRangeMissingDatatypeIri)))
∷ [])
nestedDataRangeMissingDatatypeResult : ElaborationResult
nestedDataRangeMissingDatatypeResult =
elaborateStructuralKernelStrict nestedDataRangeMissingDatatypeDocument
nestedDataRangeMissingDatatypeDiagnostics :
diagnostics nestedDataRangeMissingDatatypeResult ≡
singleDiagnostic (undeclaredDatatypeDiagnostic dataRangeMissingDatatypeIri)
nestedDataRangeMissingDatatypeDiagnostics =
refl
nestedDataRangeMissingDatatypeRejected :
Clean nestedDataRangeMissingDatatypeResult → ⊥
nestedDataRangeMissingDatatypeRejected clean =
clean
dataOneOfMissingLiteralDatatypeDocument : RawOntology
dataOneOfMissingLiteralDatatypeDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rawAnnotated []
(rawDataPropertyRange
(rawDataProperty rejectedDataPropertyIri)
(rawDataOneOf
(rawLiteral "hello" absent absent ∷ [])))
∷ [])
dataOneOfMissingLiteralDatatypeResult : ElaborationResult
dataOneOfMissingLiteralDatatypeResult =
elaborateStructuralKernelStrict dataOneOfMissingLiteralDatatypeDocument
dataOneOfMissingLiteralDatatypeDiagnostics :
diagnostics dataOneOfMissingLiteralDatatypeResult ≡
singleDiagnostic missingLiteralDatatypeDiagnostic
dataOneOfMissingLiteralDatatypeDiagnostics =
refl
dataOneOfMissingLiteralDatatypeRejected :
Clean dataOneOfMissingLiteralDatatypeResult → ⊥
dataOneOfMissingLiteralDatatypeRejected clean =
clean
datatypeRestrictionMissingDatatypeDocument : RawOntology
datatypeRestrictionMissingDatatypeDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rawAnnotated []
(rawDataPropertyRange
(rawDataProperty rejectedDataPropertyIri)
(rawDatatypeRestriction dataRangeMissingDatatypeIri []))
∷ [])
datatypeRestrictionMissingDatatypeResult : ElaborationResult
datatypeRestrictionMissingDatatypeResult =
elaborateStructuralKernelStrict datatypeRestrictionMissingDatatypeDocument
datatypeRestrictionMissingDatatypeDiagnostics :
diagnostics datatypeRestrictionMissingDatatypeResult ≡
singleDiagnostic (undeclaredDatatypeDiagnostic dataRangeMissingDatatypeIri)
datatypeRestrictionMissingDatatypeDiagnostics =
refl
datatypeRestrictionMissingDatatypeRejected :
Clean datatypeRestrictionMissingDatatypeResult → ⊥
datatypeRestrictionMissingDatatypeRejected clean =
clean
datatypeRestrictionFacetDocument : RawOntology
datatypeRestrictionFacetDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rejectedDatatypeAxiom ∷
rawAnnotated []
(rawDataPropertyRange
(rawDataProperty rejectedDataPropertyIri)
(rawDatatypeRestriction
rejectedDatatypeIri
(rawFacetRestriction
rejectedDatatypeIri
(rawLiteral "5" absent absent)
∷ [])))
∷ [])
datatypeRestrictionFacetResult : ElaborationResult
datatypeRestrictionFacetResult =
elaborateStructuralKernelStrict datatypeRestrictionFacetDocument
datatypeRestrictionFacetDiagnostics :
diagnostics datatypeRestrictionFacetResult ≡
singleDiagnostic missingLiteralDatatypeDiagnostic
datatypeRestrictionFacetDiagnostics =
refl
datatypeRestrictionFacetRejected :
Clean datatypeRestrictionFacetResult → ⊥
datatypeRestrictionFacetRejected clean =
clean
missingLiteralDatatypeDocument : RawOntology
missingLiteralDatatypeDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rejectedIndividualAxiom ∷
rawAnnotated []
(rawDataPropertyAssertion
(rawDataProperty rejectedDataPropertyIri)
(rawNamedIndividual rejectedIndividualIri)
(rawLiteral "hello" absent absent))
∷ [])
missingLiteralDatatypeResult : ElaborationResult
missingLiteralDatatypeResult =
elaborateStructuralKernelStrict missingLiteralDatatypeDocument
missingLiteralDatatypeDiagnostics :
diagnostics missingLiteralDatatypeResult ≡
singleDiagnostic missingLiteralDatatypeDiagnostic
missingLiteralDatatypeDiagnostics =
refl
missingLiteralDatatypeRejected :
Clean missingLiteralDatatypeResult → ⊥
missingLiteralDatatypeRejected clean =
clean
undeclaredLiteralDatatypeIri : RawIRI
undeclaredLiteralDatatypeIri =
rawIRI "http://example.test/MissingDatatype"
undeclaredLiteralDatatypeDocument : RawOntology
undeclaredLiteralDatatypeDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rejectedIndividualAxiom ∷
rawAnnotated []
(rawDataPropertyAssertion
(rawDataProperty rejectedDataPropertyIri)
(rawNamedIndividual rejectedIndividualIri)
(rawLiteral
"hello"
(present undeclaredLiteralDatatypeIri)
absent))
∷ [])
undeclaredLiteralDatatypeResult : ElaborationResult
undeclaredLiteralDatatypeResult =
elaborateStructuralKernelStrict undeclaredLiteralDatatypeDocument
undeclaredLiteralDatatypeDiagnostics :
diagnostics undeclaredLiteralDatatypeResult ≡
singleDiagnostic (undeclaredDatatypeDiagnostic undeclaredLiteralDatatypeIri)
undeclaredLiteralDatatypeDiagnostics =
refl
undeclaredLiteralDatatypeRejected :
Clean undeclaredLiteralDatatypeResult → ⊥
undeclaredLiteralDatatypeRejected clean =
clean
languageTaggedLiteralDocument : RawOntology
languageTaggedLiteralDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rejectedDataPropertyAxiom ∷
rejectedIndividualAxiom ∷
rejectedDatatypeAxiom ∷
rawAnnotated []
(rawDataPropertyAssertion
(rawDataProperty rejectedDataPropertyIri)
(rawNamedIndividual rejectedIndividualIri)
(rawLiteral "hello" (present rejectedDatatypeIri) (present "en")))
∷ [])
languageTaggedLiteralResult : ElaborationResult
languageTaggedLiteralResult =
elaborateStructuralKernelStrict languageTaggedLiteralDocument
languageTaggedLiteralDiagnostics :
diagnostics languageTaggedLiteralResult ≡
singleDiagnostic (unsupportedLanguageTaggedLiteralDiagnostic "en")
languageTaggedLiteralDiagnostics =
refl
languageTaggedLiteralRejected :
Clean languageTaggedLiteralResult → ⊥
languageTaggedLiteralRejected clean =
clean
dataHasValueMissingDatatypeDocument : RawOntology
dataHasValueMissingDatatypeDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawClassAxiom ∷
rejectedDataPropertyAxiom ∷
rawAnnotated []
(rawSubClassOf
(rawNamedClass rawClassIri)
(rawDataHasValue
(rawDataProperty rejectedDataPropertyIri)
(rawLiteral "hello" absent absent)))
∷ [])
dataHasValueMissingDatatypeResult : ElaborationResult
dataHasValueMissingDatatypeResult =
elaborateStructuralKernelStrict dataHasValueMissingDatatypeDocument
dataHasValueMissingDatatypeDiagnostics :
diagnostics dataHasValueMissingDatatypeResult ≡
singleDiagnostic missingLiteralDatatypeDiagnostic
dataHasValueMissingDatatypeDiagnostics =
refl
dataHasValueMissingDatatypeRejected :
Clean dataHasValueMissingDatatypeResult → ⊥
dataHasValueMissingDatatypeRejected clean =
clean
missingAnnotationPropertyIri : RawIRI
missingAnnotationPropertyIri =
rawIRI "http://example.test/MissingAnnotationProperty"
annotationAssertionSubjectIri : RawIRI
annotationAssertionSubjectIri =
rawIRI "http://example.test/AnnotationSubject"
annotationAssertionValueIri : RawIRI
annotationAssertionValueIri =
rawIRI "http://example.test/AnnotationValue"
undeclaredAnnotationPropertyDocument : RawOntology
undeclaredAnnotationPropertyDocument =
rawOntology
anonymousSource
absent
absent
[]
[]
(rawAnnotated []
(rawAnnotationAssertion
missingAnnotationPropertyIri
(rawAnnotationSubjectIRI annotationAssertionSubjectIri)
(rawAnnotationValueIRI annotationAssertionValueIri))
∷ [])
undeclaredAnnotationPropertyResult : ElaborationResult
undeclaredAnnotationPropertyResult =
elaborateStructuralKernelStrict undeclaredAnnotationPropertyDocument
undeclaredAnnotationPropertyDiagnostics :
diagnostics undeclaredAnnotationPropertyResult ≡
singleDiagnostic
(undeclaredAnnotationPropertyDiagnostic missingAnnotationPropertyIri)
undeclaredAnnotationPropertyDiagnostics =
refl
undeclaredAnnotationPropertyRejected :
Clean undeclaredAnnotationPropertyResult → ⊥
undeclaredAnnotationPropertyRejected clean =
clean