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

module OWL2.Examples.Cardinality where

open import OWL2.Prelude
import Cubical.Data.Prod.Base as Prod
import OWL2.Portable.Syntax as P
import OWL2.Portable.Semantics as PS
open import OWL2.Syntax
open import OWL2.DirectSemantics
open import OWL2.DirectSemantics.Lemmas

data CardinalityIRI : Type₀ where
  cardinalityDocument : CardinalityIRI

data CardinalityClass : Type₀ where
  Person : CardinalityClass

data CardinalityObjectProperty : Type₀ where
  hasSpouse : CardinalityObjectProperty

data CardinalityDataProperty : Type₀ where
  hasAge : CardinalityDataProperty

data CardinalityDatatype : Type₀ where
  integerDatatype : CardinalityDatatype

data CardinalityIndividual : Type₀ where
  Alice Bob : CardinalityIndividual

data CardinalityLiteral : Type₀ where
  age42 : CardinalityLiteral

data CardinalityFacet : Type₀ where
  noFacet : CardinalityFacet

data CardinalityAnnotationProperty : Type₀ where
  label : CardinalityAnnotationProperty

CardinalitySignature : Signature ℓ-zero
CardinalitySignature .IRI =
  CardinalityIRI
CardinalitySignature .ClassName =
  CardinalityClass
CardinalitySignature .ObjectPropertyName =
  CardinalityObjectProperty
CardinalitySignature .DataPropertyName =
  CardinalityDataProperty
CardinalitySignature .DatatypeName =
  CardinalityDatatype
CardinalitySignature .IndividualName =
  CardinalityIndividual
CardinalitySignature .Literal =
  CardinalityLiteral
CardinalitySignature .FacetName =
  CardinalityFacet
CardinalitySignature .AnnotationPropertyName =
  CardinalityAnnotationProperty

PersonC : ClassExpression CardinalitySignature
PersonC =
  namedClass Person

HasSpouse : ObjectPropertyExpression CardinalitySignature
HasSpouse =
  objectProperty hasSpouse

HasAge : DataPropertyExpression CardinalitySignature
HasAge =
  dataProperty hasAge

IntegerRange : DataRange CardinalitySignature
IntegerRange =
  datatype integerDatatype

ExactlyOneSpouse : ClassExpression CardinalitySignature
ExactlyOneSpouse =
  objectExactCardinality 1 HasSpouse (present PersonC)

ExactlyOneAge : ClassExpression CardinalitySignature
ExactlyOneAge =
  dataExactCardinality 1 HasAge (present IntegerRange)

cardinalityOntology : Ontology CardinalitySignature
cardinalityOntology =
  ontology
    (cardinalityDocument ∷ [])
    []
    ( declaration (classEntity Person)
    ∷ declaration (objectPropertyEntity hasSpouse)
    ∷ declaration (dataPropertyEntity hasAge)
    ∷ declaration (datatypeEntity integerDatatype)
    ∷ classAssertion PersonC Alice
    ∷ classAssertion PersonC Bob
    ∷ objectPropertyAssertion HasSpouse Alice Bob
    ∷ classAssertion ExactlyOneSpouse Alice
    ∷ dataPropertyAssertion HasAge Alice age42
    ∷ classAssertion ExactlyOneAge Alice
    ∷ [] )

data CardinalityObject : Type₀ where
  aliceObject bobObject : CardinalityObject

data CardinalityData : Type₀ where
  age42Value : CardinalityData

data IsPerson : CardinalityObject → Type₀ where
  alicePerson : IsPerson aliceObject
  bobPerson : IsPerson bobObject

CardinalityClassDenotation :
  CardinalityClass → CardinalityObject → Type₀
CardinalityClassDenotation Person =
  IsPerson

data SpouseRel : CardinalityObject → CardinalityObject → Type₀ where
  aliceBobSpouse : SpouseRel aliceObject bobObject

CardinalityObjectPropertyDenotation :
  CardinalityObjectProperty →
  CardinalityObject → CardinalityObject → Type₀
CardinalityObjectPropertyDenotation hasSpouse =
  SpouseRel

data AgeRel : CardinalityObject → CardinalityData → Type₀ where
  aliceAge42 : AgeRel aliceObject age42Value

CardinalityDataPropertyDenotation :
  CardinalityDataProperty →
  CardinalityObject → CardinalityData → Type₀
CardinalityDataPropertyDenotation hasAge =
  AgeRel

CardinalityDatatypeDenotation :
  CardinalityDatatype → CardinalityData → Type₀
CardinalityDatatypeDenotation integerDatatype age42Value =
  Unit*

CardinalityFacetDenotation :
  CardinalityDatatype → CardinalityFacet → CardinalityLiteral →
  CardinalityData → Type₀
CardinalityFacetDenotation integerDatatype noFacet age42 age42Value =
  Unit*

CardinalityIndividualDenotation :
  CardinalityIndividual → CardinalityObject
CardinalityIndividualDenotation Alice =
  aliceObject
CardinalityIndividualDenotation Bob =
  bobObject

CardinalityLiteralDenotation :
  CardinalityLiteral → CardinalityData
CardinalityLiteralDenotation age42 =
  age42Value

cardinalityInterpretation :
  Interpretation CardinalitySignature ℓ-zero ℓ-zero ℓ-zero
cardinalityInterpretation .ObjectDomain =
  CardinalityObject
cardinalityInterpretation .DataDomain =
  CardinalityData
cardinalityInterpretation .classDenotation =
  CardinalityClassDenotation
cardinalityInterpretation .objectPropertyDenotation =
  CardinalityObjectPropertyDenotation
