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

module OWL2.OBOGraph.Validate where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Foundation.Maybe
open import OWL2.OBOGraph.Syntax
import OWL2.OBOGraph.References as Ref
import OWL2.OBOGraph.ToPortable as OGP
import OWL2.Portable.Declarations as Decl
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P

private
  concatMap : ∀ {ℓA ℓB} {A : Type ℓA} {B : Type ℓB} →
              (A → List B) → List A → List B
  concatMap f [] =
    []
  concatMap f (x ∷ xs) =
    f x ++ concatMap f xs

  singleGraphDocument : Graph → GraphDocument
  singleGraphDocument g =
    graphDocument (g ∷ [])

  validationCode : String → DiagnosticCode
  validationCode name =
    mkDiagnosticCode "obograph.validate" name

  diagnosticsForList :
    ∀ {A : Type₀} → (A → Diagnostic) → List A → Diagnostics
  diagnosticsForList diagnosticFor [] =
    []
  diagnosticsForList diagnosticFor (x ∷ xs) =
    diagnosticFor x ∷ diagnosticsForList diagnosticFor xs

  emptyListFromCleanDiagnostics :
    ∀ {A : Type₀}
      (diagnosticFor : A → Diagnostic)
      (xs : List A) →
    CleanDiagnostics (diagnosticsForList diagnosticFor xs) →
    xs ≡ []
  emptyListFromCleanDiagnostics diagnosticFor [] clean =
    refl
  emptyListFromCleanDiagnostics diagnosticFor (x ∷ xs) ()

data MetaSubject : Type₀ where
  graphMetaSubject :
    Optional String → MetaSubject
  nodeMetaSubject :
    String → MetaSubject
  edgeMetaSubject :
    String → String → String → MetaSubject
  equivalentNodesSetMetaSubject :
    Optional String → List String → MetaSubject

record MetaUnsupportedEntry : Type₀ where
  constructor metaUnsupportedEntry
  field
    metaUnsupportedSubject : MetaSubject
    metaUnsupportedText    : String

open MetaUnsupportedEntry public

record GraphUnsupportedEntry : Type₀ where
  constructor graphUnsupportedEntry
  field
    graphUnsupportedEntryGraphId : Optional String
    graphUnsupportedEntryText    : String

open GraphUnsupportedEntry public

record ImportWarningAssertion : Type₀ where
  constructor importWarningAssertion
  field
    importWarningSubject : P.AnnotationSubject
    importWarningValue   : P.AnnotationValue
    importWarningAxiom   : P.Annotated P.Axiom

open ImportWarningAssertion public

metaUnsupportedEntriesFor : MetaSubject → Meta → List MetaUnsupportedEntry
metaUnsupportedEntriesFor subject m =
  map (metaUnsupportedEntry subject) (unsupported m)

metaUnsupportedEntriesInNode : Node → List MetaUnsupportedEntry
metaUnsupportedEntriesInNode n =
  metaUnsupportedEntriesFor (nodeMetaSubject (nodeId n)) (nodeMeta n)

metaUnsupportedEntriesInEdge : Edge → List MetaUnsupportedEntry
metaUnsupportedEntriesInEdge e =
  metaUnsupportedEntriesFor
    (edgeMetaSubject (edgeSubject e) (edgePredicate e) (edgeObject e))
    (edgeMeta e)

metaUnsupportedEntriesInEquivalentNodesSet :
  EquivalentNodesSet → List MetaUnsupportedEntry
metaUnsupportedEntriesInEquivalentNodesSet s =
  metaUnsupportedEntriesFor
    (equivalentNodesSetMetaSubject (representativeNodeId s) (nodeIds s))
    (equivalentMeta s)

metaUnsupportedEntriesInGraph : Graph → List MetaUnsupportedEntry
metaUnsupportedEntriesInGraph g =
  metaUnsupportedEntriesFor (graphMetaSubject (graphId g)) (graphMeta g)
  ++ concatMap metaUnsupportedEntriesInNode (nodes g)
  ++ concatMap metaUnsupportedEntriesInEdge (edges g)
  ++ concatMap
       metaUnsupportedEntriesInEquivalentNodesSet
       (equivalentNodesSets g)

