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

module OWL2.DirectSemantics.Ontology where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.DirectSemantics
open import OWL2.Ontology.ImportClosure

record OntologyDocument
  {ℓSig : Level}
  (Sig : Signature ℓSig)
  : Type ℓSig where
  constructor ontologyDocument
  field
    documentOntology : Ontology Sig

open OntologyDocument public

documentFromOntology :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  Ontology Sig →
  OntologyDocument Sig
documentFromOntology =
  ontologyDocument

SatisfiesOntologyDocument :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  OntologyDocument Sig →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
SatisfiesOntologyDocument I doc =
  SatisfiesOntology I (documentOntology doc)

DocumentModel :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  OntologyDocument Sig →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
DocumentModel =
  SatisfiesOntologyDocument

satisfiesDocumentOntology :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {doc : OntologyDocument Sig} →
  SatisfiesOntologyDocument I doc →
  SatisfiesOntology I (documentOntology doc)
satisfiesDocumentOntology model =
  model

satisfiesDocumentFromOntology :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O : Ontology Sig} →
  SatisfiesOntology I O →
  SatisfiesOntologyDocument I (documentFromOntology O)
satisfiesDocumentFromOntology model =
  model

SatisfiesOntologyDocumentImportClosure :
  ∀ {ℓSig ℓGraph ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  ImportGraph Sig ℓGraph →
  OntologyDocument Sig →
  Type
    (ℓ-max
      (SemLevel ℓSig ℓObj ℓData ℓSem)
      (ℓ-max ℓSig ℓGraph))
SatisfiesOntologyDocumentImportClosure I graph doc =
  SatisfiesImportClosure I graph (documentOntology doc)

DocumentImportClosureModel :
  ∀ {ℓSig ℓGraph ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  ImportGraph Sig ℓGraph →
  OntologyDocument Sig →
  Type
    (ℓ-max
      (SemLevel ℓSig ℓObj ℓData ℓSem)
      (ℓ-max ℓSig ℓGraph))
DocumentImportClosureModel =
  SatisfiesOntologyDocumentImportClosure

satisfiesDocumentImportClosureRoot :
  ∀ {ℓSig ℓGraph ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {graph : ImportGraph Sig ℓGraph}
    {doc : OntologyDocument Sig} →
  SatisfiesOntologyDocumentImportClosure I graph doc →
  SatisfiesOntologyDocument I doc
satisfiesDocumentImportClosureRoot model =
  satisfiesImportClosureRoot model