OWL2.Corpus.Rejected.RawImports

{-# OPTIONS --safe --cubical #-}

module OWL2.Corpus.Rejected.RawImports where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab
open import OWL2.Elab.ImportProject.Legacy
open import OWL2.Raw

rejectedVocabularyOntologyIRI rejectedProjectOntologyIRI : RawIRI
rejectedVocabularyOntologyIRI =
  rawIRI "http://example.test/imports/vocabulary"
rejectedProjectOntologyIRI =
  rawIRI "http://example.test/imports/project"

rejectedVocabularyVersionIRI : RawIRI
rejectedVocabularyVersionIRI =
  rawIRI "http://example.test/imports/vocabulary/version/1"

rejectedTransitiveLeafOntologyIRI rejectedTransitiveMiddleOntologyIRI
  rejectedTransitiveProjectOntologyIRI : RawIRI
rejectedTransitiveLeafOntologyIRI =
  rawIRI "http://example.test/imports/transitive/leaf"
rejectedTransitiveMiddleOntologyIRI =
  rawIRI "http://example.test/imports/transitive/middle"
rejectedTransitiveProjectOntologyIRI =
  rawIRI "http://example.test/imports/transitive/project"

rejectedDataVocabularyOntologyIRI rejectedDataProjectOntologyIRI : RawIRI
rejectedDataVocabularyOntologyIRI =
  rawIRI "http://example.test/imports/data/vocabulary"
rejectedDataProjectOntologyIRI =
  rawIRI "http://example.test/imports/data/project"

rejectedPunnedVocabularyOntologyIRI rejectedPunnedProjectOntologyIRI : RawIRI
rejectedPunnedVocabularyOntologyIRI =
  rawIRI "http://example.test/imports/punned/vocabulary"
rejectedPunnedProjectOntologyIRI =
  rawIRI "http://example.test/imports/punned/project"

rejectedNonSimpleKeyVocabularyOntologyIRI
  rejectedNonSimpleKeyProjectOntologyIRI : RawIRI
rejectedNonSimpleKeyVocabularyOntologyIRI =
  rawIRI "http://example.test/imports/non-simple-key/vocabulary"
rejectedNonSimpleKeyProjectOntologyIRI =
  rawIRI "http://example.test/imports/non-simple-key/project"

rejectedResolvedVocabularyOntologyIRI
  rejectedUnresolvedClassProjectOntologyIRI
  rejectedUnresolvedPropertyProjectOntologyIRI : RawIRI
rejectedResolvedVocabularyOntologyIRI =
  rawIRI "http://example.test/imports/resolved/vocabulary"
rejectedUnresolvedClassProjectOntologyIRI =
  rawIRI "http://example.test/imports/resolved/missing-class-project"
rejectedUnresolvedPropertyProjectOntologyIRI =
  rawIRI "http://example.test/imports/resolved/missing-property-project"

rejectedResourceClassIRI rejectedProjectDatasetClassIRI : RawIRI
rejectedResourceClassIRI =
  rawIRI "http://example.test/imports#Resource"
rejectedProjectDatasetClassIRI =
  rawIRI "http://example.test/imports#ProjectDataset"

rejectedMissingImportedClassIRI rejectedMissingImportedObjectPropertyIRI :
  RawIRI
rejectedMissingImportedClassIRI =
  rawIRI "http://example.test/imports/resolved#MissingClass"
rejectedMissingImportedObjectPropertyIRI =
  rawIRI "http://example.test/imports/resolved#missingProperty"

rejectedTransitiveMiddleClassIRI rejectedTransitiveRootClassIRI : RawIRI
rejectedTransitiveMiddleClassIRI =
  rawIRI "http://example.test/imports/transitive#MiddleResource"
rejectedTransitiveRootClassIRI =
  rawIRI "http://example.test/imports/transitive#RootDataset"

rejectedSharedTitleIRI rejectedMissingStringDatatypeIRI
  rejectedDatasetOneIRI rejectedDataDatasetClassIRI : RawIRI
rejectedSharedTitleIRI =
  rawIRI "http://example.test/imports/data#title"
rejectedMissingStringDatatypeIRI =
  rawIRI "http://www.w3.org/2001/XMLSchema#string"
rejectedDatasetOneIRI =
  rawIRI "http://example.test/imports/data#dataset-1"
rejectedDataDatasetClassIRI =
  rawIRI "http://example.test/imports/data#Dataset"

rejectedCrossDocumentPunnedIRI : RawIRI
rejectedCrossDocumentPunnedIRI =
  rawIRI "http://example.test/imports/punned#Entity"

rejectedNonSimpleKeyClassIRI rejectedNonSimpleKeyPropertyIRI : RawIRI
rejectedNonSimpleKeyClassIRI =
  rawIRI "http://example.test/imports/non-simple-key#Dataset"
rejectedNonSimpleKeyPropertyIRI =
  rawIRI "http://example.test/imports/non-simple-key#relatedTo"

rejectedResourceDeclaration : RawAnnotated RawAxiom
rejectedResourceDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass rejectedResourceClassIRI))

