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

module OWL2.DirectSemantics.Datatype where

open import OWL2.Prelude
open import OWL2.Syntax
import OWL2.Datatype.Map as DM

DataDomain :
  ∀ {ℓSig ℓLex ℓData ℓRel}
    {Sig : Signature ℓSig} →
  DM.DatatypeMap Sig ℓLex ℓData ℓRel → Type ℓData
DataDomain M =
  DM.DataValue (DM.rawMap M)

datatypeDenotation :
  ∀ {ℓSig ℓLex ℓData ℓRel}
    {Sig : Signature ℓSig} →
  (M : DM.DatatypeMap Sig ℓLex ℓData ℓRel) →
  DatatypeName Sig → DataDomain M →
  Type (DM.DatatypeMapLevel ℓSig ℓLex ℓData ℓRel)
datatypeDenotation M =
  DM.mapDatatypeMembership M

literalDenotation :
  ∀ {ℓSig ℓLex ℓData ℓRel}
    {Sig : Signature ℓSig} →
  (M : DM.DatatypeMap Sig ℓLex ℓData ℓRel) →
  Literal Sig → DataDomain M
literalDenotation M =
  DM.literalDenotation M

facetDenotation :
  ∀ {ℓSig ℓLex ℓData ℓRel}
    {Sig : Signature ℓSig} →
  (M : DM.DatatypeMap Sig ℓLex ℓData ℓRel) →
  DatatypeName Sig → FacetName Sig → Literal Sig → DataDomain M →
  Type (DM.DatatypeMapLevel ℓSig ℓLex ℓData ℓRel)
facetDenotation M =
  DM.mapFacetSatisfaction M

DataEq :
  ∀ {ℓSig ℓLex ℓData ℓRel}
    {Sig : Signature ℓSig} →
  (M : DM.DatatypeMap Sig ℓLex ℓData ℓRel) →
  DataDomain M → DataDomain M →
  Type (DM.DatatypeMapLevel ℓSig ℓLex ℓData ℓRel)
DataEq M =
  DM.valueEqual (DM.rawMap M)

LiteralEq :
  ∀ {ℓSig ℓLex ℓData ℓRel}
    {Sig : Signature ℓSig} →
  (M : DM.DatatypeMap Sig ℓLex ℓData ℓRel) →
  Literal Sig → Literal Sig →
  Type (DM.DatatypeMapLevel ℓSig ℓLex ℓData ℓRel)
LiteralEq M =
  DM.LiteralEqual M