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

module OWL2.OBOGraph.References where

open import OWL2.Prelude
open import OWL2.OBOGraph.Syntax

private
  concatMap : ∀ {A B : Type₀} → (A → List B) → List A → List B
  concatMap f [] =
    []
  concatMap f (x ∷ xs) =
    f x ++ concatMap f xs

  optionalToList : ∀ {A : Type₀} → Optional A → List A
  optionalToList absent =
    []
  optionalToList (present x) =
    x ∷ []

data NodeReferencePosition : Type₀ where
  edgeSubjectReference :
    String → String → String → NodeReferencePosition
  edgePredicateReference :
    String → String → String → NodeReferencePosition
  edgeObjectReference :
    String → String → String → NodeReferencePosition
  equivalentRepresentativeReference :
    List String → NodeReferencePosition
  equivalentNodeReference :
    Optional String → List String → NodeReferencePosition
  logicalDefinedClassReference :
    String → NodeReferencePosition
  logicalGenusReference :
    String → NodeReferencePosition
  logicalRestrictionPropertyReference :
    String → String → NodeReferencePosition
  logicalRestrictionFillerReference :
    String → String → NodeReferencePosition
  domainRangePredicateReference :
    List String → List String → NodeReferencePosition
  domainClassReference :
    String → NodeReferencePosition
  rangeClassReference :
    String → NodeReferencePosition
  domainRangeAllValuesFromSubjectReference :
    String → String → String → NodeReferencePosition
  domainRangeAllValuesFromPredicateReference :
    String → String → String → NodeReferencePosition
  domainRangeAllValuesFromObjectReference :
    String → String → String → NodeReferencePosition
  propertyChainSuperPropertyReference :
    List String → NodeReferencePosition
  propertyChainMemberReference :
    String → NodeReferencePosition

record NodeReferenceFact : Type₀ where
  constructor nodeReferenceFact
  field
    referenceGraphId :
      Optional String
    referencedNodeId :
      String
    referencePosition :
      NodeReferencePosition

open NodeReferenceFact public

record MissingNodeReference : Type₀ where
  constructor missingNodeReference
  field
    missingReferenceGraphId :
      Optional String
    missingReferenceNodeId :
      String
    missingReferencePosition :
      NodeReferencePosition

open MissingNodeReference public

nodeIdDeclared : String → List Node → Bool
nodeIdDeclared text [] =
  false
nodeIdDeclared text (n ∷ ns) with primStringEquality text (nodeId n)
... | true =
  true
... | false =
  nodeIdDeclared text ns

isSpecialEdgePredicate : String → Bool
isSpecialEdgePredicate predicate =
  if primStringEquality predicate "is_a" then true else
  if primStringEquality predicate "type" then true else
  if primStringEquality predicate "subPropertyOf" then true else
  primStringEquality predicate "inverseOf"

nodeReferenceFactFor :
  Optional String → String → NodeReferencePosition → NodeReferenceFact
nodeReferenceFactFor graphId text position =
  nodeReferenceFact graphId text position

nodeReferenceFactsInEdge :
  Optional String → Edge → List NodeReferenceFact
nodeReferenceFactsInEdge graphId e =
  nodeReferenceFactFor
    graphId
    (edgeSubject e)
    (edgeSubjectReference (edgeSubject e) (edgePredicate e) (edgeObject e))
  ∷
  nodeReferenceFactFor
    graphId
    (edgeObject e)
    (edgeObjectReference (edgeSubject e) (edgePredicate e) (edgeObject e))
  ∷
  predicateReference (edgePredicate e)
  where
  predicateReference : String → List NodeReferenceFact
  predicateReference predicate with isSpecialEdgePredicate predicate
  ... | true =
    []
  ... | false =
    nodeReferenceFactFor
      graphId
      predicate
      (edgePredicateReference (edgeSubject e) predicate (edgeObject e))
    ∷ []

nodeReferenceFactsInEquivalentNodesSet :
  Optional String → EquivalentNodesSet → List NodeReferenceFact
nodeReferenceFactsInEquivalentNodesSet graphId s =
  map
    (λ text →
      nodeReferenceFactFor
        graphId
        text
        (equivalentRepresentativeReference (nodeIds s)))
    (optionalToList (representativeNodeId s))
  ++
  map
    (λ text →
      nodeReferenceFactFor
        graphId
        text
        (equivalentNodeReference (representativeNodeId s) (nodeIds s)))
    (nodeIds s)

nodeReferenceFactsInExistentialRestriction :
  Optional String → String → ExistentialRestriction → List NodeReferenceFact
nodeReferenceFactsInExistentialRestriction graphId defined r =
  nodeReferenceFactFor
    graphId
    (restrictionPropertyId r)
    (logicalRestrictionPropertyReference
      defined
      (restrictionFillerId r))
  ∷
  nodeReferenceFactFor
    graphId
    (restrictionFillerId r)
    (logicalRestrictionFillerReference
      defined
      (restrictionPropertyId r))
  ∷ []

