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

module OWL2.Ontology.ImportClosure where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.DirectSemantics
open import OWL2.DirectSemantics.Entailment using (_∈_; here; there)

record ImportGraph
  {ℓSig : Level}
  (Sig : Signature ℓSig)
  (ℓGraph : Level)
  : Type (ℓ-suc (ℓ-max ℓSig ℓGraph)) where
  field
    contains :
      Ontology Sig → Type (ℓ-max ℓSig ℓGraph)
    resolvesImport :
      Ontology Sig →
      IRI Sig →
      Ontology Sig →
      Type (ℓ-max ℓSig ℓGraph)

open ImportGraph public

record ResolvedImport
  {ℓSig ℓGraph : Level}
  {Sig : Signature ℓSig}
  (graph : ImportGraph Sig ℓGraph)
  (source : Ontology Sig)
  (importIRI : IRI Sig)
  : Type (ℓ-max ℓSig ℓGraph) where
  constructor resolvedImport
  field
    resolvedOntology : Ontology Sig
    resolvedBy :
      resolvesImport graph source importIRI resolvedOntology

open ResolvedImport public

record MissingImport
  {ℓSig ℓGraph : Level}
  {Sig : Signature ℓSig}
  (graph : ImportGraph Sig ℓGraph)
  : Type (ℓ-max ℓSig ℓGraph) where
  constructor missingImport
  field
    missingImportSource : Ontology Sig
    missingImportIRI : IRI Sig
    missingImportSourcePresent :
      contains graph missingImportSource
    missingImportDeclared :
      missingImportIRI ∈ imports missingImportSource
    missingImportUnresolved :
      ∀ target →
      resolvesImport graph missingImportSource missingImportIRI target →
      ⊥

open MissingImport public

NoMissingImports :
  ∀ {ℓSig ℓGraph}
    {Sig : Signature ℓSig} →
  ImportGraph Sig ℓGraph →
  Type (ℓ-max ℓSig ℓGraph)
NoMissingImports graph =
  ∀ {source importIRI} →
    contains graph source →
    importIRI ∈ imports source →
    ResolvedImport graph source importIRI

noMissingImportsRejectsMissing :
  ∀ {ℓSig ℓGraph}
    {Sig : Signature ℓSig}
    {graph : ImportGraph Sig ℓGraph} →
  NoMissingImports graph →
  MissingImport graph →
  ⊥
noMissingImportsRejectsMissing noMissing missing
  with noMissing
    (missingImportSourcePresent missing)
    (missingImportDeclared missing)
... | resolvedImport target resolved =
  missingImportUnresolved missing target resolved

record ImportGraphExtension
  {ℓSig ℓOldGraph ℓNewGraph : Level}
  {Sig : Signature ℓSig}
  (oldGraph : ImportGraph Sig ℓOldGraph)
  (newGraph : ImportGraph Sig ℓNewGraph)
  : Type (ℓ-max ℓSig (ℓ-max ℓOldGraph ℓNewGraph)) where
  field
    extendsContains :
      ∀ ontology →
      contains oldGraph ontology →
      contains newGraph ontology
    extendsResolvesImport :
      ∀ source importIRI target →
      resolvesImport oldGraph source importIRI target →
      resolvesImport newGraph source importIRI target

open ImportGraphExtension public

importGraphExtensionRefl :
  ∀ {ℓSig ℓGraph}
    {Sig : Signature ℓSig}
    {graph : ImportGraph Sig ℓGraph} →
  ImportGraphExtension graph graph
importGraphExtensionRefl .extendsContains _ ontology-present =
  ontology-present
importGraphExtensionRefl .extendsResolvesImport _ _ _ import-resolved =
  import-resolved

resolvedImportMonotone :
  ∀ {ℓSig ℓOldGraph ℓNewGraph}
    {Sig : Signature ℓSig}
    {oldGraph : ImportGraph Sig ℓOldGraph}
    {newGraph : ImportGraph Sig ℓNewGraph}
    {source : Ontology Sig}
    {importIRI : IRI Sig} →
  ImportGraphExtension oldGraph newGraph →
  ResolvedImport oldGraph source importIRI →
  ResolvedImport newGraph source importIRI
resolvedImportMonotone extension (resolvedImport target resolved) =
  resolvedImport target
    (extendsResolvesImport extension _ _ _ resolved)

