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

module OWL2.Examples.OBOGraph.Json.CheckResult where

open import OWL2.Prelude using (_≡_; refl; absent; tt)
open import OWL2.Check.Result
  using
    ( Clean
    ; EvidenceAvailable
    ; EvidenceUnavailable
    ; cleanEvidence
    ; evidence?
    ; evidenceFromClean
    ; evidenceUnavailable
    )
import OWL2.Examples.OBOGraph.Json.ABox as ABox
import OWL2.Examples.OBOGraph.Json.PropertyChainAxiom as PropertyChainAxiom
import OWL2.OBOGraph.Check as Check
import OWL2.OBOGraph.Report as Report
import OWL2.OBOGraph.Validate as Validate

aboxCheckResult : Check.OBOGraphDocumentCheckResult
aboxCheckResult =
  Check.checkOBOGraphDocument ABox.graphDocument

aboxCheckClean : Clean aboxCheckResult
aboxCheckClean =
  tt

aboxCheckEvidence : EvidenceAvailable aboxCheckResult
aboxCheckEvidence =
  cleanEvidence aboxCheckResult aboxCheckClean

aboxCheckReportView :
  Check.obographDocumentReport
    (evidenceFromClean aboxCheckResult aboxCheckClean)
  ≡ Report.reportDocument ABox.graphDocument
aboxCheckReportView =
  refl

aboxCheckComplete :
  Validate.CompleteGraphDocument ABox.graphDocument
aboxCheckComplete =
  Check.completeGraphDocumentFromClean aboxCheckResult aboxCheckClean

shortPropertyChainCheckResult : Check.OBOGraphDocumentCheckResult
shortPropertyChainCheckResult =
  Check.checkOBOGraphDocument PropertyChainAxiom.shortChainGraphDocument

shortPropertyChainCheckEvidenceAbsent :
  evidence? shortPropertyChainCheckResult ≡ absent
shortPropertyChainCheckEvidenceAbsent =
  refl

shortPropertyChainCheckEvidenceUnavailable :
  EvidenceUnavailable shortPropertyChainCheckResult
shortPropertyChainCheckEvidenceUnavailable =
  evidenceUnavailable
    shortPropertyChainCheckResult
    shortPropertyChainCheckEvidenceAbsent