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

module OWL2.Examples.FacetRestriction 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

data FacetIRI : Type₀ where
  facetDocument : FacetIRI

data FacetClass : Type₀ where
  Adult : FacetClass

data FacetObjectProperty : Type₀ where
  noObjectProperty : FacetObjectProperty

data FacetDataProperty : Type₀ where
  hasAge : FacetDataProperty

data FacetDatatype : Type₀ where
  integerDatatype : FacetDatatype

data FacetIndividual : Type₀ where
  Alice : FacetIndividual

data FacetLiteral : Type₀ where
  tenLiteral fortyTwoLiteral sevenLiteral : FacetLiteral

data AgeFacet : Type₀ where
  minInclusive : AgeFacet

data FacetAnnotationProperty : Type₀ where
  label : FacetAnnotationProperty

FacetSignature : Signature ℓ-zero
FacetSignature .IRI =
  FacetIRI
FacetSignature .ClassName =
  FacetClass
FacetSignature .ObjectPropertyName =
  FacetObjectProperty
FacetSignature .DataPropertyName =
  FacetDataProperty
FacetSignature .DatatypeName =
  FacetDatatype
FacetSignature .IndividualName =
  FacetIndividual
FacetSignature .Literal =
  FacetLiteral
FacetSignature .FacetName =
  AgeFacet
FacetSignature .AnnotationPropertyName =
  FacetAnnotationProperty

AdultC : ClassExpression FacetSignature
AdultC =
  namedClass Adult

HasAge : DataPropertyExpression FacetSignature
HasAge =
  dataProperty hasAge

AtLeastTenRange : DataRange FacetSignature
AtLeastTenRange =
  datatypeRestriction
    integerDatatype
    (facetRestriction minInclusive tenLiteral ∷ [])

AdultByAge : ClassExpression FacetSignature
AdultByAge =
  dataSomeValuesFrom HasAge AtLeastTenRange

facetOntology : Ontology FacetSignature
facetOntology =
  ontology
    (facetDocument ∷ [])
    []
    ( declaration (classEntity Adult)
    ∷ declaration (dataPropertyEntity hasAge)
    ∷ declaration (datatypeEntity integerDatatype)
    ∷ dataPropertyRange HasAge AtLeastTenRange
    ∷ dataPropertyAssertion HasAge Alice fortyTwoLiteral
    ∷ classAssertion AdultByAge Alice
    ∷ [] )

data FacetObject : Type₀ where
  aliceObject : FacetObject

data FacetData : Type₀ where
  age42Value age7Value : FacetData

FacetClassDenotation : FacetClass → FacetObject → Type₀
FacetClassDenotation Adult aliceObject =
  Unit*

FacetObjectPropertyDenotation :
  FacetObjectProperty → FacetObject → FacetObject → Type₀
FacetObjectPropertyDenotation noObjectProperty x y =
  ⊥*

data AgeRel : FacetObject → FacetData → Type₀ where
  aliceAge42 : AgeRel aliceObject age42Value

FacetDataPropertyDenotation :
  FacetDataProperty → FacetObject → FacetData → Type₀
FacetDataPropertyDenotation hasAge =
  AgeRel

FacetDatatypeDenotation : FacetDatatype → FacetData → Type₀
FacetDatatypeDenotation integerDatatype age42Value =
  Unit*
FacetDatatypeDenotation integerDatatype age7Value =
  Unit*

FacetFacetDenotation :
  FacetDatatype → AgeFacet → FacetLiteral → FacetData → Type₀
FacetFacetDenotation integerDatatype minInclusive tenLiteral age42Value =
  Unit*
FacetFacetDenotation integerDatatype minInclusive tenLiteral age7Value =
  ⊥*
FacetFacetDenotation integerDatatype minInclusive fortyTwoLiteral value =
  Unit*
FacetFacetDenotation integerDatatype minInclusive sevenLiteral value =
  Unit*

FacetIndividualDenotation : FacetIndividual → FacetObject
FacetIndividualDenotation Alice =
  aliceObject

FacetLiteralDenotation : FacetLiteral → FacetData
FacetLiteralDenotation tenLiteral =
  age7Value
FacetLiteralDenotation fortyTwoLiteral =
  age42Value
FacetLiteralDenotation sevenLiteral =
  age7Value

facetInterpretation : Interpretation FacetSignature ℓ-zero ℓ-zero ℓ-zero
facetInterpretation .ObjectDomain =
  FacetObject
facetInterpretation .DataDomain =
  FacetData
facetInterpretation .classDenotation =
  FacetClassDenotation
facetInterpretation .objectPropertyDenotation =
  FacetObjectPropertyDenotation
facetInterpretation .dataPropertyDenotation =
  FacetDataPropertyDenotation
facetInterpretation .datatypeDenotation =
  FacetDatatypeDenotation
facetInterpretation .facetDenotation =
  FacetFacetDenotation
facetInterpretation .individualDenotation =
  FacetIndividualDenotation
facetInterpretation .literalDenotation =
  FacetLiteralDenotation

age42InAtLeastTenRange :
  evalDataRange facetInterpretation AtLeastTenRange age42Value
age42InAtLeastTenRange =
  lift tt , (lift tt , lift tt)

age7NotInAtLeastTenRange :
  ¬ evalDataRange facetInterpretation AtLeastTenRange age7Value
age7NotInAtLeastTenRange (_ , (() , _))

hasAgeRangeAtLeastTen :
  SatisfiesAxiom facetInterpretation
    (dataPropertyRange HasAge AtLeastTenRange)
hasAgeRangeAtLeastTen aliceObject age42Value aliceAge42 =
  age42InAtLeastTenRange

aliceHasAge42 :
  SatisfiesAxiom facetInterpretation
    (dataPropertyAssertion HasAge Alice fortyTwoLiteral)
aliceHasAge42 =
  aliceAge42

aliceAdultByAge :
  SatisfiesAxiom facetInterpretation
    (classAssertion AdultByAge Alice)
aliceAdultByAge =
  age42Value , (aliceAge42 , age42InAtLeastTenRange)

facetOntologySatisfied :
  SatisfiesOntology facetInterpretation facetOntology
facetOntologySatisfied =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ hasAgeRangeAtLeastTen
  (Prod._,_ aliceHasAge42
  (Prod._,_ aliceAdultByAge
    (lift tt))))))

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

portableHasAge portableInteger : P.Name
portableHasAge =
  P.named portableHasAgeIRI
portableInteger =
  P.named portableIntegerIRI

portableTen : P.Literal
portableTen =
  P.typedLiteral "10" portableInteger

portableDatatypeRestriction : P.DataRange
portableDatatypeRestriction =
  P.datatypeRestriction
    portableInteger
    (P.facetRestriction portableMinInclusiveIRI portableTen ∷ [])

translatedPortableDatatypeRestriction :
  PS.translateDataRange portableDatatypeRestriction ≡
  present
    (datatypeRestriction
      portableInteger
      (facetRestriction portableMinInclusiveIRI portableTen ∷ []))
translatedPortableDatatypeRestriction =
  refl

portableFacetSomeValues : P.ClassExpression
portableFacetSomeValues =
  P.dataSomeValuesFrom
    (P.dataProperty portableHasAge)
    portableDatatypeRestriction

translatedPortableFacetSomeValues :
  PS.translateClassExpression portableFacetSomeValues ≡
  present
    (dataSomeValuesFrom
      (dataProperty portableHasAge)
      (datatypeRestriction
        portableInteger
        (facetRestriction portableMinInclusiveIRI portableTen ∷ [])))
translatedPortableFacetSomeValues =
  refl