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

module OWL2.Examples.WebProtege.ProfilesRL where

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

acceptedNamedSubclassRL :
  RL.RLAxiom (P.subClassOf A.CuratedDatasetC A.DatasetC)
acceptedNamedSubclassRL =
  tt*

acceptedObjectPropertyAssertionRL :
  RL.RLAxiom
    (P.objectPropertyAssertion A.HasCurator A.datasetOne A.alice)
acceptedObjectPropertyAssertionRL =
  tt*

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

simpleRLAxioms : List (P.Annotated P.Axiom)
simpleRLAxioms =
  A.declarationAxioms ++ simpleRLLogicalAxioms ++ A.annotationAssertionAxioms

simpleRLOntology : P.Ontology
simpleRLOntology =
  P.ontology
    (P.ontologyIRI A.webProtegeOntologyIRI absent)
    []
    []
    simpleRLAxioms

simpleRLDocument : P.OntologyDocument
simpleRLDocument =
  P.ontologyDocument (A.webProtegePrefix ∷ []) simpleRLOntology

simpleRLDocumentAccepted : RL.RLDocument simpleRLDocument
simpleRLDocumentAccepted =
  tt*

simpleRLDocumentHasNoNonRLFeatures :
  RL.ontologyDocumentNonRLFeatures simpleRLDocument ≡ []
simpleRLDocumentHasNoNonRLFeatures =
  refl

simpleRLDocumentClassifierAccepts :
  RL.isRLDocument simpleRLDocument ≡ true
simpleRLDocumentClassifierAccepts =
  refl

simpleRLDocumentReportHasNoFeatures :
  RL.nonRLFeatures (RL.ontologyDocumentReport simpleRLDocument) ≡ []
simpleRLDocumentReportHasNoFeatures =
  refl

rejectedExistentialSuperclassAxiom : P.Axiom
rejectedExistentialSuperclassAxiom =
  P.subClassOf A.CuratedDatasetC A.CuratedByContributorC

rejectedExistentialSuperclassFeatures :
  RL.axiomNonRLFeatures rejectedExistentialSuperclassAxiom ≡
  RL.objectSomeValuesFromFeature ∷ []
rejectedExistentialSuperclassFeatures =
  refl

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

rejectedUnionFeatures :
  RL.classExpressionNonRLFeatures rejectedUnionClass ≡
  RL.objectUnionOfFeature ∷ []
rejectedUnionFeatures =
  refl

rejectedExactCardinalityClass : P.ClassExpression
rejectedExactCardinalityClass =
  P.objectExactCardinality  A.HasCurator (present A.ContributorC)

rejectedExactCardinalityFeatures :
  RL.classExpressionNonRLFeatures rejectedExactCardinalityClass ≡
  RL.objectExactCardinalityFeature ∷ []
rejectedExactCardinalityFeatures =
  refl

rejectedDataComplementRange : P.DataRange
rejectedDataComplementRange =
  P.dataComplementOf P.dataTop

rejectedDataComplementRangeFeatures :
  RL.dataRangeNonRLFeatures rejectedDataComplementRange ≡
  RL.dataComplementOfFeature ∷ []
rejectedDataComplementRangeFeatures =
  refl

stringDatatype : P.DatatypeName
stringDatatype =
  P.reserved P.xsdStringIRI

rejectedDatatypeDefinitionAxiom : P.Axiom
rejectedDatatypeDefinitionAxiom =
  P.datatypeDefinition stringDatatype P.dataTop

rejectedDatatypeDefinitionAxiomFeatures :
  RL.axiomNonRLFeatures rejectedDatatypeDefinitionAxiom ≡
  RL.datatypeDefinitionAxiomFeature ∷ []
rejectedDatatypeDefinitionAxiomFeatures =
  refl

rejectedRLProfileOntology : P.Ontology
rejectedRLProfileOntology =
  P.ontology
    P.anonymousOntology
    []
    []
    (A.axiom rejectedExistentialSuperclassAxiom ∷ [])

rejectedRLProfileDocument : P.OntologyDocument
rejectedRLProfileDocument =
  P.ontologyDocument [] rejectedRLProfileOntology

rejectedRLProfileDocumentFeatures :
  RL.ontologyDocumentNonRLFeatures rejectedRLProfileDocument ≡
  RL.objectSomeValuesFromFeature ∷ []
rejectedRLProfileDocumentFeatures =
  refl

rejectedRLProfileDocumentClassifierRejects :
  RL.isRLDocument rejectedRLProfileDocument ≡ false
rejectedRLProfileDocumentClassifierRejects =
  refl