rejectedProjectDatasetDeclaration : RawAnnotated RawAxiom
rejectedProjectDatasetDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass rejectedProjectDatasetClassIRI))

rejectedTransitiveMiddleDeclaration rejectedTransitiveRootDeclaration :
  RawAnnotated RawAxiom
rejectedTransitiveMiddleDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass rejectedTransitiveMiddleClassIRI))
rejectedTransitiveRootDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass rejectedTransitiveRootClassIRI))

rejectedTransitiveRootSubClassMiddleAxiom : RawAnnotated RawAxiom
rejectedTransitiveRootSubClassMiddleAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass rejectedTransitiveRootClassIRI)
      (rawNamedClass rejectedTransitiveMiddleClassIRI))

rejectedSharedTitleDeclaration rejectedDatasetOneDeclaration
  rejectedDataDatasetDeclaration : RawAnnotated RawAxiom
rejectedSharedTitleDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawDataProperty rejectedSharedTitleIRI))
rejectedDatasetOneDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawIndividual rejectedDatasetOneIRI))
rejectedDataDatasetDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass rejectedDataDatasetClassIRI))

rejectedDatasetOneClassAssertion : RawAnnotated RawAxiom
rejectedDatasetOneClassAssertion =
  rawAnnotated []
    (rawClassAssertion
      (rawNamedClass rejectedDataDatasetClassIRI)
      (rawNamedIndividual rejectedDatasetOneIRI))

rejectedMissingDatatypeTitleLiteral : RawLiteral
rejectedMissingDatatypeTitleLiteral =
  rawLiteral "Dataset one" (present rejectedMissingStringDatatypeIRI) absent

rejectedDatasetTitleAssertion : RawAnnotated RawAxiom
rejectedDatasetTitleAssertion =
  rawAnnotated []
    (rawDataPropertyAssertion
      (rawDataProperty rejectedSharedTitleIRI)
      (rawNamedIndividual rejectedDatasetOneIRI)
      rejectedMissingDatatypeTitleLiteral)

rejectedPunnedClassDeclaration rejectedPunnedObjectPropertyDeclaration :
  RawAnnotated RawAxiom
rejectedPunnedClassDeclaration =
  rawAnnotated []
    (rawDeclaration
      (rawEntity rawClass rejectedCrossDocumentPunnedIRI))
rejectedPunnedObjectPropertyDeclaration =
  rawAnnotated []
    (rawDeclaration
      (rawEntity rawObjectProperty rejectedCrossDocumentPunnedIRI))

rejectedNonSimpleKeyClassDeclaration
  rejectedNonSimpleKeyPropertyDeclaration : RawAnnotated RawAxiom
rejectedNonSimpleKeyClassDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass rejectedNonSimpleKeyClassIRI))
rejectedNonSimpleKeyPropertyDeclaration =
  rawAnnotated []
    (rawDeclaration
      (rawEntity rawObjectProperty rejectedNonSimpleKeyPropertyIRI))

rejectedNonSimpleKeyTransitiveAxiom : RawAnnotated RawAxiom
rejectedNonSimpleKeyTransitiveAxiom =
  rawAnnotated []
    (rawTransitiveObjectProperty
      (rawObjectProperty rejectedNonSimpleKeyPropertyIRI))

rejectedNonSimpleKeyHasKeyAxiom : RawAnnotated RawAxiom
rejectedNonSimpleKeyHasKeyAxiom =
  rawAnnotated []
    (rawHasKey
      (rawNamedClass rejectedNonSimpleKeyClassIRI)
      (rawObjectProperty rejectedNonSimpleKeyPropertyIRI ∷ [])
      [])

rejectedResolvedVocabularyResourceDeclaration : RawAnnotated RawAxiom
rejectedResolvedVocabularyResourceDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass rejectedResourceClassIRI))

rejectedUnresolvedClassSubClassAxiom : RawAnnotated RawAxiom
rejectedUnresolvedClassSubClassAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass rejectedProjectDatasetClassIRI)
      (rawNamedClass rejectedMissingImportedClassIRI))

