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

module OWL2.Portable.ImportClosure where

open import OWL2.Prelude
import OWL2.DirectSemantics as D
import OWL2.DirectSemantics.Entailment as Entailment
import OWL2.Ontology.ImportClosure as Import
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax as S

semanticOntologyOfDocument :
  P.OntologyDocument → S.Ontology Sem.PortableSignature
semanticOntologyOfDocument document =
  Sem.semanticOntology (Sem.partialTranslateOntologyDocument document)

record PortableImportGraph
  (ℓGraph : Level)
  : Type (ℓ-suc ℓGraph) where
  field
    containsDocument :
      P.OntologyDocument → Type ℓGraph
    resolvesDocumentImport :
      P.OntologyDocument →
      P.IRI →
      P.OntologyDocument →
      Type ℓGraph

open PortableImportGraph public

record ResolvedPortableImport
  {ℓGraph : Level}
  (graph : PortableImportGraph ℓGraph)
  (source : P.OntologyDocument)
  (importIRI : P.IRI)
  : Type ℓGraph where
  constructor resolvedPortableImport
  field
    resolvedDocument :
      P.OntologyDocument
    resolvedDocumentBy :
      resolvesDocumentImport graph source importIRI resolvedDocument

open ResolvedPortableImport public

record MissingPortableImport
  {ℓGraph : Level}
  (graph : PortableImportGraph ℓGraph)
  : Type ℓGraph where
  constructor missingPortableImport
  field
    missingImportSourceDocument :
      P.OntologyDocument
    missingImportIRI :
      P.IRI
    missingImportSourcePresent :
      containsDocument graph missingImportSourceDocument
    missingImportDeclared :
      Entailment._∈_
        missingImportIRI
        (P.imports (P.documentOntology missingImportSourceDocument))
    missingImportUnresolved :
      ∀ targetDocument →
      resolvesDocumentImport
        graph
        missingImportSourceDocument
        missingImportIRI
        targetDocument →
      ⊥

open MissingPortableImport public

NoMissingPortableImports :
  ∀ {ℓGraph : Level} →
  PortableImportGraph ℓGraph →
  Type ℓGraph
NoMissingPortableImports graph =
  ∀ {source importIRI} →
  containsDocument graph source →
  Entailment._∈_ importIRI (P.imports (P.documentOntology source)) →
  ResolvedPortableImport graph source importIRI

noMissingPortableImportsRejectsMissing :
  ∀ {ℓGraph : Level}
    {graph : PortableImportGraph ℓGraph} →
  NoMissingPortableImports graph →
  MissingPortableImport graph →
  ⊥
noMissingPortableImportsRejectsMissing noMissing missing
  with noMissing
    (missingImportSourcePresent missing)
    (missingImportDeclared missing)
... | resolvedPortableImport target resolved =
  missingImportUnresolved missing target resolved

record PortableImportGraphExtension
  {ℓOldGraph ℓNewGraph : Level}
  (oldGraph : PortableImportGraph ℓOldGraph)
  (newGraph : PortableImportGraph ℓNewGraph)
  : Type (ℓ-max ℓOldGraph ℓNewGraph) where
  field
    extendsContainsDocument :
      ∀ document →
      containsDocument oldGraph document →
      containsDocument newGraph document
    extendsResolvesDocumentImport :
      ∀ source importIRI target →
      resolvesDocumentImport oldGraph source importIRI target →
      resolvesDocumentImport newGraph source importIRI target

open PortableImportGraphExtension public

portableImportGraphExtensionRefl :
  ∀ {ℓGraph : Level}
    {graph : PortableImportGraph ℓGraph} →
  PortableImportGraphExtension graph graph
portableImportGraphExtensionRefl .extendsContainsDocument _ document-present =
  document-present
portableImportGraphExtensionRefl .extendsResolvesDocumentImport _ _ _ resolved =
  resolved

resolvedPortableImportMonotone :
  ∀ {ℓOldGraph ℓNewGraph : Level}
    {oldGraph : PortableImportGraph ℓOldGraph}
    {newGraph : PortableImportGraph ℓNewGraph}
    {source : P.OntologyDocument}
    {importIRI : P.IRI} →
  PortableImportGraphExtension oldGraph newGraph →
  ResolvedPortableImport oldGraph source importIRI →
  ResolvedPortableImport newGraph source importIRI
resolvedPortableImportMonotone
  extension
  (resolvedPortableImport target resolved) =
  resolvedPortableImport target
    (extendsResolvesDocumentImport extension _ _ _ resolved)