data InImportClosure
  {ℓSig ℓGraph : Level}
  {Sig : Signature ℓSig}
  (graph : ImportGraph Sig ℓGraph)
  (root : Ontology Sig)
  : Ontology Sig → Type (ℓ-max ℓSig ℓGraph) where
  closureRoot :
    InImportClosure graph root root
  closureImport :
    ∀ {source target importIRI} →
    InImportClosure graph root source →
    importIRI ∈ imports source →
    resolvesImport graph source importIRI target →
    InImportClosure graph root target

record ClosedImportGraph
  {ℓSig ℓGraph : Level}
  {Sig : Signature ℓSig}
  (graph : ImportGraph Sig ℓGraph)
  : Type (ℓ-suc (ℓ-max ℓSig ℓGraph)) where
  field
    resolvedOntologiesPresent :
      ∀ {source target importIRI} →
      contains graph source →
      resolvesImport graph source importIRI target →
      contains graph target

open ClosedImportGraph public

SatisfiesImportClosure :
  ∀ {ℓSig ℓGraph ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  ImportGraph Sig ℓGraph →
  Ontology Sig →
  Type
    (ℓ-max
      (SemLevel ℓSig ℓObj ℓData ℓSem)
      (ℓ-max ℓSig ℓGraph))
SatisfiesImportClosure I graph root =
  ∀ target →
    InImportClosure graph root target →
    SatisfiesOntology I target

ImportClosureModel :
  ∀ {ℓSig ℓGraph ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  ImportGraph Sig ℓGraph →
  Ontology Sig →
  Type
    (ℓ-max
      (SemLevel ℓSig ℓObj ℓData ℓSem)
      (ℓ-max ℓSig ℓGraph))
ImportClosureModel =
  SatisfiesImportClosure

satisfiesImportClosureRoot :
  ∀ {ℓSig ℓGraph ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {graph : ImportGraph Sig ℓGraph}
    {root : Ontology Sig} →
  SatisfiesImportClosure I graph root →
  SatisfiesOntology I root
satisfiesImportClosureRoot model =
  model _ closureRoot

satisfiesImportClosureTarget :
  ∀ {ℓSig ℓGraph ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {graph : ImportGraph Sig ℓGraph}
    {root target : Ontology Sig} →
  InImportClosure graph root target →
  SatisfiesImportClosure I graph root →
  SatisfiesOntology I target
satisfiesImportClosureTarget target∈closure model =
  model _ target∈closure

containsImportClosureRoot :
  ∀ {ℓSig ℓGraph}
    {Sig : Signature ℓSig}
    {graph : ImportGraph Sig ℓGraph}
    {root target : Ontology Sig} →
  contains graph root →
  ClosedImportGraph graph →
  InImportClosure graph root target →
  contains graph target
containsImportClosureRoot root-present graph-closed closureRoot =
  root-present
containsImportClosureRoot
  {graph = graph}
  root-present
  graph-closed
  (closureImport source∈closure _ import-resolved) =
  resolvedOntologiesPresent graph-closed
    (containsImportClosureRoot root-present graph-closed source∈closure)
    import-resolved

inImportClosureMonotone :
  ∀ {ℓSig ℓOldGraph ℓNewGraph}
    {Sig : Signature ℓSig}
    {oldGraph : ImportGraph Sig ℓOldGraph}
    {newGraph : ImportGraph Sig ℓNewGraph}
    {root target : Ontology Sig} →
  ImportGraphExtension oldGraph newGraph →
  InImportClosure oldGraph root target →
  InImportClosure newGraph root target
inImportClosureMonotone extension closureRoot =
  closureRoot
inImportClosureMonotone
  extension
  (closureImport source∈closure import-declared import-resolved) =
  closureImport
    (inImportClosureMonotone extension source∈closure)
    import-declared
    (extendsResolvesImport extension _ _ _ import-resolved)

satisfiesImportClosureMonotone :
  ∀ {ℓSig ℓOldGraph ℓNewGraph ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {oldGraph : ImportGraph Sig ℓOldGraph}
    {newGraph : ImportGraph Sig ℓNewGraph}
    {root : Ontology Sig} →
  ImportGraphExtension oldGraph newGraph →
  SatisfiesImportClosure I newGraph root →
  SatisfiesImportClosure I oldGraph root
satisfiesImportClosureMonotone extension model target target∈closure =
  model target
    (inImportClosureMonotone extension target∈closure)