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

module OWL2.Datatype.XSD.Core where

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

data XSDCoreDatatypeKind : Type₀ where
  xsdStringKind xsdBooleanKind unsupportedDatatypeKind : XSDCoreDatatypeKind

data XSDCoreLexical : Type₀ where
  lexicalString       : String → XSDCoreLexical
  lexicalBooleanTrue  : XSDCoreLexical
  lexicalBooleanFalse : XSDCoreLexical

lexicalText : XSDCoreLexical → String
lexicalText (lexicalString text) =
  text
lexicalText lexicalBooleanTrue =
  "true"
lexicalText lexicalBooleanFalse =
  "false"

data XSDCoreValue : Type₀ where
  stringValue  : String → XSDCoreValue
  booleanValue : Bool → XSDCoreValue

record XSDCoreNames
  {ℓSig : Level}
  (Sig : Signature ℓSig)
  : Type ℓSig where
  field
    xsdString  : DatatypeName Sig
    xsdBoolean : DatatypeName Sig

    datatypeKind :
      DatatypeName Sig → XSDCoreDatatypeKind

open XSDCoreNames public

data XSDCoreKindLexicalSpace
  {ℓ : Level}
  : XSDCoreDatatypeKind → XSDCoreLexical → Type ℓ where
  stringLexical :
    (text : String) →
    XSDCoreKindLexicalSpace xsdStringKind (lexicalString text)
  booleanTrueLexical :
    XSDCoreKindLexicalSpace xsdBooleanKind lexicalBooleanTrue
  booleanFalseLexical :
    XSDCoreKindLexicalSpace xsdBooleanKind lexicalBooleanFalse

data XSDCoreKindValueSpace
  {ℓ : Level}
  : XSDCoreDatatypeKind → XSDCoreValue → Type ℓ where
  stringMember :
    (text : String) →
    XSDCoreKindValueSpace xsdStringKind (stringValue text)
  booleanMember :
    (bool : Bool) →
    XSDCoreKindValueSpace xsdBooleanKind (booleanValue bool)

data XSDCoreKindLexicalToValue
  {ℓ : Level}
  : XSDCoreDatatypeKind → XSDCoreLexical → XSDCoreValue → Type ℓ where
  stringToValue :
    (text : String) →
    XSDCoreKindLexicalToValue
      xsdStringKind
      (lexicalString text)
      (stringValue text)
  booleanTrueToValue :
    XSDCoreKindLexicalToValue
      xsdBooleanKind
      lexicalBooleanTrue
      (booleanValue true)
  booleanFalseToValue :
    XSDCoreKindLexicalToValue
      xsdBooleanKind
      lexicalBooleanFalse
      (booleanValue false)

data XSDCoreValueEqual
  {ℓ : Level}
  : XSDCoreValue → XSDCoreValue → Type ℓ where
  sameStringValue :
    (text : String) →
    XSDCoreValueEqual (stringValue text) (stringValue text)
  sameBooleanValue :
    (bool : Bool) →
    XSDCoreValueEqual (booleanValue bool) (booleanValue bool)

XSDCoreLexicalSpace :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  XSDCoreNames Sig →
  DatatypeName Sig → XSDCoreLexical → Type ℓSig
XSDCoreLexicalSpace names d =
  XSDCoreKindLexicalSpace (datatypeKind names d)

XSDCoreValueSpace :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  XSDCoreNames Sig →
  DatatypeName Sig → XSDCoreValue → Type ℓSig
XSDCoreValueSpace names d =
  XSDCoreKindValueSpace (datatypeKind names d)

XSDCoreLexicalToValue :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  XSDCoreNames Sig →
  DatatypeName Sig → XSDCoreLexical → XSDCoreValue → Type ℓSig
XSDCoreLexicalToValue names d =
  XSDCoreKindLexicalToValue (datatypeKind names d)

record XSDCoreLiteralView
  {ℓSig : Level}
  {Sig : Signature ℓSig}
  (names : XSDCoreNames Sig)
  : Type ℓSig where
  field
    literalDatatypeName :
      Literal Sig → DatatypeName Sig
    literalLexicalForm :
      Literal Sig → XSDCoreLexical
    literalValue :
      Literal Sig → XSDCoreValue
    literalToValue :
      (lit : Literal Sig) →
      XSDCoreLexicalToValue
        names
        (literalDatatypeName lit)
        (literalLexicalForm lit)
        (literalValue lit)

open XSDCoreLiteralView public

record XSDCoreFacetSemantics
  {ℓSig : Level}
  {Sig : Signature ℓSig}
  (names : XSDCoreNames Sig)
  : Type (ℓ-suc ℓSig) where
  field
    FacetSatisfied :
      DatatypeName Sig →
      FacetName Sig →
      Literal Sig →
      XSDCoreValue →
      Type ℓSig

    facetRespectsValueEqual :
      (d : DatatypeName Sig) →
      (facet : FacetName Sig) →
      (restrictionValue : Literal Sig) →
      (left right : XSDCoreValue) →
      XSDCoreValueEqual {ℓSig} left right →
      FacetSatisfied d facet restrictionValue left →
      FacetSatisfied d facet restrictionValue right