data InPortableImportClosure
  {ℓGraph : Level}
  (graph : PortableImportGraph ℓGraph)
  (root : P.OntologyDocument)
  : P.OntologyDocument → Type ℓGraph where
  portableClosureRoot :
    InPortableImportClosure graph root root
  portableClosureImport :
    ∀ {source target importIRI} →
    InPortableImportClosure graph root source →
    Entailment._∈_ importIRI (P.imports (P.documentOntology source)) →
    resolvesDocumentImport graph source importIRI target →
    InPortableImportClosure graph root target

record ClosedPortableImportGraph
  {ℓGraph : Level}
  (graph : PortableImportGraph ℓGraph)
  : Type (ℓ-suc ℓGraph) where
  field
    resolvedDocumentsPresent :
      ∀ {source target importIRI} →
      containsDocument graph source →
      resolvesDocumentImport graph source importIRI target →
      containsDocument graph target

open ClosedPortableImportGraph public

containsPortableImportClosureRoot :
  ∀ {ℓGraph : Level}
    {graph : PortableImportGraph ℓGraph}
    {root target : P.OntologyDocument} →
  containsDocument graph root →
  ClosedPortableImportGraph graph →
  InPortableImportClosure graph root target →
  containsDocument graph target
containsPortableImportClosureRoot root-present graph-closed portableClosureRoot =
  root-present
containsPortableImportClosureRoot
  root-present
  graph-closed
  (portableClosureImport source∈closure _ import-resolved) =
  resolvedDocumentsPresent graph-closed
    (containsPortableImportClosureRoot
      root-present
      graph-closed
      source∈closure)
    import-resolved

TranslatedContains :
  ∀ {ℓGraph : Level} →
  PortableImportGraph ℓGraph →
  S.Ontology Sem.PortableSignature →
  Type ℓGraph
TranslatedContains graph semanticOntology =
  Σ P.OntologyDocument
    (λ document →
      containsDocument graph document
      ×
      (semanticOntologyOfDocument document ≡ semanticOntology))

TranslatedResolvesImport :
  ∀ {ℓGraph : Level} →
  PortableImportGraph ℓGraph →
  S.Ontology Sem.PortableSignature →
  P.IRI →
  S.Ontology Sem.PortableSignature →
  Type ℓGraph
TranslatedResolvesImport graph sourceOntology importIRI targetOntology =
  Σ P.OntologyDocument
    (λ sourceDocument →
      Σ P.OntologyDocument
        (λ targetDocument →
          (semanticOntologyOfDocument sourceDocument ≡ sourceOntology)
          ×
          (semanticOntologyOfDocument targetDocument ≡ targetOntology)
          ×
          resolvesDocumentImport
            graph
            sourceDocument
            importIRI
            targetDocument))

translatedImportGraph :
  ∀ {ℓGraph : Level} →
  PortableImportGraph ℓGraph →
  Import.ImportGraph Sem.PortableSignature ℓGraph
translatedImportGraph graph .Import.contains semanticOntology =
  TranslatedContains graph semanticOntology
translatedImportGraph graph .Import.resolvesImport
  sourceOntology
  importIRI
  targetOntology =
  TranslatedResolvesImport graph sourceOntology importIRI targetOntology

translatedContainsFromPortable :
  ∀ {ℓGraph : Level}
    {graph : PortableImportGraph ℓGraph}
    {document : P.OntologyDocument} →
  containsDocument graph document →
  Import.contains
    (translatedImportGraph graph)
    (semanticOntologyOfDocument document)
translatedContainsFromPortable {document = document} document-present =
  document , document-present , refl

translatedResolvedImportFromPortable :
  ∀ {ℓGraph : Level}
    {graph : PortableImportGraph ℓGraph}
    {source target : P.OntologyDocument}
    {importIRI : P.IRI} →
  resolvesDocumentImport graph source importIRI target →
  Import.resolvesImport
    (translatedImportGraph graph)
    (semanticOntologyOfDocument source)
    importIRI
    (semanticOntologyOfDocument target)
translatedResolvedImportFromPortable
  {graph = graph}
  {source = source}
  {target = target}
  {importIRI = importIRI}
  resolved =
  source , target , (refl , (refl , resolved))

portableClosureToSemantic :
  ∀ {ℓGraph : Level}
    {graph : PortableImportGraph ℓGraph}
    {root target : P.OntologyDocument} →
  InPortableImportClosure graph root target →
  Import.InImportClosure
    (translatedImportGraph graph)
    (semanticOntologyOfDocument root)
    (semanticOntologyOfDocument target)
portableClosureToSemantic {graph = graph} portableClosureRoot =
  Import.closureRoot