metaUnsupportedEntriesInDocument : GraphDocument → List MetaUnsupportedEntry
metaUnsupportedEntriesInDocument (graphDocument gs) =
  concatMap metaUnsupportedEntriesInGraph gs

graphUnsupportedEntriesInGraph : Graph → List GraphUnsupportedEntry
graphUnsupportedEntriesInGraph g =
  map (graphUnsupportedEntry (graphId g)) (graphUnsupported g)

graphUnsupportedEntriesInDocument : GraphDocument → List GraphUnsupportedEntry
graphUnsupportedEntriesInDocument (graphDocument gs) =
  concatMap graphUnsupportedEntriesInGraph gs

SourceReferenceCoverageGap : Type₀
SourceReferenceCoverageGap =
  Ref.MissingNodeReference

sourceReferenceCoverageGapsInGraph :
  Graph → List SourceReferenceCoverageGap
sourceReferenceCoverageGapsInGraph =
  Ref.missingNodeReferencesInGraph

sourceReferenceCoverageGapsInDocument :
  GraphDocument → List SourceReferenceCoverageGap
sourceReferenceCoverageGapsInDocument =
  Ref.missingNodeReferencesInDocument

importWarningAssertionFromAxiom :
  P.Annotated P.Axiom → P.Axiom → Optional ImportWarningAssertion
importWarningAssertionFromAxiom ax (P.annotationAssertion property subject value)
  with primStringEquality (P.payload property) OGP.ffImportWarning
... | true =
  present (importWarningAssertion subject value ax)
... | false =
  absent
importWarningAssertionFromAxiom ax _ =
  absent

importWarningAssertions : P.OntologyDocument → List ImportWarningAssertion
importWarningAssertions doc =
  filterMap
    (λ ax → importWarningAssertionFromAxiom ax (P.body ax))
    (P.axioms (P.documentOntology doc))

semanticUnsupportedAxioms :
  P.OntologyDocument → List (P.Annotated P.Axiom)
semanticUnsupportedAxioms doc =
  Sem.unsupported (Sem.partialTranslateOntologyDocument doc)

declarationRoleCollisions :
  P.OntologyDocument → List PK.DeclarationCollision
declarationRoleCollisions doc =
  PK.owl2DLOntologyDocumentDeclarationCollisions doc

propertyRoleUsageConflicts :
  P.OntologyDocument → List PK.PropertyUsageConflict
propertyRoleUsageConflicts doc =
  PK.ontologyDocumentPropertyRoleUsageConflicts doc

undeclaredEntityUses :
  P.OntologyDocument → List Decl.UndeclaredEntityUse
undeclaredEntityUses doc =
  Decl.ontologyDocumentUndeclaredEntityUses doc

importWarningAssertionsInGraph : Graph → List ImportWarningAssertion
importWarningAssertionsInGraph g =
  importWarningAssertions (OGP.toOntologyDocument (singleGraphDocument g))

importWarningAssertionsInDocument : GraphDocument → List ImportWarningAssertion
importWarningAssertionsInDocument doc =
  importWarningAssertions (OGP.toOntologyDocument doc)

semanticUnsupportedAxiomsInGraph :
  Graph → List (P.Annotated P.Axiom)
semanticUnsupportedAxiomsInGraph g =
  semanticUnsupportedAxioms (OGP.toOntologyDocument (singleGraphDocument g))

semanticUnsupportedAxiomsInDocument :
  GraphDocument → List (P.Annotated P.Axiom)
semanticUnsupportedAxiomsInDocument doc =
  semanticUnsupportedAxioms (OGP.toOntologyDocument doc)

declarationRoleCollisionsInGraph :
  Graph → List PK.DeclarationCollision
declarationRoleCollisionsInGraph g =
  declarationRoleCollisions (OGP.toOntologyDocument (singleGraphDocument g))

declarationRoleCollisionsInDocument :
  GraphDocument → List PK.DeclarationCollision
declarationRoleCollisionsInDocument doc =
  declarationRoleCollisions (OGP.toOntologyDocument doc)

propertyRoleUsageConflictsInGraph :
  Graph → List PK.PropertyUsageConflict
propertyRoleUsageConflictsInGraph g =
  propertyRoleUsageConflicts (OGP.toOntologyDocument (singleGraphDocument g))

