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

module OWL2.Examples.PropertyChain where

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

data ChainIRI : Type₀ where
  chainDocument : ChainIRI

data ChainClass : Type₀ where
  Person : ChainClass

data ChainObjectProperty : Type₀ where
  hasParent hasGrandparent : ChainObjectProperty

data ChainDataProperty : Type₀ where
  noDataProperty : ChainDataProperty

data ChainDatatype : Type₀ where
  noDatatype : ChainDatatype

data ChainIndividual : Type₀ where
  Alice Bob Carol : ChainIndividual

data ChainLiteral : Type₀ where
  noLiteral : ChainLiteral

data ChainFacet : Type₀ where
  noFacet : ChainFacet

data ChainAnnotationProperty : Type₀ where
  label : ChainAnnotationProperty

ChainSignature : Signature ℓ-zero
ChainSignature .IRI =
  ChainIRI
ChainSignature .ClassName =
  ChainClass
ChainSignature .ObjectPropertyName =
  ChainObjectProperty
ChainSignature .DataPropertyName =
  ChainDataProperty
ChainSignature .DatatypeName =
  ChainDatatype
ChainSignature .IndividualName =
  ChainIndividual
ChainSignature .Literal =
  ChainLiteral
ChainSignature .FacetName =
  ChainFacet
ChainSignature .AnnotationPropertyName =
  ChainAnnotationProperty

PersonC : ClassExpression ChainSignature
PersonC =
  namedClass Person

HasParent HasGrandparent : ObjectPropertyExpression ChainSignature
HasParent =
  objectProperty hasParent
HasGrandparent =
  objectProperty hasGrandparent

ParentParentChain : SubObjectPropertyExpression ChainSignature
ParentParentChain =
  subObjectPropertyChain HasParent HasParent []

chainOntology : Ontology ChainSignature
chainOntology =
  ontology
    (chainDocument ∷ [])
    []
    ( declaration (classEntity Person)
    ∷ declaration (objectPropertyEntity hasParent)
    ∷ declaration (objectPropertyEntity hasGrandparent)
    ∷ subObjectPropertyOf ParentParentChain HasGrandparent
    ∷ objectPropertyAssertion HasParent Alice Bob
    ∷ objectPropertyAssertion HasParent Bob Carol
    ∷ objectPropertyAssertion HasGrandparent Alice Carol
    ∷ [] )

data ChainObject : Type₀ where
  aliceObject bobObject carolObject : ChainObject

data ChainData : Type₀ where
  noDataValue : ChainData

data IsPerson : ChainObject → Type₀ where
  alicePerson : IsPerson aliceObject
  bobPerson : IsPerson bobObject
  carolPerson : IsPerson carolObject

ChainClassDenotation : ChainClass → ChainObject → Type₀
ChainClassDenotation Person =
  IsPerson

data ParentRel : ChainObject → ChainObject → Type₀ where
  aliceBobParent : ParentRel aliceObject bobObject
  bobCarolParent : ParentRel bobObject carolObject

data GrandparentRel : ChainObject → ChainObject → Type₀ where
  grandparentFromParents :
    ∀ {x y z} → ParentRel x y → ParentRel y z → GrandparentRel x z

ChainObjectPropertyDenotation :
  ChainObjectProperty → ChainObject → ChainObject → Type₀
ChainObjectPropertyDenotation hasParent =
  ParentRel
ChainObjectPropertyDenotation hasGrandparent =
  GrandparentRel

ChainDataPropertyDenotation :
  ChainDataProperty → ChainObject → ChainData → Type₀
ChainDataPropertyDenotation noDataProperty x y =
  ⊥*

ChainDatatypeDenotation : ChainDatatype → ChainData → Type₀
ChainDatatypeDenotation noDatatype noDataValue =
  Unit*

ChainFacetDenotation :
  ChainDatatype → ChainFacet → ChainLiteral → ChainData → Type₀
ChainFacetDenotation noDatatype noFacet noLiteral noDataValue =
  Unit*

ChainIndividualDenotation : ChainIndividual → ChainObject
ChainIndividualDenotation Alice =
  aliceObject
ChainIndividualDenotation Bob =
  bobObject
ChainIndividualDenotation Carol =
  carolObject

ChainLiteralDenotation : ChainLiteral → ChainData
ChainLiteralDenotation noLiteral =
  noDataValue

chainInterpretation : Interpretation ChainSignature ℓ-zero ℓ-zero ℓ-zero
chainInterpretation .ObjectDomain =
  ChainObject
chainInterpretation .DataDomain =
  ChainData
chainInterpretation .classDenotation =
  ChainClassDenotation
chainInterpretation .objectPropertyDenotation =
  ChainObjectPropertyDenotation
chainInterpretation .dataPropertyDenotation =
  ChainDataPropertyDenotation
chainInterpretation .datatypeDenotation =
  ChainDatatypeDenotation
chainInterpretation .facetDenotation =
  ChainFacetDenotation
chainInterpretation .individualDenotation =
  ChainIndividualDenotation
chainInterpretation .literalDenotation =
  ChainLiteralDenotation

parentParentImpliesGrandparent :
  SatisfiesAxiom chainInterpretation
    (subObjectPropertyOf ParentParentChain HasGrandparent)
parentParentImpliesGrandparent x z (y , (xy , yz)) =
  grandparentFromParents xy yz

aliceHasParentBob :
  SatisfiesAxiom chainInterpretation
    (objectPropertyAssertion HasParent Alice Bob)
aliceHasParentBob =
  aliceBobParent

bobHasParentCarol :
  SatisfiesAxiom chainInterpretation
    (objectPropertyAssertion HasParent Bob Carol)
bobHasParentCarol =
  bobCarolParent

aliceHasGrandparentCarol :
  SatisfiesAxiom chainInterpretation
    (objectPropertyAssertion HasGrandparent Alice Carol)
aliceHasGrandparentCarol =
  grandparentFromParents aliceBobParent bobCarolParent

aliceHasGrandparentCarolByChain :
  evalObjectProperty chainInterpretation
    HasGrandparent aliceObject carolObject
aliceHasGrandparentCarolByChain =
  objectSubProperty
    {I = chainInterpretation}
    {p = ParentParentChain}
    {q = HasGrandparent}
    {x = aliceObject}
    {y = carolObject}
    parentParentImpliesGrandparent
    (objectPropertyChain₂Intro
      {I = chainInterpretation}
      {p = HasParent}
      {q = HasParent}
      {x = aliceObject}
      {y = bobObject}
      {z = carolObject}
      aliceBobParent
      bobCarolParent)

chainOntologySatisfied :
  SatisfiesOntology chainInterpretation chainOntology
chainOntologySatisfied =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ parentParentImpliesGrandparent
  (Prod._,_ aliceHasParentBob
  (Prod._,_ bobHasParentCarol
  (Prod._,_ aliceHasGrandparentCarol
    (lift tt)))))))