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

module OWL2.Examples.Family where

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

data FamilyIRI : Type₀ where
  familyDocument : FamilyIRI

data FamilyClass : Type₀ where
  Person Woman Man : FamilyClass

data FamilyObjectProperty : Type₀ where
  hasWife hasSpouse hasParent : FamilyObjectProperty

data FamilyDataProperty : Type₀ where
  age : FamilyDataProperty

data FamilyDatatype : Type₀ where
  integer : FamilyDatatype

data FamilyIndividual : Type₀ where
  John Mary Bill : FamilyIndividual

data FamilyLiteral : Type₀ where
  fortyTwo : FamilyLiteral

data FamilyFacet : Type₀ where
  noFacet : FamilyFacet

data FamilyAnnotationProperty : Type₀ where
  label : FamilyAnnotationProperty

FamilySignature : Signature ℓ-zero
FamilySignature .IRI =
  FamilyIRI
FamilySignature .ClassName =
  FamilyClass
FamilySignature .ObjectPropertyName =
  FamilyObjectProperty
FamilySignature .DataPropertyName =
  FamilyDataProperty
FamilySignature .DatatypeName =
  FamilyDatatype
FamilySignature .IndividualName =
  FamilyIndividual
FamilySignature .Literal =
  FamilyLiteral
FamilySignature .FacetName =
  FamilyFacet
FamilySignature .AnnotationPropertyName =
  FamilyAnnotationProperty

PersonC WomanC ManC : ClassExpression FamilySignature
PersonC =
  namedClass Person
WomanC =
  namedClass Woman
ManC =
  namedClass Man

HasWife HasSpouse HasParent : ObjectPropertyExpression FamilySignature
HasWife =
  objectProperty hasWife
HasSpouse =
  objectProperty hasSpouse
HasParent =
  objectProperty hasParent

Age : DataPropertyExpression FamilySignature
Age =
  dataProperty age

IntegerRange : DataRange FamilySignature
IntegerRange =
  datatype integer

familyOntology : Ontology FamilySignature
familyOntology =
  ontology
    (familyDocument ∷ [])
    []
    ( declaration (classEntity Person)
    ∷ declaration (classEntity Woman)
    ∷ declaration (objectPropertyEntity hasWife)
    ∷ subClassOf WomanC PersonC
    ∷ subClassOf ManC PersonC
    ∷ objectPropertyDomain HasWife ManC
    ∷ objectPropertyRange HasWife WomanC
    ∷ subObjectPropertyOf (subObjectProperty HasWife) HasSpouse
    ∷ classAssertion ManC John
    ∷ classAssertion WomanC Mary
    ∷ objectPropertyAssertion HasWife John Mary
    ∷ negativeObjectPropertyAssertion HasWife Bill Mary
    ∷ dataPropertyRange Age IntegerRange
    ∷ dataPropertyAssertion Age John fortyTwo
    ∷ [] )

data FamilyObject : Type₀ where
  johnObject maryObject billObject : FamilyObject

data FamilyData : Type₀ where
  number42 : FamilyData

data IsPerson : FamilyObject → Type₀ where
  johnPerson : IsPerson johnObject
  maryPerson : IsPerson maryObject
  billPerson : IsPerson billObject

data IsWoman : FamilyObject → Type₀ where
  maryWoman : IsWoman maryObject

data IsMan : FamilyObject → Type₀ where
  johnMan : IsMan johnObject

FamilyClassDenotation : FamilyClass → FamilyObject → Type₀
FamilyClassDenotation Person =
  IsPerson
FamilyClassDenotation Woman =
  IsWoman
FamilyClassDenotation Man =
  IsMan

data WifeRel : FamilyObject → FamilyObject → Type₀ where
  johnMaryWife : WifeRel johnObject maryObject

data SpouseRel : FamilyObject → FamilyObject → Type₀ where
  spouseFromWife :
    ∀ {x y} → WifeRel x y → SpouseRel x y

data ParentRel : FamilyObject → FamilyObject → Type₀ where

FamilyObjectPropertyDenotation :
  FamilyObjectProperty → FamilyObject → FamilyObject → Type₀
FamilyObjectPropertyDenotation hasWife =
  WifeRel
FamilyObjectPropertyDenotation hasSpouse =
  SpouseRel
FamilyObjectPropertyDenotation hasParent =
  ParentRel