rejectedUnresolvedPropertyRestrictionAxiom : RawAnnotated RawAxiom
rejectedUnresolvedPropertyRestrictionAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass rejectedProjectDatasetClassIRI)
      (rawObjectSomeValuesFrom
        (rawObjectProperty rejectedMissingImportedObjectPropertyIRI)
        (rawNamedClass rejectedResourceClassIRI)))

rejectedProjectDocument rejectedVocabularyDocument
  rejectedDuplicateVocabularyDocument
  rejectedVersionedVocabularyDocument : RawOntology
rejectedProjectDocument =
  rawOntology
    anonymousSource
    (present rejectedProjectOntologyIRI)
    absent
    (rejectedVocabularyOntologyIRI ∷ [])
    []
    (rejectedProjectDatasetDeclaration ∷ [])
rejectedVocabularyDocument =
  rawOntology
    anonymousSource
    (present rejectedVocabularyOntologyIRI)
    absent
    []
    []
    (rejectedResourceDeclaration ∷ [])
rejectedDuplicateVocabularyDocument =
  rawOntology
    anonymousSource
    (present rejectedVocabularyOntologyIRI)
    absent
    []
    []
    []
rejectedVersionedVocabularyDocument =
  rawOntology
    anonymousSource
    (present rejectedVocabularyOntologyIRI)
    (present rejectedVocabularyVersionIRI)
    []
    []
    []

rejectedTransitiveMiddleDocument rejectedTransitiveProjectDocument :
  RawOntology
rejectedTransitiveMiddleDocument =
  rawOntology
    anonymousSource
    (present rejectedTransitiveMiddleOntologyIRI)
    absent
    (rejectedTransitiveLeafOntologyIRI ∷ [])
    []
    (rejectedTransitiveMiddleDeclaration ∷ [])
rejectedTransitiveProjectDocument =
  rawOntology
    anonymousSource
    (present rejectedTransitiveProjectOntologyIRI)
    absent
    (rejectedTransitiveMiddleOntologyIRI ∷ [])
    []
    ( rejectedTransitiveRootDeclaration
    ∷ rejectedTransitiveRootSubClassMiddleAxiom
    ∷ [] )

rejectedDataProjectDocument rejectedDataVocabularyDocument : RawOntology
rejectedDataProjectDocument =
  rawOntology
    anonymousSource
    (present rejectedDataProjectOntologyIRI)
    absent
    (rejectedDataVocabularyOntologyIRI ∷ [])
    []
    ( rejectedDataDatasetDeclaration
    ∷ rejectedDatasetOneDeclaration
    ∷ rejectedDatasetOneClassAssertion
    ∷ rejectedDatasetTitleAssertion
    ∷ [] )
rejectedDataVocabularyDocument =
  rawOntology
    anonymousSource
    (present rejectedDataVocabularyOntologyIRI)
    absent
    []
    []
    (rejectedSharedTitleDeclaration ∷ [])

rejectedPunnedProjectDocument rejectedPunnedVocabularyDocument : RawOntology
rejectedPunnedProjectDocument =
  rawOntology
    anonymousSource
    (present rejectedPunnedProjectOntologyIRI)
    absent
    (rejectedPunnedVocabularyOntologyIRI ∷ [])
    []
    (rejectedPunnedClassDeclaration ∷ [])
rejectedPunnedVocabularyDocument =
  rawOntology
    anonymousSource
    (present rejectedPunnedVocabularyOntologyIRI)
    absent
    []
    []
    (rejectedPunnedObjectPropertyDeclaration ∷ [])

rejectedNonSimpleKeyProjectDocument
  rejectedNonSimpleKeyVocabularyDocument : RawOntology
rejectedNonSimpleKeyProjectDocument =
  rawOntology
    anonymousSource
    (present rejectedNonSimpleKeyProjectOntologyIRI)
    absent
    (rejectedNonSimpleKeyVocabularyOntologyIRI ∷ [])
    []
    ( rejectedNonSimpleKeyClassDeclaration
    ∷ rejectedNonSimpleKeyHasKeyAxiom
    ∷ [] )
rejectedNonSimpleKeyVocabularyDocument =
  rawOntology
    anonymousSource
    (present rejectedNonSimpleKeyVocabularyOntologyIRI)
    absent
    []
    []
    ( rejectedNonSimpleKeyPropertyDeclaration
    ∷ rejectedNonSimpleKeyTransitiveAxiom
    ∷ [] )

rejectedResolvedVocabularyDocument
  rejectedUnresolvedClassProjectDocument
  rejectedUnresolvedPropertyProjectDocument : RawOntology
