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

module OWL2.Examples.OBOGraph.References where

open import OWL2.Prelude
open import OWL2.OBOGraph.Syntax
import OWL2.OBOGraph.Validate as Validate

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

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

graphFrom : List Node → List Edge → Graph
graphFrom ns es =
  graph absent absent emptyMeta ns es [] [] [] [] []

declaredEdgeGraph : Graph
declaredEdgeGraph =
  graphFrom
    ( nodeClass "A"
    ∷ nodeClass "B"
    ∷ nodeObjectProperty "R"
    ∷ [] )
    ( edge "A" "R" "B" emptyMeta ∷ [] )

declaredEdgeGraphCovered :
  Validate.NoSourceReferenceCoverageGapsInGraph declaredEdgeGraph
declaredEdgeGraphCovered =
  tt*

specialPredicateGraph : Graph
specialPredicateGraph =
  graphFrom
    ( nodeClass "A"
    ∷ nodeClass "B"
    ∷ [] )
    ( edge "A" "is_a" "B" emptyMeta ∷ [] )

specialPredicateGraphCovered :
  Validate.NoSourceReferenceCoverageGapsInGraph specialPredicateGraph
specialPredicateGraphCovered =
  tt*

missingObjectGraph : Graph
missingObjectGraph =
  graphFrom
    ( nodeClass "A"
    ∷ nodeObjectProperty "R"
    ∷ [] )
    ( edge "A" "R" "B" emptyMeta ∷ [] )

missingObjectGraphRejected :
  ¬ Validate.NoSourceReferenceCoverageGapsInGraph missingObjectGraph
missingObjectGraphRejected impossible =
  impossible

chainMissingMemberGraph : Graph
chainMissingMemberGraph =
  graph
    absent
    absent
    emptyMeta
    ( nodeObjectProperty "R"
    ∷ nodeObjectProperty "S"
    ∷ [] )
    []
    []
    []
    []
    (propertyChainAxiom "R" ("S" ∷ "T" ∷ []) emptyMeta ∷ [])
    []

chainMissingMemberRejected :
  ¬ Validate.NoSourceReferenceCoverageGapsInGraph chainMissingMemberGraph
chainMissingMemberRejected impossible =
  impossible

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

allValuesFromMissingPredicateRejected :
  ¬ Validate.NoSourceReferenceCoverageGapsInGraph
      allValuesFromMissingPredicateGraph
allValuesFromMissingPredicateRejected impossible =
  impossible