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

module OWL2.Datatype.Map where

open import OWL2.Prelude
open import OWL2.Syntax

DatatypeMapLevel : Level → Level → Level → Level → Level
DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel =
  ℓ-max (ℓ-max (ℓ-max ℓSig ℓLex) ℓValue) ℓRel

record RawDatatypeMap
  {ℓSig : Level}
  (Sig : Signature ℓSig)
  (ℓLex ℓValue ℓRel : Level)
  : Type (ℓ-suc (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)) where
  field
    LexicalForm : Type ℓLex
    DataValue   : Type ℓValue

    literalDatatype :
      Literal Sig → DatatypeName Sig
    literalLexicalForm :
      Literal Sig → LexicalForm

    lexicalSpace :
      DatatypeName Sig → LexicalForm →
      Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
    valueSpace :
      DatatypeName Sig → DataValue →
      Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
    lexicalToValue :
      DatatypeName Sig → LexicalForm → DataValue →
      Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)

    valueEqual :
      DataValue → DataValue →
      Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
    facetSatisfaction :
      DatatypeName Sig → FacetName Sig → Literal Sig → DataValue →
      Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)

open RawDatatypeMap public

LexicalSpace :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : RawDatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig →
  LexicalForm M → Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
LexicalSpace M d lex =
  lexicalSpace M d lex

ValueSpace :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : RawDatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig →
  DataValue M → Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
ValueSpace M d value =
  valueSpace M d value

LexicalToValue :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : RawDatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig →
  LexicalForm M → DataValue M →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
LexicalToValue M d lex value =
  lexicalToValue M d lex value

LiteralInterpretation :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : RawDatatypeMap Sig ℓLex ℓValue ℓRel) →
  Literal Sig → DataValue M →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
LiteralInterpretation M lit value =
  lexicalToValue M
    (literalDatatype M lit)
    (literalLexicalForm M lit)
    value

DatatypeMembership :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : RawDatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig → DataValue M →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
DatatypeMembership M d value =
  valueSpace M d value

LiteralDatatypeMembership :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : RawDatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig → Literal Sig →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
LiteralDatatypeMembership M d lit =
  Σ (DataValue M)
    (λ value →
      LiteralInterpretation M lit value
      ×
      DatatypeMembership M d value)

LiteralValueEqual :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : RawDatatypeMap Sig ℓLex ℓValue ℓRel) →
  Literal Sig → Literal Sig →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
LiteralValueEqual M left right =
  Σ (DataValue M)
    (λ leftValue →
      Σ (DataValue M)
        (λ rightValue →
          LiteralInterpretation M left leftValue
          ×
          LiteralInterpretation M right rightValue
          ×
          valueEqual M leftValue rightValue))

SatisfiesFacet :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : RawDatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig → FacetName Sig → Literal Sig → DataValue M →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
SatisfiesFacet M d facet lit value =
  facetSatisfaction M d facet lit value

record DatatypeMap
  {ℓSig : Level}
  (Sig : Signature ℓSig)
  (ℓLex ℓValue ℓRel : Level)
  : Type (ℓ-suc (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)) where
  constructor datatypeMap
  field
    rawMap : RawDatatypeMap Sig ℓLex ℓValue ℓRel

    lexicalToValueSound :
      (d : DatatypeName Sig) →
      (lex : LexicalForm rawMap) →
      (value : DataValue rawMap) →
      LexicalToValue rawMap d lex value →
      LexicalSpace rawMap d lex × DatatypeMembership rawMap d value

    literalInterpretationTotal :
      (lit : Literal Sig) →
      Σ (DataValue rawMap) (LiteralInterpretation rawMap lit)

    literalInterpretationFunctional :
      (lit : Literal Sig) →
      (left right : DataValue rawMap) →
      LiteralInterpretation rawMap lit left →
      LiteralInterpretation rawMap lit right →
      valueEqual rawMap left right

    valueEqualRefl :
      (value : DataValue rawMap) →
      valueEqual rawMap value value
    valueEqualSym :
      (left right : DataValue rawMap) →
      valueEqual rawMap left right →
      valueEqual rawMap right left
    valueEqualTrans :
      (left middle right : DataValue rawMap) →
      valueEqual rawMap left middle →
      valueEqual rawMap middle right →
      valueEqual rawMap left right

    datatypeMembershipRespectsValueEqual :
      (d : DatatypeName Sig) →
      (left right : DataValue rawMap) →
      valueEqual rawMap left right →
      DatatypeMembership rawMap d left →
      DatatypeMembership rawMap d right

    facetSatisfactionRespectsValueEqual :
      (d : DatatypeName Sig) →
      (facet : FacetName Sig) →
      (restrictionValue : Literal Sig) →
      (left right : DataValue rawMap) →
      valueEqual rawMap left right →
      SatisfiesFacet rawMap d facet restrictionValue left →
      SatisfiesFacet rawMap d facet restrictionValue right

