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

module OWL2.Examples.WebProtege.Imports where

open import OWL2.Prelude
import Cubical.Data.Prod.Base as Prod
open import OWL2.Syntax
open import OWL2.DirectSemantics
open import OWL2.DirectSemantics.Entailment using (_∈_; here; there)
open import OWL2.Ontology.ImportClosure
open import OWL2.DirectSemantics.Ontology
import OWL2.Portable.Check.SemanticSupport as CheckSemantic
import OWL2.Portable.ImportClosure as PortableImport
import OWL2.Portable.Semantics as PortableSem
import OWL2.Portable.Syntax as P

data WebProtegeImportIRI : Type₀ where
  vocabularyIRI projectIRI : WebProtegeImportIRI

data WebProtegeImportClass : Type₀ where
  Resource ProjectDataset : WebProtegeImportClass

data WebProtegeImportObjectProperty : Type₀ where

data WebProtegeImportDataProperty : Type₀ where

data WebProtegeImportDatatype : Type₀ where

data WebProtegeImportIndividual : Type₀ where
  exampleDataset : WebProtegeImportIndividual

data WebProtegeImportLiteral : Type₀ where

data WebProtegeImportFacet : Type₀ where

data WebProtegeImportAnnotationProperty : Type₀ where

WebProtegeImportSignature : Signature ℓ-zero
WebProtegeImportSignature .IRI =
  WebProtegeImportIRI
WebProtegeImportSignature .ClassName =
  WebProtegeImportClass
WebProtegeImportSignature .ObjectPropertyName =
  WebProtegeImportObjectProperty
WebProtegeImportSignature .DataPropertyName =
  WebProtegeImportDataProperty
WebProtegeImportSignature .DatatypeName =
  WebProtegeImportDatatype
WebProtegeImportSignature .IndividualName =
  WebProtegeImportIndividual
WebProtegeImportSignature .Literal =
  WebProtegeImportLiteral
WebProtegeImportSignature .FacetName =
  WebProtegeImportFacet
WebProtegeImportSignature .AnnotationPropertyName =
  WebProtegeImportAnnotationProperty

ResourceC ProjectDatasetC : ClassExpression WebProtegeImportSignature
ResourceC =
  namedClass Resource
ProjectDatasetC =
  namedClass ProjectDataset

vocabularyOntology projectOntology : Ontology WebProtegeImportSignature
vocabularyOntology =
  ontology
    (vocabularyIRI ∷ [])
    []
    ( declaration (classEntity Resource)
    ∷ [] )
projectOntology =
  ontology
    (projectIRI ∷ [])
    (vocabularyIRI ∷ [])
    ( declaration (classEntity ProjectDataset)
    ∷ declaration (individualEntity exampleDataset)
    ∷ subClassOf ProjectDatasetC ResourceC
    ∷ classAssertion ProjectDatasetC exampleDataset
    ∷ [] )

vocabularyDocument projectDocument :
  OntologyDocument WebProtegeImportSignature
vocabularyDocument =
  documentFromOntology vocabularyOntology
projectDocument =
  documentFromOntology projectOntology

data WebProtegeImportGraphContains :
  Ontology WebProtegeImportSignature → Type₀ where
  containsVocabulary :
    WebProtegeImportGraphContains vocabularyOntology
  containsProject :
    WebProtegeImportGraphContains projectOntology

data WebProtegeImportGraphResolves :
  Ontology WebProtegeImportSignature →
  WebProtegeImportIRI →
  Ontology WebProtegeImportSignature →
  Type₀ where
  resolvesProjectVocabulary :
    WebProtegeImportGraphResolves
      projectOntology
      vocabularyIRI
      vocabularyOntology

webProtegeImportGraph :
  ImportGraph WebProtegeImportSignature ℓ-zero
webProtegeImportGraph .contains =
  WebProtegeImportGraphContains
webProtegeImportGraph .resolvesImport =
  WebProtegeImportGraphResolves

closedWebProtegeImportGraph :
  ClosedImportGraph webProtegeImportGraph
closedWebProtegeImportGraph .resolvedOntologiesPresent
  _ resolvesProjectVocabulary =
  containsVocabulary

