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

module OWL2.Corpus.Rejected.OBOGraph.Raw where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab
open import OWL2.Import.OBOGraph
open import OWL2.Import.OBOGraph.Raw
open import OWL2.OBOGraph.Syntax
import OWL2.Corpus.Rejected.OBOGraph.Policy as RejectedPolicy
import OWL2.Examples.OBOGraph.References as References
import OWL2.OBOGraph.References as Ref

nodeClass : String → Node
nodeClass text =
  node text absent classNode absent emptyMeta

nodeIndividual : String → Node
nodeIndividual text =
  node text absent individualNode absent emptyMeta

nodeDataProperty : String → Node
nodeDataProperty text =
  node text absent propertyNode (present dataProperty) emptyMeta

nodeObjectProperty : String → Node
nodeObjectProperty text =
  node text absent propertyNode (present objectProperty) emptyMeta

rawLossyPropertyValue : PropertyValue
rawLossyPropertyValue =
  propertyValue
    "http://example.test/metadata"
    "2026-06-27"
    (present "xsd:date")

rawLossyPropertyValueGraph : Graph
rawLossyPropertyValueGraph =
  graph
    absent
    absent
    (meta
      absent
      []
      []
      []
      []
      (rawLossyPropertyValue ∷ [])
      false
      [])
    []
    []
    []
    []
    []
    []
    []

rawLossyPropertyValueDocument : GraphDocument
rawLossyPropertyValueDocument =
  graphDocument (rawLossyPropertyValueGraph ∷ [])

rawLossyPropertyValueRawResult : OBOGraphRawImportResult
rawLossyPropertyValueRawResult =
  importOBOGraphRawStrict rawLossyPropertyValueDocument

rawLossyPropertyValueDiagnostics :
  diagnostics rawLossyPropertyValueRawResult ≡
  singleDiagnostic
    (lossyPropertyValueTypeDiagnostic rawLossyPropertyValue "xsd:date")
rawLossyPropertyValueDiagnostics =
  refl

rawLossyPropertyValueRejected :
  Clean rawLossyPropertyValueRawResult → ⊥
rawLossyPropertyValueRejected clean =
  clean

rawLossyPropertyValueEvidenceAbsent :
  evidence? rawLossyPropertyValueRawResult ≡ absent
rawLossyPropertyValueEvidenceAbsent =
  refl

rawLossyPropertyValueEvidenceUnavailable :
  EvidenceUnavailable rawLossyPropertyValueRawResult
rawLossyPropertyValueEvidenceUnavailable =
  evidenceUnavailable
    rawLossyPropertyValueRawResult
    rawLossyPropertyValueEvidenceAbsent

missingPropertyTypeCheckedResult : OBOGraphCheckedImportResult
missingPropertyTypeCheckedResult =
  importOBOGraphCheckedStrict RejectedPolicy.missingPropertyTypeDocument

missingPropertyTypeCheckedDiagnostics :
  diagnostics missingPropertyTypeCheckedResult ≡
  singleDiagnostic
    (missingPropertyTypeDiagnostic RejectedPolicy.missingPropertyTypeNode)
missingPropertyTypeCheckedDiagnostics =
  refl

missingPropertyTypeCheckedRejected :
  Clean missingPropertyTypeCheckedResult → ⊥
missingPropertyTypeCheckedRejected clean =
  clean

missingPropertyTypeCheckedEvidenceAbsent :
  evidence? missingPropertyTypeCheckedResult ≡ absent
missingPropertyTypeCheckedEvidenceAbsent =
  refl

missingPropertyTypeCheckedEvidenceUnavailable :
  EvidenceUnavailable missingPropertyTypeCheckedResult
missingPropertyTypeCheckedEvidenceUnavailable =
  evidenceUnavailable
    missingPropertyTypeCheckedResult
    missingPropertyTypeCheckedEvidenceAbsent

unknownPropertyTypeCheckedResult : OBOGraphCheckedImportResult
unknownPropertyTypeCheckedResult =
  importOBOGraphCheckedStrict RejectedPolicy.unknownPropertyTypeDocument

