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

module OWL2.OBOGraph.Report where

open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
import OWL2.OBOGraph.References as Ref
open import OWL2.OBOGraph.Syntax
import OWL2.OBOGraph.Validate as V
import OWL2.Portable.Declarations as Decl
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Syntax as P

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

record GraphShapeCounts : Type₀ where
  constructor graphShapeCounts
  field
    shapeNodeCount :
      ℕ
    shapeEdgeCount :
      ℕ
    shapeEquivalentNodesSetCount :
      ℕ
    shapeLogicalDefinitionAxiomCount :
      ℕ
    shapeDomainRangeAxiomCount :
      ℕ
    shapePropertyChainAxiomCount :
      ℕ

open GraphShapeCounts public

shapeCounts : Graph → GraphShapeCounts
shapeCounts g =
  graphShapeCounts
    (listCount (nodes g))
    (listCount (edges g))
    (listCount (equivalentNodesSets g))
    (listCount (logicalDefinitionAxioms g))
    (listCount (domainRangeAxioms g))
    (listCount (propertyChainAxioms g))

documentShapeCounts : GraphDocument → List GraphShapeCounts
documentShapeCounts (graphDocument []) =
  []
documentShapeCounts (graphDocument (g ∷ gs)) =
  shapeCounts g ∷ documentShapeCounts (graphDocument gs)

record GraphReport : Type₀ where
  constructor graphReport
  field
    graphReportId :
      Optional String
    graphReportShape :
      GraphShapeCounts
    graphReportMetaUnsupportedEntries :
      List V.MetaUnsupportedEntry
    graphReportGraphUnsupportedEntries :
      List V.GraphUnsupportedEntry
    graphReportSourceReferenceCoverageGaps :
      List Ref.MissingNodeReference
    graphReportImportWarningAssertions :
      List V.ImportWarningAssertion
    graphReportSemanticUnsupportedAxioms :
      List (P.Annotated P.Axiom)
    graphReportDeclarationRoleCollisions :
      List PK.DeclarationCollision
    graphReportPropertyRoleUsageConflicts :
      List PK.PropertyUsageConflict
    graphReportUndeclaredEntityUses :
      List Decl.UndeclaredEntityUse
    graphReportMetaUnsupportedCount :
      ℕ
    graphReportGraphUnsupportedCount :
      ℕ
    graphReportSourceReferenceCoverageGapCount :
      ℕ
    graphReportImportWarningCount :
      ℕ
    graphReportSemanticUnsupportedCount :
      ℕ
    graphReportDeclarationRoleCollisionCount :
      ℕ
    graphReportPropertyRoleUsageConflictCount :
      ℕ
    graphReportUndeclaredEntityUseCount :
      ℕ

open GraphReport public

reportGraph : Graph → GraphReport
reportGraph g =
  graphReport
    (graphId g)
    (shapeCounts g)
    metaEntries
    graphEntries
    sourceReferenceGaps
    importWarnings
    semanticUnsupported
    declarationCollisions
    propertyUsageConflicts
    undeclaredUses
    (listCount metaEntries)
    (listCount graphEntries)
    (listCount sourceReferenceGaps)
    (listCount importWarnings)
    (listCount semanticUnsupported)
    (listCount declarationCollisions)
    (listCount propertyUsageConflicts)
    (listCount undeclaredUses)
  where
  metaEntries : List V.MetaUnsupportedEntry
  metaEntries =
    V.metaUnsupportedEntriesInGraph g

  graphEntries : List V.GraphUnsupportedEntry
  graphEntries =
    V.graphUnsupportedEntriesInGraph g

  sourceReferenceGaps : List Ref.MissingNodeReference
  sourceReferenceGaps =
    V.sourceReferenceCoverageGapsInGraph g

  importWarnings : List V.ImportWarningAssertion
  importWarnings =
    V.importWarningAssertionsInGraph g

  semanticUnsupported : List (P.Annotated P.Axiom)
  semanticUnsupported =
    V.semanticUnsupportedAxiomsInGraph g

  declarationCollisions : List PK.DeclarationCollision
  declarationCollisions =
    V.declarationRoleCollisionsInGraph g

  propertyUsageConflicts : List PK.PropertyUsageConflict
  propertyUsageConflicts =
    V.propertyRoleUsageConflictsInGraph g

  undeclaredUses : List Decl.UndeclaredEntityUse
  undeclaredUses =
    V.undeclaredEntityUsesInGraph g

