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

module OWL2.Examples.WebProtege.DL where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
import OWL2.Examples.WebProtege.Annotations as Annotations
import OWL2.Portable.Check.WebProtege as WebProtegeCheck
import OWL2.Portable.GlobalRestrictions as GR
import OWL2.Portable.Syntax as P
import OWL2.Portable.WebProtegeReport as Report

name : String → P.Name
name text =
  P.named (P.iri text)

className : String → P.ClassName
className =
  name

propertyName : String → P.Name
propertyName =
  name

individualName : String → P.NamedIndividualName
individualName =
  P.iri

axiom : P.Axiom → P.Annotated P.Axiom
axiom body =
  P.annotated [] body

document : List (P.Annotated P.Axiom) → P.OntologyDocument
document axioms =
  P.ontologyDocument []
    (P.ontology P.anonymousOntology [] [] axioms)

webProtegeAnnotatedReport : Report.DocumentReport
webProtegeAnnotatedReport =
  Report.reportDocument Annotations.annotatedDocument

webProtegeAnnotatedModuleReport : Report.ModuleReport
webProtegeAnnotatedModuleReport =
  Report.reportModule
    "OWL2.Examples.WebProtege.Annotations"
    Annotations.annotatedDocument

webProtegeAnnotatedCheckResult :
  WebProtegeCheck.WebProtegeDocumentCheckResult
webProtegeAnnotatedCheckResult =
  WebProtegeCheck.checkWebProtegeDocument Annotations.annotatedDocument

webProtegeAnnotatedCheckDiagnostics :
  diagnostics webProtegeAnnotatedCheckResult ≡ noDiagnostics
webProtegeAnnotatedCheckDiagnostics =
  refl

webProtegeAnnotatedCheckClean :
  Clean webProtegeAnnotatedCheckResult
webProtegeAnnotatedCheckClean =
  tt

webProtegeAnnotatedCheckEvidence :
  WebProtegeCheck.WebProtegeDocumentEvidence
    Annotations.annotatedDocument
webProtegeAnnotatedCheckEvidence =
  WebProtegeCheck.webProtegeEvidenceFromClean
    webProtegeAnnotatedCheckResult
    webProtegeAnnotatedCheckClean

webProtegeAnnotatedComplete :
  Report.CompleteWebProtegeDocument Annotations.annotatedDocument
webProtegeAnnotatedComplete =
  WebProtegeCheck.completeWebProtegeDocumentFromClean
    webProtegeAnnotatedCheckResult
    webProtegeAnnotatedCheckClean

webProtegeAnnotatedCheckReportView :
  WebProtegeCheck.webProtegeReport webProtegeAnnotatedCheckEvidence ≡
  Report.reportDocument Annotations.annotatedDocument
webProtegeAnnotatedCheckReportView =
  refl

webProtegeAnnotatedCheckRestrictions :
  GR.WebProtegeImplementedGlobalRestrictions Annotations.annotatedDocument
webProtegeAnnotatedCheckRestrictions =
  WebProtegeCheck.webProtegeImplementedRestrictionsFromClean
    webProtegeAnnotatedCheckResult
    webProtegeAnnotatedCheckClean

webProtegeAnnotatedUndeclaredCount :
  Report.documentReportUndeclaredEntityUseCount
    webProtegeAnnotatedReport
  ≡ 
webProtegeAnnotatedUndeclaredCount =
  refl

webProtegeAnnotatedDeclarationCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    webProtegeAnnotatedReport
  ≡ 
webProtegeAnnotatedDeclarationCollisionCount =
  refl

webProtegeAnnotatedPropertyCollisionCount :
  Report.documentReportPropertyRoleUsageConflictCount
    webProtegeAnnotatedReport
  ≡ 
webProtegeAnnotatedPropertyCollisionCount =
  refl

webProtegeAnnotatedSemanticUnsupportedCount :
  Report.documentReportSemanticUnsupportedCount
    webProtegeAnnotatedReport
  ≡ 
webProtegeAnnotatedSemanticUnsupportedCount =
  refl

