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

module OWL2.Portable.Check.WebProtege where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Foundation.Maybe
import OWL2.Portable.Check.Declarations as DeclarationCheck
import OWL2.Portable.Check.PropertyRoles as PropertyRoleCheck
import OWL2.Portable.Check.SemanticSupport as SemanticSupportCheck
import OWL2.Portable.Declarations as Declarations
import OWL2.Portable.GlobalRestrictions as GlobalRestrictions
import OWL2.Portable.PropertyKinds as PropertyKinds
import OWL2.Portable.Semantics as Semantics
import OWL2.Portable.Syntax as P
import OWL2.Portable.WebProtegeReport as Report

noUndeclaredEntityUsesFromDiagnostics :
  (uses : List Declarations.UndeclaredEntityUse) →
  CleanDiagnostics (DeclarationCheck.undeclaredEntityUseDiagnostics uses) →
  Declarations.NoUndeclaredEntityUses uses
noUndeclaredEntityUsesFromDiagnostics [] clean =
  tt*
noUndeclaredEntityUsesFromDiagnostics (use ∷ uses) ()

noDeclarationRoleCollisionsFromDiagnostics :
  (collisions : List PropertyKinds.DeclarationCollision) →
  CleanDiagnostics
    (DeclarationCheck.declarationRoleCollisionDiagnostics collisions) →
  PropertyKinds.NoCollisions collisions
noDeclarationRoleCollisionsFromDiagnostics [] clean =
  tt*
noDeclarationRoleCollisionsFromDiagnostics (collision ∷ collisions) ()

noPropertyUsageConflictsFromDiagnostics :
  (conflicts : List PropertyKinds.PropertyUsageConflict) →
  CleanDiagnostics
    (PropertyRoleCheck.propertyRoleUsageConflictDiagnostics conflicts) →
  PropertyKinds.NoPropertyUsageConflicts conflicts
noPropertyUsageConflictsFromDiagnostics [] clean =
  tt*
noPropertyUsageConflictsFromDiagnostics (conflict ∷ conflicts) ()

completeWebProtegeSemanticTranslationFromDiagnostics :
  (unsupported : List (P.Annotated P.Axiom)) →
  CleanDiagnostics
    (SemanticSupportCheck.unsupportedSemanticAxiomDiagnostics unsupported) →
  unsupported ≡ []
completeWebProtegeSemanticTranslationFromDiagnostics [] clean =
  refl
completeWebProtegeSemanticTranslationFromDiagnostics (axiom ∷ unsupported) ()

declarationCoverageFromDiagnostics :
  (document : P.OntologyDocument) →
  CleanDiagnostics (DeclarationCheck.declarationDiagnostics document) →
  GlobalRestrictions.NoDeclarationCoverageGaps document
declarationCoverageFromDiagnostics document clean =
  noUndeclaredEntityUsesFromDiagnostics
    (Declarations.ontologyDocumentUndeclaredEntityUses document)
    (cleanAppendLeft
      (DeclarationCheck.undeclaredEntityUseDiagnostics
        (Declarations.ontologyDocumentUndeclaredEntityUses document))
      (DeclarationCheck.declarationRoleCollisionDiagnostics
        (PropertyKinds.owl2DLOntologyDocumentDeclarationCollisions document))
      clean)

declarationRolesFromDiagnostics :
  (document : P.OntologyDocument) →
  CleanDiagnostics (DeclarationCheck.declarationDiagnostics document) →
  GlobalRestrictions.NoDeclarationRoleCollisions document
declarationRolesFromDiagnostics document clean =
  noDeclarationRoleCollisionsFromDiagnostics
    (PropertyKinds.owl2DLOntologyDocumentDeclarationCollisions document)
    (cleanAppendRight
      (DeclarationCheck.undeclaredEntityUseDiagnostics
        (Declarations.ontologyDocumentUndeclaredEntityUses document))
      (DeclarationCheck.declarationRoleCollisionDiagnostics
        (PropertyKinds.owl2DLOntologyDocumentDeclarationCollisions document))
      clean)

propertyRolesFromDiagnostics :
  (document : P.OntologyDocument) →
  CleanDiagnostics (PropertyRoleCheck.propertyRoleDiagnostics document) →
  GlobalRestrictions.NoPropertyRoleUsageConflicts document
propertyRolesFromDiagnostics document clean =
  noPropertyUsageConflictsFromDiagnostics
    (PropertyKinds.ontologyDocumentPropertyRoleUsageConflicts document)
    clean

semanticSupportFromDiagnostics :
  (document : P.OntologyDocument) →
  CleanDiagnostics (SemanticSupportCheck.semanticSupportDiagnostics document) →
  GlobalRestrictions.NoSemanticUnsupportedAxioms document