unknownPropertyTypeCheckedDiagnostics :
  diagnostics unknownPropertyTypeCheckedResult ≡
  singleDiagnostic
    (unknownPropertyTypeDiagnostic RejectedPolicy.unknownPropertyTypeNode)
unknownPropertyTypeCheckedDiagnostics =
  refl

unknownPropertyTypeCheckedRejected :
  Clean unknownPropertyTypeCheckedResult → ⊥
unknownPropertyTypeCheckedRejected clean =
  clean

unknownPropertyTypeCheckedEvidenceAbsent :
  evidence? unknownPropertyTypeCheckedResult ≡ absent
unknownPropertyTypeCheckedEvidenceAbsent =
  refl

unknownPropertyTypeCheckedEvidenceUnavailable :
  EvidenceUnavailable unknownPropertyTypeCheckedResult
unknownPropertyTypeCheckedEvidenceUnavailable =
  evidenceUnavailable
    unknownPropertyTypeCheckedResult
    unknownPropertyTypeCheckedEvidenceAbsent

lossyPropertyValueCheckedResult : OBOGraphCheckedImportResult
lossyPropertyValueCheckedResult =
  importOBOGraphCheckedStrict RejectedPolicy.lossyPropertyValueDocument

lossyPropertyValueCheckedDiagnostics :
  diagnostics lossyPropertyValueCheckedResult ≡
  singleDiagnostic
    (lossyPropertyValueTypeDiagnostic
      RejectedPolicy.lossyPropertyValue
      "xsd:date")
lossyPropertyValueCheckedDiagnostics =
  refl

lossyPropertyValueCheckedRejected :
  Clean lossyPropertyValueCheckedResult → ⊥
lossyPropertyValueCheckedRejected clean =
  clean

lossyPropertyValueCheckedEvidenceAbsent :
  evidence? lossyPropertyValueCheckedResult ≡ absent
lossyPropertyValueCheckedEvidenceAbsent =
  refl

lossyPropertyValueCheckedEvidenceUnavailable :
  EvidenceUnavailable lossyPropertyValueCheckedResult
lossyPropertyValueCheckedEvidenceUnavailable =
  evidenceUnavailable
    lossyPropertyValueCheckedResult
    lossyPropertyValueCheckedEvidenceAbsent

unsupportedDomainRangeGraph : Graph
unsupportedDomainRangeGraph =
  graph
    absent
    absent
    emptyMeta
    (nodeClass "A" ∷
     nodeClass "B" ∷
     nodeObjectProperty "R" ∷ [])
    []
    []
    []
    (domainRangeAxiom "R" ("A" ∷ []) [] [] emptyMeta ∷ [])
    []
    []

unsupportedDomainRangeDocument : GraphDocument
unsupportedDomainRangeDocument =
  graphDocument (unsupportedDomainRangeGraph ∷ [])

unsupportedDomainRangeRawResult : OBOGraphRawImportResult
unsupportedDomainRangeRawResult =
  importOBOGraphRawStrict unsupportedDomainRangeDocument

unsupportedDomainRangeDiagnostics :
  diagnostics unsupportedDomainRangeRawResult ≡
  singleDiagnostic unsupportedDomainRangeDiagnostic
unsupportedDomainRangeDiagnostics =
  refl

unsupportedDomainRangeRejected :
  Clean unsupportedDomainRangeRawResult → ⊥
unsupportedDomainRangeRejected clean =
  clean

unsupportedDomainRangeEvidenceAbsent :
  evidence? unsupportedDomainRangeRawResult ≡ absent
unsupportedDomainRangeEvidenceAbsent =
  refl

unsupportedDomainRangeEvidenceUnavailable :
  EvidenceUnavailable unsupportedDomainRangeRawResult
unsupportedDomainRangeEvidenceUnavailable =
  evidenceUnavailable
    unsupportedDomainRangeRawResult
    unsupportedDomainRangeEvidenceAbsent

badTypeEdge : Edge
badTypeEdge =
  edge "A" "type" "B" emptyMeta

badTypeGraph : Graph
badTypeGraph =
  graph
    absent
    absent
    emptyMeta
    (nodeClass "A" ∷
     nodeClass "B" ∷ [])
    (badTypeEdge ∷ [])
    []
    []
    []
    []
    []