open DatatypeMap public

literalDenotation :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  Literal Sig → DataValue (rawMap M)
literalDenotation M lit =
  fst (literalInterpretationTotal M lit)

literalDenotationInterprets :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  (lit : Literal Sig) →
  LiteralInterpretation (rawMap M) lit (literalDenotation M lit)
literalDenotationInterprets M lit =
  snd (literalInterpretationTotal M lit)

literalDenotationInDeclaredDatatype :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  (lit : Literal Sig) →
  DatatypeMembership
    (rawMap M)
    (literalDatatype (rawMap M) lit)
    (literalDenotation M lit)
literalDenotationInDeclaredDatatype M lit =
  snd
    (lexicalToValueSound M
      (literalDatatype (rawMap M) lit)
      (literalLexicalForm (rawMap M) lit)
      (literalDenotation M lit)
      (literalDenotationInterprets M lit))

literalLexicalFormInDeclaredDatatype :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  (lit : Literal Sig) →
  LexicalSpace
    (rawMap M)
    (literalDatatype (rawMap M) lit)
    (literalLexicalForm (rawMap M) lit)
literalLexicalFormInDeclaredDatatype M lit =
  fst
    (lexicalToValueSound M
      (literalDatatype (rawMap M) lit)
      (literalLexicalForm (rawMap M) lit)
      (literalDenotation M lit)
      (literalDenotationInterprets M lit))

mapDatatypeMembership :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig → DataValue (rawMap M) →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
mapDatatypeMembership M =
  DatatypeMembership (rawMap M)

LiteralEqual :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  Literal Sig → Literal Sig →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
LiteralEqual M left right =
  valueEqual
    (rawMap M)
    (literalDenotation M left)
    (literalDenotation M right)

literalEqualRefl :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  (lit : Literal Sig) →
  LiteralEqual M lit lit
literalEqualRefl M lit =
  valueEqualRefl M (literalDenotation M lit)

literalEqualSym :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  (left right : Literal Sig) →
  LiteralEqual M left right →
  LiteralEqual M right left
literalEqualSym M left right =
  valueEqualSym M (literalDenotation M left) (literalDenotation M right)

literalEqualTrans :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  (left middle right : Literal Sig) →
  LiteralEqual M left middle →
  LiteralEqual M middle right →
  LiteralEqual M left right
literalEqualTrans M left middle right =
  valueEqualTrans M
    (literalDenotation M left)
    (literalDenotation M middle)
    (literalDenotation M right)

mapFacetSatisfaction :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig → FacetName Sig → Literal Sig →
  DataValue (rawMap M) →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
mapFacetSatisfaction M =
  SatisfiesFacet (rawMap M)

LiteralSatisfiesFacet :
  ∀ {ℓSig ℓLex ℓValue ℓRel}
    {Sig : Signature ℓSig} →
  (M : DatatypeMap Sig ℓLex ℓValue ℓRel) →
  DatatypeName Sig → FacetName Sig → Literal Sig → Literal Sig →
  Type (DatatypeMapLevel ℓSig ℓLex ℓValue ℓRel)
LiteralSatisfiesFacet M d facet restrictionValue lit =
  mapFacetSatisfaction M d facet restrictionValue (literalDenotation M lit)