OWL2.Portable.Equality

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

module OWL2.Portable.Equality where

open import OWL2.Prelude
open import Cubical.Relation.Nullary.Base using (Dec; Discrete; yes; no)
import Cubical.Data.Nat.Properties as NatProperties
import OWL2.Data.String as String
import OWL2.Portable.Syntax as P

private
  optionalEquality :
    ∀ {A : Type₀} →
    Discrete A →
    (left right : A) →
    Optional (left ≡ right)
  optionalEquality discrete left right
    with discrete left right
  ... | yes equal =
    present equal
  ... | no unequal =
    absent

  encodeFromRefl :
    ∀ {A : Type₀} →
    (Code : A → A → Type₀) →
    ((value : A) → Code value value) →
    (left right : A) →
    left ≡ right →
    Code left right
  encodeFromRefl Code reflCode left right equal =
    subst (Code left) equal (reflCode left)

  discreteFromCode :
    ∀ {A : Type₀} →
    (Code : A → A → Type₀) →
    ((value : A) → Code value value) →
    ((left right : A) → Code left right → left ≡ right) →
    ((left right : A) → Dec (Code left right)) →
    Discrete A
  discreteFromCode Code reflCode decode decCode left right
    with decCode left right
  ... | yes code =
    yes (decode left right code)
  ... | no notCode =
    no (λ equal → notCode (encodeFromRefl Code reflCode left right equal))

  iriPayload : P.IRI → String
  iriPayload (P.iri payload) =
    payload

private
  reservedIRIIndex : P.ReservedIRI → ℕ
  reservedIRIIndex P.owlThingIRI =
    0
  reservedIRIIndex P.owlNothingIRI =
    1
  reservedIRIIndex P.owlTopObjectPropertyIRI =
    2
  reservedIRIIndex P.owlBottomObjectPropertyIRI =
    3
  reservedIRIIndex P.owlTopDataPropertyIRI =
    4
  reservedIRIIndex P.owlBottomDataPropertyIRI =
    5
  reservedIRIIndex P.rdfPlainLiteralIRI =
    6
  reservedIRIIndex P.rdfsLiteralIRI =
    7
  reservedIRIIndex P.xsdStringIRI =
    8

  reservedIRIFromIndex : ℕ → P.ReservedIRI
  reservedIRIFromIndex 0 =
    P.owlThingIRI
  reservedIRIFromIndex 1 =
    P.owlNothingIRI
  reservedIRIFromIndex 2 =
    P.owlTopObjectPropertyIRI
  reservedIRIFromIndex 3 =
    P.owlBottomObjectPropertyIRI
  reservedIRIFromIndex 4 =
    P.owlTopDataPropertyIRI
  reservedIRIFromIndex 5 =
    P.owlBottomDataPropertyIRI
  reservedIRIFromIndex 6 =
    P.rdfPlainLiteralIRI
  reservedIRIFromIndex 7 =
    P.rdfsLiteralIRI
  reservedIRIFromIndex _ =
    P.xsdStringIRI

  reservedIRIFromIndexRoundTrip :
    (iri : P.ReservedIRI) →
    reservedIRIFromIndex (reservedIRIIndex iri) ≡ iri
  reservedIRIFromIndexRoundTrip P.owlThingIRI =
    refl
  reservedIRIFromIndexRoundTrip P.owlNothingIRI =
    refl
  reservedIRIFromIndexRoundTrip P.owlTopObjectPropertyIRI =
    refl
  reservedIRIFromIndexRoundTrip P.owlBottomObjectPropertyIRI =
    refl
  reservedIRIFromIndexRoundTrip P.owlTopDataPropertyIRI =
    refl
  reservedIRIFromIndexRoundTrip P.owlBottomDataPropertyIRI =
    refl
  reservedIRIFromIndexRoundTrip P.rdfPlainLiteralIRI =
    refl
  reservedIRIFromIndexRoundTrip P.rdfsLiteralIRI =
    refl
  reservedIRIFromIndexRoundTrip P.xsdStringIRI =
    refl

  reservedIRIIndexInjective :
    (left right : P.ReservedIRI) →
    reservedIRIIndex left ≡ reservedIRIIndex right →
    left ≡ right
  reservedIRIIndexInjective left right equalIndex =
    sym (reservedIRIFromIndexRoundTrip left)
    ∙ cong reservedIRIFromIndex equalIndex
    ∙ reservedIRIFromIndexRoundTrip right

reservedIRIDiscrete : Discrete P.ReservedIRI
reservedIRIDiscrete left right
  with NatProperties.discreteℕ
        (reservedIRIIndex left)
        (reservedIRIIndex right)
