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

module OWL2.Examples.WebProtege.ProfileRestrictions where

open import OWL2.Prelude
import OWL2.Examples.WebProtege.Annotations as A
import OWL2.Portable.ProfileRestrictions as PR
import OWL2.Portable.Syntax as P
import OWL2.Profiles.EL as EL
import OWL2.Profiles.QL as QL
import OWL2.Profiles.RL as RL

axiom : P.Axiom → P.Annotated P.Axiom
axiom =
  A.axiom

document : List (P.Annotated P.Axiom) → P.OntologyDocument
document axioms =
  P.ontologyDocument
    (A.webProtegePrefix ∷ [])
    (P.ontology
      (P.ontologyIRI A.webProtegeOntologyIRI absent)
      []
      []
      axioms)

acceptedLogicalAxioms : List (P.Annotated P.Axiom)
acceptedLogicalAxioms =
  axiom (P.subClassOf A.CuratedDatasetC A.DatasetC)
  ∷ axiom (P.classAssertion A.CuratedDatasetC A.datasetOne)
  ∷ axiom (P.classAssertion A.ContributorC A.alice)
  ∷ axiom (P.objectPropertyAssertion A.HasCurator A.datasetOne A.alice)
  ∷ []

acceptedProfileDocument : P.OntologyDocument
acceptedProfileDocument =
  document (A.declarationAxioms ++ acceptedLogicalAxioms)

acceptedProfileReport : PR.ProfileRestrictionsReport
acceptedProfileReport =
  PR.reportProfileRestrictions acceptedProfileDocument

acceptedProfileNonELFeatures :
  PR.profileRestrictionsNonELFeatures acceptedProfileReport ≡ []
acceptedProfileNonELFeatures =
  refl

acceptedProfileNonQLFeatures :
  PR.profileRestrictionsNonQLFeatures acceptedProfileReport ≡ []
acceptedProfileNonQLFeatures =
  refl

acceptedProfileNonRLFeatures :
  PR.profileRestrictionsNonRLFeatures acceptedProfileReport ≡ []
acceptedProfileNonRLFeatures =
  refl

acceptedProfileNonELFeatureCount :
  PR.profileRestrictionsNonELFeatureCount acceptedProfileReport ≡ 0
acceptedProfileNonELFeatureCount =
  refl

acceptedProfileNonQLFeatureCount :
  PR.profileRestrictionsNonQLFeatureCount acceptedProfileReport ≡ 0
acceptedProfileNonQLFeatureCount =
  refl

acceptedProfileNonRLFeatureCount :
  PR.profileRestrictionsNonRLFeatureCount acceptedProfileReport ≡ 0
acceptedProfileNonRLFeatureCount =
  refl

acceptedProfileEL :
  PR.NoNonELProfileFeatures acceptedProfileDocument
acceptedProfileEL =
  tt*

acceptedProfileQL :
  PR.NoNonQLProfileFeatures acceptedProfileDocument
acceptedProfileQL =
  tt*

acceptedProfileRL :
  PR.NoNonRLProfileFeatures acceptedProfileDocument
acceptedProfileRL =
  tt*

acceptedProfileAll :
  PR.AllProfileDocument acceptedProfileDocument
acceptedProfileAll =
  PR.allProfileRestrictions tt* tt* tt*

elRejectedAxiom : P.Annotated P.Axiom
elRejectedAxiom =
  axiom
    (P.disjointClasses
      (P.twoOrMore A.DatasetC A.ContributorC []))

elRejectedDocument : P.OntologyDocument
elRejectedDocument =
  document (elRejectedAxiom ∷ [])

elRejectedReport : PR.ProfileRestrictionsReport
elRejectedReport =
  PR.reportProfileRestrictions elRejectedDocument

elRejectedFeatures :
  PR.profileRestrictionsNonELFeatures elRejectedReport ≡
  EL.disjointClassesAxiomFeature ∷ []
elRejectedFeatures =
  refl

elRejectedFeatureCount :
  PR.profileRestrictionsNonELFeatureCount elRejectedReport ≡ 1
elRejectedFeatureCount =
  refl

elRejectedByPackagedPredicate :
  ¬ PR.NoNonELProfileFeatures elRejectedDocument
elRejectedByPackagedPredicate impossible =
  impossible

qlRejectedAxiom : P.Annotated P.Axiom
qlRejectedAxiom =
  axiom (P.functionalObjectProperty A.HasCurator)

qlRejectedDocument : P.OntologyDocument
qlRejectedDocument =
  document (qlRejectedAxiom ∷ [])

qlRejectedReport : PR.ProfileRestrictionsReport
qlRejectedReport =
  PR.reportProfileRestrictions qlRejectedDocument

qlRejectedFeatures :
  PR.profileRestrictionsNonQLFeatures qlRejectedReport ≡
  QL.functionalObjectPropertyAxiomFeature ∷ []
qlRejectedFeatures =
  refl

qlRejectedFeatureCount :
  PR.profileRestrictionsNonQLFeatureCount qlRejectedReport ≡ 1
qlRejectedFeatureCount =
  refl

qlRejectedByPackagedPredicate :
  ¬ PR.NoNonQLProfileFeatures qlRejectedDocument
qlRejectedByPackagedPredicate impossible =
  impossible

rlRejectedAxiom : P.Annotated P.Axiom
rlRejectedAxiom =
  axiom
    (P.subClassOf
      A.CuratedDatasetC
      A.CuratedByContributorC)

rlRejectedDocument : P.OntologyDocument
rlRejectedDocument =
  document (rlRejectedAxiom ∷ [])

rlRejectedReport : PR.ProfileRestrictionsReport
rlRejectedReport =
  PR.reportProfileRestrictions rlRejectedDocument

rlRejectedFeatures :
  PR.profileRestrictionsNonRLFeatures rlRejectedReport ≡
  RL.objectSomeValuesFromFeature ∷ []
rlRejectedFeatures =
  refl

rlRejectedFeatureCount :
  PR.profileRestrictionsNonRLFeatureCount rlRejectedReport ≡ 1
rlRejectedFeatureCount =
  refl

rlRejectedByPackagedPredicate :
  ¬ PR.NoNonRLProfileFeatures rlRejectedDocument
rlRejectedByPackagedPredicate impossible =
  impossible