semanticSupportFromDiagnostics document clean =
  completeWebProtegeSemanticTranslationFromDiagnostics
    (Semantics.unsupported (Semantics.partialTranslateOntologyDocument document))
    clean

webProtegeDiagnostics : P.OntologyDocument → Diagnostics
webProtegeDiagnostics document =
  DeclarationCheck.declarationDiagnostics document ++
  PropertyRoleCheck.propertyRoleDiagnostics document ++
  SemanticSupportCheck.semanticSupportDiagnostics document

webProtegeImplementedRestrictionsFromDiagnostics :
  (document : P.OntologyDocument) →
  CleanDiagnostics (webProtegeDiagnostics document) →
  GlobalRestrictions.WebProtegeImplementedGlobalRestrictions document
webProtegeImplementedRestrictionsFromDiagnostics document clean =
  GlobalRestrictions.webProtegeImplementedGlobalRestrictions
    (GlobalRestrictions.owl2DLImplementedGlobalRestrictions
      declarationCoverage
      declarationRoles
      propertyRoles
      semanticSupport)
    semanticSupport
    (GlobalRestrictions.annotationErasureMatchesSemanticsProof document)
    (GlobalRestrictions.annotationErasureIgnoresAnnotationsProof document)
  where
  declarationDiagnostics : Diagnostics
  declarationDiagnostics =
    DeclarationCheck.declarationDiagnostics document

  propertyRoleDiagnostics : Diagnostics
  propertyRoleDiagnostics =
    PropertyRoleCheck.propertyRoleDiagnostics document

  semanticSupportDiagnostics : Diagnostics
  semanticSupportDiagnostics =
    SemanticSupportCheck.semanticSupportDiagnostics document

  restDiagnostics : Diagnostics
  restDiagnostics =
    propertyRoleDiagnostics ++ semanticSupportDiagnostics

  declarationClean :
    CleanDiagnostics declarationDiagnostics
  declarationClean =
    cleanAppendLeft declarationDiagnostics restDiagnostics clean

  restClean :
    CleanDiagnostics restDiagnostics
  restClean =
    cleanAppendRight declarationDiagnostics restDiagnostics clean

  propertyRolesClean :
    CleanDiagnostics propertyRoleDiagnostics
  propertyRolesClean =
    cleanAppendLeft propertyRoleDiagnostics semanticSupportDiagnostics restClean

  semanticSupportClean :
    CleanDiagnostics semanticSupportDiagnostics
  semanticSupportClean =
    cleanAppendRight propertyRoleDiagnostics semanticSupportDiagnostics restClean

  declarationCoverage :
    GlobalRestrictions.NoDeclarationCoverageGaps document
  declarationCoverage =
    declarationCoverageFromDiagnostics document declarationClean

  declarationRoles :
    GlobalRestrictions.NoDeclarationRoleCollisions document
  declarationRoles =
    declarationRolesFromDiagnostics document declarationClean

  propertyRoles :
    GlobalRestrictions.NoPropertyRoleUsageConflicts document
  propertyRoles =
    propertyRolesFromDiagnostics document propertyRolesClean

  semanticSupport :
    GlobalRestrictions.NoSemanticUnsupportedAxioms document
  semanticSupport =
    semanticSupportFromDiagnostics document semanticSupportClean

record WebProtegeDocumentEvidence
  (document : P.OntologyDocument)
  : Type₀ where
  constructor webProtegeDocumentEvidence
  field
    webProtegeReport :
      Report.DocumentReport
    webProtegeReportRecorded :
      webProtegeReport ≡ Report.reportDocument document
    webProtegeImplementedRestrictions :
      GlobalRestrictions.WebProtegeImplementedGlobalRestrictions document

open WebProtegeDocumentEvidence public

record WebProtegeDocumentCheckMeaning
  (document : P.OntologyDocument)
  (evidence : WebProtegeDocumentEvidence document)
  : Type₀ where
  constructor webProtegeDocumentCheckMeaning
  field
    webProtegeMeaningReportRecorded :
      webProtegeReport evidence ≡ Report.reportDocument document
    webProtegeMeaningRestrictions :
      GlobalRestrictions.WebProtegeImplementedGlobalRestrictions document

open WebProtegeDocumentCheckMeaning public

WebProtegeDocumentCheckResult : Type₀
WebProtegeDocumentCheckResult =
  CheckResult
    P.OntologyDocument
    WebProtegeDocumentEvidence
    WebProtegeDocumentCheckMeaning

webProtegeEvidenceFromCleanDiagnostics :
  (document : P.OntologyDocument) →
  CleanDiagnostics (webProtegeDiagnostics document) →
  WebProtegeDocumentEvidence document
