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

module OWL2.OBOGraph.Check 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.Report as Report
import OWL2.OBOGraph.Validate as Validate

obographValidationDiagnostics : GraphDocument → Diagnostics
obographValidationDiagnostics =
  Validate.graphDocumentValidationDiagnostics

record OBOGraphDocumentEvidence (doc : GraphDocument) : Type₀ where
  constructor obographDocumentEvidence
  field
    obographDocumentReport :
      Report.DocumentReport
    obographDocumentReportView :
      obographDocumentReport ≡ Report.reportDocument doc
    obographDocumentComplete :
      Validate.CompleteGraphDocument doc

open OBOGraphDocumentEvidence public

record OBOGraphDocumentCheckMeaning
  (doc : GraphDocument)
  (evidence : OBOGraphDocumentEvidence doc)
  : Type₀ where
  constructor obographDocumentCheckMeaning
  field
    obographCheckedReportView :
      obographDocumentReport evidence ≡ Report.reportDocument doc
    obographCheckedCompleteDocument :
      Validate.CompleteGraphDocument doc

open OBOGraphDocumentCheckMeaning public

OBOGraphDocumentCheckResult : Type₀
OBOGraphDocumentCheckResult =
  CheckResult
    GraphDocument
    OBOGraphDocumentEvidence
    OBOGraphDocumentCheckMeaning

obographDocumentEvidenceFromCleanDiagnostics :
  (doc : GraphDocument) →
  CleanDiagnostics (obographValidationDiagnostics doc) →
  OBOGraphDocumentEvidence doc
obographDocumentEvidenceFromCleanDiagnostics doc clean =
  obographDocumentEvidence
    (Report.reportDocument doc)
    refl
    (Validate.graphDocumentCompleteFromCleanDiagnostics doc clean)

obographDocumentEvidence? :
  (doc : GraphDocument) →
  Optional (OBOGraphDocumentEvidence doc)
obographDocumentEvidence? doc =
  evidenceFromCleanDiagnostics
    (obographValidationDiagnostics doc)
    (obographDocumentEvidenceFromCleanDiagnostics doc)

obographDocumentCleanEvidence :
  (doc : GraphDocument) →
  CleanDiagnostics (obographValidationDiagnostics doc) →
  Present (obographDocumentEvidence? doc)
obographDocumentCleanEvidence doc =
  cleanEvidenceFromCleanDiagnostics
    (obographValidationDiagnostics doc)
    (obographDocumentEvidenceFromCleanDiagnostics doc)

obographDocumentSound :
  (doc : GraphDocument) →
  (proof : Present (obographDocumentEvidence? doc)) →
  OBOGraphDocumentCheckMeaning doc (presentValue proof)
obographDocumentSound doc proof =
  obographDocumentCheckMeaning
    (obographDocumentReportView (presentValue proof))
    (obographDocumentComplete (presentValue proof))

checkOBOGraphDocument : GraphDocument → OBOGraphDocumentCheckResult
checkOBOGraphDocument doc =
  checkResult
    doc
    validationDiagnostics
    (diagnosticsClean? validationDiagnostics)
    (obographDocumentEvidence? doc)
    (obographDocumentCleanEvidence doc)
    (obographDocumentSound doc)
  where
  validationDiagnostics : Diagnostics
  validationDiagnostics =
    obographValidationDiagnostics doc

obographDocumentReportFromClean :
  (result : OBOGraphDocumentCheckResult) →
  Clean result →
  Report.DocumentReport
obographDocumentReportFromClean result clean =
  obographDocumentReport (evidenceFromClean result clean)

completeGraphDocumentFromClean :
  (result : OBOGraphDocumentCheckResult) →
  Clean result →
  Validate.CompleteGraphDocument (input result)
completeGraphDocumentFromClean result clean =
  obographDocumentComplete (evidenceFromClean result clean)

obographDocumentSoundFromClean :
  (result : OBOGraphDocumentCheckResult) →
  (clean : Clean result) →
  OBOGraphDocumentCheckMeaning
    (input result)
    (evidenceFromClean result clean)
obographDocumentSoundFromClean result clean =
  soundFromClean result clean