propertyRoleUsageConflictsInDocument :
  GraphDocument → List PK.PropertyUsageConflict
propertyRoleUsageConflictsInDocument doc =
  propertyRoleUsageConflicts (OGP.toOntologyDocument doc)

undeclaredEntityUsesInGraph :
  Graph → List Decl.UndeclaredEntityUse
undeclaredEntityUsesInGraph g =
  undeclaredEntityUses (OGP.toOntologyDocument (singleGraphDocument g))

undeclaredEntityUsesInDocument :
  GraphDocument → List Decl.UndeclaredEntityUse
undeclaredEntityUsesInDocument doc =
  undeclaredEntityUses (OGP.toOntologyDocument doc)

NoMetaUnsupportedInGraph : Graph → Type₀
NoMetaUnsupportedInGraph g =
  metaUnsupportedEntriesInGraph g ≡ []

NoMetaUnsupportedInDocument : GraphDocument → Type₀
NoMetaUnsupportedInDocument doc =
  metaUnsupportedEntriesInDocument doc ≡ []

NoGraphUnsupportedInGraph : Graph → Type₀
NoGraphUnsupportedInGraph g =
  graphUnsupportedEntriesInGraph g ≡ []

NoGraphUnsupportedInDocument : GraphDocument → Type₀
NoGraphUnsupportedInDocument doc =
  graphUnsupportedEntriesInDocument doc ≡ []

NoSourceReferenceCoverageGapsInGraph : Graph → Type₀
NoSourceReferenceCoverageGapsInGraph g =
  Ref.NoMissingNodeReferences (sourceReferenceCoverageGapsInGraph g)

NoSourceReferenceCoverageGapsInDocument : GraphDocument → Type₀
NoSourceReferenceCoverageGapsInDocument doc =
  Ref.NoMissingNodeReferences (sourceReferenceCoverageGapsInDocument doc)

NoImportWarningAssertions : P.OntologyDocument → Type₀
NoImportWarningAssertions doc =
  importWarningAssertions doc ≡ []

NoImportWarningAssertionsInGraph : Graph → Type₀
NoImportWarningAssertionsInGraph g =
  importWarningAssertionsInGraph g ≡ []

NoImportWarningAssertionsInDocument : GraphDocument → Type₀
NoImportWarningAssertionsInDocument doc =
  importWarningAssertionsInDocument doc ≡ []

NoSemanticUnsupportedAxioms : P.OntologyDocument → Type₀
NoSemanticUnsupportedAxioms doc =
  semanticUnsupportedAxioms doc ≡ []

NoSemanticUnsupportedAxiomsInGraph : Graph → Type₀
NoSemanticUnsupportedAxiomsInGraph g =
  semanticUnsupportedAxiomsInGraph g ≡ []

NoSemanticUnsupportedAxiomsInDocument : GraphDocument → Type₀
NoSemanticUnsupportedAxiomsInDocument doc =
  semanticUnsupportedAxiomsInDocument doc ≡ []

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

NoDeclarationRoleCollisionsInGraph : Graph → Type₀
NoDeclarationRoleCollisionsInGraph g =
  PK.NoCollisions (declarationRoleCollisionsInGraph g)

NoDeclarationRoleCollisionsInDocument : GraphDocument → Type₀
NoDeclarationRoleCollisionsInDocument doc =
  PK.NoCollisions (declarationRoleCollisionsInDocument doc)

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

NoPropertyRoleUsageConflictsInGraph : Graph → Type₀
NoPropertyRoleUsageConflictsInGraph g =
  PK.NoPropertyUsageConflicts (propertyRoleUsageConflictsInGraph g)

NoPropertyRoleUsageConflictsInDocument : GraphDocument → Type₀
NoPropertyRoleUsageConflictsInDocument doc =
  PK.NoPropertyUsageConflicts (propertyRoleUsageConflictsInDocument doc)

NoUndeclaredEntityUses : P.OntologyDocument → Type₀
NoUndeclaredEntityUses doc =
  Decl.AllEntityUsesDeclared doc

NoUndeclaredEntityUsesInGraph : Graph → Type₀
NoUndeclaredEntityUsesInGraph g =
  Decl.NoUndeclaredEntityUses (undeclaredEntityUsesInGraph g)

