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

module OWL2.Portable.WebProtegeReport where

open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
import OWL2.Portable.AnnotationErasure as Erasure
import OWL2.Portable.Declarations as Decl
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax as S

listCount : ∀ {ℓ} {A : Type ℓ} → List A → ℕ
listCount [] =
  zero
listCount (x ∷ xs) =
  suc (listCount xs)

axiomErasures :
  List (P.Annotated P.Axiom) → List Erasure.AxiomErasure
axiomErasures [] =
  []
axiomErasures (ax ∷ axioms) =
  Erasure.eraseAnnotatedAxiom ax ∷ axiomErasures axioms

ontologyAxiomErasures :
  P.Ontology → List Erasure.AxiomErasure
ontologyAxiomErasures ont =
  axiomErasures (P.axioms ont)

ontologyDocumentAxiomErasures :
  P.OntologyDocument → List Erasure.AxiomErasure
ontologyDocumentAxiomErasures document =
  ontologyAxiomErasures (P.documentOntology document)

translatedAxiomErasureCount : List Erasure.AxiomErasure → ℕ
translatedAxiomErasureCount [] =
  zero
translatedAxiomErasureCount
  (Erasure.translatesToSemanticAxioms axioms ∷ erasures) =
  suc (translatedAxiomErasureCount erasures)
translatedAxiomErasureCount
  (Erasure.semanticallyErasedAnnotationAxiom ∷ erasures) =
  translatedAxiomErasureCount erasures
translatedAxiomErasureCount
  (Erasure.unsupportedByPortableSemantics ∷ erasures) =
  translatedAxiomErasureCount erasures

erasedAnnotationAxiomCount : List Erasure.AxiomErasure → ℕ
erasedAnnotationAxiomCount [] =
  zero
erasedAnnotationAxiomCount
  (Erasure.translatesToSemanticAxioms axioms ∷ erasures) =
  erasedAnnotationAxiomCount erasures
erasedAnnotationAxiomCount
  (Erasure.semanticallyErasedAnnotationAxiom ∷ erasures) =
  suc (erasedAnnotationAxiomCount erasures)
erasedAnnotationAxiomCount
  (Erasure.unsupportedByPortableSemantics ∷ erasures) =
  erasedAnnotationAxiomCount erasures

unsupportedAxiomErasureCount : List Erasure.AxiomErasure → ℕ
unsupportedAxiomErasureCount [] =
  zero
unsupportedAxiomErasureCount
  (Erasure.translatesToSemanticAxioms axioms ∷ erasures) =
  unsupportedAxiomErasureCount erasures
unsupportedAxiomErasureCount
  (Erasure.semanticallyErasedAnnotationAxiom ∷ erasures) =
  unsupportedAxiomErasureCount erasures
unsupportedAxiomErasureCount
  (Erasure.unsupportedByPortableSemantics ∷ erasures) =
  suc (unsupportedAxiomErasureCount erasures)

AnnotationErasureMatchesSemantics : P.OntologyDocument → Type₀
AnnotationErasureMatchesSemantics document =
  Erasure.eraseOntologyDocument document ≡
  Sem.semanticOntology (Sem.partialTranslateOntologyDocument document)

AnnotationErasureIgnoresAnnotations : P.OntologyDocument → Type₀
AnnotationErasureIgnoresAnnotations document =
  Erasure.eraseOntologyDocument document ≡
  Erasure.eraseOntologyDocument
    (Erasure.stripOntologyDocumentAnnotations document)

annotationErasureMatchesSemanticsProof :
  (document : P.OntologyDocument) →
  AnnotationErasureMatchesSemantics document
annotationErasureMatchesSemanticsProof =
  Erasure.eraseOntologyDocumentMatchesSemantics

annotationErasureIgnoresAnnotationsProof :
  (document : P.OntologyDocument) →
  AnnotationErasureIgnoresAnnotations document
annotationErasureIgnoresAnnotationsProof =
  Erasure.semanticErasureIgnoresAnnotations