record DocumentReport : Type₀ where
  constructor documentReport
  field
    documentReportGraphs :
      List GraphReport
    documentReportMetaUnsupportedEntries :
      List V.MetaUnsupportedEntry
    documentReportGraphUnsupportedEntries :
      List V.GraphUnsupportedEntry
    documentReportSourceReferenceCoverageGaps :
      List Ref.MissingNodeReference
    documentReportImportWarningAssertions :
      List V.ImportWarningAssertion
    documentReportSemanticUnsupportedAxioms :
      List (P.Annotated P.Axiom)
    documentReportDeclarationRoleCollisions :
      List PK.DeclarationCollision
    documentReportPropertyRoleUsageConflicts :
      List PK.PropertyUsageConflict
    documentReportUndeclaredEntityUses :
      List Decl.UndeclaredEntityUse
    documentReportMetaUnsupportedCount :
      ℕ
    documentReportGraphUnsupportedCount :
      ℕ
    documentReportSourceReferenceCoverageGapCount :
      ℕ
    documentReportImportWarningCount :
      ℕ
    documentReportSemanticUnsupportedCount :
      ℕ
    documentReportDeclarationRoleCollisionCount :
      ℕ
    documentReportPropertyRoleUsageConflictCount :
      ℕ
    documentReportUndeclaredEntityUseCount :
      ℕ

open DocumentReport public

reportDocument : GraphDocument → DocumentReport
reportDocument doc@(graphDocument gs) =
  documentReport
    (map reportGraph gs)
    metaEntries
    graphEntries
    sourceReferenceGaps
    importWarnings
    semanticUnsupported
    declarationCollisions
    propertyUsageConflicts
    undeclaredUses
    (listCount metaEntries)
    (listCount graphEntries)
    (listCount sourceReferenceGaps)
    (listCount importWarnings)
    (listCount semanticUnsupported)
    (listCount declarationCollisions)
    (listCount propertyUsageConflicts)
    (listCount undeclaredUses)
  where
  metaEntries : List V.MetaUnsupportedEntry
  metaEntries =
    V.metaUnsupportedEntriesInDocument doc

  graphEntries : List V.GraphUnsupportedEntry
  graphEntries =
    V.graphUnsupportedEntriesInDocument doc

  sourceReferenceGaps : List Ref.MissingNodeReference
  sourceReferenceGaps =
    V.sourceReferenceCoverageGapsInDocument doc

  importWarnings : List V.ImportWarningAssertion
  importWarnings =
    V.importWarningAssertionsInDocument doc

  semanticUnsupported : List (P.Annotated P.Axiom)
  semanticUnsupported =
    V.semanticUnsupportedAxiomsInDocument doc

  declarationCollisions : List PK.DeclarationCollision
  declarationCollisions =
    V.declarationRoleCollisionsInDocument doc

  propertyUsageConflicts : List PK.PropertyUsageConflict
  propertyUsageConflicts =
    V.propertyRoleUsageConflictsInDocument doc

  undeclaredUses : List Decl.UndeclaredEntityUse
  undeclaredUses =
    V.undeclaredEntityUsesInDocument doc

record ModuleReport : Type₀ where
  constructor moduleReport
  field
    moduleReportName :
      String
    moduleDocumentReport :
      DocumentReport

open ModuleReport public

reportModule : String → GraphDocument → ModuleReport
reportModule name doc =
  moduleReport name (reportDocument doc)