open XSDCoreFacetSemantics public

trivialFacetSemantics :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  (names : XSDCoreNames Sig) →
  XSDCoreFacetSemantics names
trivialFacetSemantics names .FacetSatisfied d facet restrictionValue value =
  Unit*
trivialFacetSemantics names .facetRespectsValueEqual
  d facet restrictionValue left right valueEq satisfied =
  tt*

xsdCoreRawDatatypeMap :
  ∀ {ℓSig}
    {Sig : Signature ℓSig}
    {names : XSDCoreNames Sig} →
  XSDCoreLiteralView names →
  XSDCoreFacetSemantics names →
  DM.RawDatatypeMap Sig ℓ-zero ℓ-zero ℓSig
xsdCoreRawDatatypeMap view facets .DM.LexicalForm =
  XSDCoreLexical
xsdCoreRawDatatypeMap view facets .DM.DataValue =
  XSDCoreValue
xsdCoreRawDatatypeMap view facets .DM.literalDatatype =
  literalDatatypeName view
xsdCoreRawDatatypeMap view facets .DM.literalLexicalForm =
  literalLexicalForm view
xsdCoreRawDatatypeMap {names = names} view facets .DM.lexicalSpace =
  XSDCoreLexicalSpace names
xsdCoreRawDatatypeMap {names = names} view facets .DM.valueSpace =
  XSDCoreValueSpace names
xsdCoreRawDatatypeMap {names = names} view facets .DM.lexicalToValue =
  XSDCoreLexicalToValue names
xsdCoreRawDatatypeMap view facets .DM.valueEqual =
  XSDCoreValueEqual
xsdCoreRawDatatypeMap view facets .DM.facetSatisfaction =
  FacetSatisfied facets

xsdCoreKindLexicalToValueSound :
  ∀ {ℓ} →
  (kind : XSDCoreDatatypeKind) →
  (lex : XSDCoreLexical) →
  (value : XSDCoreValue) →
  XSDCoreKindLexicalToValue {ℓ} kind lex value →
  XSDCoreKindLexicalSpace {ℓ} kind lex ×
  XSDCoreKindValueSpace {ℓ} kind value
xsdCoreKindLexicalToValueSound
  .xsdStringKind
  .(lexicalString text)
  .(stringValue text)
  (stringToValue text) =
  stringLexical text , stringMember text
xsdCoreKindLexicalToValueSound
  .xsdBooleanKind
  .lexicalBooleanTrue
  .(booleanValue true)
  booleanTrueToValue =
  booleanTrueLexical , booleanMember true
xsdCoreKindLexicalToValueSound
  .xsdBooleanKind
  .lexicalBooleanFalse
  .(booleanValue false)
  booleanFalseToValue =
  booleanFalseLexical , booleanMember false

xsdCoreLexicalToValueSound :
  ∀ {ℓSig}
    {Sig : Signature ℓSig}
    {names : XSDCoreNames Sig} →
  (d : DatatypeName Sig) →
  (lex : XSDCoreLexical) →
  (value : XSDCoreValue) →
  XSDCoreLexicalToValue names d lex value →
  XSDCoreLexicalSpace names d lex ×
  XSDCoreValueSpace names d value
xsdCoreLexicalToValueSound {names = names} d =
  xsdCoreKindLexicalToValueSound (datatypeKind names d)

xsdCoreKindLexicalFunctional :
  ∀ {ℓ} →
  (kind : XSDCoreDatatypeKind) →
  (lex : XSDCoreLexical) →
  (left right : XSDCoreValue) →
  XSDCoreKindLexicalToValue {ℓ} kind lex left →
  XSDCoreKindLexicalToValue {ℓ} kind lex right →
  XSDCoreValueEqual {ℓ} left right
xsdCoreKindLexicalFunctional
  .xsdStringKind
  .(lexicalString text)
  .(stringValue text)
  .(stringValue text)
  (stringToValue text)
  (stringToValue .text) =
  sameStringValue text
xsdCoreKindLexicalFunctional
  .xsdBooleanKind
  .lexicalBooleanTrue
  .(booleanValue true)
  .(booleanValue true)
  booleanTrueToValue
  booleanTrueToValue =
  sameBooleanValue true
xsdCoreKindLexicalFunctional
  .xsdBooleanKind
  .lexicalBooleanFalse
  .(booleanValue false)
  .(booleanValue false)
  booleanFalseToValue
  booleanFalseToValue =
  sameBooleanValue false

xsdCoreLiteralFunctional :
  ∀ {ℓSig}
    {Sig : Signature ℓSig}
    {names : XSDCoreNames Sig}
    (view : XSDCoreLiteralView names) →
  (lit : Literal Sig) →
  (left right : XSDCoreValue) →
  XSDCoreLexicalToValue
    names
    (literalDatatypeName view lit)
    (literalLexicalForm view lit)
    left →
  XSDCoreLexicalToValue
    names
    (literalDatatypeName view lit)
    (literalLexicalForm view lit)
    right →
  XSDCoreValueEqual {ℓSig} left right