NoUndeclaredEntityUsesInDocument : GraphDocument → Type₀
NoUndeclaredEntityUsesInDocument doc =
  Decl.NoUndeclaredEntityUses (undeclaredEntityUsesInDocument doc)

record CompleteGraph (g : Graph) : Type₀ where
  constructor completeGraph
  field
    completeGraphMetaUnsupported :
      NoMetaUnsupportedInGraph g
    completeGraphUnsupported :
      NoGraphUnsupportedInGraph g
    completeGraphSourceReferenceCoverage :
      NoSourceReferenceCoverageGapsInGraph g
    completeGraphImportWarnings :
      NoImportWarningAssertionsInGraph g
    completeGraphSemanticUnsupported :
      NoSemanticUnsupportedAxiomsInGraph g
    completeGraphDeclarationRoleCollisions :
      NoDeclarationRoleCollisionsInGraph g
    completeGraphPropertyRoleUsageConflicts :
      NoPropertyRoleUsageConflictsInGraph g
    completeGraphUndeclaredEntityUses :
      NoUndeclaredEntityUsesInGraph g

open CompleteGraph public

record CompleteGraphDocument (doc : GraphDocument) : Type₀ where
  constructor completeGraphDocument
  field
    completeDocumentMetaUnsupported :
      NoMetaUnsupportedInDocument doc
    completeDocumentGraphUnsupported :
      NoGraphUnsupportedInDocument doc
    completeDocumentSourceReferenceCoverage :
      NoSourceReferenceCoverageGapsInDocument doc
    completeDocumentImportWarnings :
      NoImportWarningAssertionsInDocument doc
    completeDocumentSemanticUnsupported :
      NoSemanticUnsupportedAxiomsInDocument doc
    completeDocumentDeclarationRoleCollisions :
      NoDeclarationRoleCollisionsInDocument doc
    completeDocumentPropertyRoleUsageConflicts :
      NoPropertyRoleUsageConflictsInDocument doc
    completeDocumentUndeclaredEntityUses :
      NoUndeclaredEntityUsesInDocument doc

open CompleteGraphDocument public

metaUnsupportedDiagnostic : MetaUnsupportedEntry → Diagnostic
metaUnsupportedDiagnostic entry =
  diagnostic
    (validationCode "meta-unsupported")
    severityError
    rootSourcePath
    (metaUnsupportedText entry)

graphUnsupportedDiagnostic : GraphUnsupportedEntry → Diagnostic
graphUnsupportedDiagnostic entry =
  diagnostic
    (validationCode "graph-unsupported")
    severityError
    rootSourcePath
    (graphUnsupportedEntryText entry)

sourceReferenceCoverageGapDiagnostic :
  SourceReferenceCoverageGap → Diagnostic
sourceReferenceCoverageGapDiagnostic gap =
  diagnostic
    (validationCode "source-reference-coverage-gap")
    severityError
    rootSourcePath
    "OBOGraph source reference points at a node not declared in its graph."

importWarningDiagnostic : ImportWarningAssertion → Diagnostic
importWarningDiagnostic warning =
  diagnostic
    (validationCode "import-warning-annotation")
    severityError
    rootSourcePath
    "OBOGraph import emitted a warning annotation."

semanticUnsupportedDiagnostic : P.Annotated P.Axiom → Diagnostic
semanticUnsupportedDiagnostic axiom =
  diagnostic
    (validationCode "semantic-unsupported-axiom")
    severityError
    rootSourcePath
    "Portable axiom is outside the implemented semantic translation."

declarationRoleCollisionDiagnostic : PK.DeclarationCollision → Diagnostic
declarationRoleCollisionDiagnostic collision =
  diagnostic
    (validationCode "declaration-role-collision")
    severityError
    rootSourcePath
    "Portable translation declares one entity IRI with incompatible roles."

propertyRoleUsageConflictDiagnostic : PK.PropertyUsageConflict → Diagnostic
propertyRoleUsageConflictDiagnostic conflict =
  diagnostic
    (validationCode "property-role-usage-conflict")
    severityError
    rootSourcePath
    "Portable translation uses one property IRI with incompatible roles."

