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

module OWL2.DirectSemantics.Expansions where

open import OWL2.Prelude
import Cubical.Data.Prod.Base as Prod
open import OWL2.Syntax
open import OWL2.DirectSemantics

disjointUnionClassExpression :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  ClassName Sig →
  ClassExpression Sig →
  ClassExpression Sig →
  List (ClassExpression Sig) →
  ClassExpression Sig
disjointUnionClassExpression c first second rest =
  objectUnionOf (first ∷ second ∷ rest)

disjointUnionEquivalentAxiom :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  ClassName Sig →
  ClassExpression Sig →
  ClassExpression Sig →
  List (ClassExpression Sig) →
  Axiom Sig
disjointUnionEquivalentAxiom c first second rest =
  equivalentClasses
    ( namedClass c
    ∷ disjointUnionClassExpression c first second rest
    ∷ [] )

disjointUnionDisjointAxiom :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  ClassExpression Sig →
  ClassExpression Sig →
  List (ClassExpression Sig) →
  Axiom Sig
disjointUnionDisjointAxiom first second rest =
  disjointClasses (first ∷ second ∷ rest)

disjointUnionExpansion :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  ClassName Sig →
  ClassExpression Sig →
  ClassExpression Sig →
  List (ClassExpression Sig) →
  List (Axiom Sig)
disjointUnionExpansion c first second rest =
  disjointUnionEquivalentAxiom c first second rest
  ∷ disjointUnionDisjointAxiom first second rest
  ∷ []

satisfiesDisjointUnionEquivalent :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassName Sig}
    {first second : ClassExpression Sig}
    {rest : List (ClassExpression Sig)} →
  AllList
    (disjointUnionExpansion c first second rest)
    (SatisfiesAxiom I) →
  SatisfiesAxiom I (disjointUnionEquivalentAxiom c first second rest)
satisfiesDisjointUnionEquivalent expansionSatisfied =
  Prod.proj₁ expansionSatisfied

satisfiesDisjointUnionDisjoint :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassName Sig}
    {first second : ClassExpression Sig}
    {rest : List (ClassExpression Sig)} →
  AllList
    (disjointUnionExpansion c first second rest)
    (SatisfiesAxiom I) →
  SatisfiesAxiom I (disjointUnionDisjointAxiom first second rest)
satisfiesDisjointUnionDisjoint expansionSatisfied =
  Prod.proj₁ (Prod.proj₂ expansionSatisfied)

inverseObjectPropertiesExpansion :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  ObjectPropertyExpression Sig →
  ObjectPropertyExpression Sig →
  Axiom Sig
inverseObjectPropertiesExpansion p q =
  equivalentObjectProperties
    (p ∷ objectInverseOf q ∷ [])

inverseObjectPropertiesForward :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p q : ObjectPropertyExpression Sig}
    {x y : ObjectDomain I} →
  SatisfiesAxiom I (inverseObjectPropertiesExpansion p q) →
  evalObjectProperty I p x y →
  evalObjectProperty I q y x
inverseObjectPropertiesForward {x = x} {y = y} inverseSatisfied pxy =
  fst (Prod.proj₁ (fst inverseSatisfied)) (x , y) pxy

inverseObjectPropertiesBackward :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p q : ObjectPropertyExpression Sig}
    {x y : ObjectDomain I} →
  SatisfiesAxiom I (inverseObjectPropertiesExpansion p q) →
  evalObjectProperty I q y x →
  evalObjectProperty I p x y
inverseObjectPropertiesBackward {x = x} {y = y} inverseSatisfied qyx =
  snd (Prod.proj₁ (fst inverseSatisfied)) (x , y) qyx