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

module OWL2.DirectSemantics.Interpretation where

open import OWL2.Prelude
open import OWL2.Syntax
import OWL2.DirectSemantics as DS

record NonEmpty {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor inhabited
  field
    witness : A

open NonEmpty public

record DomainWitnesses
  {ℓSig ℓObj ℓData ℓSem : Level}
  {Sig : Signature ℓSig}
  (I : DS.Interpretation Sig ℓObj ℓData ℓSem)
  : Type (ℓ-max ℓObj ℓData) where
  constructor domainWitnesses
  field
    objectDomainNonEmpty : NonEmpty (DS.ObjectDomain I)
    dataDomainNonEmpty   : NonEmpty (DS.DataDomain I)

open DomainWitnesses public

record NonEmptyInterpretation
  {ℓSig : Level}
  (Sig : Signature ℓSig)
  (ℓObj ℓData ℓSem : Level)
  : Type (ℓ-suc (DS.SemLevel ℓSig ℓObj ℓData ℓSem)) where
  constructor nonEmptyInterpretation
  field
    interpretation   : DS.Interpretation Sig ℓObj ℓData ℓSem
    nonEmptyDomains  : DomainWitnesses interpretation

open NonEmptyInterpretation public

objectDomainWitness :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (packaged : NonEmptyInterpretation Sig ℓObj ℓData ℓSem) →
  DS.ObjectDomain (interpretation packaged)
objectDomainWitness packaged =
  witness (objectDomainNonEmpty (nonEmptyDomains packaged))

dataDomainWitness :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (packaged : NonEmptyInterpretation Sig ℓObj ℓData ℓSem) →
  DS.DataDomain (interpretation packaged)
dataDomainWitness packaged =
  witness (dataDomainNonEmpty (nonEmptyDomains packaged))

packNonEmptyInterpretation :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : DS.Interpretation Sig ℓObj ℓData ℓSem) →
  DS.ObjectDomain I →
  DS.DataDomain I →
  NonEmptyInterpretation Sig ℓObj ℓData ℓSem
packNonEmptyInterpretation I objectWitness dataWitness =
  nonEmptyInterpretation
    I
    (domainWitnesses
      (inhabited objectWitness)
      (inhabited dataWitness))

objectDomainNonEmptyFromIndividual :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : DS.Interpretation Sig ℓObj ℓData ℓSem) →
  IndividualName Sig →
  NonEmpty (DS.ObjectDomain I)
objectDomainNonEmptyFromIndividual I namedIndividual =
  inhabited (DS.individualDenotation I namedIndividual)

dataDomainNonEmptyFromLiteral :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : DS.Interpretation Sig ℓObj ℓData ℓSem) →
  Literal Sig →
  NonEmpty (DS.DataDomain I)
dataDomainNonEmptyFromLiteral I lit =
  inhabited (DS.literalDenotation I lit)

domainWitnessesFromIndividualAndLiteral :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : DS.Interpretation Sig ℓObj ℓData ℓSem) →
  IndividualName Sig →
  Literal Sig →
  DomainWitnesses I
domainWitnessesFromIndividualAndLiteral I namedIndividual lit =
  domainWitnesses
    (objectDomainNonEmptyFromIndividual I namedIndividual)
    (dataDomainNonEmptyFromLiteral I lit)

packFromIndividualAndLiteral :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : DS.Interpretation Sig ℓObj ℓData ℓSem) →
  IndividualName Sig →
  Literal Sig →
  NonEmptyInterpretation Sig ℓObj ℓData ℓSem
packFromIndividualAndLiteral I namedIndividual lit =
  nonEmptyInterpretation
    I
    (domainWitnessesFromIndividualAndLiteral I namedIndividual lit)

packUnderlyingInterpretation :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    (I : DS.Interpretation Sig ℓObj ℓData ℓSem)
    (objectWitness : DS.ObjectDomain I)
    (dataWitness : DS.DataDomain I) →
  interpretation
    (packNonEmptyInterpretation I objectWitness dataWitness)
  ≡ I
packUnderlyingInterpretation I objectWitness dataWitness =
  refl

packObjectDomainWitness :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    (I : DS.Interpretation Sig ℓObj ℓData ℓSem)
    (objectWitness : DS.ObjectDomain I)
    (dataWitness : DS.DataDomain I) →
  objectDomainWitness
    (packNonEmptyInterpretation I objectWitness dataWitness)
  ≡ objectWitness
packObjectDomainWitness I objectWitness dataWitness =
  refl

packDataDomainWitness :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    (I : DS.Interpretation Sig ℓObj ℓData ℓSem)
    (objectWitness : DS.ObjectDomain I)
    (dataWitness : DS.DataDomain I) →
  dataDomainWitness
    (packNonEmptyInterpretation I objectWitness dataWitness)
  ≡ dataWitness
packDataDomainWitness I objectWitness dataWitness =
  refl