projectVocabularyImportResolved :
  ResolvedImport
    webProtegeImportGraph
    projectOntology
    vocabularyIRI
projectVocabularyImportResolved =
  resolvedImport vocabularyOntology resolvesProjectVocabulary

webProtegeImportsHaveNoMissing :
  NoMissingImports webProtegeImportGraph
webProtegeImportsHaveNoMissing containsVocabulary ()
webProtegeImportsHaveNoMissing containsProject here =
  projectVocabularyImportResolved
webProtegeImportsHaveNoMissing containsProject (there ())

webProtegeRejectsMissingImport :
  MissingImport webProtegeImportGraph → ⊥
webProtegeRejectsMissingImport =
  noMissingImportsRejectsMissing webProtegeImportsHaveNoMissing

data MissingVocabularyImportGraphContains :
  Ontology WebProtegeImportSignature → Type₀ where
  containsMissingProject :
    MissingVocabularyImportGraphContains projectOntology

data MissingVocabularyImportGraphResolves :
  Ontology WebProtegeImportSignature →
  WebProtegeImportIRI →
  Ontology WebProtegeImportSignature →
  Type₀ where

missingVocabularyImportGraph :
  ImportGraph WebProtegeImportSignature ℓ-zero
missingVocabularyImportGraph .contains =
  MissingVocabularyImportGraphContains
missingVocabularyImportGraph .resolvesImport =
  MissingVocabularyImportGraphResolves

missingProjectVocabularyImport :
  MissingImport missingVocabularyImportGraph
missingProjectVocabularyImport =
  missingImport
    projectOntology
    vocabularyIRI
    containsMissingProject
    here
    (λ _ ())

projectInProjectImportClosure :
  InImportClosure webProtegeImportGraph projectOntology projectOntology
projectInProjectImportClosure =
  closureRoot

vocabularyInProjectImportClosure :
  InImportClosure webProtegeImportGraph projectOntology vocabularyOntology
vocabularyInProjectImportClosure =
  closureImport closureRoot here resolvesProjectVocabulary

vocabularyPresentFromProjectClosure :
  contains webProtegeImportGraph vocabularyOntology
vocabularyPresentFromProjectClosure =
  containsImportClosureRoot
    containsProject
    closedWebProtegeImportGraph
    vocabularyInProjectImportClosure

data WebProtegeImportObject : Type₀ where
  exampleDatasetObject : WebProtegeImportObject

data WebProtegeImportData : Type₀ where
  noDataValue : WebProtegeImportData

data IsResource : WebProtegeImportObject → Type₀ where
  exampleDatasetResource : IsResource exampleDatasetObject

data IsProjectDataset : WebProtegeImportObject → Type₀ where
  exampleDatasetProject : IsProjectDataset exampleDatasetObject

WebProtegeImportClassDenotation :
  WebProtegeImportClass → WebProtegeImportObject → Type₀
WebProtegeImportClassDenotation Resource =
  IsResource
WebProtegeImportClassDenotation ProjectDataset =
  IsProjectDataset

WebProtegeImportObjectPropertyDenotation :
  WebProtegeImportObjectProperty →
  WebProtegeImportObject → WebProtegeImportObject → Type₀
WebProtegeImportObjectPropertyDenotation ()

WebProtegeImportDataPropertyDenotation :
  WebProtegeImportDataProperty →
  WebProtegeImportObject → WebProtegeImportData → Type₀
WebProtegeImportDataPropertyDenotation ()

WebProtegeImportDatatypeDenotation :
  WebProtegeImportDatatype → WebProtegeImportData → Type₀
WebProtegeImportDatatypeDenotation ()

WebProtegeImportFacetDenotation :
  WebProtegeImportDatatype →
  WebProtegeImportFacet →
  WebProtegeImportLiteral →
  WebProtegeImportData →
  Type₀
WebProtegeImportFacetDenotation ()

WebProtegeImportIndividualDenotation :
  WebProtegeImportIndividual → WebProtegeImportObject
WebProtegeImportIndividualDenotation exampleDataset =
  exampleDatasetObject

WebProtegeImportLiteralDenotation :
  WebProtegeImportLiteral → WebProtegeImportData
WebProtegeImportLiteralDenotation ()