undeclaredEntityUseDiagnostic : Decl.UndeclaredEntityUse → Diagnostic
undeclaredEntityUseDiagnostic use =
  diagnostic
    (validationCode "undeclared-entity-use")
    severityError
    rootSourcePath
    "Portable translation uses an entity not covered by declarations."

metaUnsupportedDiagnostics :
  List MetaUnsupportedEntry → Diagnostics
metaUnsupportedDiagnostics =
  diagnosticsForList metaUnsupportedDiagnostic

graphUnsupportedDiagnostics :
  List GraphUnsupportedEntry → Diagnostics
graphUnsupportedDiagnostics =
  diagnosticsForList graphUnsupportedDiagnostic

sourceReferenceCoverageGapDiagnostics :
  List SourceReferenceCoverageGap → Diagnostics
sourceReferenceCoverageGapDiagnostics =
  diagnosticsForList sourceReferenceCoverageGapDiagnostic

importWarningDiagnostics :
  List ImportWarningAssertion → Diagnostics
importWarningDiagnostics =
  diagnosticsForList importWarningDiagnostic

semanticUnsupportedDiagnostics :
  List (P.Annotated P.Axiom) → Diagnostics
semanticUnsupportedDiagnostics =
  diagnosticsForList semanticUnsupportedDiagnostic

declarationRoleCollisionDiagnostics :
  List PK.DeclarationCollision → Diagnostics
declarationRoleCollisionDiagnostics =
  diagnosticsForList declarationRoleCollisionDiagnostic

propertyRoleUsageConflictDiagnostics :
  List PK.PropertyUsageConflict → Diagnostics
propertyRoleUsageConflictDiagnostics =
  diagnosticsForList propertyRoleUsageConflictDiagnostic

undeclaredEntityUseDiagnostics :
  List Decl.UndeclaredEntityUse → Diagnostics
undeclaredEntityUseDiagnostics =
  diagnosticsForList undeclaredEntityUseDiagnostic

graphDocumentValidationDiagnostics : GraphDocument → Diagnostics
graphDocumentValidationDiagnostics doc =
  metaUnsupportedDiagnostics
    (metaUnsupportedEntriesInDocument doc)
  ++
  graphUnsupportedDiagnostics
    (graphUnsupportedEntriesInDocument doc)
  ++
  sourceReferenceCoverageGapDiagnostics
    (sourceReferenceCoverageGapsInDocument doc)
  ++
  importWarningDiagnostics
    (importWarningAssertionsInDocument doc)
  ++
  semanticUnsupportedDiagnostics
    (semanticUnsupportedAxiomsInDocument doc)
  ++
  declarationRoleCollisionDiagnostics
    (declarationRoleCollisionsInDocument doc)
  ++
  propertyRoleUsageConflictDiagnostics
    (propertyRoleUsageConflictsInDocument doc)
  ++
  undeclaredEntityUseDiagnostics
    (undeclaredEntityUsesInDocument doc)

noMetaUnsupportedFromDiagnostics :
  (entries : List MetaUnsupportedEntry) →
  CleanDiagnostics (metaUnsupportedDiagnostics entries) →
  entries ≡ []
noMetaUnsupportedFromDiagnostics =
  emptyListFromCleanDiagnostics metaUnsupportedDiagnostic

noGraphUnsupportedFromDiagnostics :
  (entries : List GraphUnsupportedEntry) →
  CleanDiagnostics (graphUnsupportedDiagnostics entries) →
  entries ≡ []
noGraphUnsupportedFromDiagnostics =
  emptyListFromCleanDiagnostics graphUnsupportedDiagnostic

noSourceReferenceCoverageGapsFromDiagnostics :
  (gaps : List SourceReferenceCoverageGap) →
  CleanDiagnostics (sourceReferenceCoverageGapDiagnostics gaps) →
  Ref.NoMissingNodeReferences gaps
noSourceReferenceCoverageGapsFromDiagnostics [] clean =
  tt*
noSourceReferenceCoverageGapsFromDiagnostics (gap ∷ gaps) ()

noImportWarningsFromDiagnostics :
  (warnings : List ImportWarningAssertion) →
  CleanDiagnostics (importWarningDiagnostics warnings) →
  warnings ≡ []