rejectedResolvedVocabularyDocument =
  rawOntology
    anonymousSource
    (present rejectedResolvedVocabularyOntologyIRI)
    absent
    []
    []
    (rejectedResolvedVocabularyResourceDeclaration ∷ [])
rejectedUnresolvedClassProjectDocument =
  rawOntology
    anonymousSource
    (present rejectedUnresolvedClassProjectOntologyIRI)
    absent
    (rejectedResolvedVocabularyOntologyIRI ∷ [])
    []
    ( rejectedProjectDatasetDeclaration
    ∷ rejectedUnresolvedClassSubClassAxiom
    ∷ [] )
rejectedUnresolvedPropertyProjectDocument =
  rawOntology
    anonymousSource
    (present rejectedUnresolvedPropertyProjectOntologyIRI)
    absent
    (rejectedResolvedVocabularyOntologyIRI ∷ [])
    []
    ( rejectedProjectDatasetDeclaration
    ∷ rejectedUnresolvedPropertyRestrictionAxiom
    ∷ [] )

missingImportProject : RawImportProject
missingImportProject =
  rawImportProject rejectedProjectDocument []

missingImportProjectResult :
  ImportProjectElaborationResult strictPolicy
missingImportProjectResult =
  elaborateImportProjectStrict missingImportProject

missingImportProjectDiagnostics :
  diagnostics missingImportProjectResult ≡
  singleDiagnostic (missingImportDiagnostic rejectedVocabularyOntologyIRI)
missingImportProjectDiagnostics =
  refl

missingImportProjectEvidenceAbsent :
  evidence? missingImportProjectResult ≡ absent
missingImportProjectEvidenceAbsent =
  refl

missingImportProjectRejected :
  Clean missingImportProjectResult → ⊥
missingImportProjectRejected clean =
  clean

missingImportProjectEvidenceUnavailable :
  EvidenceUnavailable missingImportProjectResult
missingImportProjectEvidenceUnavailable =
  evidenceUnavailable
    missingImportProjectResult
    missingImportProjectEvidenceAbsent

missingImportProjectVocabularyImportIDAbsent :
  ontologyIDInDocuments
    (importOntologyID rejectedVocabularyOntologyIRI)
    (projectDocuments missingImportProject) ≡
  false
missingImportProjectVocabularyImportIDAbsent =
  refl

duplicateOntologyIRIProject : RawImportProject
duplicateOntologyIRIProject =
  rawImportProject
    rejectedProjectDocument
    (rejectedVocabularyDocument ∷ rejectedDuplicateVocabularyDocument ∷ [])

duplicateOntologyIRIProjectResult :
  ImportProjectElaborationResult strictPolicy
duplicateOntologyIRIProjectResult =
  elaborateImportProjectStrict duplicateOntologyIRIProject

duplicateOntologyIRIProjectDiagnostics :
  diagnostics duplicateOntologyIRIProjectResult ≡
  singleDiagnostic
    (duplicateOntologyIRIDiagnostic rejectedVocabularyOntologyIRI) ++
  singleDiagnostic
    (ambiguousImportDiagnostic rejectedVocabularyOntologyIRI)
duplicateOntologyIRIProjectDiagnostics =
  refl

duplicateOntologyIRIProjectEvidenceAbsent :
  evidence? duplicateOntologyIRIProjectResult ≡ absent
duplicateOntologyIRIProjectEvidenceAbsent =
  refl

duplicateOntologyIRIProjectDuplicateIDFound :
  rawOntologyIDInList
    (sourceOntologyID rejectedDuplicateVocabularyDocument)
    (sourceOntologyID rejectedVocabularyDocument ∷ []) ≡
  true
duplicateOntologyIRIProjectDuplicateIDFound =
  refl

duplicateOntologyIRIProjectRejected :
  Clean duplicateOntologyIRIProjectResult → ⊥
duplicateOntologyIRIProjectRejected clean =
  clean

duplicateOntologyIRIProjectEvidenceUnavailable :
  EvidenceUnavailable duplicateOntologyIRIProjectResult
duplicateOntologyIRIProjectEvidenceUnavailable =
  evidenceUnavailable
    duplicateOntologyIRIProjectResult
    duplicateOntologyIRIProjectEvidenceAbsent

ambiguousImportProject : RawImportProject
ambiguousImportProject =
  rawImportProject
    rejectedProjectDocument
    (rejectedVocabularyDocument ∷ rejectedVersionedVocabularyDocument ∷ [])

transitiveMissingImportProject : RawImportProject
transitiveMissingImportProject =
  rawImportProject
    rejectedTransitiveProjectDocument
    (rejectedTransitiveMiddleDocument ∷ [])