data AgeRel : FamilyObject → FamilyData → Type₀ where
  johnAge42 : AgeRel johnObject number42

FamilyDataPropertyDenotation :
  FamilyDataProperty → FamilyObject → FamilyData → Type₀
FamilyDataPropertyDenotation age =
  AgeRel

FamilyDatatypeDenotation : FamilyDatatype → FamilyData → Type₀
FamilyDatatypeDenotation integer number42 =
  Unit

FamilyFacetDenotation :
  FamilyDatatype → FamilyFacet → FamilyLiteral → FamilyData → Type₀
FamilyFacetDenotation integer noFacet fortyTwo number42 =
  Unit*

FamilyIndividualDenotation : FamilyIndividual → FamilyObject
FamilyIndividualDenotation John =
  johnObject
FamilyIndividualDenotation Mary =
  maryObject
FamilyIndividualDenotation Bill =
  billObject

FamilyLiteralDenotation : FamilyLiteral → FamilyData
FamilyLiteralDenotation fortyTwo =
  number42

familyInterpretation : Interpretation FamilySignature ℓ-zero ℓ-zero ℓ-zero
familyInterpretation .ObjectDomain =
  FamilyObject
familyInterpretation .DataDomain =
  FamilyData
familyInterpretation .classDenotation =
  FamilyClassDenotation
familyInterpretation .objectPropertyDenotation =
  FamilyObjectPropertyDenotation
familyInterpretation .dataPropertyDenotation =
  FamilyDataPropertyDenotation
familyInterpretation .datatypeDenotation =
  FamilyDatatypeDenotation
familyInterpretation .facetDenotation =
  FamilyFacetDenotation
familyInterpretation .individualDenotation =
  FamilyIndividualDenotation
familyInterpretation .literalDenotation =
  FamilyLiteralDenotation

wifeImpliesSpouse :
  SatisfiesAxiom familyInterpretation
    (subObjectPropertyOf (subObjectProperty HasWife) HasSpouse)
wifeImpliesSpouse x y wife =
  spouseFromWife wife

womanSubPerson :
  SatisfiesAxiom familyInterpretation
    (subClassOf WomanC PersonC)
womanSubPerson maryObject maryWoman =
  maryPerson

manSubPerson :
  SatisfiesAxiom familyInterpretation
    (subClassOf ManC PersonC)
manSubPerson johnObject johnMan =
  johnPerson

hasWifeDomain :
  SatisfiesAxiom familyInterpretation
    (objectPropertyDomain HasWife ManC)
hasWifeDomain johnObject maryObject johnMaryWife =
  johnMan

hasWifeRange :
  SatisfiesAxiom familyInterpretation
    (objectPropertyRange HasWife WomanC)
hasWifeRange johnObject maryObject johnMaryWife =
  maryWoman

billDoesNotHaveWifeMary :
  SatisfiesAxiom familyInterpretation
    (negativeObjectPropertyAssertion HasWife Bill Mary)
billDoesNotHaveWifeMary ()

ageRangeInteger :
  SatisfiesAxiom familyInterpretation
    (dataPropertyRange Age IntegerRange)
ageRangeInteger johnObject number42 johnAge42 =
  tt

johnHasWifeMary :
  SatisfiesAxiom familyInterpretation
    (objectPropertyAssertion HasWife John Mary)
johnHasWifeMary =
  johnMaryWife

johnIsPersonByMan :
  evalClass familyInterpretation PersonC johnObject
johnIsPersonByMan =
  johnPerson

johnIsSomebodyWithAWife :
  evalClass familyInterpretation
    (objectSomeValuesFrom HasWife WomanC)
    johnObject
johnIsSomebodyWithAWife =
  maryObject , (johnMaryWife , maryWoman)

familyOntologySatisfied :
  SatisfiesOntology familyInterpretation familyOntology
familyOntologySatisfied =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ womanSubPerson
  (Prod._,_ manSubPerson
  (Prod._,_ hasWifeDomain
  (Prod._,_ hasWifeRange
  (Prod._,_ wifeImpliesSpouse
  (Prod._,_ johnMan
  (Prod._,_ maryWoman
  (Prod._,_ johnMaryWife
  (Prod._,_ billDoesNotHaveWifeMary
  (Prod._,_ ageRangeInteger
  (Prod._,_ johnAge42
    (lift tt))))))))))))))