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

module OWL2.Portable.ObjectPropertyKeys where

open import OWL2.Prelude
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax as S
import OWL2.Syntax.Regularity as Reg

portableObjectPropertyBaseKey : P.ObjectPropertyExpression → String
portableObjectPropertyBaseKey (P.objectProperty p) =
  PK.nameKey p
portableObjectPropertyBaseKey P.topObjectProperty =
  PK.reservedIRIKey P.owlTopObjectPropertyIRI
portableObjectPropertyBaseKey P.bottomObjectProperty =
  PK.reservedIRIKey P.owlBottomObjectPropertyIRI
portableObjectPropertyBaseKey (P.objectInverseOf p) =
  portableObjectPropertyBaseKey p

syntaxObjectPropertyBaseKey :
  S.ObjectPropertyExpression Sem.PortableSignature → String
syntaxObjectPropertyBaseKey (S.objectProperty p) =
  PK.nameKey p
syntaxObjectPropertyBaseKey S.topObjectProperty =
  PK.reservedIRIKey P.owlTopObjectPropertyIRI
syntaxObjectPropertyBaseKey S.bottomObjectProperty =
  PK.reservedIRIKey P.owlBottomObjectPropertyIRI
syntaxObjectPropertyBaseKey (S.objectInverseOf p) =
  syntaxObjectPropertyBaseKey p

syntaxObjectPropertyBaseKeyTranslate :
  (property : P.ObjectPropertyExpression) →
  syntaxObjectPropertyBaseKey
    (Sem.translateObjectPropertyExpression property)
  ≡
  portableObjectPropertyBaseKey property
syntaxObjectPropertyBaseKeyTranslate (P.objectProperty p) =
  refl
syntaxObjectPropertyBaseKeyTranslate P.topObjectProperty =
  refl
syntaxObjectPropertyBaseKeyTranslate P.bottomObjectProperty =
  refl
syntaxObjectPropertyBaseKeyTranslate (P.objectInverseOf p) =
  syntaxObjectPropertyBaseKeyTranslate p

syntaxObjectPropertyBaseKeyInverse :
  (property : S.ObjectPropertyExpression Sem.PortableSignature) →
  syntaxObjectPropertyBaseKey
    (Reg.inverseObjectPropertyExpression property)
  ≡
  syntaxObjectPropertyBaseKey property
syntaxObjectPropertyBaseKeyInverse (S.objectProperty p) =
  refl
syntaxObjectPropertyBaseKeyInverse S.topObjectProperty =
  refl
syntaxObjectPropertyBaseKeyInverse S.bottomObjectProperty =
  refl
syntaxObjectPropertyBaseKeyInverse (S.objectInverseOf p) =
  refl