OWL2.Examples.OBOGraph.Json.Validation

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

module OWL2.Examples.OBOGraph.Json.Validation where

open import OWL2.Prelude using ([]; _∷_; _≡_; refl; tt*)
import OWL2.OBOGraph.Report as Report
import OWL2.OBOGraph.Validate as Validate

import OWL2.Examples.OBOGraph.Json.AllValuesFromEdges as AllValuesFromEdges
import OWL2.Examples.OBOGraph.Json.ABox as ABox
import OWL2.Examples.OBOGraph.Json.EquivNodeSetTest as EquivNodeSetTest
import OWL2.Examples.OBOGraph.Json.LogicalDefinitionTest as LogicalDefinitionTest
import OWL2.Examples.OBOGraph.Json.Nucleus as Nucleus
import OWL2.Examples.OBOGraph.Json.ObsoletionExample as ObsoletionExample
import OWL2.Examples.OBOGraph.Json.PropertyChainAllValues as PropertyChainAllValues
import OWL2.Examples.OBOGraph.Json.PropertyChainAxiom as PropertyChainAxiom
import OWL2.Examples.OBOGraph.Json.ROCore as ROCore
import OWL2.Examples.OBOGraph.Json.SYMP as SYMP
import OWL2.Examples.OBOGraph.Json.UO as UO

allValuesFromEdgesReport : Report.ModuleReport
allValuesFromEdgesReport =
  Report.reportModule
    "OWL2.Examples.OBOGraph.Json.AllValuesFromEdges"
    AllValuesFromEdges.graphDocument

aboxReport : Report.ModuleReport
aboxReport =
  Report.reportModule "OWL2.Examples.OBOGraph.Json.ABox" ABox.graphDocument

equivNodeSetTestReport : Report.ModuleReport
equivNodeSetTestReport =
  Report.reportModule
    "OWL2.Examples.OBOGraph.Json.EquivNodeSetTest"
    EquivNodeSetTest.graphDocument

logicalDefinitionTestReport : Report.ModuleReport
logicalDefinitionTestReport =
  Report.reportModule
    "OWL2.Examples.OBOGraph.Json.LogicalDefinitionTest"
    LogicalDefinitionTest.graphDocument

nucleusReport : Report.ModuleReport
nucleusReport =
  Report.reportModule "OWL2.Examples.OBOGraph.Json.Nucleus" Nucleus.graphDocument

obsoletionExampleReport : Report.ModuleReport
obsoletionExampleReport =
  Report.reportModule
    "OWL2.Examples.OBOGraph.Json.ObsoletionExample"
    ObsoletionExample.graphDocument

propertyChainAllValuesReport : Report.ModuleReport
propertyChainAllValuesReport =
  Report.reportModule
    "OWL2.Examples.OBOGraph.Json.PropertyChainAllValues"
    PropertyChainAllValues.graphDocument

propertyChainAxiomReport : Report.ModuleReport
propertyChainAxiomReport =
  Report.reportModule
    "OWL2.Examples.OBOGraph.Json.PropertyChainAxiom"
    PropertyChainAxiom.propertyChainGraphDocument

roCoreReport : Report.ModuleReport
roCoreReport =
  Report.reportModule "OWL2.Examples.OBOGraph.Json.ROCore" ROCore.graphDocument

sympReport : Report.ModuleReport
sympReport =
  Report.reportModule "OWL2.Examples.OBOGraph.Json.SYMP" SYMP.graphDocument

uoReport : Report.ModuleReport
uoReport =
  Report.reportModule "OWL2.Examples.OBOGraph.Json.UO" UO.graphDocument

allValuesFromEdgesComplete :
  Validate.CompleteGraphDocument AllValuesFromEdges.graphDocument
allValuesFromEdgesComplete =
  Validate.completeGraphDocument refl refl tt* refl refl tt* tt* tt*

aboxComplete : Validate.CompleteGraphDocument ABox.graphDocument
aboxComplete =
  Validate.completeGraphDocument refl refl tt* refl refl tt* tt* tt*

logicalDefinitionTestComplete :
  Validate.CompleteGraphDocument LogicalDefinitionTest.graphDocument
logicalDefinitionTestComplete =
  Validate.completeGraphDocument refl refl tt* refl refl tt* tt* tt*

obsoletionExampleComplete :
  Validate.CompleteGraphDocument ObsoletionExample.graphDocument