sharedDataPropertyMissingDatatypeImportProject : RawImportProject
sharedDataPropertyMissingDatatypeImportProject =
  rawImportProject
    rejectedDataProjectDocument
    (rejectedDataVocabularyDocument ∷ [])

crossDocumentPunningImportProject : RawImportProject
crossDocumentPunningImportProject =
  rawImportProject
    rejectedPunnedProjectDocument
    (rejectedPunnedVocabularyDocument ∷ [])

importedNonSimpleKeyProject : RawImportProject
importedNonSimpleKeyProject =
  rawImportProject
    rejectedNonSimpleKeyProjectDocument
    (rejectedNonSimpleKeyVocabularyDocument ∷ [])

projectScopedUndeclaredImportedClassProject : RawImportProject
projectScopedUndeclaredImportedClassProject =
  rawImportProject
    rejectedUnresolvedClassProjectDocument
    (rejectedResolvedVocabularyDocument ∷ [])

projectScopedUndeclaredImportedPropertyProject : RawImportProject
projectScopedUndeclaredImportedPropertyProject =
  rawImportProject
    rejectedUnresolvedPropertyProjectDocument
    (rejectedResolvedVocabularyDocument ∷ [])

ambiguousImportProjectResult :
  ImportProjectElaborationResult strictPolicy
ambiguousImportProjectResult =
  elaborateImportProjectStrict ambiguousImportProject

ambiguousImportProjectDiagnostics :
  diagnostics ambiguousImportProjectResult ≡
  singleDiagnostic (ambiguousImportDiagnostic rejectedVocabularyOntologyIRI)
ambiguousImportProjectDiagnostics =
  refl

ambiguousImportProjectEvidenceAbsent :
  evidence? ambiguousImportProjectResult ≡ absent
ambiguousImportProjectEvidenceAbsent =
  refl

ambiguousImportProjectRejected :
  Clean ambiguousImportProjectResult → ⊥
ambiguousImportProjectRejected clean =
  clean

ambiguousImportProjectEvidenceUnavailable :
  EvidenceUnavailable ambiguousImportProjectResult
ambiguousImportProjectEvidenceUnavailable =
  evidenceUnavailable
    ambiguousImportProjectResult
    ambiguousImportProjectEvidenceAbsent

ambiguousImportProjectIRIIsAmbiguous :
  ontologyIRIAmbiguousInDocuments
    rejectedVocabularyOntologyIRI
    (projectDocuments ambiguousImportProject) ≡
  true
ambiguousImportProjectIRIIsAmbiguous =
  refl

ambiguousImportProjectExactIDsNotDuplicate :
  rawOntologyIDInList
    (sourceOntologyID rejectedVersionedVocabularyDocument)
    (sourceOntologyID rejectedVocabularyDocument ∷ []) ≡
  false
ambiguousImportProjectExactIDsNotDuplicate =
  refl

transitiveMissingImportProjectResult :
  ImportProjectElaborationResult strictPolicy
transitiveMissingImportProjectResult =
  elaborateImportProjectStrict transitiveMissingImportProject

transitiveMissingImportProjectDiagnostics :
  diagnostics transitiveMissingImportProjectResult ≡
  singleDiagnostic
    (missingImportDiagnostic rejectedTransitiveLeafOntologyIRI)
transitiveMissingImportProjectDiagnostics =
  refl

transitiveMissingImportProjectMissingDiagnostics :
  projectMissingDiagnostics transitiveMissingImportProject ≡
  singleDiagnostic
    (missingImportDiagnostic rejectedTransitiveLeafOntologyIRI)
transitiveMissingImportProjectMissingDiagnostics =
  refl

transitiveMissingImportProjectEvidenceAbsent :
  evidence? transitiveMissingImportProjectResult ≡ absent
transitiveMissingImportProjectEvidenceAbsent =
  refl

transitiveMissingImportProjectRejected :
  Clean transitiveMissingImportProjectResult → ⊥
transitiveMissingImportProjectRejected clean =
  clean

transitiveMissingImportProjectEvidenceUnavailable :
  EvidenceUnavailable transitiveMissingImportProjectResult
transitiveMissingImportProjectEvidenceUnavailable =
  evidenceUnavailable
    transitiveMissingImportProjectResult
    transitiveMissingImportProjectEvidenceAbsent

transitiveMissingImportProjectMiddleImportFound :
  ontologyIDInDocuments
    (importOntologyID rejectedTransitiveMiddleOntologyIRI)
    (projectDocuments transitiveMissingImportProject) ≡
  true