webProtegeEvidenceFromCleanDiagnostics document clean =
  webProtegeDocumentEvidence
    (Report.reportDocument document)
    refl
    (webProtegeImplementedRestrictionsFromDiagnostics document clean)

webProtegeEvidence? :
  (document : P.OntologyDocument) →
  Optional (WebProtegeDocumentEvidence document)
webProtegeEvidence? document =
  evidenceFromCleanDiagnostics
    (webProtegeDiagnostics document)
    (webProtegeEvidenceFromCleanDiagnostics document)

webProtegeCleanEvidence :
  (document : P.OntologyDocument) →
  CleanDiagnostics (webProtegeDiagnostics document) →
  Present (webProtegeEvidence? document)
webProtegeCleanEvidence document =
  cleanEvidenceFromCleanDiagnostics
    (webProtegeDiagnostics document)
    (webProtegeEvidenceFromCleanDiagnostics document)

webProtegeSound :
  (document : P.OntologyDocument) →
  (proof : Present (webProtegeEvidence? document)) →
  WebProtegeDocumentCheckMeaning document (presentValue proof)
webProtegeSound document proof =
  webProtegeDocumentCheckMeaning
    (webProtegeReportRecorded evidence)
    (webProtegeImplementedRestrictions evidence)
  where
  evidence : WebProtegeDocumentEvidence document
  evidence =
    presentValue proof

checkWebProtegeDocument :
  P.OntologyDocument →
  WebProtegeDocumentCheckResult
checkWebProtegeDocument document =
  let diagnostics = webProtegeDiagnostics document in
  record
    { input =
        document
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        webProtegeEvidence? document
    ; cleanEvidence =
        webProtegeCleanEvidence document
    ; sound =
        webProtegeSound document
    }

webProtegeEvidenceFromClean :
  (result : WebProtegeDocumentCheckResult) →
  Clean result →
  WebProtegeDocumentEvidence (input result)
webProtegeEvidenceFromClean result clean =
  evidenceFromClean result clean

webProtegeReportFromClean :
  (result : WebProtegeDocumentCheckResult) →
  Clean result →
  Report.DocumentReport
webProtegeReportFromClean result clean =
  webProtegeReport (webProtegeEvidenceFromClean result clean)

webProtegeImplementedRestrictionsFromClean :
  (result : WebProtegeDocumentCheckResult) →
  (clean : Clean result) →
  GlobalRestrictions.WebProtegeImplementedGlobalRestrictions (input result)
webProtegeImplementedRestrictionsFromClean result clean =
  webProtegeImplementedRestrictions
    (webProtegeEvidenceFromClean result clean)

completeWebProtegeDocumentFromEvidence :
  {document : P.OntologyDocument} →
  WebProtegeDocumentEvidence document →
  Report.CompleteWebProtegeDocument document
completeWebProtegeDocumentFromEvidence {document} evidence =
  Report.completeWebProtegeDocument
    (GlobalRestrictions.noDeclarationCoverageGaps owl2DLRestrictions)
    (GlobalRestrictions.noDeclarationRoleCollisions owl2DLRestrictions)
    (GlobalRestrictions.noPropertyRoleUsageConflicts owl2DLRestrictions)
    (GlobalRestrictions.noSemanticUnsupportedAxioms owl2DLRestrictions)
    (GlobalRestrictions.webProtegeAnnotationErasureUnsupported restrictions)
    (GlobalRestrictions.webProtegeAnnotationErasureMatchesSemantics restrictions)
    (GlobalRestrictions.webProtegeAnnotationErasureIgnoresAnnotations restrictions)
  where
  restrictions :
    GlobalRestrictions.WebProtegeImplementedGlobalRestrictions document
  restrictions =
    webProtegeImplementedRestrictions evidence

  owl2DLRestrictions :
    GlobalRestrictions.OWL2DLImplementedGlobalRestrictions document
  owl2DLRestrictions =
    GlobalRestrictions.webProtegeOWL2DLRestrictions restrictions

completeWebProtegeDocumentFromClean :
  (result : WebProtegeDocumentCheckResult) →
  (clean : Clean result) →
  Report.CompleteWebProtegeDocument (input result)
completeWebProtegeDocumentFromClean result clean =
  completeWebProtegeDocumentFromEvidence
    (webProtegeEvidenceFromClean result clean)

webProtegeSoundFromClean :
  (result : WebProtegeDocumentCheckResult) →
  (clean : Clean result) →
  WebProtegeDocumentCheckMeaning
    (input result)
    (webProtegeEvidenceFromClean result clean)
webProtegeSoundFromClean result clean =
  soundFromClean result clean