obsoletionExampleComplete =
  Validate.completeGraphDocument refl refl tt* refl refl tt* tt* tt*

propertyChainAllValuesComplete :
  Validate.CompleteGraphDocument PropertyChainAllValues.graphDocument
propertyChainAllValuesComplete =
  Validate.completeGraphDocument refl refl tt* refl refl tt* tt* tt*

propertyChainAxiomComplete :
  Validate.CompleteGraphDocument PropertyChainAxiom.propertyChainGraphDocument
propertyChainAxiomComplete =
  Validate.completeGraphDocument refl refl tt* refl refl tt* tt* tt*

roCoreComplete : Validate.CompleteGraphDocument ROCore.graphDocument
roCoreComplete =
  Validate.completeGraphDocument refl refl tt* refl refl tt* tt* tt*

uoComplete : Validate.CompleteGraphDocument UO.graphDocument
uoComplete =
  Validate.completeGraphDocument refl refl tt* refl refl tt* tt* tt*

allValuesFromEdgesJsonDiagnosticsClean :
  AllValuesFromEdges.jsonDiagnostics ≡ []
allValuesFromEdgesJsonDiagnosticsClean =
  refl

aboxJsonDiagnosticsClean :
  ABox.jsonDiagnostics ≡ []
aboxJsonDiagnosticsClean =
  refl

equivNodeSetTestJsonDiagnosticsClean :
  EquivNodeSetTest.jsonDiagnostics ≡ []
equivNodeSetTestJsonDiagnosticsClean =
  refl

logicalDefinitionTestJsonDiagnosticsClean :
  LogicalDefinitionTest.jsonDiagnostics ≡ []
logicalDefinitionTestJsonDiagnosticsClean =
  refl

nucleusJsonDiagnosticsClean :
  Nucleus.jsonDiagnostics ≡ []
nucleusJsonDiagnosticsClean =
  refl

obsoletionExampleJsonDiagnosticsClean :
  ObsoletionExample.jsonDiagnostics ≡ []
obsoletionExampleJsonDiagnosticsClean =
  refl

propertyChainAllValuesJsonDiagnosticsClean :
  PropertyChainAllValues.jsonDiagnostics ≡ []
propertyChainAllValuesJsonDiagnosticsClean =
  refl

roCoreJsonDiagnosticsClean :
  ROCore.jsonDiagnostics ≡ []
roCoreJsonDiagnosticsClean =
  refl

sympJsonDiagnosticsClean :
  SYMP.jsonDiagnostics ≡ []
sympJsonDiagnosticsClean =
  refl

uoJsonDiagnosticsClean :
  UO.jsonDiagnostics ≡ []
uoJsonDiagnosticsClean =
  refl

allValuesFromEdgesDomainRangeAxiomCount :
  Report.shapeDomainRangeAxiomCount
    (Report.graphReportShape
      (Report.reportGraph AllValuesFromEdges.graph))
  ≡ 1
allValuesFromEdgesDomainRangeAxiomCount =
  refl

propertyChainAxiomCount :
  Report.shapePropertyChainAxiomCount
    (Report.graphReportShape
      (Report.reportGraph PropertyChainAxiom.propertyChainGraph))
  ≡ 1
propertyChainAxiomCount =
  refl

propertyChainAllValuesShapeCounts :
  Report.documentShapeCounts PropertyChainAllValues.graphDocument
  ≡
  Report.graphShapeCounts 5 0 0 0 1 1 ∷ []
propertyChainAllValuesShapeCounts =
  refl

aboxDeclarationRoleCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    (Report.reportDocument ABox.graphDocument)
  ≡ 0
aboxDeclarationRoleCollisionCount =
  refl

logicalDefinitionTestDeclarationRoleCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    (Report.reportDocument LogicalDefinitionTest.graphDocument)
  ≡ 0
logicalDefinitionTestDeclarationRoleCollisionCount =
  refl

nucleusDeclarationRoleCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    (Report.reportDocument Nucleus.graphDocument)
  ≡ 0
nucleusDeclarationRoleCollisionCount =
  refl

obsoletionExampleDeclarationRoleCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    (Report.reportDocument ObsoletionExample.graphDocument)
  ≡ 0
obsoletionExampleDeclarationRoleCollisionCount =
  refl

uoDeclarationRoleCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    (Report.reportDocument UO.graphDocument)
  ≡ 0