transitiveMissingImportProjectMiddleImportFound =
  refl

transitiveMissingImportProjectLeafImportAbsent :
  ontologyIDInDocuments
    (importOntologyID rejectedTransitiveLeafOntologyIRI)
    (projectDocuments transitiveMissingImportProject) ≡
  false
transitiveMissingImportProjectLeafImportAbsent =
  refl

sharedDataPropertyMissingDatatypeImportProjectResult :
  ImportProjectElaborationResult strictPolicy
sharedDataPropertyMissingDatatypeImportProjectResult =
  elaborateImportProjectStrict sharedDataPropertyMissingDatatypeImportProject

sharedDataPropertyMissingDatatypeImportProjectDiagnostics :
  diagnostics sharedDataPropertyMissingDatatypeImportProjectResult ≡
  singleDiagnostic
    (undeclaredDatatypeDiagnostic rejectedMissingStringDatatypeIRI)
sharedDataPropertyMissingDatatypeImportProjectDiagnostics =
  refl

sharedDataPropertyMissingDatatypeImportProjectLegacyDiagnostics :
  diagnostics
    (elaborateCheckedImportProjectStrict
      sharedDataPropertyMissingDatatypeImportProject) ≡
  singleDiagnostic (undeclaredDataPropertyDiagnostic rejectedSharedTitleIRI) ++
  singleDiagnostic
    (undeclaredDatatypeDiagnostic rejectedMissingStringDatatypeIRI)
sharedDataPropertyMissingDatatypeImportProjectLegacyDiagnostics =
  refl

sharedDataPropertyMissingDatatypeImportProjectMissingDiagnostics :
  projectMissingDiagnostics sharedDataPropertyMissingDatatypeImportProject ≡
  noDiagnostics
sharedDataPropertyMissingDatatypeImportProjectMissingDiagnostics =
  refl

sharedDataPropertyMissingDatatypeImportProjectDataImportFound :
  ontologyIDInDocuments
    (importOntologyID rejectedDataVocabularyOntologyIRI)
    (projectDocuments sharedDataPropertyMissingDatatypeImportProject) ≡
  true
sharedDataPropertyMissingDatatypeImportProjectDataImportFound =
  refl

sharedDataPropertyMissingDatatypeImportProjectEvidenceAbsent :
  evidence? sharedDataPropertyMissingDatatypeImportProjectResult ≡ absent
sharedDataPropertyMissingDatatypeImportProjectEvidenceAbsent =
  refl

sharedDataPropertyMissingDatatypeImportProjectRejected :
  Clean sharedDataPropertyMissingDatatypeImportProjectResult → ⊥
sharedDataPropertyMissingDatatypeImportProjectRejected clean =
  clean

sharedDataPropertyMissingDatatypeImportProjectEvidenceUnavailable :
  EvidenceUnavailable sharedDataPropertyMissingDatatypeImportProjectResult
sharedDataPropertyMissingDatatypeImportProjectEvidenceUnavailable =
  evidenceUnavailable
    sharedDataPropertyMissingDatatypeImportProjectResult
    sharedDataPropertyMissingDatatypeImportProjectEvidenceAbsent

crossDocumentPunningImportProjectResult :
  ImportProjectElaborationResult strictPolicy
crossDocumentPunningImportProjectResult =
  elaborateImportProjectStrict crossDocumentPunningImportProject

crossDocumentPunningImportProjectDiagnostics :
  diagnostics crossDocumentPunningImportProjectResult ≡
  singleDiagnostic
    (punningDeclarationDiagnostic rejectedCrossDocumentPunnedIRI)
crossDocumentPunningImportProjectDiagnostics =
  refl

crossDocumentPunningLegacyResult :
  CheckedImportProjectElaborationResult strictPolicy
crossDocumentPunningLegacyResult =
  elaborateCheckedImportProjectStrict crossDocumentPunningImportProject

crossDocumentPunningLegacyDiagnostics :
  diagnostics crossDocumentPunningLegacyResult ≡ noDiagnostics
crossDocumentPunningLegacyDiagnostics =
  refl

crossDocumentPunningLegacyClean :
  Clean crossDocumentPunningLegacyResult
crossDocumentPunningLegacyClean =
  tt

crossDocumentPunningLegacyEvidence :
  EvidenceAvailable crossDocumentPunningLegacyResult
crossDocumentPunningLegacyEvidence =
  cleanEvidence
    crossDocumentPunningLegacyResult
    crossDocumentPunningLegacyClean

crossDocumentPunningImportProjectMissingDiagnostics :
  projectMissingDiagnostics crossDocumentPunningImportProject ≡
  noDiagnostics