webProtegeAnnotatedErasedAnnotationAxiomCount :
  Report.annotationErasureErasedAnnotationAxiomCount
    (Report.documentReportAnnotationErasureStatus
      webProtegeAnnotatedReport)
  ≡ 
webProtegeAnnotatedErasedAnnotationAxiomCount =
  refl

person employee : P.ClassName
person =
  className "https://example.org/webprotege/report#Person"
employee =
  className "https://example.org/webprotege/report#Employee"

missingDeclarationDocument : P.OntologyDocument
missingDeclarationDocument =
  document
    ( axiom (P.declaration (P.classEntity person))
    ∷ axiom
        (P.subClassOf
          (P.namedClass employee)
          (P.namedClass person))
    ∷ [] )

missingDeclarationReport : Report.DocumentReport
missingDeclarationReport =
  Report.reportDocument missingDeclarationDocument

missingDeclarationUndeclaredCount :
  Report.documentReportUndeclaredEntityUseCount
    missingDeclarationReport
  ≡ 
missingDeclarationUndeclaredCount =
  refl

missingDeclarationRejected :
  ¬ Report.NoDeclarationCoverageGaps missingDeclarationDocument
missingDeclarationRejected impossible =
  impossible

missingDeclarationCheckResult :
  WebProtegeCheck.WebProtegeDocumentCheckResult
missingDeclarationCheckResult =
  WebProtegeCheck.checkWebProtegeDocument missingDeclarationDocument

missingDeclarationCheckEvidenceAbsent :
  evidence? missingDeclarationCheckResult ≡ absent
missingDeclarationCheckEvidenceAbsent =
  refl

missingDeclarationCheckEvidenceUnavailable :
  EvidenceUnavailable missingDeclarationCheckResult
missingDeclarationCheckEvidenceUnavailable =
  evidenceUnavailable
    missingDeclarationCheckResult
    missingDeclarationCheckEvidenceAbsent

sharedDeclaredProperty : P.Name
sharedDeclaredProperty =
  propertyName
    "https://example.org/webprotege/report#sharedDeclaredProperty"

declarationRoleCollisionDocument : P.OntologyDocument
declarationRoleCollisionDocument =
  document
    ( axiom
        (P.declaration
          (P.objectPropertyEntity sharedDeclaredProperty))
    ∷ axiom
        (P.declaration
          (P.dataPropertyEntity sharedDeclaredProperty))
    ∷ [] )

declarationRoleCollisionReport : Report.DocumentReport
declarationRoleCollisionReport =
  Report.reportDocument declarationRoleCollisionDocument

declarationRoleCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    declarationRoleCollisionReport
  ≡ 
declarationRoleCollisionCount =
  refl

declarationRoleCollisionRejected :
  ¬ Report.NoDeclarationRoleCollisions declarationRoleCollisionDocument
declarationRoleCollisionRejected impossible =
  impossible

sharedUsageProperty : P.Name
sharedUsageProperty =
  propertyName
    "https://example.org/webprotege/report#sharedUsageProperty"

aliceIRI : P.NamedIndividualName
aliceIRI =
  individualName "https://example.org/webprotege/report#alice"

alice : P.Individual
alice =
  P.namedIndividual aliceIRI

propertyUsageCollisionDocument : P.OntologyDocument
propertyUsageCollisionDocument =
  document
    ( axiom
        (P.objectPropertyAssertion
          (P.objectProperty sharedUsageProperty)
          alice
          alice)
    ∷ axiom
        (P.dataPropertyAssertion
          (P.dataProperty sharedUsageProperty)
          alice
          (P.stringLiteral "value"))
    ∷ [] )

propertyUsageCollisionReport : Report.DocumentReport
propertyUsageCollisionReport =
  Report.reportDocument propertyUsageCollisionDocument

propertyUsageCollisionCount :
  Report.documentReportPropertyRoleUsageConflictCount
    propertyUsageCollisionReport
  ≡ 
propertyUsageCollisionCount =
  refl

propertyUsageCollisionRejected :
  ¬ Report.NoPropertyRoleUsageConflicts
      propertyUsageCollisionDocument
propertyUsageCollisionRejected impossible =
  impossible