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

module OWL2.Examples.WebProtege.Corpus where

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

data WebProtegeIRI : Type₀ where
  webProtegeDocument : WebProtegeIRI

data WebProtegeClass : Type₀ where
  WebResource Dataset CuratedDataset Contributor : WebProtegeClass

data WebProtegeObjectProperty : Type₀ where
  hasCurator : WebProtegeObjectProperty

data WebProtegeDataProperty : Type₀ where
  noDataProperty : WebProtegeDataProperty

data WebProtegeDatatype : Type₀ where
  noDatatype : WebProtegeDatatype

data WebProtegeIndividual : Type₀ where
  datasetOne draftDataset alice : WebProtegeIndividual

data WebProtegeLiteral : Type₀ where
  noLiteral : WebProtegeLiteral

data WebProtegeFacet : Type₀ where
  noFacet : WebProtegeFacet

data WebProtegeAnnotationProperty : Type₀ where
  label comment definition : WebProtegeAnnotationProperty

WebProtegeSignature : Signature ℓ-zero
WebProtegeSignature .IRI =
  WebProtegeIRI
WebProtegeSignature .ClassName =
  WebProtegeClass
WebProtegeSignature .ObjectPropertyName =
  WebProtegeObjectProperty
WebProtegeSignature .DataPropertyName =
  WebProtegeDataProperty
WebProtegeSignature .DatatypeName =
  WebProtegeDatatype
WebProtegeSignature .IndividualName =
  WebProtegeIndividual
WebProtegeSignature .Literal =
  WebProtegeLiteral
WebProtegeSignature .FacetName =
  WebProtegeFacet
WebProtegeSignature .AnnotationPropertyName =
  WebProtegeAnnotationProperty

WebResourceC DatasetC CuratedDatasetC ContributorC :
  ClassExpression WebProtegeSignature
WebResourceC =
  namedClass WebResource
DatasetC =
  namedClass Dataset
CuratedDatasetC =
  namedClass CuratedDataset
ContributorC =
  namedClass Contributor

HasCurator : ObjectPropertyExpression WebProtegeSignature
HasCurator =
  objectProperty hasCurator

CuratedByContributorC : ClassExpression WebProtegeSignature
CuratedByContributorC =
  objectSomeValuesFrom HasCurator ContributorC

webProtegeOntology : Ontology WebProtegeSignature
webProtegeOntology =
  ontology
    (webProtegeDocument ∷ [])
    []
    ( declaration (classEntity WebResource)
    ∷ declaration (classEntity Dataset)
    ∷ declaration (classEntity CuratedDataset)
    ∷ declaration (classEntity Contributor)
    ∷ declaration (objectPropertyEntity hasCurator)
    ∷ declaration (individualEntity datasetOne)
    ∷ declaration (individualEntity draftDataset)
    ∷ declaration (individualEntity alice)
    ∷ declaration (annotationPropertyEntity label)
    ∷ declaration (annotationPropertyEntity comment)
    ∷ declaration (annotationPropertyEntity definition)
    ∷ subClassOf CuratedDatasetC DatasetC
    ∷ subClassOf DatasetC WebResourceC
    ∷ subClassOf CuratedDatasetC CuratedByContributorC
    ∷ objectPropertyDomain HasCurator CuratedDatasetC
    ∷ objectPropertyRange HasCurator ContributorC
    ∷ classAssertion CuratedDatasetC datasetOne
    ∷ classAssertion DatasetC draftDataset
    ∷ classAssertion ContributorC alice
    ∷ objectPropertyAssertion HasCurator datasetOne alice
    ∷ [] )

data WebProtegeObject : Type₀ where
  datasetOneObject draftDatasetObject aliceObject : WebProtegeObject

data WebProtegeData : Type₀ where
  noDataValue : WebProtegeData

data IsWebResource : WebProtegeObject → Type₀ where
  datasetOneResource : IsWebResource datasetOneObject
  draftDatasetResource : IsWebResource draftDatasetObject

data IsDataset : WebProtegeObject → Type₀ where
  datasetOneDataset : IsDataset datasetOneObject
  draftDatasetDataset : IsDataset draftDatasetObject

data IsCuratedDataset : WebProtegeObject → Type₀ where
  datasetOneCurated : IsCuratedDataset datasetOneObject

data IsContributor : WebProtegeObject → Type₀ where
  aliceContributor : IsContributor aliceObject

WebProtegeClassDenotation :
  WebProtegeClass → WebProtegeObject → Type₀
WebProtegeClassDenotation WebResource =
  IsWebResource
WebProtegeClassDenotation Dataset =
  IsDataset
WebProtegeClassDenotation CuratedDataset =
  IsCuratedDataset
WebProtegeClassDenotation Contributor =
  IsContributor

data CuratorRel : WebProtegeObject → WebProtegeObject → Type₀ where
  datasetOneAliceCurator : CuratorRel datasetOneObject aliceObject

WebProtegeObjectPropertyDenotation :
  WebProtegeObjectProperty →
  WebProtegeObject → WebProtegeObject → Type₀
WebProtegeObjectPropertyDenotation hasCurator =
  CuratorRel

WebProtegeDataPropertyDenotation :
  WebProtegeDataProperty → WebProtegeObject → WebProtegeData → Type₀
WebProtegeDataPropertyDenotation noDataProperty x y =
  ⊥*