webProtegeImportInterpretation :
  Interpretation WebProtegeImportSignature ℓ-zero ℓ-zero ℓ-zero
webProtegeImportInterpretation .ObjectDomain =
  WebProtegeImportObject
webProtegeImportInterpretation .DataDomain =
  WebProtegeImportData
webProtegeImportInterpretation .classDenotation =
  WebProtegeImportClassDenotation
webProtegeImportInterpretation .objectPropertyDenotation =
  WebProtegeImportObjectPropertyDenotation
webProtegeImportInterpretation .dataPropertyDenotation =
  WebProtegeImportDataPropertyDenotation
webProtegeImportInterpretation .datatypeDenotation =
  WebProtegeImportDatatypeDenotation
webProtegeImportInterpretation .facetDenotation =
  WebProtegeImportFacetDenotation
webProtegeImportInterpretation .individualDenotation =
  WebProtegeImportIndividualDenotation
webProtegeImportInterpretation .literalDenotation =
  WebProtegeImportLiteralDenotation

projectDatasetSubResource :
  SatisfiesAxiom webProtegeImportInterpretation
    (subClassOf ProjectDatasetC ResourceC)
projectDatasetSubResource .exampleDatasetObject exampleDatasetProject =
  exampleDatasetResource

exampleDatasetIsProjectDataset :
  SatisfiesAxiom webProtegeImportInterpretation
    (classAssertion ProjectDatasetC exampleDataset)
exampleDatasetIsProjectDataset =
  exampleDatasetProject

vocabularyModel :
  Model webProtegeImportInterpretation vocabularyOntology
vocabularyModel =
  Prod._,_ (lift tt)
    (lift tt)

projectModel :
  Model webProtegeImportInterpretation projectOntology
projectModel =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ projectDatasetSubResource
  (Prod._,_ exampleDatasetIsProjectDataset
    (lift tt))))

projectImportClosureModel :
  ImportClosureModel
    webProtegeImportInterpretation
    webProtegeImportGraph
    projectOntology
projectImportClosureModel .projectOntology closureRoot =
  projectModel
projectImportClosureModel .vocabularyOntology
  (closureImport _ _ resolvesProjectVocabulary) =
  vocabularyModel

projectDocumentImportClosureModel :
  DocumentImportClosureModel
    webProtegeImportInterpretation
    webProtegeImportGraph
    projectDocument
projectDocumentImportClosureModel =
  projectImportClosureModel

projectDocumentModel :
  DocumentModel webProtegeImportInterpretation projectDocument
projectDocumentModel =
  satisfiesDocumentImportClosureRoot projectDocumentImportClosureModel

vocabularyModelFromProjectClosure :
  Model webProtegeImportInterpretation vocabularyOntology
vocabularyModelFromProjectClosure =
  satisfiesImportClosureTarget
    vocabularyInProjectImportClosure
    projectImportClosureModel

portableIRI : String → P.IRI
portableIRI =
  P.iri

portableName : String → P.Name
portableName text =
  P.named (P.iri text)

portableAxiom : P.Axiom → P.Annotated P.Axiom
portableAxiom body =
  P.annotated [] body

portableVocabularyIRI portableProjectIRI : P.IRI
portableVocabularyIRI =
  portableIRI "https://example.org/webprotege-imports/vocabulary"
portableProjectIRI =
  portableIRI "https://example.org/webprotege-imports/project"

portableResource portableProjectDataset : P.ClassName
portableResource =
  portableName "https://example.org/webprotege-imports#Resource"
portableProjectDataset =
  portableName "https://example.org/webprotege-imports#ProjectDataset"

portableExampleDatasetIRI : P.NamedIndividualName
portableExampleDatasetIRI =
  portableIRI "https://example.org/webprotege-imports#exampleDataset"

PortableResourceC PortableProjectDatasetC :
  ClassExpression PortableSem.PortableSignature
PortableResourceC =
  namedClass portableResource
PortableProjectDatasetC =
  namedClass portableProjectDataset

PResourceC PProjectDatasetC : P.ClassExpression
PResourceC =
  P.namedClass portableResource
PProjectDatasetC =
  P.namedClass portableProjectDataset