... | yes equalIndex =
  yes (reservedIRIIndexInjective left right equalIndex)
... | no unequalIndex =
  no (λ equalIRI → unequalIndex (cong reservedIRIIndex equalIRI))

reservedIRIEquality :
  (left right : P.ReservedIRI) → Optional (left ≡ right)
reservedIRIEquality =
  optionalEquality reservedIRIDiscrete

iriDiscrete : Discrete P.IRI
iriDiscrete (P.iri left) (P.iri right)
  with String.stringDiscrete left right
... | yes equalPayload =
  yes (cong P.iri equalPayload)
... | no unequalPayload =
  no (λ equalIRI → unequalPayload (cong iriPayload equalIRI))

iriEquality : (left right : P.IRI) → Optional (left ≡ right)
iriEquality =
  optionalEquality iriDiscrete

NameCode : P.Name → P.Name → Type₀
NameCode (P.named left) (P.named right) =
  left ≡ right
NameCode (P.reserved left) (P.reserved right) =
  left ≡ right
NameCode _ _ =
  ⊥

nameReflCode :
  (value : P.Name) →
  NameCode value value
nameReflCode (P.named value) =
  refl
nameReflCode (P.reserved value) =
  refl

nameDecode :
  (left right : P.Name) →
  NameCode left right →
  left ≡ right
nameDecode (P.named left) (P.named right) equal =
  cong P.named equal
nameDecode (P.named left) (P.reserved right) ()
nameDecode (P.reserved left) (P.named right) ()
nameDecode (P.reserved left) (P.reserved right) equal =
  cong P.reserved equal

nameCodeDec :
  (left right : P.Name) →
  Dec (NameCode left right)
nameCodeDec (P.named left) (P.named right) =
  iriDiscrete left right
nameCodeDec (P.named left) (P.reserved right) =
  no (λ empty → empty)
nameCodeDec (P.reserved left) (P.named right) =
  no (λ empty → empty)
nameCodeDec (P.reserved left) (P.reserved right) =
  reservedIRIDiscrete left right

nameDiscrete : Discrete P.Name
nameDiscrete =
  discreteFromCode NameCode nameReflCode nameDecode nameCodeDec

nameEquality : (left right : P.Name) → Optional (left ≡ right)
nameEquality =
  optionalEquality nameDiscrete

ObjectPropertyExpressionCode :
  P.ObjectPropertyExpression →
  P.ObjectPropertyExpression →
  Type₀
ObjectPropertyExpressionCode
  (P.objectProperty left)
  (P.objectProperty right) =
  left ≡ right
ObjectPropertyExpressionCode
  P.topObjectProperty
  P.topObjectProperty =
  Unit*
ObjectPropertyExpressionCode
  P.bottomObjectProperty
  P.bottomObjectProperty =
  Unit*
ObjectPropertyExpressionCode
  (P.objectInverseOf left)
  (P.objectInverseOf right) =
  left ≡ right
ObjectPropertyExpressionCode _ _ =
  ⊥

objectPropertyExpressionReflCode :
  (value : P.ObjectPropertyExpression) →
  ObjectPropertyExpressionCode value value
objectPropertyExpressionReflCode (P.objectProperty value) =
  refl
objectPropertyExpressionReflCode P.topObjectProperty =
  tt*
objectPropertyExpressionReflCode P.bottomObjectProperty =
  tt*
objectPropertyExpressionReflCode (P.objectInverseOf value) =
  refl

objectPropertyExpressionDecode :
  (left right : P.ObjectPropertyExpression) →
  ObjectPropertyExpressionCode left right →
  left ≡ right
objectPropertyExpressionDecode
  (P.objectProperty left)
  (P.objectProperty right)
  equal =
  cong P.objectProperty equal
objectPropertyExpressionDecode
  (P.objectProperty left)
  P.topObjectProperty
  ()
objectPropertyExpressionDecode
  (P.objectProperty left)
  P.bottomObjectProperty
  ()
objectPropertyExpressionDecode
  (P.objectProperty left)
  (P.objectInverseOf right)
  ()
objectPropertyExpressionDecode
  P.topObjectProperty
  (P.objectProperty right)
  ()
objectPropertyExpressionDecode
  P.topObjectProperty
  P.topObjectProperty
  code =
  refl
objectPropertyExpressionDecode
  P.topObjectProperty
  P.bottomObjectProperty
  ()
objectPropertyExpressionDecode
  P.topObjectProperty
  (P.objectInverseOf right)
  ()
