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

module OWL2.Examples.HasKey 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 KeyIRI : Type₀ where
  keyDocument : KeyIRI

data KeyClass : Type₀ where
  Person : KeyClass

data KeyObjectProperty : Type₀ where
  noObjectProperty : KeyObjectProperty

data KeyDataProperty : Type₀ where
  hasSSN : KeyDataProperty

data KeyDatatype : Type₀ where
  stringDatatype : KeyDatatype

data KeyIndividual : Type₀ where
  Alice AliceAlias : KeyIndividual

data KeyLiteral : Type₀ where
  ssn123 : KeyLiteral

data KeyFacet : Type₀ where
  noFacet : KeyFacet

data KeyAnnotationProperty : Type₀ where
  label : KeyAnnotationProperty

KeySignature : Signature ℓ-zero
KeySignature .IRI =
  KeyIRI
KeySignature .ClassName =
  KeyClass
KeySignature .ObjectPropertyName =
  KeyObjectProperty
KeySignature .DataPropertyName =
  KeyDataProperty
KeySignature .DatatypeName =
  KeyDatatype
KeySignature .IndividualName =
  KeyIndividual
KeySignature .Literal =
  KeyLiteral
KeySignature .FacetName =
  KeyFacet
KeySignature .AnnotationPropertyName =
  KeyAnnotationProperty

PersonC : ClassExpression KeySignature
PersonC =
  namedClass Person

HasSSN : DataPropertyExpression KeySignature
HasSSN =
  dataProperty hasSSN

PersonSSNKey : PropertyKey KeySignature
PersonSSNKey =
  propertyKey [] (HasSSN ∷ [])

keyOntology : Ontology KeySignature
keyOntology =
  ontology
    (keyDocument ∷ [])
    []
    ( declaration (classEntity Person)
    ∷ declaration (dataPropertyEntity hasSSN)
    ∷ hasKey PersonC PersonSSNKey
    ∷ classAssertion PersonC Alice
    ∷ classAssertion PersonC AliceAlias
    ∷ dataPropertyAssertion HasSSN Alice ssn123
    ∷ dataPropertyAssertion HasSSN AliceAlias ssn123
    ∷ [] )

data KeyObject : Type₀ where
  aliceObject : KeyObject

data KeyData : Type₀ where
  ssn123Value : KeyData

data IsPerson : KeyObject → Type₀ where
  alicePerson : IsPerson aliceObject

KeyClassDenotation : KeyClass → KeyObject → Type₀
KeyClassDenotation Person =
  IsPerson

KeyObjectPropertyDenotation :
  KeyObjectProperty → KeyObject → KeyObject → Type₀
KeyObjectPropertyDenotation noObjectProperty x y =
  ⊥*

data SSNRel : KeyObject → KeyData → Type₀ where
  aliceSSN123 : SSNRel aliceObject ssn123Value

KeyDataPropertyDenotation :
  KeyDataProperty → KeyObject → KeyData → Type₀
KeyDataPropertyDenotation hasSSN =
  SSNRel

KeyDatatypeDenotation : KeyDatatype → KeyData → Type₀
KeyDatatypeDenotation stringDatatype ssn123Value =
  Unit*

KeyFacetDenotation :
  KeyDatatype → KeyFacet → KeyLiteral → KeyData → Type₀
KeyFacetDenotation stringDatatype noFacet ssn123 ssn123Value =
  Unit*

KeyIndividualDenotation : KeyIndividual → KeyObject
KeyIndividualDenotation Alice =
  aliceObject
KeyIndividualDenotation AliceAlias =
  aliceObject

KeyLiteralDenotation : KeyLiteral → KeyData
KeyLiteralDenotation ssn123 =
  ssn123Value

keyInterpretation : Interpretation KeySignature ℓ-zero ℓ-zero ℓ-zero
keyInterpretation .ObjectDomain =
  KeyObject
keyInterpretation .DataDomain =
  KeyData
keyInterpretation .classDenotation =
  KeyClassDenotation
keyInterpretation .objectPropertyDenotation =
  KeyObjectPropertyDenotation
keyInterpretation .dataPropertyDenotation =
  KeyDataPropertyDenotation
keyInterpretation .datatypeDenotation =
  KeyDatatypeDenotation
keyInterpretation .facetDenotation =
  KeyFacetDenotation
keyInterpretation .individualDenotation =
  KeyIndividualDenotation
keyInterpretation .literalDenotation =
  KeyLiteralDenotation

personSSNKeySatisfied :
  SatisfiesAxiom keyInterpretation (hasKey PersonC PersonSSNKey)
personSSNKeySatisfied Alice Alice alicePerson alicePerson shared =
  lift refl
personSSNKeySatisfied Alice AliceAlias alicePerson alicePerson shared =
  lift refl
personSSNKeySatisfied AliceAlias Alice alicePerson alicePerson shared =
  lift refl
personSSNKeySatisfied AliceAlias AliceAlias alicePerson alicePerson shared =
  lift refl

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

aliceAliasIsPerson :
  SatisfiesAxiom keyInterpretation (classAssertion PersonC AliceAlias)
aliceAliasIsPerson =
  alicePerson

aliceHasSSN123 :
  SatisfiesAxiom keyInterpretation
    (dataPropertyAssertion HasSSN Alice ssn123)
aliceHasSSN123 =
  aliceSSN123

aliceAliasHasSSN123 :
  SatisfiesAxiom keyInterpretation
    (dataPropertyAssertion HasSSN AliceAlias ssn123)
aliceAliasHasSSN123 =
  aliceSSN123

aliceAliasSharedSSN :
  SharedDataPropertyValue keyInterpretation HasSSN aliceObject aliceObject
aliceAliasSharedSSN =
  sharedDataPropertyValueIntro
    {I = keyInterpretation}
    {p = HasSSN}
    {x = aliceObject}
    {y = aliceObject}
    {z = ssn123Value}
    aliceSSN123
    aliceSSN123

aliceAliasSharedKey :
  SharedKey keyInterpretation PersonSSNKey aliceObject aliceObject
aliceAliasSharedKey =
  lift tt ,
  Prod._,_ aliceAliasSharedSSN (lift tt)

aliceAliasSameByKey :
  ObjectEq keyInterpretation
    (individualDenotation keyInterpretation Alice)
    (individualDenotation keyInterpretation AliceAlias)
aliceAliasSameByKey =
  hasKeyApply
    {I = keyInterpretation}
    {c = PersonC}
    {key = PersonSSNKey}
    {a = Alice}
    {b = AliceAlias}
    personSSNKeySatisfied
    aliceIsPerson
    aliceAliasIsPerson
    aliceAliasSharedKey

keyOntologySatisfied :
  SatisfiesOntology keyInterpretation keyOntology
keyOntologySatisfied =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ personSSNKeySatisfied
  (Prod._,_ aliceIsPerson
  (Prod._,_ aliceAliasIsPerson
  (Prod._,_ aliceHasSSN123
  (Prod._,_ aliceAliasHasSSN123
    (lift tt)))))))