portableVocabularyOntology portableProjectOntology : P.Ontology
portableVocabularyOntology =
  P.ontology
    (P.ontologyIRI portableVocabularyIRI absent)
    []
    []
    ( portableAxiom (P.declaration (P.classEntity portableResource))
    ∷ [] )
portableProjectOntology =
  P.ontology
    (P.ontologyIRI portableProjectIRI absent)
    (portableVocabularyIRI ∷ [])
    []
    ( portableAxiom (P.declaration (P.classEntity portableProjectDataset))
    ∷ portableAxiom
        (P.declaration
          (P.namedIndividualEntity portableExampleDatasetIRI))
    ∷ portableAxiom (P.subClassOf PProjectDatasetC PResourceC)
    ∷ portableAxiom
        (P.classAssertion
          PProjectDatasetC
          (P.namedIndividual portableExampleDatasetIRI))
    ∷ [] )

portableVocabularyDocument portableProjectDocument : P.OntologyDocument
portableVocabularyDocument =
  P.ontologyDocument [] portableVocabularyOntology
portableProjectDocument =
  P.ontologyDocument [] portableProjectOntology

portableVocabularyTranslationComplete :
  PortableSem.CompleteSemanticTranslation portableVocabularyDocument
portableVocabularyTranslationComplete =
  CheckSemantic.completeSemanticTranslationFromClean
    portableVocabularyDocument
    tt

portableProjectTranslationComplete :
  PortableSem.CompleteSemanticTranslation portableProjectDocument
portableProjectTranslationComplete =
  CheckSemantic.completeSemanticTranslationFromClean
    portableProjectDocument
    tt

portableDocumentImports : P.OntologyDocument → List P.IRI
portableDocumentImports document =
  P.imports (P.documentOntology document)

data PortableWebProtegeImportGraphContains :
  P.OntologyDocument → Type₀ where
  containsPortableVocabulary :
    ∀ {document} →
    document ≡ portableVocabularyDocument →
    PortableWebProtegeImportGraphContains document
  containsPortableProject :
    ∀ {document} →
    document ≡ portableProjectDocument →
    PortableWebProtegeImportGraphContains document

data PortableWebProtegeImportGraphResolves :
  P.OntologyDocument →
  P.IRI →
  P.OntologyDocument →
  Type₀ where
  resolvesPortableProjectVocabulary :
    ∀ {source importIRI target} →
    source ≡ portableProjectDocument →
    importIRI ≡ portableVocabularyIRI →
    target ≡ portableVocabularyDocument →
    PortableWebProtegeImportGraphResolves
      source
      importIRI
      target

portableWebProtegeImportGraph :
  PortableImport.PortableImportGraph ℓ-zero
portableWebProtegeImportGraph .PortableImport.containsDocument =
  PortableWebProtegeImportGraphContains
portableWebProtegeImportGraph .PortableImport.resolvesDocumentImport =
  PortableWebProtegeImportGraphResolves

closedPortableWebProtegeImportGraph :
  PortableImport.ClosedPortableImportGraph portableWebProtegeImportGraph
closedPortableWebProtegeImportGraph .PortableImport.resolvedDocumentsPresent
  _
  (resolvesPortableProjectVocabulary _ _ targetEq) =
  containsPortableVocabulary targetEq

portableProjectVocabularyImportResolved :
  PortableImport.ResolvedPortableImport
    portableWebProtegeImportGraph
    portableProjectDocument
    portableVocabularyIRI
portableProjectVocabularyImportResolved =
  PortableImport.resolvedPortableImport
    portableVocabularyDocument
    (resolvesPortableProjectVocabulary refl refl refl)

portableVocabularyHasNoImports :
  ∀ {source importIRI} →
  source ≡ portableVocabularyDocument →
  importIRI ∈ portableDocumentImports source →
  ⊥
portableVocabularyHasNoImports {importIRI = importIRI} sourceEq member
  with subst
        (λ document → importIRI ∈ portableDocumentImports document)
        sourceEq
        member
... | ()

portableProjectImportMembershipResolved :
  ∀ {source importIRI} →
  source ≡ portableProjectDocument →
  importIRI ∈ portableDocumentImports source →
  PortableImport.ResolvedPortableImport
    portableWebProtegeImportGraph
    source
    importIRI