crossDocumentPunningImportProjectMissingDiagnostics =
  refl

crossDocumentPunningImportProjectStructuralDiagnostics :
  projectScopedStructuralDiagnostics crossDocumentPunningImportProject ≡
  singleDiagnostic
    (punningDeclarationDiagnostic rejectedCrossDocumentPunnedIRI)
crossDocumentPunningImportProjectStructuralDiagnostics =
  refl

crossDocumentPunningImportProjectImportFound :
  ontologyIDInDocuments
    (importOntologyID rejectedPunnedVocabularyOntologyIRI)
    (projectDocuments crossDocumentPunningImportProject) ≡
  true
crossDocumentPunningImportProjectImportFound =
  refl

crossDocumentPunningImportProjectEvidenceAbsent :
  evidence? crossDocumentPunningImportProjectResult ≡ absent
crossDocumentPunningImportProjectEvidenceAbsent =
  refl

crossDocumentPunningImportProjectRejected :
  Clean crossDocumentPunningImportProjectResult → ⊥
crossDocumentPunningImportProjectRejected clean =
  clean

crossDocumentPunningImportProjectEvidenceUnavailable :
  EvidenceUnavailable crossDocumentPunningImportProjectResult
crossDocumentPunningImportProjectEvidenceUnavailable =
  evidenceUnavailable
    crossDocumentPunningImportProjectResult
    crossDocumentPunningImportProjectEvidenceAbsent

importedNonSimpleKeyProjectResult :
  ImportProjectElaborationResult strictPolicy
importedNonSimpleKeyProjectResult =
  elaborateImportProjectStrict importedNonSimpleKeyProject

importedNonSimpleKeyProjectDiagnostics :
  diagnostics importedNonSimpleKeyProjectResult ≡
  singleDiagnostic
    (nonSimpleObjectPropertyDiagnostic rejectedNonSimpleKeyPropertyIRI)
importedNonSimpleKeyProjectDiagnostics =
  refl

importedNonSimpleKeyProjectMissingDiagnostics :
  projectMissingDiagnostics importedNonSimpleKeyProject ≡
  noDiagnostics
importedNonSimpleKeyProjectMissingDiagnostics =
  refl

importedNonSimpleKeyProjectRootScopedDiagnostics :
  projectDocumentScopedDiagnostics
    importedNonSimpleKeyProject
    rejectedNonSimpleKeyProjectDocument ≡
  singleDiagnostic
    (nonSimpleObjectPropertyDiagnostic rejectedNonSimpleKeyPropertyIRI)
importedNonSimpleKeyProjectRootScopedDiagnostics =
  refl

importedNonSimpleKeyProjectLegacyDiagnostics :
  diagnostics
    (elaborateCheckedImportProjectStrict importedNonSimpleKeyProject) ≡
  singleDiagnostic
    (undeclaredObjectPropertyDiagnostic rejectedNonSimpleKeyPropertyIRI)
importedNonSimpleKeyProjectLegacyDiagnostics =
  refl

importedNonSimpleKeyProjectImportFound :
  ontologyIDInDocuments
    (importOntologyID rejectedNonSimpleKeyVocabularyOntologyIRI)
    (projectDocuments importedNonSimpleKeyProject) ≡
  true
importedNonSimpleKeyProjectImportFound =
  refl

importedNonSimpleKeyProjectEvidenceAbsent :
  evidence? importedNonSimpleKeyProjectResult ≡ absent
importedNonSimpleKeyProjectEvidenceAbsent =
  refl

importedNonSimpleKeyProjectRejected :
  Clean importedNonSimpleKeyProjectResult → ⊥
importedNonSimpleKeyProjectRejected clean =
  clean

importedNonSimpleKeyProjectEvidenceUnavailable :
  EvidenceUnavailable importedNonSimpleKeyProjectResult
importedNonSimpleKeyProjectEvidenceUnavailable =
  evidenceUnavailable
    importedNonSimpleKeyProjectResult
    importedNonSimpleKeyProjectEvidenceAbsent

projectScopedUndeclaredImportedClassProjectResult :
  ImportProjectElaborationResult strictPolicy
projectScopedUndeclaredImportedClassProjectResult =
  elaborateImportProjectStrict projectScopedUndeclaredImportedClassProject

projectScopedUndeclaredImportedClassProjectDiagnostics :
  diagnostics projectScopedUndeclaredImportedClassProjectResult ≡
  singleDiagnostic
    (undeclaredClassDiagnostic rejectedMissingImportedClassIRI)
