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

module OWL2.Examples.WebProtege.CardinalityRestrictions where

open import OWL2.Prelude
import OWL2.Examples.WebProtege.Annotations as A
import OWL2.Portable.CardinalityRestrictions as CR
import OWL2.Portable.Syntax as P

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)

reviewScoreIRI : P.IRI
reviewScoreIRI =
  P.iri "https://example.org/webprotege#reviewScore"

reviewScore : P.DataPropertyName
reviewScore =
  P.named reviewScoreIRI

xsdString : P.DatatypeName
xsdString =
  P.reserved P.xsdStringIRI

ReviewScore : P.DataPropertyExpression
ReviewScore =
  P.dataProperty reviewScore

StringRange : P.DataRange
StringRange =
  P.datatype xsdString

localDeclarationAxioms : List (P.Annotated P.Axiom)
localDeclarationAxioms =
  axiom (P.declaration (P.dataPropertyEntity reviewScore))
  ∷ axiom (P.declaration (P.datatypeEntity xsdString))
  ∷ []

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

AtMostThreeContributorCurators : P.ClassExpression
AtMostThreeContributorCurators =
  P.objectMaxCardinality
    3
    A.HasCurator
    (present A.ContributorC)

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

AtLeastOneReviewScore : P.ClassExpression
AtLeastOneReviewScore =
  P.dataMinCardinality
    1
    ReviewScore
    (present StringRange)

AtMostThreeReviewScores : P.ClassExpression
AtMostThreeReviewScores =
  P.dataMaxCardinality
    3
    ReviewScore
    (present StringRange)

ExactlyOneReviewScore : P.ClassExpression
ExactlyOneReviewScore =
  P.dataExactCardinality
    1
    ReviewScore
    (present StringRange)

cardinalityAxioms : List (P.Annotated P.Axiom)
cardinalityAxioms =
  axiom (P.subClassOf A.CuratedDatasetC AtLeastOneContributorCurator)
  ∷ axiom (P.subClassOf A.CuratedDatasetC AtMostThreeContributorCurators)
  ∷ axiom (P.subClassOf A.CuratedDatasetC ExactlyOneContributorCurator)
  ∷ axiom (P.subClassOf A.CuratedDatasetC AtLeastOneReviewScore)
  ∷ axiom (P.subClassOf A.CuratedDatasetC AtMostThreeReviewScores)
  ∷ axiom (P.subClassOf A.CuratedDatasetC ExactlyOneReviewScore)
  ∷ []

cardinalityDocument : P.OntologyDocument
cardinalityDocument =
  document
    ( A.declarationAxioms
      ++ localDeclarationAxioms
      ++ cardinalityAxioms )

cardinalityReport : CR.CardinalityRestrictionsReport
cardinalityReport =
  CR.reportCardinalityRestrictions cardinalityDocument

cardinalityDocumentObjectRestrictionCount :
  CR.reportObjectCardinalityRestrictionCount cardinalityReport ≡ 3
cardinalityDocumentObjectRestrictionCount =
  refl

cardinalityDocumentDataRestrictionCount :
  CR.reportDataCardinalityRestrictionCount cardinalityReport ≡ 3
cardinalityDocumentDataRestrictionCount =
  refl

cardinalityDocumentRestrictionCount :
  CR.reportCardinalityRestrictionCount cardinalityReport ≡ 6
cardinalityDocumentRestrictionCount =
  refl

cardinalityDocumentUnsafeIssueCount :
  CR.reportUnsafeCardinalityRestrictionIssueCount cardinalityReport ≡ 0
cardinalityDocumentUnsafeIssueCount =
  refl

cardinalityDocumentAllSafe :
  CR.NoUnsafeCardinalityRestrictions cardinalityDocument
cardinalityDocumentAllSafe =
  tt*

cardinalityDocumentClassified :
  CR.CardinalityRestrictionsExplicitlyClassified cardinalityDocument
cardinalityDocumentClassified =
  CR.cardinalityRestrictionsExplicitlyClassifiedProof cardinalityDocument

annotatedDocumentReport : CR.CardinalityRestrictionsReport
annotatedDocumentReport =
  CR.reportCardinalityRestrictions A.annotatedDocument

annotatedDocumentRestrictionCount :
  CR.reportCardinalityRestrictionCount annotatedDocumentReport ≡ 0
annotatedDocumentRestrictionCount =
  refl

annotatedDocumentNoCardinalityRestrictions :
  CR.NoCardinalityRestrictions A.annotatedDocument
annotatedDocumentNoCardinalityRestrictions =
  tt*

cardinalityDocumentRejectedByNoCardinalityPredicate :
  ¬ CR.NoCardinalityRestrictions cardinalityDocument
cardinalityDocumentRejectedByNoCardinalityPredicate impossible =
  impossible

UnsafeTopObjectCardinality : P.ClassExpression
UnsafeTopObjectCardinality =
  P.objectMinCardinality
    1
    P.topObjectProperty
    (present A.ContributorC)

UnsafeTopDataCardinality : P.ClassExpression
UnsafeTopDataCardinality =
  P.dataMinCardinality
    1
    P.topDataProperty
    (present StringRange)

unsafeCardinalityDocument : P.OntologyDocument
unsafeCardinalityDocument =
  document
    ( A.declarationAxioms
      ++ localDeclarationAxioms
      ++ ( axiom (P.subClassOf A.CuratedDatasetC UnsafeTopObjectCardinality)
         ∷ axiom (P.subClassOf A.CuratedDatasetC UnsafeTopDataCardinality)
         ∷ [] ) )

unsafeCardinalityReport : CR.CardinalityRestrictionsReport
unsafeCardinalityReport =
  CR.reportCardinalityRestrictions unsafeCardinalityDocument

unsafeCardinalityDocumentObjectRestrictionCount :
  CR.reportObjectCardinalityRestrictionCount unsafeCardinalityReport ≡ 1
unsafeCardinalityDocumentObjectRestrictionCount =
  refl

unsafeCardinalityDocumentDataRestrictionCount :
  CR.reportDataCardinalityRestrictionCount unsafeCardinalityReport ≡ 1
unsafeCardinalityDocumentDataRestrictionCount =
  refl

unsafeCardinalityDocumentUnsafeIssueCount :
  CR.reportUnsafeCardinalityRestrictionIssueCount
    unsafeCardinalityReport
  ≡ 2
unsafeCardinalityDocumentUnsafeIssueCount =
  refl

unsafeCardinalityDocumentRejectedBySafetyPredicate :
  ¬ CR.NoUnsafeCardinalityRestrictions unsafeCardinalityDocument
unsafeCardinalityDocumentRejectedBySafetyPredicate impossible =
  impossible