noImportWarningsFromDiagnostics =
  emptyListFromCleanDiagnostics importWarningDiagnostic

noSemanticUnsupportedFromDiagnostics :
  (axioms : List (P.Annotated P.Axiom)) →
  CleanDiagnostics (semanticUnsupportedDiagnostics axioms) →
  axioms ≡ []
noSemanticUnsupportedFromDiagnostics =
  emptyListFromCleanDiagnostics semanticUnsupportedDiagnostic

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

noPropertyRoleUsageConflictsFromDiagnostics :
  (conflicts : List PK.PropertyUsageConflict) →
  CleanDiagnostics (propertyRoleUsageConflictDiagnostics conflicts) →
  PK.NoPropertyUsageConflicts conflicts
noPropertyRoleUsageConflictsFromDiagnostics [] clean =
  tt*
noPropertyRoleUsageConflictsFromDiagnostics (conflict ∷ conflicts) ()

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

graphDocumentCompleteFromCleanDiagnostics :
  (doc : GraphDocument) →
  CleanDiagnostics (graphDocumentValidationDiagnostics doc) →
  CompleteGraphDocument doc
graphDocumentCompleteFromCleanDiagnostics doc clean =
  completeGraphDocument
    (noMetaUnsupportedFromDiagnostics metas metasClean)
    (noGraphUnsupportedFromDiagnostics
      graphUnsupportedEntries
      graphUnsupportedEntriesClean)
    (noSourceReferenceCoverageGapsFromDiagnostics
      sourceReferenceCoverageGaps
      sourceReferenceCoverageGapsClean)
    (noImportWarningsFromDiagnostics importWarnings importWarningsClean)
    (noSemanticUnsupportedFromDiagnostics
      semanticUnsupportedEntries
      semanticUnsupportedEntriesClean)
    (noDeclarationRoleCollisionsFromDiagnostics
      declarationRoleCollisionEntries
      declarationRoleCollisionEntriesClean)
    (noPropertyRoleUsageConflictsFromDiagnostics
      propertyRoleUsageConflictEntries
      propertyRoleUsageConflictEntriesClean)
    (noUndeclaredEntityUsesFromDiagnostics
      undeclaredEntityUseEntries
      undeclaredEntityUseEntriesClean)
  where
  metas : List MetaUnsupportedEntry
  metas =
    metaUnsupportedEntriesInDocument doc

  graphUnsupportedEntries : List GraphUnsupportedEntry
  graphUnsupportedEntries =
    graphUnsupportedEntriesInDocument doc

  sourceReferenceCoverageGaps : List SourceReferenceCoverageGap
  sourceReferenceCoverageGaps =
    sourceReferenceCoverageGapsInDocument doc

  importWarnings : List ImportWarningAssertion
  importWarnings =
    importWarningAssertionsInDocument doc

  semanticUnsupportedEntries : List (P.Annotated P.Axiom)
  semanticUnsupportedEntries =
    semanticUnsupportedAxiomsInDocument doc

  declarationRoleCollisionEntries : List PK.DeclarationCollision
  declarationRoleCollisionEntries =
    declarationRoleCollisionsInDocument doc

  propertyRoleUsageConflictEntries : List PK.PropertyUsageConflict
  propertyRoleUsageConflictEntries =
    propertyRoleUsageConflictsInDocument doc

  undeclaredEntityUseEntries : List Decl.UndeclaredEntityUse
  undeclaredEntityUseEntries =
    undeclaredEntityUsesInDocument doc

  metasDiagnostics : Diagnostics
  metasDiagnostics =
    metaUnsupportedDiagnostics metas

  graphUnsupportedEntryDiagnostics : Diagnostics
  graphUnsupportedEntryDiagnostics =
    graphUnsupportedDiagnostics graphUnsupportedEntries

  sourceReferenceCoverageGapsDiagnostics : Diagnostics
  sourceReferenceCoverageGapsDiagnostics =
    sourceReferenceCoverageGapDiagnostics sourceReferenceCoverageGaps

  importWarningsDiagnostics : Diagnostics
  importWarningsDiagnostics =
    importWarningDiagnostics importWarnings

  semanticUnsupportedEntryDiagnostics : Diagnostics
  semanticUnsupportedEntryDiagnostics =
    semanticUnsupportedDiagnostics semanticUnsupportedEntries

  declarationRoleCollisionEntryDiagnostics : Diagnostics
  declarationRoleCollisionEntryDiagnostics =
    declarationRoleCollisionDiagnostics declarationRoleCollisionEntries

  propertyRoleUsageConflictEntryDiagnostics : Diagnostics
  propertyRoleUsageConflictEntryDiagnostics =
    propertyRoleUsageConflictDiagnostics propertyRoleUsageConflictEntries

  undeclaredEntityUseEntryDiagnostics : Diagnostics
  undeclaredEntityUseEntryDiagnostics =
    undeclaredEntityUseDiagnostics undeclaredEntityUseEntries

  rest₀ : Diagnostics
  rest₀ =
    graphUnsupportedEntryDiagnostics
    ++ sourceReferenceCoverageGapsDiagnostics
    ++ importWarningsDiagnostics
    ++ semanticUnsupportedEntryDiagnostics
    ++ declarationRoleCollisionEntryDiagnostics
    ++ propertyRoleUsageConflictEntryDiagnostics
    ++ undeclaredEntityUseEntryDiagnostics

  rest₁ : Diagnostics
  rest₁ =
    sourceReferenceCoverageGapsDiagnostics
    ++ importWarningsDiagnostics
    ++ semanticUnsupportedEntryDiagnostics
    ++ declarationRoleCollisionEntryDiagnostics
    ++ propertyRoleUsageConflictEntryDiagnostics
    ++ undeclaredEntityUseEntryDiagnostics

  rest₂ : Diagnostics
  rest₂ =
    importWarningsDiagnostics
    ++ semanticUnsupportedEntryDiagnostics
    ++ declarationRoleCollisionEntryDiagnostics
    ++ propertyRoleUsageConflictEntryDiagnostics
    ++ undeclaredEntityUseEntryDiagnostics

  rest₃ : Diagnostics
  rest₃ =
    semanticUnsupportedEntryDiagnostics
    ++ declarationRoleCollisionEntryDiagnostics
    ++ propertyRoleUsageConflictEntryDiagnostics
    ++ undeclaredEntityUseEntryDiagnostics

  rest₄ : Diagnostics
  rest₄ =
    declarationRoleCollisionEntryDiagnostics
    ++ propertyRoleUsageConflictEntryDiagnostics
    ++ undeclaredEntityUseEntryDiagnostics

  rest₅ : Diagnostics
  rest₅ =
    propertyRoleUsageConflictEntryDiagnostics
    ++ undeclaredEntityUseEntryDiagnostics

  metasClean : CleanDiagnostics metasDiagnostics
  metasClean =
    cleanAppendLeft metasDiagnostics rest₀ clean

  rest₀Clean : CleanDiagnostics rest₀
  rest₀Clean =
    cleanAppendRight metasDiagnostics rest₀ clean

  graphUnsupportedEntriesClean :
    CleanDiagnostics graphUnsupportedEntryDiagnostics
  graphUnsupportedEntriesClean =
    cleanAppendLeft graphUnsupportedEntryDiagnostics rest₁ rest₀Clean

  rest₁Clean : CleanDiagnostics rest₁
  rest₁Clean =
    cleanAppendRight graphUnsupportedEntryDiagnostics rest₁ rest₀Clean

  sourceReferenceCoverageGapsClean :
    CleanDiagnostics sourceReferenceCoverageGapsDiagnostics
  sourceReferenceCoverageGapsClean =
    cleanAppendLeft
      sourceReferenceCoverageGapsDiagnostics
      rest₂
      rest₁Clean

  rest₂Clean : CleanDiagnostics rest₂
  rest₂Clean =
    cleanAppendRight
      sourceReferenceCoverageGapsDiagnostics
      rest₂
      rest₁Clean

  importWarningsClean : CleanDiagnostics importWarningsDiagnostics
  importWarningsClean =
    cleanAppendLeft importWarningsDiagnostics rest₃ rest₂Clean

  rest₃Clean : CleanDiagnostics rest₃
  rest₃Clean =
    cleanAppendRight importWarningsDiagnostics rest₃ rest₂Clean

  semanticUnsupportedEntriesClean :
    CleanDiagnostics semanticUnsupportedEntryDiagnostics
  semanticUnsupportedEntriesClean =
    cleanAppendLeft semanticUnsupportedEntryDiagnostics rest₄ rest₃Clean

  rest₄Clean : CleanDiagnostics rest₄
  rest₄Clean =
    cleanAppendRight semanticUnsupportedEntryDiagnostics rest₄ rest₃Clean

  declarationRoleCollisionEntriesClean :
    CleanDiagnostics declarationRoleCollisionEntryDiagnostics
  declarationRoleCollisionEntriesClean =
    cleanAppendLeft declarationRoleCollisionEntryDiagnostics rest₅ rest₄Clean

  rest₅Clean : CleanDiagnostics rest₅
  rest₅Clean =
    cleanAppendRight declarationRoleCollisionEntryDiagnostics rest₅ rest₄Clean

  propertyRoleUsageConflictEntriesClean :
    CleanDiagnostics propertyRoleUsageConflictEntryDiagnostics
  propertyRoleUsageConflictEntriesClean =
    cleanAppendLeft
      propertyRoleUsageConflictEntryDiagnostics
      undeclaredEntityUseEntryDiagnostics
      rest₅Clean

  undeclaredEntityUseEntriesClean :
    CleanDiagnostics undeclaredEntityUseEntryDiagnostics
  undeclaredEntityUseEntriesClean =
    cleanAppendRight
      propertyRoleUsageConflictEntryDiagnostics
      undeclaredEntityUseEntryDiagnostics
      rest₅Clean

