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

module OWL2.Examples.WebProtege.Constructors where

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

import OWL2.Examples.Cardinality
import OWL2.Examples.Family
import OWL2.Examples.HasKey
import OWL2.Examples.PropertyChain

data ConstructorIRI : Type₀ where
  constructorDocument : ConstructorIRI

data ConstructorClass : Type₀ where
  Dataset TextDataset ImageDataset : ConstructorClass

data ConstructorObjectProperty : Type₀ where
  hasPart partOf : ConstructorObjectProperty

data ConstructorDataProperty : Type₀ where
  noDataProperty : ConstructorDataProperty

data ConstructorDatatype : Type₀ where
  noDatatype : ConstructorDatatype

data ConstructorIndividual : Type₀ where
  textDatasetIndividual imageDatasetIndividual : ConstructorIndividual

data ConstructorLiteral : Type₀ where
  noLiteral : ConstructorLiteral

data ConstructorFacet : Type₀ where
  noFacet : ConstructorFacet

data ConstructorAnnotationProperty : Type₀ where
  label : ConstructorAnnotationProperty

ConstructorSignature : Signature ℓ-zero
ConstructorSignature .IRI =
  ConstructorIRI
ConstructorSignature .ClassName =
  ConstructorClass
ConstructorSignature .ObjectPropertyName =
  ConstructorObjectProperty
ConstructorSignature .DataPropertyName =
  ConstructorDataProperty
ConstructorSignature .DatatypeName =
  ConstructorDatatype
ConstructorSignature .IndividualName =
  ConstructorIndividual
ConstructorSignature .Literal =
  ConstructorLiteral
ConstructorSignature .FacetName =
  ConstructorFacet
ConstructorSignature .AnnotationPropertyName =
  ConstructorAnnotationProperty

DatasetC TextDatasetC ImageDatasetC :
  ClassExpression ConstructorSignature
DatasetC =
  namedClass Dataset
TextDatasetC =
  namedClass TextDataset
ImageDatasetC =
  namedClass ImageDataset

HasPart PartOf : ObjectPropertyExpression ConstructorSignature
HasPart =
  objectProperty hasPart
PartOf =
  objectProperty partOf

constructorOntology : Ontology ConstructorSignature
constructorOntology =
  ontology
    (constructorDocument ∷ [])
    []
    ( declaration (classEntity Dataset)
    ∷ declaration (classEntity TextDataset)
    ∷ declaration (classEntity ImageDataset)
    ∷ declaration (objectPropertyEntity hasPart)
    ∷ declaration (objectPropertyEntity partOf)
    ∷ disjointUnionExpansion Dataset TextDatasetC ImageDatasetC []
    ++ ( inverseObjectPropertiesExpansion HasPart PartOf
       ∷ classAssertion TextDatasetC textDatasetIndividual
       ∷ classAssertion ImageDatasetC imageDatasetIndividual
       ∷ objectPropertyAssertion HasPart
           textDatasetIndividual imageDatasetIndividual
       ∷ objectPropertyAssertion PartOf
           imageDatasetIndividual textDatasetIndividual
       ∷ [] ) )

data ConstructorObject : Type₀ where
  textDatasetObject imageDatasetObject : ConstructorObject

data ConstructorData : Type₀ where
  noDataValue : ConstructorData

data IsDataset : ConstructorObject → Type₀ where
  textDatasetIsDataset : IsDataset textDatasetObject
  imageDatasetIsDataset : IsDataset imageDatasetObject

data IsTextDataset : ConstructorObject → Type₀ where
  textDatasetIsTextDataset : IsTextDataset textDatasetObject

data IsImageDataset : ConstructorObject → Type₀ where
  imageDatasetIsImageDataset : IsImageDataset imageDatasetObject

ConstructorClassDenotation :
  ConstructorClass → ConstructorObject → Type₀
ConstructorClassDenotation Dataset =
  IsDataset
ConstructorClassDenotation TextDataset =
  IsTextDataset
ConstructorClassDenotation ImageDataset =
  IsImageDataset

data HasPartRel : ConstructorObject → ConstructorObject → Type₀ where
  textHasImagePart :
    HasPartRel textDatasetObject imageDatasetObject

data PartOfRel : ConstructorObject → ConstructorObject → Type₀ where
  imagePartOfText :
    PartOfRel imageDatasetObject textDatasetObject