record AnnotationErasureStatus
  (document : P.OntologyDocument) : Type₀ where
  constructor annotationErasureStatus
  field
    annotationErasureAxiomErasures :
      List Erasure.AxiomErasure
    annotationErasureTranslatedAxiomCount :
      ℕ
    annotationErasureErasedAnnotationAxiomCount :
      ℕ
    annotationErasureUnsupportedAxiomCount :
      ℕ
    annotationErasureErasedOntology :
      S.Ontology Sem.PortableSignature
    annotationErasureStrippedDocument :
      P.OntologyDocument
    annotationErasureMatchesSemantics :
      annotationErasureErasedOntology ≡
      Sem.semanticOntology (Sem.partialTranslateOntologyDocument document)
    annotationErasureIgnoresAnnotations :
      annotationErasureErasedOntology ≡
      Erasure.eraseOntologyDocument annotationErasureStrippedDocument

open AnnotationErasureStatus public

annotationErasureStatusFor :
  (document : P.OntologyDocument) → AnnotationErasureStatus document
annotationErasureStatusFor document =
  annotationErasureStatus
    erasures
    (translatedAxiomErasureCount erasures)
    (erasedAnnotationAxiomCount erasures)
    (unsupportedAxiomErasureCount erasures)
    (Erasure.eraseOntologyDocument document)
    (Erasure.stripOntologyDocumentAnnotations document)
    (annotationErasureMatchesSemanticsProof document)
    (annotationErasureIgnoresAnnotationsProof document)
  where
  erasures : List Erasure.AxiomErasure
  erasures =
    ontologyDocumentAxiomErasures document

record DocumentReport : Type₀ where
  constructor documentReport
  field
    documentReportDocument :
      P.OntologyDocument
    documentReportDeclarationFacts :
      List PK.DeclarationFact
    documentReportEntityUses :
      List Decl.EntityUseFact
    documentReportUndeclaredEntityUses :
      List Decl.UndeclaredEntityUse
    documentReportDeclarationRoleCollisions :
      List PK.DeclarationCollision
    documentReportPropertyRoleUsageConflicts :
      List PK.PropertyUsageConflict
    documentReportSemanticTranslation :
      Sem.SemanticTranslation
    documentReportSemanticUnsupportedAxioms :
      List (P.Annotated P.Axiom)
    documentReportAnnotationErasureStatus :
      AnnotationErasureStatus documentReportDocument
    documentReportDeclarationFactCount :
      ℕ
    documentReportEntityUseCount :
      ℕ
    documentReportUndeclaredEntityUseCount :
      ℕ
    documentReportDeclarationRoleCollisionCount :
      ℕ
    documentReportPropertyRoleUsageConflictCount :
      ℕ
    documentReportSemanticUnsupportedCount :
      ℕ

open DocumentReport public

reportDocument : P.OntologyDocument → DocumentReport
reportDocument document =
  documentReport
    document
    declarationFacts
    entityUses
    undeclaredUses
    declarationCollisions
    propertyUsageConflicts
    semanticTranslation
    semanticUnsupported
    (annotationErasureStatusFor document)
    (listCount declarationFacts)
    (listCount entityUses)
    (listCount undeclaredUses)
    (listCount declarationCollisions)
    (listCount propertyUsageConflicts)
    (listCount semanticUnsupported)
  where
  declarationFacts : List PK.DeclarationFact
  declarationFacts =
    PK.ontologyDocumentDeclarationFacts document

  entityUses : List Decl.EntityUseFact
  entityUses =
    Decl.ontologyDocumentEntityUses document

  undeclaredUses : List Decl.UndeclaredEntityUse
  undeclaredUses =
    Decl.ontologyDocumentUndeclaredEntityUses document

  declarationCollisions : List PK.DeclarationCollision
  declarationCollisions =
    PK.owl2DLOntologyDocumentDeclarationCollisions document

  propertyUsageConflicts : List PK.PropertyUsageConflict
  propertyUsageConflicts =
    PK.ontologyDocumentPropertyRoleUsageConflicts document

  semanticTranslation : Sem.SemanticTranslation
  semanticTranslation =
    Sem.partialTranslateOntologyDocument document

  semanticUnsupported : List (P.Annotated P.Axiom)
  semanticUnsupported =
    Sem.unsupported semanticTranslation