nodeReferenceFactsInLogicalDefinitionAxiom :
  Optional String → LogicalDefinitionAxiom → List NodeReferenceFact
nodeReferenceFactsInLogicalDefinitionAxiom graphId a =
  nodeReferenceFactFor
    graphId
    (definedClassId a)
    (logicalDefinedClassReference (definedClassId a))
  ∷
  map
    (λ text →
      nodeReferenceFactFor
        graphId
        text
        (logicalGenusReference (definedClassId a)))
    (genusIds a)
  ++
  concatMap
    (nodeReferenceFactsInExistentialRestriction graphId (definedClassId a))
    (restrictions a)

nodeReferenceFactsInAllValuesFromEdge :
  Optional String → Edge → List NodeReferenceFact
nodeReferenceFactsInAllValuesFromEdge graphId e =
  nodeReferenceFactFor
    graphId
    (edgeSubject e)
    (domainRangeAllValuesFromSubjectReference
      (edgeSubject e)
      (edgePredicate e)
      (edgeObject e))
  ∷
  nodeReferenceFactFor
    graphId
    (edgePredicate e)
    (domainRangeAllValuesFromPredicateReference
      (edgeSubject e)
      (edgePredicate e)
      (edgeObject e))
  ∷
  nodeReferenceFactFor
    graphId
    (edgeObject e)
    (domainRangeAllValuesFromObjectReference
      (edgeSubject e)
      (edgePredicate e)
      (edgeObject e))
  ∷ []

nodeReferenceFactsInDomainRangeAxiom :
  Optional String → DomainRangeAxiom → List NodeReferenceFact
nodeReferenceFactsInDomainRangeAxiom graphId a =
  nodeReferenceFactFor
    graphId
    (domainRangePredicate a)
    (domainRangePredicateReference (domainClassIds a) (rangeClassIds a))
  ∷
  map
    (λ text →
      nodeReferenceFactFor
        graphId
        text
        (domainClassReference (domainRangePredicate a)))
    (domainClassIds a)
  ++
  map
    (λ text →
      nodeReferenceFactFor
        graphId
        text
        (rangeClassReference (domainRangePredicate a)))
    (rangeClassIds a)
  ++ concatMap
       (nodeReferenceFactsInAllValuesFromEdge graphId)
       (allValuesFromEdges a)

nodeReferenceFactsInPropertyChainAxiom :
  Optional String → PropertyChainAxiom → List NodeReferenceFact
nodeReferenceFactsInPropertyChainAxiom graphId a =
  nodeReferenceFactFor
    graphId
    (chainPredicateId a)
    (propertyChainSuperPropertyReference (chainPredicateIds a))
  ∷
  map
    (λ text →
      nodeReferenceFactFor
        graphId
        text
        (propertyChainMemberReference (chainPredicateId a)))
    (chainPredicateIds a)

nodeReferenceFactsInGraph : Graph → List NodeReferenceFact
nodeReferenceFactsInGraph g =
  concatMap (nodeReferenceFactsInEdge (graphId g)) (edges g)
  ++ concatMap
       (nodeReferenceFactsInEquivalentNodesSet (graphId g))
       (equivalentNodesSets g)
  ++ concatMap
       (nodeReferenceFactsInLogicalDefinitionAxiom (graphId g))
       (logicalDefinitionAxioms g)
  ++ concatMap
       (nodeReferenceFactsInDomainRangeAxiom (graphId g))
       (domainRangeAxioms g)
  ++ concatMap
       (nodeReferenceFactsInPropertyChainAxiom (graphId g))
       (propertyChainAxioms g)

nodeReferenceFactsInDocument :
  GraphDocument → List NodeReferenceFact
nodeReferenceFactsInDocument (graphDocument gs) =
  concatMap nodeReferenceFactsInGraph gs

maybeMissingNodeReference :
  List Node → NodeReferenceFact → Optional MissingNodeReference
maybeMissingNodeReference nodes fact
  with nodeIdDeclared (referencedNodeId fact) nodes
... | true =
  absent
... | false =
  present
    (missingNodeReference
      (referenceGraphId fact)
      (referencedNodeId fact)
      (referencePosition fact))

missingNodeReferencesInGraph : Graph → List MissingNodeReference
missingNodeReferencesInGraph g =
  filterMap
    (maybeMissingNodeReference (nodes g))
    (nodeReferenceFactsInGraph g)

missingNodeReferencesInDocument :
  GraphDocument → List MissingNodeReference
missingNodeReferencesInDocument (graphDocument gs) =
  concatMap missingNodeReferencesInGraph gs

NoMissingNodeReferences : List MissingNodeReference → Type₀
NoMissingNodeReferences [] =
  Unit*
NoMissingNodeReferences (_ ∷ _) =
  ⊥

AllSourceNodeReferencesDeclared : GraphDocument → Type₀
AllSourceNodeReferencesDeclared doc =
  NoMissingNodeReferences (missingNodeReferencesInDocument doc)