xsdCoreLiteralFunctional {names = names} view lit left right =
  xsdCoreKindLexicalFunctional
    (datatypeKind names (literalDatatypeName view lit))
    (literalLexicalForm view lit)
    left
    right

xsdCoreValueEqualRefl :
  ∀ {ℓ} →
  (value : XSDCoreValue) →
  XSDCoreValueEqual {ℓ} value value
xsdCoreValueEqualRefl (stringValue text) =
  sameStringValue text
xsdCoreValueEqualRefl (booleanValue bool) =
  sameBooleanValue bool

xsdCoreValueEqualSym :
  ∀ {ℓ} →
  (left right : XSDCoreValue) →
  XSDCoreValueEqual {ℓ} left right →
  XSDCoreValueEqual {ℓ} right left
xsdCoreValueEqualSym
  .(stringValue text)
  .(stringValue text)
  (sameStringValue text) =
  sameStringValue text
xsdCoreValueEqualSym
  .(booleanValue bool)
  .(booleanValue bool)
  (sameBooleanValue bool) =
  sameBooleanValue bool

xsdCoreValueEqualTrans :
  ∀ {ℓ} →
  (left middle right : XSDCoreValue) →
  XSDCoreValueEqual {ℓ} left middle →
  XSDCoreValueEqual {ℓ} middle right →
  XSDCoreValueEqual {ℓ} left right
xsdCoreValueEqualTrans
  .(stringValue text)
  .(stringValue text)
  .(stringValue text)
  (sameStringValue text)
  (sameStringValue .text) =
  sameStringValue text
xsdCoreValueEqualTrans
  .(booleanValue bool)
  .(booleanValue bool)
  .(booleanValue bool)
  (sameBooleanValue bool)
  (sameBooleanValue .bool) =
  sameBooleanValue bool

xsdCoreKindMembershipRespectsValueEqual :
  ∀ {ℓ} →
  (kind : XSDCoreDatatypeKind) →
  (left right : XSDCoreValue) →
  XSDCoreValueEqual {ℓ} left right →
  XSDCoreKindValueSpace {ℓ} kind left →
  XSDCoreKindValueSpace {ℓ} kind right
xsdCoreKindMembershipRespectsValueEqual
  .xsdStringKind
  .(stringValue text)
  .(stringValue text)
  (sameStringValue text)
  (stringMember .text) =
  stringMember text
xsdCoreKindMembershipRespectsValueEqual
  .xsdBooleanKind
  .(booleanValue bool)
  .(booleanValue bool)
  (sameBooleanValue bool)
  (booleanMember .bool) =
  booleanMember bool

xsdCoreMembershipRespectsValueEqual :
  ∀ {ℓSig}
    {Sig : Signature ℓSig}
    {names : XSDCoreNames Sig} →
  (d : DatatypeName Sig) →
  (left right : XSDCoreValue) →
  XSDCoreValueEqual {ℓSig} left right →
  XSDCoreValueSpace names d left →
  XSDCoreValueSpace names d right
xsdCoreMembershipRespectsValueEqual {names = names} d =
  xsdCoreKindMembershipRespectsValueEqual (datatypeKind names d)

xsdCoreDatatypeMap :
  ∀ {ℓSig}
    {Sig : Signature ℓSig}
    {names : XSDCoreNames Sig} →
  XSDCoreLiteralView names →
  XSDCoreFacetSemantics names →
  DM.DatatypeMap Sig ℓ-zero ℓ-zero ℓSig
xsdCoreDatatypeMap {names = names} view facets .DM.rawMap =
  xsdCoreRawDatatypeMap view facets
xsdCoreDatatypeMap {names = names} view facets .DM.lexicalToValueSound
  d lex value maps =
  xsdCoreLexicalToValueSound {names = names} d lex value maps
xsdCoreDatatypeMap {names = names} view facets .DM.literalInterpretationTotal lit =
  literalValue view lit , literalToValue view lit
xsdCoreDatatypeMap {names = names} view facets .DM.literalInterpretationFunctional =
  xsdCoreLiteralFunctional view
xsdCoreDatatypeMap {names = names} view facets .DM.valueEqualRefl =
  xsdCoreValueEqualRefl
xsdCoreDatatypeMap {names = names} view facets .DM.valueEqualSym =
  xsdCoreValueEqualSym
xsdCoreDatatypeMap {names = names} view facets .DM.valueEqualTrans =
  xsdCoreValueEqualTrans
xsdCoreDatatypeMap {names = names} view facets .DM.datatypeMembershipRespectsValueEqual
  d left right valueEq member =
  xsdCoreMembershipRespectsValueEqual {names = names} d left right valueEq member
xsdCoreDatatypeMap {names = names} view facets .DM.facetSatisfactionRespectsValueEqual =
  facetRespectsValueEqual facets