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

module OWL2.Examples.WebProtege.ProfilesQL where

open import OWL2.Prelude
import OWL2.Examples.WebProtege.Annotations as A
import OWL2.Portable.Syntax as P
import OWL2.Profiles.QL as QL

hasCuratorInverseQL :
  QL.QLObjectPropertyExpression (P.objectInverseOf A.HasCurator)
hasCuratorInverseQL =
  tt*

curatedByContributorQLSuper :
  QL.QLSuperClassExpression A.CuratedByContributorC
curatedByContributorQLSuper =
  tt*

curatedByContributorQLClass :
  QL.QLClassExpression A.CuratedByContributorC
curatedByContributorQLClass =
  tt*

curatedByContributorRejectedAsSubClass :
  QL.subClassExpressionNonQLFeatures A.CuratedByContributorC ≡
  QL.objectSomeValuesFromSubClassFillerFeature ∷ []
curatedByContributorRejectedAsSubClass =
  refl

acceptedSubclassQL :
  QL.QLAxiom
    (P.subClassOf A.CuratedDatasetC A.CuratedByContributorC)
acceptedSubclassQL =
  tt*

plainDocumentQL : QL.QLDocument A.plainDocument
plainDocumentQL =
  tt*

annotatedDocumentQL : QL.QLDocument A.annotatedDocument
annotatedDocumentQL =
  tt*

annotatedDocumentHasNoNonQLFeatures :
  QL.ontologyDocumentNonQLFeatures A.annotatedDocument ≡ []
annotatedDocumentHasNoNonQLFeatures =
  refl

annotatedDocumentClassifierAccepts :
  QL.isQLDocument A.annotatedDocument ≡ true
annotatedDocumentClassifierAccepts =
  refl

rejectedUnionClass : P.ClassExpression
rejectedUnionClass =
  P.objectUnionOf
    (P.twoOrMore A.DatasetC A.ContributorC [])

rejectedUnionFeatures :
  QL.classExpressionNonQLFeatures rejectedUnionClass ≡
  QL.objectUnionOfFeature ∷ []
rejectedUnionFeatures =
  refl

rejectedCardinalityClass : P.ClassExpression
rejectedCardinalityClass =
  P.objectMinCardinality  A.HasCurator (present A.ContributorC)

rejectedCardinalityFeatures :
  QL.classExpressionNonQLFeatures rejectedCardinalityClass ≡
  QL.objectMinCardinalityFeature ∷ []
rejectedCardinalityFeatures =
  refl

rejectedExistentialSubclassAxiom : P.Annotated P.Axiom
rejectedExistentialSubclassAxiom =
  P.annotated
    []
    (P.subClassOf A.CuratedByContributorC A.DatasetC)

rejectedExistentialSubclassAxiomFeatures :
  QL.annotatedAxiomNonQLFeatures rejectedExistentialSubclassAxiom ≡
  QL.objectSomeValuesFromSubClassFillerFeature ∷ []
rejectedExistentialSubclassAxiomFeatures =
  refl

rejectedNonAtomicClassAssertion : P.Annotated P.Axiom
rejectedNonAtomicClassAssertion =
  P.annotated
    []
    (P.classAssertion A.CuratedByContributorC A.datasetOne)

rejectedNonAtomicClassAssertionFeatures :
  QL.annotatedAxiomNonQLFeatures rejectedNonAtomicClassAssertion ≡
  QL.nonAtomicClassAssertionFeature ∷ []
rejectedNonAtomicClassAssertionFeatures =
  refl

xsdStringRange rdfsLiteralRange : P.DataRange
xsdStringRange =
  P.datatype (P.reserved P.xsdStringIRI)
rdfsLiteralRange =
  P.datatype (P.reserved P.rdfsLiteralIRI)

rejectedDataUnionRange : P.DataRange
rejectedDataUnionRange =
  P.dataUnionOf
    (P.twoOrMore xsdStringRange rdfsLiteralRange [])

rejectedDataUnionFeatures :
  QL.dataRangeNonQLFeatures rejectedDataUnionRange ≡
  QL.dataUnionOfFeature ∷ []
rejectedDataUnionFeatures =
  refl

rejectedPropertyChainAxiom : P.Annotated P.Axiom
rejectedPropertyChainAxiom =
  P.annotated
    []
    (P.subObjectPropertyOf
      (P.subObjectPropertyChain
        (P.objectPropertyChain
          (P.twoOrMore A.HasCurator A.HasCurator [])))
      A.HasCurator)

rejectedPropertyChainAxiomFeatures :
  QL.annotatedAxiomNonQLFeatures rejectedPropertyChainAxiom ≡
  QL.objectPropertyChainFeature ∷ []
rejectedPropertyChainAxiomFeatures =
  refl

rejectedFunctionalObjectPropertyAxiom : P.Annotated P.Axiom
rejectedFunctionalObjectPropertyAxiom =
  P.annotated [] (P.functionalObjectProperty A.HasCurator)

rejectedFunctionalObjectPropertyAxiomFeatures :
  QL.annotatedAxiomNonQLFeatures rejectedFunctionalObjectPropertyAxiom ≡
  QL.functionalObjectPropertyAxiomFeature ∷ []
rejectedFunctionalObjectPropertyAxiomFeatures =
  refl

rejectedProfileOntology : P.Ontology
rejectedProfileOntology =
  P.ontology
    P.anonymousOntology
    []
    []
    (rejectedFunctionalObjectPropertyAxiom ∷ [])

rejectedProfileDocument : P.OntologyDocument
rejectedProfileDocument =
  P.ontologyDocument [] rejectedProfileOntology

rejectedProfileDocumentFeatures :
  QL.ontologyDocumentNonQLFeatures rejectedProfileDocument ≡
  QL.functionalObjectPropertyAxiomFeature ∷ []
rejectedProfileDocumentFeatures =
  refl

rejectedProfileDocumentClassifierRejects :
  QL.isQLDocument rejectedProfileDocument ≡ false
rejectedProfileDocumentClassifierRejects =
  refl