portableClosureToSemantic
  {graph = graph}
  (portableClosureImport
    {source = source}
    {target = target}
    {importIRI = importIRI}
    source∈closure
    import-declared
    import-resolved) =
  Import.closureImport
    (portableClosureToSemantic source∈closure)
    import-declared
    (translatedResolvedImportFromPortable
      {graph = graph}
      {source = source}
      {target = target}
      {importIRI = importIRI}
      import-resolved)

inPortableImportClosureMonotone :
  ∀ {ℓOldGraph ℓNewGraph : Level}
    {oldGraph : PortableImportGraph ℓOldGraph}
    {newGraph : PortableImportGraph ℓNewGraph}
    {root target : P.OntologyDocument} →
  PortableImportGraphExtension oldGraph newGraph →
  InPortableImportClosure oldGraph root target →
  InPortableImportClosure newGraph root target
inPortableImportClosureMonotone extension portableClosureRoot =
  portableClosureRoot
inPortableImportClosureMonotone
  extension
  (portableClosureImport source∈closure import-declared import-resolved) =
  portableClosureImport
    (inPortableImportClosureMonotone extension source∈closure)
    import-declared
    (extendsResolvesDocumentImport extension _ _ _ import-resolved)

PortableSatisfiesImportClosure :
  ∀ {ℓGraph ℓObj ℓData ℓSem : Level} →
  D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem →
  PortableImportGraph ℓGraph →
  P.OntologyDocument →
  Type (ℓ-max (D.SemLevel ℓ-zero ℓObj ℓData ℓSem) ℓGraph)
PortableSatisfiesImportClosure I graph root =
  ∀ target →
  InPortableImportClosure graph root target →
  Sem.PartialSatisfiesOntologyDocument I target

PortableImportClosureModel :
  ∀ {ℓGraph ℓObj ℓData ℓSem : Level} →
  D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem →
  PortableImportGraph ℓGraph →
  P.OntologyDocument →
  Type (ℓ-max (D.SemLevel ℓ-zero ℓObj ℓData ℓSem) ℓGraph)
PortableImportClosureModel =
  PortableSatisfiesImportClosure

GenericPortableImportClosureModel :
  ∀ {ℓGraph ℓObj ℓData ℓSem : Level} →
  D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem →
  PortableImportGraph ℓGraph →
  P.OntologyDocument →
  Type (ℓ-max (D.SemLevel ℓ-zero ℓObj ℓData ℓSem) ℓGraph)
GenericPortableImportClosureModel I graph root =
  Import.ImportClosureModel
    I
    (translatedImportGraph graph)
    (semanticOntologyOfDocument root)

genericPortableImportClosureModelToPortable :
  ∀ {ℓGraph ℓObj ℓData ℓSem : Level}
    {I : D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem}
    {graph : PortableImportGraph ℓGraph}
    {root : P.OntologyDocument} →
  GenericPortableImportClosureModel I graph root →
  PortableImportClosureModel I graph root
genericPortableImportClosureModelToPortable model target target∈closure =
  model (semanticOntologyOfDocument target)
    (portableClosureToSemantic target∈closure)

portableImportClosureRootModel :
  ∀ {ℓGraph ℓObj ℓData ℓSem : Level}
    {I : D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem}
    {graph : PortableImportGraph ℓGraph}
    {root : P.OntologyDocument} →
  PortableImportClosureModel I graph root →
  Sem.PartialModel I root
portableImportClosureRootModel model =
  model _ portableClosureRoot

portableImportClosureTargetModel :
  ∀ {ℓGraph ℓObj ℓData ℓSem : Level}
    {I : D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem}
    {graph : PortableImportGraph ℓGraph}
    {root target : P.OntologyDocument} →
  InPortableImportClosure graph root target →
  PortableImportClosureModel I graph root →
  Sem.PartialModel I target
portableImportClosureTargetModel target∈closure model =
  model _ target∈closure

portableSatisfiesImportClosureMonotone :
  ∀ {ℓOldGraph ℓNewGraph ℓObj ℓData ℓSem : Level}
    {oldGraph : PortableImportGraph ℓOldGraph}
    {newGraph : PortableImportGraph ℓNewGraph}
    {I : D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem}
    {root : P.OntologyDocument} →
  PortableImportGraphExtension oldGraph newGraph →
  PortableSatisfiesImportClosure I newGraph root →
  PortableSatisfiesImportClosure I oldGraph root
portableSatisfiesImportClosureMonotone extension model target target∈closure =
  model target
    (inPortableImportClosureMonotone extension target∈closure)