record GraphDocumentValidationMeaning
  (doc : GraphDocument)
  (complete : CompleteGraphDocument doc)
  : Type₀ where
  constructor graphDocumentValidationMeaning
  field
    validationCompleteDocument :
      CompleteGraphDocument doc
    validationCompleteDocumentPreserved :
      validationCompleteDocument ≡ complete

open GraphDocumentValidationMeaning public

GraphDocumentValidationResult : Type₀
GraphDocumentValidationResult =
  CheckResult
    GraphDocument
    CompleteGraphDocument
    GraphDocumentValidationMeaning

graphDocumentValidationEvidence? :
  (doc : GraphDocument) →
  Optional (CompleteGraphDocument doc)
graphDocumentValidationEvidence? doc =
  evidenceFromCleanDiagnostics
    (graphDocumentValidationDiagnostics doc)
    (graphDocumentCompleteFromCleanDiagnostics doc)

graphDocumentValidationCleanEvidence :
  (doc : GraphDocument) →
  CleanDiagnostics (graphDocumentValidationDiagnostics doc) →
  Present (graphDocumentValidationEvidence? doc)
graphDocumentValidationCleanEvidence doc =
  cleanEvidenceFromCleanDiagnostics
    (graphDocumentValidationDiagnostics doc)
    (graphDocumentCompleteFromCleanDiagnostics doc)