record ModuleReport : Type₀ where
  constructor moduleReport
  field
    moduleReportName :
      String
    moduleReportDocument :
      P.OntologyDocument
    moduleDocumentReport :
      DocumentReport

open ModuleReport public

reportModule : String → P.OntologyDocument → ModuleReport
reportModule name document =
  moduleReport name document (reportDocument document)

NoDeclarationCoverageGaps : P.OntologyDocument → Type₀
NoDeclarationCoverageGaps document =
  Decl.AllEntityUsesDeclared document

NoDeclarationRoleCollisions : P.OntologyDocument → Type₀
NoDeclarationRoleCollisions document =
  PK.OWL2DLDeclarationRolesConsistent document

NoPropertyRoleUsageConflicts : P.OntologyDocument → Type₀
NoPropertyRoleUsageConflicts document =
  PK.PropertyRoleUsageConsistent document

NoSemanticUnsupportedAxioms : P.OntologyDocument → Type₀
NoSemanticUnsupportedAxioms document =
  Sem.CompleteSemanticTranslation document

NoAnnotationErasureUnsupportedAxioms : P.OntologyDocument → Type₀
NoAnnotationErasureUnsupportedAxioms document =
  Erasure.unsupportedAxiomsOfOntologyDocument document ≡ []

NoReportDeclarationCoverageGaps : DocumentReport → Type₀
NoReportDeclarationCoverageGaps report =
  Decl.NoUndeclaredEntityUses
    (documentReportUndeclaredEntityUses report)

NoReportDeclarationRoleCollisions : DocumentReport → Type₀
NoReportDeclarationRoleCollisions report =
  PK.NoCollisions
    (documentReportDeclarationRoleCollisions report)

NoReportPropertyRoleUsageConflicts : DocumentReport → Type₀
NoReportPropertyRoleUsageConflicts report =
  PK.NoPropertyUsageConflicts
    (documentReportPropertyRoleUsageConflicts report)

NoReportSemanticUnsupportedAxioms : DocumentReport → Type₀
NoReportSemanticUnsupportedAxioms report =
  documentReportSemanticUnsupportedAxioms report ≡ []

NoReportAnnotationErasureUnsupportedAxioms :
  DocumentReport → Type₀
NoReportAnnotationErasureUnsupportedAxioms report =
  annotationErasureUnsupportedAxiomCount
    (documentReportAnnotationErasureStatus report)
  ≡ zero

record CleanReport (report : DocumentReport) : Type₀ where
  constructor cleanReport
  field
    cleanReportDeclarationCoverage :
      NoReportDeclarationCoverageGaps report
    cleanReportDeclarationRoles :
      NoReportDeclarationRoleCollisions report
    cleanReportPropertyRoles :
      NoReportPropertyRoleUsageConflicts report
    cleanReportSemanticTranslation :
      NoReportSemanticUnsupportedAxioms report
    cleanReportAnnotationErasure :
      NoReportAnnotationErasureUnsupportedAxioms report

open CleanReport public

CleanDocument : P.OntologyDocument → Type₀
CleanDocument document =
  CleanReport (reportDocument document)

record CompleteWebProtegeDocument
  (document : P.OntologyDocument) : Type₀ where
  constructor completeWebProtegeDocument
  field
    completeDocumentDeclarationCoverage :
      NoDeclarationCoverageGaps document
    completeDocumentDeclarationRoles :
      NoDeclarationRoleCollisions document
    completeDocumentPropertyRoles :
      NoPropertyRoleUsageConflicts document
    completeDocumentSemanticTranslation :
      NoSemanticUnsupportedAxioms document
    completeDocumentAnnotationErasureUnsupported :
      NoAnnotationErasureUnsupportedAxioms document
    completeDocumentAnnotationErasureMatchesSemantics :
      AnnotationErasureMatchesSemantics document
    completeDocumentAnnotationErasureIgnoresAnnotations :
      AnnotationErasureIgnoresAnnotations document

open CompleteWebProtegeDocument public