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

module OWL2.Corpus.Accepted.OBOGraph.Policy where

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

knownObjectPropertyNode : Node
knownObjectPropertyNode =
  node
    "http://example.test/hasPart"
    absent
    propertyNode
    (present objectProperty)
    emptyMeta

knownObjectPropertyGraph : Graph
knownObjectPropertyGraph =
  graph
    absent
    absent
    emptyMeta
    (knownObjectPropertyNode ∷ [])
    []
    []
    []
    []
    []
    []

knownObjectPropertyDocument : GraphDocument
knownObjectPropertyDocument =
  graphDocument (knownObjectPropertyGraph ∷ [])

knownObjectPropertyStrictPolicyResult :
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence strictPolicy)
    (OBOGraphPolicyMeaning strictPolicy)
knownObjectPropertyStrictPolicyResult =
  checkOBOGraphStrictPolicy knownObjectPropertyDocument

knownObjectPropertyStrictPolicyClean :
  Clean knownObjectPropertyStrictPolicyResult
knownObjectPropertyStrictPolicyClean =
  tt

knownObjectPropertyStrictPolicyEvidence :
  EvidenceAvailable knownObjectPropertyStrictPolicyResult
knownObjectPropertyStrictPolicyEvidence =
  cleanEvidence
    knownObjectPropertyStrictPolicyResult
    knownObjectPropertyStrictPolicyClean

knownObjectPropertyStrictImportPolicyEvidence :
  ImportPolicyEvidence strictPolicy
knownObjectPropertyStrictImportPolicyEvidence =
  obographImportPolicyEvidence
    (evidenceValue
      knownObjectPropertyStrictPolicyResult
      knownObjectPropertyStrictPolicyEvidence)

knownObjectPropertyStrictModeRecorded :
  recordedMode knownObjectPropertyStrictImportPolicyEvidence ≡ strict
knownObjectPropertyStrictModeRecorded =
  refl

knownObjectPropertyStrictUnknownPropertyKindsRecorded :
  recordedAllowUnknownPropertyKinds
    knownObjectPropertyStrictImportPolicyEvidence ≡ false
knownObjectPropertyStrictUnknownPropertyKindsRecorded =
  refl

knownObjectPropertyStrictLossyMappingsRecorded :
  recordedAllowLossyMappings
    knownObjectPropertyStrictImportPolicyEvidence ≡ false
knownObjectPropertyStrictLossyMappingsRecorded =
  refl