graphDocumentValidationSound :
  (doc : GraphDocument) →
  (proof : Present (graphDocumentValidationEvidence? doc)) →
  GraphDocumentValidationMeaning doc (presentValue proof)
graphDocumentValidationSound doc proof =
  graphDocumentValidationMeaning
    (presentValue proof)
    refl

validateGraphDocument : GraphDocument → GraphDocumentValidationResult
validateGraphDocument doc =
  checkResult
    doc
    validationDiagnostics
    (diagnosticsClean? validationDiagnostics)
    (graphDocumentValidationEvidence? doc)
    (graphDocumentValidationCleanEvidence doc)
    (graphDocumentValidationSound doc)
  where
  validationDiagnostics : Diagnostics
  validationDiagnostics =
    graphDocumentValidationDiagnostics doc

completeGraphDocumentFromValidationClean :
  (result : GraphDocumentValidationResult) →
  Clean result →
  CompleteGraphDocument (input result)
completeGraphDocumentFromValidationClean result clean =
  evidenceFromClean result clean

validatedGraphDocumentFromClean :
  (result : GraphDocumentValidationResult) →
  (clean : Clean result) →
  GraphDocumentValidationMeaning
    (input result)
    (completeGraphDocumentFromValidationClean result clean)
validatedGraphDocumentFromClean result clean =
  soundFromClean result clean