projectScopedUndeclaredImportedClassProjectDiagnostics =
  refl

projectScopedUndeclaredImportedClassProjectMissingDiagnostics :
  projectMissingDiagnostics projectScopedUndeclaredImportedClassProject ≡
  noDiagnostics
projectScopedUndeclaredImportedClassProjectMissingDiagnostics =
  refl

projectScopedUndeclaredImportedClassProjectRootScopedDiagnostics :
  projectDocumentScopedDiagnostics
    projectScopedUndeclaredImportedClassProject
    rejectedUnresolvedClassProjectDocument ≡
  singleDiagnostic
    (undeclaredClassDiagnostic rejectedMissingImportedClassIRI)
projectScopedUndeclaredImportedClassProjectRootScopedDiagnostics =
  refl

projectScopedUndeclaredImportedClassProjectImportFound :
  ontologyIDInDocuments
    (importOntologyID rejectedResolvedVocabularyOntologyIRI)
    (projectDocuments projectScopedUndeclaredImportedClassProject) ≡
  true
projectScopedUndeclaredImportedClassProjectImportFound =
  refl

projectScopedUndeclaredImportedClassProjectEvidenceAbsent :
  evidence? projectScopedUndeclaredImportedClassProjectResult ≡ absent
projectScopedUndeclaredImportedClassProjectEvidenceAbsent =
  refl

projectScopedUndeclaredImportedClassProjectRejected :
  Clean projectScopedUndeclaredImportedClassProjectResult → ⊥
projectScopedUndeclaredImportedClassProjectRejected clean =
  clean

projectScopedUndeclaredImportedClassProjectEvidenceUnavailable :
  EvidenceUnavailable projectScopedUndeclaredImportedClassProjectResult
projectScopedUndeclaredImportedClassProjectEvidenceUnavailable =
  evidenceUnavailable
    projectScopedUndeclaredImportedClassProjectResult
    projectScopedUndeclaredImportedClassProjectEvidenceAbsent

projectScopedUndeclaredImportedPropertyProjectResult :
  ImportProjectElaborationResult strictPolicy
projectScopedUndeclaredImportedPropertyProjectResult =
  elaborateImportProjectStrict projectScopedUndeclaredImportedPropertyProject

projectScopedUndeclaredImportedPropertyProjectDiagnostics :
  diagnostics projectScopedUndeclaredImportedPropertyProjectResult ≡
  singleDiagnostic
    (undeclaredObjectPropertyDiagnostic
      rejectedMissingImportedObjectPropertyIRI)
projectScopedUndeclaredImportedPropertyProjectDiagnostics =
  refl

projectScopedUndeclaredImportedPropertyProjectMissingDiagnostics :
  projectMissingDiagnostics projectScopedUndeclaredImportedPropertyProject ≡
  noDiagnostics
projectScopedUndeclaredImportedPropertyProjectMissingDiagnostics =
  refl

projectScopedUndeclaredImportedPropertyProjectRootScopedDiagnostics :
  projectDocumentScopedDiagnostics
    projectScopedUndeclaredImportedPropertyProject
    rejectedUnresolvedPropertyProjectDocument ≡
  singleDiagnostic
    (undeclaredObjectPropertyDiagnostic
      rejectedMissingImportedObjectPropertyIRI)
projectScopedUndeclaredImportedPropertyProjectRootScopedDiagnostics =
  refl

projectScopedUndeclaredImportedPropertyProjectImportFound :
  ontologyIDInDocuments
    (importOntologyID rejectedResolvedVocabularyOntologyIRI)
    (projectDocuments projectScopedUndeclaredImportedPropertyProject) ≡
  true
projectScopedUndeclaredImportedPropertyProjectImportFound =
  refl

projectScopedUndeclaredImportedPropertyProjectEvidenceAbsent :
  evidence? projectScopedUndeclaredImportedPropertyProjectResult ≡ absent
projectScopedUndeclaredImportedPropertyProjectEvidenceAbsent =
  refl

projectScopedUndeclaredImportedPropertyProjectRejected :
  Clean projectScopedUndeclaredImportedPropertyProjectResult → ⊥
projectScopedUndeclaredImportedPropertyProjectRejected clean =
  clean

projectScopedUndeclaredImportedPropertyProjectEvidenceUnavailable :
  EvidenceUnavailable projectScopedUndeclaredImportedPropertyProjectResult
projectScopedUndeclaredImportedPropertyProjectEvidenceUnavailable =
  evidenceUnavailable
    projectScopedUndeclaredImportedPropertyProjectResult
    projectScopedUndeclaredImportedPropertyProjectEvidenceAbsent