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

module OWL2.Examples.WebProtege.Profiles where

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

curatedByContributorEL : EL.ELClassExpression A.CuratedByContributorC
curatedByContributorEL =
  tt*

acceptedSubclassEL :
  EL.ELAxiom
    (P.subClassOf A.CuratedDatasetC A.CuratedByContributorC)
acceptedSubclassEL =
  tt*

plainDocumentEL : EL.ELDocument A.plainDocument
plainDocumentEL =
  tt*

annotatedDocumentEL : EL.ELDocument A.annotatedDocument
annotatedDocumentEL =
  tt*

annotatedDocumentHasNoNonELFeatures :
  EL.ontologyDocumentNonELFeatures A.annotatedDocument ≡ []
annotatedDocumentHasNoNonELFeatures =
  refl

annotatedDocumentClassifierAccepts :
  EL.isELDocument A.annotatedDocument ≡ true
annotatedDocumentClassifierAccepts =
  refl

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

rejectedUnionFeatures :
  EL.classExpressionNonELFeatures rejectedUnionClass ≡
  EL.objectUnionOfFeature ∷ []
rejectedUnionFeatures =
  refl

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

rejectedCardinalityFeatures :
  EL.classExpressionNonELFeatures rejectedCardinalityClass ≡
  EL.objectMinCardinalityFeature ∷ []
rejectedCardinalityFeatures =
  refl

rejectedDisjointAxiom : P.Annotated P.Axiom
rejectedDisjointAxiom =
  P.annotated
    []
    (P.disjointClasses
      (P.twoOrMore A.DatasetC A.ContributorC []))

rejectedDisjointAxiomFeatures :
  EL.annotatedAxiomNonELFeatures rejectedDisjointAxiom ≡
  EL.disjointClassesAxiomFeature ∷ []
rejectedDisjointAxiomFeatures =
  refl

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

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

rejectedProfileDocumentFeatures :
  EL.ontologyDocumentNonELFeatures rejectedProfileDocument ≡
  EL.disjointClassesAxiomFeature ∷ []
rejectedProfileDocumentFeatures =
  refl

rejectedProfileDocumentClassifierRejects :
  EL.isELDocument rejectedProfileDocument ≡ false
rejectedProfileDocumentClassifierRejects =
  refl