ConstructorObjectPropertyDenotation :
  ConstructorObjectProperty →
  ConstructorObject → ConstructorObject → Type₀
ConstructorObjectPropertyDenotation hasPart =
  HasPartRel
ConstructorObjectPropertyDenotation partOf =
  PartOfRel

ConstructorDataPropertyDenotation :
  ConstructorDataProperty → ConstructorObject → ConstructorData → Type₀
ConstructorDataPropertyDenotation noDataProperty x y =
  ⊥*

ConstructorDatatypeDenotation :
  ConstructorDatatype → ConstructorData → Type₀
ConstructorDatatypeDenotation noDatatype noDataValue =
  Unit*

ConstructorFacetDenotation :
  ConstructorDatatype → ConstructorFacet → ConstructorLiteral →
  ConstructorData → Type₀
ConstructorFacetDenotation noDatatype noFacet noLiteral noDataValue =
  Unit*

ConstructorIndividualDenotation :
  ConstructorIndividual → ConstructorObject
ConstructorIndividualDenotation textDatasetIndividual =
  textDatasetObject
ConstructorIndividualDenotation imageDatasetIndividual =
  imageDatasetObject

ConstructorLiteralDenotation : ConstructorLiteral → ConstructorData
ConstructorLiteralDenotation noLiteral =
  noDataValue

constructorInterpretation :
  Interpretation ConstructorSignature ℓ-zero ℓ-zero ℓ-zero
constructorInterpretation .ObjectDomain =
  ConstructorObject
constructorInterpretation .DataDomain =
  ConstructorData
constructorInterpretation .classDenotation =
  ConstructorClassDenotation
constructorInterpretation .objectPropertyDenotation =
  ConstructorObjectPropertyDenotation
constructorInterpretation .dataPropertyDenotation =
  ConstructorDataPropertyDenotation
constructorInterpretation .datatypeDenotation =
  ConstructorDatatypeDenotation
constructorInterpretation .facetDenotation =
  ConstructorFacetDenotation
constructorInterpretation .individualDenotation =
  ConstructorIndividualDenotation
constructorInterpretation .literalDenotation =
  ConstructorLiteralDenotation

datasetIsTextOrImage :
  SatisfiesAxiom constructorInterpretation
    (subClassOf
      DatasetC
      (disjointUnionClassExpression
        Dataset TextDatasetC ImageDatasetC []))
datasetIsTextOrImage textDatasetObject textDatasetIsDataset =
  inl textDatasetIsTextDataset
datasetIsTextOrImage imageDatasetObject imageDatasetIsDataset =
  inr (inl imageDatasetIsImageDataset)

textOrImageIsDataset :
  SatisfiesAxiom constructorInterpretation
    (subClassOf
      (disjointUnionClassExpression
        Dataset TextDatasetC ImageDatasetC [])
      DatasetC)
textOrImageIsDataset .textDatasetObject (inl textDatasetIsTextDataset) =
  textDatasetIsDataset
textOrImageIsDataset .imageDatasetObject (inr (inl imageDatasetIsImageDataset)) =
  imageDatasetIsDataset
textOrImageIsDataset x (inr (inr ()))

datasetEquivalentToDisjointUnion :
  SatisfiesAxiom constructorInterpretation
    (disjointUnionEquivalentAxiom Dataset TextDatasetC ImageDatasetC [])
datasetEquivalentToDisjointUnion =
  equivalentClasses₂Intro
    {I = constructorInterpretation}
    {c = DatasetC}
    {d = disjointUnionClassExpression
      Dataset TextDatasetC ImageDatasetC []}
    datasetIsTextOrImage
    textOrImageIsDataset

textDisjointImage :
  Disjoint
    (evalClass constructorInterpretation TextDatasetC)
    (evalClass constructorInterpretation ImageDatasetC)
textDisjointImage textDatasetObject textDatasetIsTextDataset ()

textAndImageDisjoint :
  SatisfiesAxiom constructorInterpretation
    (disjointUnionDisjointAxiom TextDatasetC ImageDatasetC [])
textAndImageDisjoint =
  Prod._,_
    textDisjointImage
    (lift tt) ,
  (lift tt , lift tt)