badTypeDocument : GraphDocument
badTypeDocument =
  graphDocument (badTypeGraph ∷ [])

badTypeRawResult : OBOGraphRawImportResult
badTypeRawResult =
  importOBOGraphRawStrict badTypeDocument

badTypeDiagnostics :
  diagnostics badTypeRawResult ≡
  singleDiagnostic (unsupportedTypeEdgeDiagnostic badTypeEdge)
badTypeDiagnostics =
  refl

badTypeRejected : Clean badTypeRawResult → ⊥
badTypeRejected clean =
  clean

badTypeEvidenceAbsent :
  evidence? badTypeRawResult ≡ absent
badTypeEvidenceAbsent =
  refl

badTypeEvidenceUnavailable :
  EvidenceUnavailable badTypeRawResult
badTypeEvidenceUnavailable =
  evidenceUnavailable badTypeRawResult badTypeEvidenceAbsent

badTypeCheckedResult : OBOGraphCheckedImportResult
badTypeCheckedResult =
  importOBOGraphCheckedStrict badTypeDocument

badTypeCheckedDiagnostics :
  diagnostics badTypeCheckedResult ≡
  singleDiagnostic (unsupportedTypeEdgeDiagnostic badTypeEdge)
badTypeCheckedDiagnostics =
  refl

badTypeCheckedRejected :
  Clean badTypeCheckedResult → ⊥
badTypeCheckedRejected clean =
  clean

badTypeCheckedEvidenceAbsent :
  evidence? badTypeCheckedResult ≡ absent
badTypeCheckedEvidenceAbsent =
  refl

badTypeCheckedEvidenceUnavailable :
  EvidenceUnavailable badTypeCheckedResult
badTypeCheckedEvidenceUnavailable =
  evidenceUnavailable badTypeCheckedResult badTypeCheckedEvidenceAbsent

obographStructuralOntologyIRIGraph : Graph
obographStructuralOntologyIRIGraph =
  graph
    (present "http://example.test/obograph/ontology")
    absent
    emptyMeta
    []
    []
    []
    []
    []
    []
    []

obographStructuralOntologyIRIDocument : GraphDocument
obographStructuralOntologyIRIDocument =
  graphDocument (obographStructuralOntologyIRIGraph ∷ [])

obographStructuralOntologyIRIRawResult : OBOGraphRawImportResult
obographStructuralOntologyIRIRawResult =
  importOBOGraphRawStrict obographStructuralOntologyIRIDocument

obographStructuralOntologyIRIRawClean :
  Clean obographStructuralOntologyIRIRawResult
obographStructuralOntologyIRIRawClean =
  tt

obographStructuralOntologyIRICheckedResult : OBOGraphCheckedImportResult
obographStructuralOntologyIRICheckedResult =
  importOBOGraphCheckedStrict obographStructuralOntologyIRIDocument

obographStructuralOntologyIRICheckedDiagnostics :
  diagnostics obographStructuralOntologyIRICheckedResult ≡
  singleDiagnostic structuralUnsupportedOntologyIRIDiagnostic
obographStructuralOntologyIRICheckedDiagnostics =
  refl

obographStructuralOntologyIRICheckedRejected :
  Clean obographStructuralOntologyIRICheckedResult → ⊥
obographStructuralOntologyIRICheckedRejected clean =
  clean

obographStructuralOntologyIRICheckedEvidenceAbsent :
  evidence? obographStructuralOntologyIRICheckedResult ≡ absent
obographStructuralOntologyIRICheckedEvidenceAbsent =
  refl

dataPredicateRelationEdge : Edge
dataPredicateRelationEdge =
  edge "A" "D" "B" emptyMeta

dataPredicateRelationGraph : Graph
dataPredicateRelationGraph =
  graph
    absent
    absent
    emptyMeta
    (nodeClass "A" ∷
     nodeClass "B" ∷
     nodeDataProperty "D" ∷ [])
    (dataPredicateRelationEdge ∷ [])
    []
    []
    []
    []
    []