portableProjectImportMembershipResolved
  {importIRI = importIRI}
  sourceEq
  member
  with subst
        (λ document → importIRI ∈ portableDocumentImports document)
        sourceEq
        member
... | here =
  PortableImport.resolvedPortableImport
    portableVocabularyDocument
    (resolvesPortableProjectVocabulary sourceEq refl refl)
... | there ()

portableWebProtegeImportsHaveNoMissing :
  PortableImport.NoMissingPortableImports portableWebProtegeImportGraph
portableWebProtegeImportsHaveNoMissing
  (containsPortableVocabulary sourceEq)
  member
  with portableVocabularyHasNoImports sourceEq member
... | ()
portableWebProtegeImportsHaveNoMissing
  (containsPortableProject sourceEq)
  member =
  portableProjectImportMembershipResolved sourceEq member

portableWebProtegeRejectsMissingImport :
  PortableImport.MissingPortableImport portableWebProtegeImportGraph → ⊥
portableWebProtegeRejectsMissingImport =
  PortableImport.noMissingPortableImportsRejectsMissing
    portableWebProtegeImportsHaveNoMissing

data PortableMissingVocabularyImportGraphContains :
  P.OntologyDocument → Type₀ where
  containsPortableMissingProject :
    ∀ {document} →
    document ≡ portableProjectDocument →
    PortableMissingVocabularyImportGraphContains document

data PortableMissingVocabularyImportGraphResolves :
  P.OntologyDocument →
  P.IRI →
  P.OntologyDocument →
  Type₀ where

portableMissingVocabularyImportGraph :
  PortableImport.PortableImportGraph ℓ-zero
portableMissingVocabularyImportGraph .PortableImport.containsDocument =
  PortableMissingVocabularyImportGraphContains
portableMissingVocabularyImportGraph .PortableImport.resolvesDocumentImport =
  PortableMissingVocabularyImportGraphResolves

portableMissingProjectVocabularyImport :
  PortableImport.MissingPortableImport portableMissingVocabularyImportGraph
portableMissingProjectVocabularyImport =
  PortableImport.missingPortableImport
    portableProjectDocument
    portableVocabularyIRI
    (containsPortableMissingProject refl)
    here
    (λ _ ())

portableProjectInProjectImportClosure :
  PortableImport.InPortableImportClosure
    portableWebProtegeImportGraph
    portableProjectDocument
    portableProjectDocument
portableProjectInProjectImportClosure =
  PortableImport.portableClosureRoot

portableVocabularyInProjectImportClosure :
  PortableImport.InPortableImportClosure
    portableWebProtegeImportGraph
    portableProjectDocument
    portableVocabularyDocument
portableVocabularyInProjectImportClosure =
  PortableImport.portableClosureImport
    PortableImport.portableClosureRoot
    here
    (resolvesPortableProjectVocabulary refl refl refl)

portableVocabularyPresentFromProjectClosure :
  PortableImport.containsDocument
    portableWebProtegeImportGraph
    portableVocabularyDocument
portableVocabularyPresentFromProjectClosure =
  PortableImport.containsPortableImportClosureRoot
    (containsPortableProject refl)
    closedPortableWebProtegeImportGraph
    portableVocabularyInProjectImportClosure

portableVocabularySemanticImportClosure :
  InImportClosure
    (PortableImport.translatedImportGraph portableWebProtegeImportGraph)
    (PortableImport.semanticOntologyOfDocument portableProjectDocument)
    (PortableImport.semanticOntologyOfDocument portableVocabularyDocument)
portableVocabularySemanticImportClosure =
  PortableImport.portableClosureToSemantic
    portableVocabularyInProjectImportClosure

data PortableImportObject : Type₀ where
  portableExampleDatasetObject : PortableImportObject

data PortableImportData : Type₀ where
  portableNoDataValue : PortableImportData

PortableImportClassDenotation :
  P.ClassName → PortableImportObject → Type₀
PortableImportClassDenotation _ _ =
  Unit*

PortableImportObjectPropertyDenotation :
  P.ObjectPropertyName →
  PortableImportObject → PortableImportObject → Type₀