objectPropertyExpressionDecode
  P.bottomObjectProperty
  (P.objectProperty right)
  ()
objectPropertyExpressionDecode
  P.bottomObjectProperty
  P.topObjectProperty
  ()
objectPropertyExpressionDecode
  P.bottomObjectProperty
  P.bottomObjectProperty
  code =
  refl
objectPropertyExpressionDecode
  P.bottomObjectProperty
  (P.objectInverseOf right)
  ()
objectPropertyExpressionDecode
  (P.objectInverseOf left)
  (P.objectProperty right)
  ()
objectPropertyExpressionDecode
  (P.objectInverseOf left)
  P.topObjectProperty
  ()
objectPropertyExpressionDecode
  (P.objectInverseOf left)
  P.bottomObjectProperty
  ()
objectPropertyExpressionDecode
  (P.objectInverseOf left)
  (P.objectInverseOf right)
  equal =
  cong P.objectInverseOf equal

objectPropertyExpressionDiscrete : Discrete P.ObjectPropertyExpression
objectPropertyExpressionDiscrete
  (P.objectProperty left)
  (P.objectProperty right)
  with nameDiscrete left right
... | yes equalName =
  yes (cong P.objectProperty equalName)
... | no unequalName =
  no
    (λ equalProperty →
      unequalName
        (encodeFromRefl
          ObjectPropertyExpressionCode
          objectPropertyExpressionReflCode
          (P.objectProperty left)
          (P.objectProperty right)
          equalProperty))
objectPropertyExpressionDiscrete
  (P.objectProperty left)
  P.topObjectProperty =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      (P.objectProperty left)
      P.topObjectProperty)
objectPropertyExpressionDiscrete
  (P.objectProperty left)
  P.bottomObjectProperty =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      (P.objectProperty left)
      P.bottomObjectProperty)
objectPropertyExpressionDiscrete
  (P.objectProperty left)
  (P.objectInverseOf right) =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      (P.objectProperty left)
      (P.objectInverseOf right))
objectPropertyExpressionDiscrete
  P.topObjectProperty
  (P.objectProperty right) =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      P.topObjectProperty
      (P.objectProperty right))
objectPropertyExpressionDiscrete
  P.topObjectProperty
  P.topObjectProperty =
  yes refl
objectPropertyExpressionDiscrete
  P.topObjectProperty
  P.bottomObjectProperty =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      P.topObjectProperty
      P.bottomObjectProperty)
objectPropertyExpressionDiscrete
  P.topObjectProperty
  (P.objectInverseOf right) =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      P.topObjectProperty
      (P.objectInverseOf right))
objectPropertyExpressionDiscrete
  P.bottomObjectProperty
  (P.objectProperty right) =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      P.bottomObjectProperty
      (P.objectProperty right))
objectPropertyExpressionDiscrete
  P.bottomObjectProperty
  P.topObjectProperty =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      P.bottomObjectProperty
      P.topObjectProperty)
objectPropertyExpressionDiscrete
  P.bottomObjectProperty
  P.bottomObjectProperty =
  yes refl
objectPropertyExpressionDiscrete
  P.bottomObjectProperty
  (P.objectInverseOf right) =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      P.bottomObjectProperty
      (P.objectInverseOf right))
objectPropertyExpressionDiscrete
  (P.objectInverseOf left)
  (P.objectProperty right) =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      (P.objectInverseOf left)
      (P.objectProperty right))
objectPropertyExpressionDiscrete
  (P.objectInverseOf left)
  P.topObjectProperty =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      (P.objectInverseOf left)
      P.topObjectProperty)
objectPropertyExpressionDiscrete
  (P.objectInverseOf left)
  P.bottomObjectProperty =
  no
    (encodeFromRefl
      ObjectPropertyExpressionCode
      objectPropertyExpressionReflCode
      (P.objectInverseOf left)
      P.bottomObjectProperty)
objectPropertyExpressionDiscrete
  (P.objectInverseOf left)
  (P.objectInverseOf right)
  with objectPropertyExpressionDiscrete left right
... | yes equalProperty =
  yes (cong P.objectInverseOf equalProperty)
... | no unequalProperty =
  no
    (λ equalInverse →
      unequalProperty
        (encodeFromRefl
          ObjectPropertyExpressionCode
          objectPropertyExpressionReflCode
          (P.objectInverseOf left)
          (P.objectInverseOf right)
          equalInverse))

objectPropertyExpressionEquality :
  (left right : P.ObjectPropertyExpression) →
  Optional (left ≡ right)
objectPropertyExpressionEquality =
  optionalEquality objectPropertyExpressionDiscrete