dataPredicateRelationDocument : GraphDocument
dataPredicateRelationDocument =
  graphDocument (dataPredicateRelationGraph ∷ [])

dataPredicateRelationRawResult : OBOGraphRawImportResult
dataPredicateRelationRawResult =
  importOBOGraphRawStrict dataPredicateRelationDocument

dataPredicateRelationDiagnostics :
  diagnostics dataPredicateRelationRawResult ≡
  singleDiagnostic
    (unsupportedDeclaredRelationEdgeDiagnostic dataPredicateRelationEdge)
dataPredicateRelationDiagnostics =
  refl

dataPredicateRelationRejected :
  Clean dataPredicateRelationRawResult → ⊥
dataPredicateRelationRejected clean =
  clean

dataPredicateRelationEvidenceAbsent :
  evidence? dataPredicateRelationRawResult ≡ absent
dataPredicateRelationEvidenceAbsent =
  refl

dataPredicateRelationEvidenceUnavailable :
  EvidenceUnavailable dataPredicateRelationRawResult
dataPredicateRelationEvidenceUnavailable =
  evidenceUnavailable
    dataPredicateRelationRawResult
    dataPredicateRelationEvidenceAbsent

individualDataPredicateRelationEdge : Edge
individualDataPredicateRelationEdge =
  edge "x" "D" "y" emptyMeta

individualDataPredicateRelationGraph : Graph
individualDataPredicateRelationGraph =
  graph
    absent
    absent
    emptyMeta
    (nodeIndividual "x" ∷
     nodeIndividual "y" ∷
     nodeDataProperty "D" ∷ [])
    (individualDataPredicateRelationEdge ∷ [])
    []
    []
    []
    []
    []

individualDataPredicateRelationDocument : GraphDocument
individualDataPredicateRelationDocument =
  graphDocument (individualDataPredicateRelationGraph ∷ [])

individualDataPredicateRelationRawResult : OBOGraphRawImportResult
individualDataPredicateRelationRawResult =
  importOBOGraphRawStrict individualDataPredicateRelationDocument

individualDataPredicateRelationDiagnostics :
  diagnostics individualDataPredicateRelationRawResult ≡
  singleDiagnostic
    (unsupportedDeclaredRelationEdgeDiagnostic
      individualDataPredicateRelationEdge)
individualDataPredicateRelationDiagnostics =
  refl

individualDataPredicateRelationRejected :
  Clean individualDataPredicateRelationRawResult → ⊥
individualDataPredicateRelationRejected clean =
  clean

individualDataPredicateRelationEvidenceAbsent :
  evidence? individualDataPredicateRelationRawResult ≡ absent
individualDataPredicateRelationEvidenceAbsent =
  refl

individualDataPredicateRelationEvidenceUnavailable :
  EvidenceUnavailable individualDataPredicateRelationRawResult
individualDataPredicateRelationEvidenceUnavailable =
  evidenceUnavailable
    individualDataPredicateRelationRawResult
    individualDataPredicateRelationEvidenceAbsent

missingObjectDocument : GraphDocument
missingObjectDocument =
  graphDocument (References.missingObjectGraph ∷ [])

missingObjectRawResult : OBOGraphRawImportResult
missingObjectRawResult =
  importOBOGraphRawStrict missingObjectDocument

missingObjectReference : Ref.MissingNodeReference
missingObjectReference =
  Ref.missingNodeReference
    absent
    "B"
    (Ref.edgeObjectReference "A" "R" "B")

missingObjectDiagnostics :
  diagnostics missingObjectRawResult ≡
  singleDiagnostic (missingNodeReferenceDiagnostic missingObjectReference)
missingObjectDiagnostics =
  refl

missingObjectRejected :
  Clean missingObjectRawResult → ⊥
missingObjectRejected clean =
  clean

missingObjectEvidenceAbsent :
  evidence? missingObjectRawResult ≡ absent
missingObjectEvidenceAbsent =
  refl

missingObjectEvidenceUnavailable :
  EvidenceUnavailable missingObjectRawResult
missingObjectEvidenceUnavailable =
  evidenceUnavailable missingObjectRawResult missingObjectEvidenceAbsent