cardinalityInterpretation .dataPropertyDenotation =
  CardinalityDataPropertyDenotation
cardinalityInterpretation .datatypeDenotation =
  CardinalityDatatypeDenotation
cardinalityInterpretation .facetDenotation =
  CardinalityFacetDenotation
cardinalityInterpretation .individualDenotation =
  CardinalityIndividualDenotation
cardinalityInterpretation .literalDenotation =
  CardinalityLiteralDenotation

aliceIsPerson :
  SatisfiesAxiom cardinalityInterpretation
    (classAssertion PersonC Alice)
aliceIsPerson =
  alicePerson

bobIsPerson :
  SatisfiesAxiom cardinalityInterpretation
    (classAssertion PersonC Bob)
bobIsPerson =
  bobPerson

aliceHasSpouseBob :
  SatisfiesAxiom cardinalityInterpretation
    (objectPropertyAssertion HasSpouse Alice Bob)
aliceHasSpouseBob =
  aliceBobSpouse

aliceBobSpouseFiller :
  ObjectCardinalityFiller
    cardinalityInterpretation
    HasSpouse
    (present PersonC)
    aliceObject
    bobObject
aliceBobSpouseFiller =
  aliceBobSpouse , bobPerson

spouseUniqueForAlice :
  ∀ y z →
  ObjectCardinalityFiller
    cardinalityInterpretation HasSpouse (present PersonC) aliceObject y →
  ObjectCardinalityFiller
    cardinalityInterpretation HasSpouse (present PersonC) aliceObject z →
  ObjectEq cardinalityInterpretation y z
spouseUniqueForAlice .bobObject .bobObject
  (aliceBobSpouse , bobPerson)
  (aliceBobSpouse , bobPerson) =
  lift refl

aliceHasExactlyOneSpouse :
  SatisfiesAxiom cardinalityInterpretation
    (classAssertion ExactlyOneSpouse Alice)
aliceHasExactlyOneSpouse =
  objectCardinalityExactOneIntro
    {I = cardinalityInterpretation}
    {p = HasSpouse}
    {c = present PersonC}
    {x = aliceObject}
    {y = bobObject}
    aliceBobSpouseFiller
    spouseUniqueForAlice

aliceHasAge42 :
  SatisfiesAxiom cardinalityInterpretation
    (dataPropertyAssertion HasAge Alice age42)
aliceHasAge42 =
  aliceAge42

aliceAge42Filler :
  DataCardinalityFiller
    cardinalityInterpretation
    HasAge
    (present IntegerRange)
    aliceObject
    age42Value
aliceAge42Filler =
  aliceAge42 , lift tt

ageUniqueForAlice :
  ∀ y z →
  DataCardinalityFiller
    cardinalityInterpretation HasAge (present IntegerRange) aliceObject y →
  DataCardinalityFiller
    cardinalityInterpretation HasAge (present IntegerRange) aliceObject z →
  DataEq cardinalityInterpretation y z
ageUniqueForAlice .age42Value .age42Value
  (aliceAge42 , _)
  (aliceAge42 , _) =
  lift refl

aliceHasExactlyOneAge :
  SatisfiesAxiom cardinalityInterpretation
    (classAssertion ExactlyOneAge Alice)
aliceHasExactlyOneAge =
  dataCardinalityExactOneIntro
    {I = cardinalityInterpretation}
    {p = HasAge}
    {d = present IntegerRange}
    {x = aliceObject}
    {y = age42Value}
    aliceAge42Filler
    ageUniqueForAlice

cardinalityOntologySatisfied :
  SatisfiesOntology cardinalityInterpretation cardinalityOntology
cardinalityOntologySatisfied =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ aliceIsPerson
  (Prod._,_ bobIsPerson
  (Prod._,_ aliceHasSpouseBob
  (Prod._,_ aliceHasExactlyOneSpouse
  (Prod._,_ aliceHasAge42
  (Prod._,_ aliceHasExactlyOneAge
    (lift tt))))))))))

portablePersonIRI portableHasSpouseIRI portableHasAgeIRI portableIntegerIRI :
  P.IRI
portablePersonIRI =
  P.iri "urn:ff-owl:example:Person"
portableHasSpouseIRI =
  P.iri "urn:ff-owl:example:hasSpouse"
portableHasAgeIRI =
  P.iri "urn:ff-owl:example:hasAge"
portableIntegerIRI =
  P.iri "http://www.w3.org/2001/XMLSchema#integer"

portablePerson portableHasSpouse portableHasAge portableInteger : P.Name
portablePerson =
  P.named portablePersonIRI
portableHasSpouse =
  P.named portableHasSpouseIRI
portableHasAge =
  P.named portableHasAgeIRI
portableInteger =
  P.named portableIntegerIRI

portableObjectExactCardinality : P.ClassExpression
portableObjectExactCardinality =
  P.objectExactCardinality
    1
    (P.objectProperty portableHasSpouse)
    (present (P.namedClass portablePerson))

portableDataExactCardinality : P.ClassExpression
portableDataExactCardinality =
  P.dataExactCardinality
    1
    (P.dataProperty portableHasAge)
    (present (P.datatype portableInteger))

translatedPortableObjectExactCardinality :
  PS.translateClassExpression portableObjectExactCardinality ≡
  present
    (objectExactCardinality
      1
      (objectProperty portableHasSpouse)
      (present (namedClass portablePerson)))
translatedPortableObjectExactCardinality =
  refl

translatedPortableDataExactCardinality :
  PS.translateClassExpression portableDataExactCardinality ≡
  present
    (dataExactCardinality
      1
      (dataProperty portableHasAge)
      (present (datatype portableInteger)))
translatedPortableDataExactCardinality =
  refl