WebProtegeDatatypeDenotation :
  WebProtegeDatatype → WebProtegeData → Type₀
WebProtegeDatatypeDenotation noDatatype noDataValue =
  Unit*

WebProtegeFacetDenotation :
  WebProtegeDatatype → WebProtegeFacet → WebProtegeLiteral →
  WebProtegeData → Type₀
WebProtegeFacetDenotation noDatatype noFacet noLiteral noDataValue =
  Unit*

WebProtegeIndividualDenotation :
  WebProtegeIndividual → WebProtegeObject
WebProtegeIndividualDenotation datasetOne =
  datasetOneObject
WebProtegeIndividualDenotation draftDataset =
  draftDatasetObject
WebProtegeIndividualDenotation alice =
  aliceObject

WebProtegeLiteralDenotation : WebProtegeLiteral → WebProtegeData
WebProtegeLiteralDenotation noLiteral =
  noDataValue

webProtegeInterpretation :
  Interpretation WebProtegeSignature ℓ-zero ℓ-zero ℓ-zero
webProtegeInterpretation .ObjectDomain =
  WebProtegeObject
webProtegeInterpretation .DataDomain =
  WebProtegeData
webProtegeInterpretation .classDenotation =
  WebProtegeClassDenotation
webProtegeInterpretation .objectPropertyDenotation =
  WebProtegeObjectPropertyDenotation
webProtegeInterpretation .dataPropertyDenotation =
  WebProtegeDataPropertyDenotation
webProtegeInterpretation .datatypeDenotation =
  WebProtegeDatatypeDenotation
webProtegeInterpretation .facetDenotation =
  WebProtegeFacetDenotation
webProtegeInterpretation .individualDenotation =
  WebProtegeIndividualDenotation
webProtegeInterpretation .literalDenotation =
  WebProtegeLiteralDenotation

curatedDatasetSubDataset :
  SatisfiesAxiom webProtegeInterpretation
    (subClassOf CuratedDatasetC DatasetC)
curatedDatasetSubDataset .datasetOneObject datasetOneCurated =
  datasetOneDataset

datasetSubWebResource :
  SatisfiesAxiom webProtegeInterpretation
    (subClassOf DatasetC WebResourceC)
datasetSubWebResource .datasetOneObject datasetOneDataset =
  datasetOneResource
datasetSubWebResource .draftDatasetObject draftDatasetDataset =
  draftDatasetResource

curatedDatasetHasContributor :
  SatisfiesAxiom webProtegeInterpretation
    (subClassOf CuratedDatasetC CuratedByContributorC)
curatedDatasetHasContributor .datasetOneObject datasetOneCurated =
  aliceObject , (datasetOneAliceCurator , aliceContributor)

hasCuratorDomain :
  SatisfiesAxiom webProtegeInterpretation
    (objectPropertyDomain HasCurator CuratedDatasetC)
hasCuratorDomain .datasetOneObject .aliceObject datasetOneAliceCurator =
  datasetOneCurated

hasCuratorRange :
  SatisfiesAxiom webProtegeInterpretation
    (objectPropertyRange HasCurator ContributorC)
hasCuratorRange .datasetOneObject .aliceObject datasetOneAliceCurator =
  aliceContributor

datasetOneIsCuratedDataset :
  SatisfiesAxiom webProtegeInterpretation
    (classAssertion CuratedDatasetC datasetOne)
datasetOneIsCuratedDataset =
  datasetOneCurated

draftIsDataset :
  SatisfiesAxiom webProtegeInterpretation
    (classAssertion DatasetC draftDataset)
draftIsDataset =
  draftDatasetDataset

aliceIsContributor :
  SatisfiesAxiom webProtegeInterpretation
    (classAssertion ContributorC alice)
aliceIsContributor =
  aliceContributor

datasetOneHasCuratorAlice :
  SatisfiesAxiom webProtegeInterpretation
    (objectPropertyAssertion HasCurator datasetOne alice)
datasetOneHasCuratorAlice =
  datasetOneAliceCurator

datasetOneCuratorWitness :
  evalClass webProtegeInterpretation CuratedByContributorC datasetOneObject
datasetOneCuratorWitness =
  aliceObject , (datasetOneAliceCurator , aliceContributor)

webProtegeModel :
  Model webProtegeInterpretation webProtegeOntology
webProtegeModel =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ curatedDatasetSubDataset
  (Prod._,_ datasetSubWebResource
  (Prod._,_ curatedDatasetHasContributor
  (Prod._,_ hasCuratorDomain
  (Prod._,_ hasCuratorRange
  (Prod._,_ datasetOneIsCuratedDataset
  (Prod._,_ draftIsDataset
  (Prod._,_ aliceIsContributor
  (Prod._,_ datasetOneHasCuratorAlice
    (lift tt))))))))))))))))))))

draftDatasetNotCurated :
  ¬ evalClass webProtegeInterpretation CuratedDatasetC draftDatasetObject
draftDatasetNotCurated ()

reverseTaxonomyCountermodel :
  Model webProtegeInterpretation webProtegeOntology ×
  (¬ SatisfiesAxiom webProtegeInterpretation
      (subClassOf DatasetC CuratedDatasetC))
reverseTaxonomyCountermodel =
  webProtegeModel ,
  λ datasetSubCurated →
    draftDatasetNotCurated
      (datasetSubCurated draftDatasetObject draftDatasetDataset)