uoDeclarationRoleCollisionCount =
  refl

propertyChainAxiomDeclarationRoleCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    (Report.reportDocument PropertyChainAxiom.propertyChainGraphDocument)
  ≡ 0
propertyChainAxiomDeclarationRoleCollisionCount =
  refl

propertyChainAllValuesDeclarationRoleCollisionCount :
  Report.documentReportDeclarationRoleCollisionCount
    (Report.reportDocument PropertyChainAllValues.graphDocument)
  ≡ 0
propertyChainAllValuesDeclarationRoleCollisionCount =
  refl

aboxSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument ABox.graphDocument)
  ≡ 0
aboxSourceReferenceCoverageGapCount =
  refl

logicalDefinitionTestSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument LogicalDefinitionTest.graphDocument)
  ≡ 0
logicalDefinitionTestSourceReferenceCoverageGapCount =
  refl

nucleusSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument Nucleus.graphDocument)
  ≡ 1
nucleusSourceReferenceCoverageGapCount =
  refl

obsoletionExampleSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument ObsoletionExample.graphDocument)
  ≡ 0
obsoletionExampleSourceReferenceCoverageGapCount =
  refl

equivNodeSetTestSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument EquivNodeSetTest.graphDocument)
  ≡ 5
equivNodeSetTestSourceReferenceCoverageGapCount =
  refl

roCoreSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument ROCore.graphDocument)
  ≡ 0
roCoreSourceReferenceCoverageGapCount =
  refl

sympSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument SYMP.graphDocument)
  ≡ 0
sympSourceReferenceCoverageGapCount =
  refl

uoSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument UO.graphDocument)
  ≡ 0
uoSourceReferenceCoverageGapCount =
  refl

propertyChainAxiomSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument PropertyChainAxiom.propertyChainGraphDocument)
  ≡ 0
propertyChainAxiomSourceReferenceCoverageGapCount =
  refl

propertyChainAllValuesSourceReferenceCoverageGapCount :
  Report.documentReportSourceReferenceCoverageGapCount
    (Report.reportDocument PropertyChainAllValues.graphDocument)
  ≡ 0
propertyChainAllValuesSourceReferenceCoverageGapCount =
  refl

aboxPropertyRoleUsageConflictCount :
  Report.documentReportPropertyRoleUsageConflictCount
    (Report.reportDocument ABox.graphDocument)
  ≡ 0
aboxPropertyRoleUsageConflictCount =
  refl

logicalDefinitionTestPropertyRoleUsageConflictCount :
  Report.documentReportPropertyRoleUsageConflictCount
    (Report.reportDocument LogicalDefinitionTest.graphDocument)
  ≡ 0
logicalDefinitionTestPropertyRoleUsageConflictCount =
  refl

nucleusPropertyRoleUsageConflictCount :
  Report.documentReportPropertyRoleUsageConflictCount
    (Report.reportDocument Nucleus.graphDocument)
  ≡ 0
nucleusPropertyRoleUsageConflictCount =
  refl

obsoletionExamplePropertyRoleUsageConflictCount :
  Report.documentReportPropertyRoleUsageConflictCount
    (Report.reportDocument ObsoletionExample.graphDocument)
  ≡ 0
obsoletionExamplePropertyRoleUsageConflictCount =
  refl

uoPropertyRoleUsageConflictCount :
  Report.documentReportPropertyRoleUsageConflictCount
    (Report.reportDocument UO.graphDocument)
  ≡ 0
uoPropertyRoleUsageConflictCount =
  refl

propertyChainAxiomPropertyRoleUsageConflictCount :
  Report.documentReportPropertyRoleUsageConflictCount
    (Report.reportDocument PropertyChainAxiom.propertyChainGraphDocument)
  ≡ 0
propertyChainAxiomPropertyRoleUsageConflictCount =
  refl

propertyChainAllValuesPropertyRoleUsageConflictCount :
  Report.documentReportPropertyRoleUsageConflictCount
    (Report.reportDocument PropertyChainAllValues.graphDocument)
  ≡ 0
propertyChainAllValuesPropertyRoleUsageConflictCount =
  refl

aboxUndeclaredEntityUseCount :
  Report.documentReportUndeclaredEntityUseCount
    (Report.reportDocument ABox.graphDocument)
  ≡ 0
aboxUndeclaredEntityUseCount =
  refl