disjointUnionExpansionSatisfied :
  AllList
    (disjointUnionExpansion Dataset TextDatasetC ImageDatasetC [])
    (SatisfiesAxiom constructorInterpretation)
disjointUnionExpansionSatisfied =
  Prod._,_
    datasetEquivalentToDisjointUnion
    (Prod._,_ textAndImageDisjoint (lift tt))

textHasPartImpliesImagePartOfText :
  evalObjectProperty constructorInterpretation
    HasPart textDatasetObject imageDatasetObject →
  evalObjectProperty constructorInterpretation
    (objectInverseOf PartOf) textDatasetObject imageDatasetObject
textHasPartImpliesImagePartOfText textHasImagePart =
  imagePartOfText

imagePartOfTextImpliesTextHasPart :
  evalObjectProperty constructorInterpretation
    (objectInverseOf PartOf) textDatasetObject imageDatasetObject →
  evalObjectProperty constructorInterpretation
    HasPart textDatasetObject imageDatasetObject
imagePartOfTextImpliesTextHasPart imagePartOfText =
  textHasImagePart

hasPartSameAsInversePartOf :
  SameExtension
    (λ xy →
      evalObjectProperty constructorInterpretation
        HasPart (fst xy) (snd xy))
    (λ xy →
      evalObjectProperty constructorInterpretation
        (objectInverseOf PartOf) (fst xy) (snd xy))
hasPartSameAsInversePartOf =
  (λ where
    (textDatasetObject , imageDatasetObject) textHasImagePart →
      imagePartOfText) ,
  (λ where
    (textDatasetObject , imageDatasetObject) imagePartOfText →
      textHasImagePart)

inverseObjectPropertiesSatisfied :
  SatisfiesAxiom constructorInterpretation
    (inverseObjectPropertiesExpansion HasPart PartOf)
inverseObjectPropertiesSatisfied =
  Prod._,_
    hasPartSameAsInversePartOf
    (lift tt) ,
  (lift tt , lift tt)

imagePartOfTextByInverseExpansion :
  evalObjectProperty constructorInterpretation
    PartOf imageDatasetObject textDatasetObject
imagePartOfTextByInverseExpansion =
  inverseObjectPropertiesForward
    {I = constructorInterpretation}
    {p = HasPart}
    {q = PartOf}
    {x = textDatasetObject}
    {y = imageDatasetObject}
    inverseObjectPropertiesSatisfied
    textHasImagePart

textHasImagePartByInverseExpansion :
  evalObjectProperty constructorInterpretation
    HasPart textDatasetObject imageDatasetObject
textHasImagePartByInverseExpansion =
  inverseObjectPropertiesBackward
    {I = constructorInterpretation}
    {p = HasPart}
    {q = PartOf}
    {x = textDatasetObject}
    {y = imageDatasetObject}
    inverseObjectPropertiesSatisfied
    imagePartOfText

textDatasetIsText :
  SatisfiesAxiom constructorInterpretation
    (classAssertion TextDatasetC textDatasetIndividual)
textDatasetIsText =
  textDatasetIsTextDataset

imageDatasetIsImage :
  SatisfiesAxiom constructorInterpretation
    (classAssertion ImageDatasetC imageDatasetIndividual)
imageDatasetIsImage =
  imageDatasetIsImageDataset

textHasImagePartAssertion :
  SatisfiesAxiom constructorInterpretation
    (objectPropertyAssertion HasPart
      textDatasetIndividual imageDatasetIndividual)
textHasImagePartAssertion =
  textHasImagePart

imagePartOfTextAssertion :
  SatisfiesAxiom constructorInterpretation
    (objectPropertyAssertion PartOf
      imageDatasetIndividual textDatasetIndividual)
imagePartOfTextAssertion =
  imagePartOfText

constructorOntologySatisfied :
  SatisfiesOntology constructorInterpretation constructorOntology
constructorOntologySatisfied =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ datasetEquivalentToDisjointUnion
  (Prod._,_ textAndImageDisjoint
  (Prod._,_ inverseObjectPropertiesSatisfied
  (Prod._,_ textDatasetIsText
  (Prod._,_ imageDatasetIsImage
  (Prod._,_ textHasImagePartAssertion
  (Prod._,_ imagePartOfTextAssertion
    (lift tt))))))))))))