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

module OWL2.Corpus.Rejected.OBOGraph.Policy where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab.Policy
open import OWL2.Import.OBOGraph.Policy
open import OWL2.OBOGraph.Syntax

missingPropertyTypeNode : Node
missingPropertyTypeNode =
  node
    "http://example.test/uncertainRelation"
    absent
    propertyNode
    absent
    emptyMeta

unknownPropertyTypeNode : Node
unknownPropertyTypeNode =
  node
    "http://example.test/unknownRelation"
    absent
    propertyNode
    (present unknownProperty)
    emptyMeta

missingPropertyTypeGraph : Graph
missingPropertyTypeGraph =
  graph
    absent
    absent
    emptyMeta
    (missingPropertyTypeNode ∷ [])
    []
    []
    []
    []
    []
    []

unknownPropertyTypeGraph : Graph
unknownPropertyTypeGraph =
  graph
    absent
    absent
    emptyMeta
    (unknownPropertyTypeNode ∷ [])
    []
    []
    []
    []
    []
    []

missingPropertyTypeDocument : GraphDocument
missingPropertyTypeDocument =
  graphDocument (missingPropertyTypeGraph ∷ [])

unknownPropertyTypeDocument : GraphDocument
unknownPropertyTypeDocument =
  graphDocument (unknownPropertyTypeGraph ∷ [])

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

lossyPropertyValueGraph : Graph
lossyPropertyValueGraph =
  graph
    absent
    absent
    (meta
      absent
      []
      []
      []
      []
      (lossyPropertyValue ∷ [])
      false
      [])
    []
    []
    []
    []
    []
    []
    []

lossyPropertyValueDocument : GraphDocument
lossyPropertyValueDocument =
  graphDocument (lossyPropertyValueGraph ∷ [])

missingPropertyTypeStrictPolicyResult :
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence strictPolicy)
    (OBOGraphPolicyMeaning strictPolicy)
missingPropertyTypeStrictPolicyResult =
  checkOBOGraphStrictPolicy missingPropertyTypeDocument

unknownPropertyTypeStrictPolicyResult :
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence strictPolicy)
    (OBOGraphPolicyMeaning strictPolicy)
unknownPropertyTypeStrictPolicyResult =
  checkOBOGraphStrictPolicy unknownPropertyTypeDocument

lossyPropertyValueStrictPolicyResult :
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence strictPolicy)
    (OBOGraphPolicyMeaning strictPolicy)
lossyPropertyValueStrictPolicyResult =
  checkOBOGraphStrictPolicy lossyPropertyValueDocument

missingPropertyTypeStrictDiagnostics :
  diagnostics missingPropertyTypeStrictPolicyResult ≡
  singleDiagnostic (missingPropertyTypeDiagnostic missingPropertyTypeNode)
missingPropertyTypeStrictDiagnostics =
  refl

unknownPropertyTypeStrictDiagnostics :
  diagnostics unknownPropertyTypeStrictPolicyResult ≡
  singleDiagnostic (unknownPropertyTypeDiagnostic unknownPropertyTypeNode)
unknownPropertyTypeStrictDiagnostics =
  refl

lossyPropertyValueStrictDiagnostics :
  diagnostics lossyPropertyValueStrictPolicyResult ≡
  singleDiagnostic
    (lossyPropertyValueTypeDiagnostic lossyPropertyValue "xsd:date")
lossyPropertyValueStrictDiagnostics =
  refl

missingPropertyTypeStrictRejected :
  Clean missingPropertyTypeStrictPolicyResult → ⊥
missingPropertyTypeStrictRejected clean =
  clean

missingPropertyTypeStrictEvidenceAbsent :
  evidence? missingPropertyTypeStrictPolicyResult ≡ absent
missingPropertyTypeStrictEvidenceAbsent =
  refl

missingPropertyTypeStrictEvidenceUnavailable :
  EvidenceUnavailable missingPropertyTypeStrictPolicyResult
missingPropertyTypeStrictEvidenceUnavailable =
  evidenceUnavailable
    missingPropertyTypeStrictPolicyResult
    missingPropertyTypeStrictEvidenceAbsent

unknownPropertyTypeStrictRejected :
  Clean unknownPropertyTypeStrictPolicyResult → ⊥
unknownPropertyTypeStrictRejected clean =
  clean

lossyPropertyValueStrictRejected :
  Clean lossyPropertyValueStrictPolicyResult → ⊥
lossyPropertyValueStrictRejected clean =
  clean

missingPropertyTypeCompatibilityResult :
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence compatibilityPolicy)
    (OBOGraphPolicyMeaning compatibilityPolicy)
missingPropertyTypeCompatibilityResult =
  checkOBOGraphCompatibilityPolicy missingPropertyTypeDocument

lossyPropertyValueCompatibilityResult :
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence compatibilityPolicy)
    (OBOGraphPolicyMeaning compatibilityPolicy)
lossyPropertyValueCompatibilityResult =
  checkOBOGraphCompatibilityPolicy lossyPropertyValueDocument

missingPropertyTypeCompatibilityClean :
  Clean missingPropertyTypeCompatibilityResult
missingPropertyTypeCompatibilityClean =
  tt

lossyPropertyValueCompatibilityClean :
  Clean lossyPropertyValueCompatibilityResult
lossyPropertyValueCompatibilityClean =
  tt

missingPropertyTypeCompatibilityEvidence :
  EvidenceAvailable missingPropertyTypeCompatibilityResult
missingPropertyTypeCompatibilityEvidence =
  cleanEvidence
    missingPropertyTypeCompatibilityResult
    missingPropertyTypeCompatibilityClean

lossyPropertyValueCompatibilityEvidence :
  EvidenceAvailable lossyPropertyValueCompatibilityResult
lossyPropertyValueCompatibilityEvidence =
  cleanEvidence
    lossyPropertyValueCompatibilityResult
    lossyPropertyValueCompatibilityClean