PortableImportObjectPropertyDenotation _ _ _ =
  ⊥

PortableImportDataPropertyDenotation :
  P.DataPropertyName →
  PortableImportObject → PortableImportData → Type₀
PortableImportDataPropertyDenotation _ _ _ =
  ⊥

PortableImportDatatypeDenotation :
  P.DatatypeName → PortableImportData → Type₀
PortableImportDatatypeDenotation _ _ =
  ⊥

PortableImportFacetDenotation :
  P.DatatypeName →
  P.FacetName →
  P.Literal →
  PortableImportData →
  Type₀
PortableImportFacetDenotation _ _ _ _ =
  ⊥

PortableImportIndividualDenotation :
  P.Individual → PortableImportObject
PortableImportIndividualDenotation _ =
  portableExampleDatasetObject

PortableImportLiteralDenotation :
  P.Literal → PortableImportData
PortableImportLiteralDenotation _ =
  portableNoDataValue

portableWebProtegeImportInterpretation :
  Interpretation PortableSem.PortableSignature ℓ-zero ℓ-zero ℓ-zero
portableWebProtegeImportInterpretation .ObjectDomain =
  PortableImportObject
portableWebProtegeImportInterpretation .DataDomain =
  PortableImportData
portableWebProtegeImportInterpretation .classDenotation =
  PortableImportClassDenotation
portableWebProtegeImportInterpretation .objectPropertyDenotation =
  PortableImportObjectPropertyDenotation
portableWebProtegeImportInterpretation .dataPropertyDenotation =
  PortableImportDataPropertyDenotation
portableWebProtegeImportInterpretation .datatypeDenotation =
  PortableImportDatatypeDenotation
portableWebProtegeImportInterpretation .facetDenotation =
  PortableImportFacetDenotation
portableWebProtegeImportInterpretation .individualDenotation =
  PortableImportIndividualDenotation
portableWebProtegeImportInterpretation .literalDenotation =
  PortableImportLiteralDenotation

portableProjectDatasetSubResource :
  SatisfiesAxiom portableWebProtegeImportInterpretation
    (subClassOf PortableProjectDatasetC PortableResourceC)
portableProjectDatasetSubResource _ _ =
  tt*

portableExampleDatasetIsProjectDataset :
  SatisfiesAxiom portableWebProtegeImportInterpretation
    (classAssertion
      PortableProjectDatasetC
      (P.namedIndividual portableExampleDatasetIRI))
portableExampleDatasetIsProjectDataset =
  tt*

portableVocabularyModel :
  PortableSem.PartialModel
    portableWebProtegeImportInterpretation
    portableVocabularyDocument
portableVocabularyModel =
  Prod._,_ (lift tt)
    (lift tt)

portableProjectModel :
  PortableSem.PartialModel
    portableWebProtegeImportInterpretation
    portableProjectDocument
portableProjectModel =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ portableProjectDatasetSubResource
  (Prod._,_ portableExampleDatasetIsProjectDataset
    (lift tt))))

portableProjectImportClosureModel :
  PortableImport.PortableImportClosureModel
    portableWebProtegeImportInterpretation
    portableWebProtegeImportGraph
    portableProjectDocument
portableProjectImportClosureModel
  .portableProjectDocument
  PortableImport.portableClosureRoot =
  portableProjectModel
portableProjectImportClosureModel
  target
  (PortableImport.portableClosureImport
    source∈closure
    importMember
    (resolvesPortableProjectVocabulary _ _ targetEq)) =
  subst
    (λ document →
      PortableSem.PartialModel
        portableWebProtegeImportInterpretation
        document)
    (sym targetEq)
    portableVocabularyModel

portableProjectDocumentModel :
  PortableSem.PartialModel
    portableWebProtegeImportInterpretation
    portableProjectDocument
portableProjectDocumentModel =
  PortableImport.portableImportClosureRootModel
    portableProjectImportClosureModel

portableVocabularyModelFromProjectClosure :
  PortableSem.PartialModel
    portableWebProtegeImportInterpretation
    portableVocabularyDocument
portableVocabularyModelFromProjectClosure =
  PortableImport.portableImportClosureTargetModel
    portableVocabularyInProjectImportClosure
    portableProjectImportClosureModel