logicalDefinitionTestUndeclaredEntityUseCount :
  Report.documentReportUndeclaredEntityUseCount
    (Report.reportDocument LogicalDefinitionTest.graphDocument)
  ≡ 0
logicalDefinitionTestUndeclaredEntityUseCount =
  refl

nucleusUndeclaredEntityUseCount :
  Report.documentReportUndeclaredEntityUseCount
    (Report.reportDocument Nucleus.graphDocument)
  ≡ 0
nucleusUndeclaredEntityUseCount =
  refl

obsoletionExampleUndeclaredEntityUseCount :
  Report.documentReportUndeclaredEntityUseCount
    (Report.reportDocument ObsoletionExample.graphDocument)
  ≡ 0
obsoletionExampleUndeclaredEntityUseCount =
  refl

uoUndeclaredEntityUseCount :
  Report.documentReportUndeclaredEntityUseCount
    (Report.reportDocument UO.graphDocument)
  ≡ 0
uoUndeclaredEntityUseCount =
  refl

propertyChainAxiomUndeclaredEntityUseCount :
  Report.documentReportUndeclaredEntityUseCount
    (Report.reportDocument PropertyChainAxiom.propertyChainGraphDocument)
  ≡ 0
propertyChainAxiomUndeclaredEntityUseCount =
  refl

propertyChainAllValuesUndeclaredEntityUseCount :
  Report.documentReportUndeclaredEntityUseCount
    (Report.reportDocument PropertyChainAllValues.graphDocument)
  ≡ 0
propertyChainAllValuesUndeclaredEntityUseCount =
  refl

uoImportWarningCount :
  Report.documentReportImportWarningCount
    (Report.reportDocument UO.graphDocument)
  ≡ 0
uoImportWarningCount =
  refl

uoSemanticUnsupportedCount :
  Report.documentReportSemanticUnsupportedCount
    (Report.reportDocument UO.graphDocument)
  ≡ 0
uoSemanticUnsupportedCount =
  refl

propertyChainAxiomImportWarningCount :
  Report.documentReportImportWarningCount
    (Report.reportDocument PropertyChainAxiom.propertyChainGraphDocument)
  ≡ 0
propertyChainAxiomImportWarningCount =
  refl

propertyChainAxiomSemanticUnsupportedCount :
  Report.documentReportSemanticUnsupportedCount
    (Report.reportDocument PropertyChainAxiom.propertyChainGraphDocument)
  ≡ 0
propertyChainAxiomSemanticUnsupportedCount =
  refl

propertyChainAllValuesImportWarningCount :
  Report.documentReportImportWarningCount
    (Report.reportDocument PropertyChainAllValues.graphDocument)
  ≡ 0
propertyChainAllValuesImportWarningCount =
  refl

propertyChainAllValuesSemanticUnsupportedCount :
  Report.documentReportSemanticUnsupportedCount
    (Report.reportDocument PropertyChainAllValues.graphDocument)
  ≡ 0
propertyChainAllValuesSemanticUnsupportedCount =
  refl

shortPropertyChainImportWarningCount :
  Report.documentReportImportWarningCount
    (Report.reportDocument PropertyChainAxiom.shortChainGraphDocument)
  ≡ 1
shortPropertyChainImportWarningCount =
  refl

equivNodeSetTestMetaUnsupportedCount :
  Report.documentReportMetaUnsupportedCount
    (Report.reportDocument EquivNodeSetTest.graphDocument)
  ≡ 11
equivNodeSetTestMetaUnsupportedCount =
  refl

nucleusMetaUnsupportedCount :
  Report.documentReportMetaUnsupportedCount
    (Report.reportDocument Nucleus.graphDocument)
  ≡ 0
nucleusMetaUnsupportedCount =
  refl

roCoreMetaUnsupportedCount :
  Report.documentReportMetaUnsupportedCount
    (Report.reportDocument ROCore.graphDocument)
  ≡ 0
roCoreMetaUnsupportedCount =
  refl

sympMetaUnsupportedCount :
  Report.documentReportMetaUnsupportedCount
    (Report.reportDocument SYMP.graphDocument)
  ≡ 0
sympMetaUnsupportedCount =
  refl

uoMetaUnsupportedCount :
  Report.documentReportMetaUnsupportedCount
    (Report.reportDocument UO.graphDocument)
  ≡ 0
uoMetaUnsupportedCount =
  refl