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

module OWL2.Import.OBOGraph.Raw where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab.Policy
open import OWL2.Foundation.List using (concatMap)
open import OWL2.Foundation.Maybe
open import OWL2.Import.OBOGraph.Policy
open import OWL2.OBOGraph.Syntax
import OWL2.OBOGraph.References as Ref
open import OWL2.Raw hiding (SourcePath; sourcePath; rootPath; fieldPath; indexPath)

private
  rawCode : String → DiagnosticCode
  rawCode name =
    mkDiagnosticCode "obograph.raw" name

  atGraph : SourcePath
  atGraph =
    sourcePath (fieldSegment "graphs" ∷ [])

  atNode : SourcePath
  atNode =
    sourcePath (fieldSegment "graphs" ∷ opaqueSegment "nodes" ∷ [])

  atEdge : SourcePath
  atEdge =
    sourcePath (fieldSegment "graphs" ∷ opaqueSegment "edges" ∷ [])

  atReference : SourcePath
  atReference =
    sourcePath (fieldSegment "graphs" ∷ opaqueSegment "references" ∷ [])

  atEquivalentNodes : SourcePath
  atEquivalentNodes =
    sourcePath (fieldSegment "graphs" ∷ opaqueSegment "equivalentNodesSets" ∷ [])

  atLogicalDefinitions : SourcePath
  atLogicalDefinitions =
    sourcePath (fieldSegment "graphs" ∷ opaqueSegment "logicalDefinitionAxioms" ∷ [])

  atDomainRange : SourcePath
  atDomainRange =
    sourcePath (fieldSegment "graphs" ∷ opaqueSegment "domainRangeAxioms" ∷ [])

  atPropertyChains : SourcePath
  atPropertyChains =
    sourcePath (fieldSegment "graphs" ∷ opaqueSegment "propertyChainAxioms" ∷ [])

  unsupportedSection : String → SourcePath → Diagnostic
  unsupportedSection name path =
    diagnostic
      (rawCode name)
      severityError
      path
      "This OBOGraph section is outside the current raw import fragment."

obographSource : SourceProvenance
obographSource =
  sourceProvenance "obograph" absent

unsupportedNodeTypeDiagnostic : Node → Diagnostic
unsupportedNodeTypeDiagnostic n =
  diagnostic
    (rawCode "unsupported-node-type")
    severityError
    atNode
    (nodeId n)

unsupportedEdgeDiagnostic : Edge → Diagnostic
unsupportedEdgeDiagnostic e =
  diagnostic
    (rawCode "unsupported-edge")
    severityError
    atEdge
    (edgePredicate e)

unsupportedDeclaredRelationEdgeDiagnostic : Edge → Diagnostic
unsupportedDeclaredRelationEdgeDiagnostic =
  unsupportedEdgeDiagnostic

unsupportedTypeEdgeDiagnostic : Edge → Diagnostic
unsupportedTypeEdgeDiagnostic =
  unsupportedEdgeDiagnostic

isANonClassEndpointDiagnostic : String → Edge → Diagnostic
isANonClassEndpointDiagnostic text e =
  diagnostic
    (rawCode "is-a-non-class-endpoint")
    severityError
    atEdge
    text

missingNodeReferenceDiagnostic : Ref.MissingNodeReference → Diagnostic
missingNodeReferenceDiagnostic missing =
  diagnostic
    (rawCode "missing-node-reference")
    severityError
    atReference
    (Ref.missingReferenceNodeId missing)

unsupportedGraphPayloadDiagnostic : Diagnostic
unsupportedGraphPayloadDiagnostic =
  unsupportedSection "unsupported-graph-payload" atGraph

unsupportedEquivalentNodesDiagnostic : Diagnostic
unsupportedEquivalentNodesDiagnostic =
  unsupportedSection "unsupported-equivalent-nodes" atEquivalentNodes

unsupportedLogicalDefinitionsDiagnostic : Diagnostic
unsupportedLogicalDefinitionsDiagnostic =
  unsupportedSection "unsupported-logical-definitions" atLogicalDefinitions

unsupportedDomainRangeDiagnostic : Diagnostic
unsupportedDomainRangeDiagnostic =
  unsupportedSection "unsupported-domain-range" atDomainRange

unsupportedPropertyChainsDiagnostic : Diagnostic
unsupportedPropertyChainsDiagnostic =
  unsupportedSection "unsupported-property-chains" atPropertyChains

rawIRIFromText : String → RawIRI
rawIRIFromText =
  rawIRI

rdfsLabel rdfsComment owlDeprecated iaoDefinition
  oboHasDbXref oboInSubset ffImportWarning xsdString
  xsdAnyURI compactXSDAnyURI : String
rdfsLabel =
  "http://www.w3.org/2000/01/rdf-schema#label"
rdfsComment =
  "http://www.w3.org/2000/01/rdf-schema#comment"
owlDeprecated =
  "http://www.w3.org/2002/07/owl#deprecated"
iaoDefinition =
  "http://purl.obolibrary.org/obo/IAO_0000115"
oboHasDbXref =
  "http://www.geneontology.org/formats/oboInOwl#hasDbXref"
oboInSubset =
  "http://www.geneontology.org/formats/oboInOwl#inSubset"
ffImportWarning =
  "https://ff-owl.local/obograph#importWarning"
xsdString =
  "http://www.w3.org/2001/XMLSchema#string"
xsdAnyURI =
  "http://www.w3.org/2001/XMLSchema#anyURI"
compactXSDAnyURI =
  "xsd:anyURI"

rawXSDStringIRI : RawIRI
rawXSDStringIRI =
  rawIRIFromText xsdString

rawStringLiteral : String → RawLiteral
rawStringLiteral text =
  rawLiteral text (present rawXSDStringIRI) absent

rawTextAnnotation : String → String → RawAnnotation
rawTextAnnotation property value =
  rawAnnotation []
    (rawIRIFromText property)
    (rawAnnotationValueLiteral (rawStringLiteral value))

propertyValueTypeIsAnyURI : String → Bool
propertyValueTypeIsAnyURI valueType with primStringEquality valueType xsdAnyURI
... | true =
  true
... | false =
  primStringEquality valueType compactXSDAnyURI

rawPropertyValueValue : PropertyValue → RawAnnotationValue
rawPropertyValueValue value with propertyValueType value
... | absent =
  rawAnnotationValueLiteral (rawStringLiteral (propertyValueText value))
... | present valueType with propertyValueTypeIsAnyURI valueType
...   | true =
  rawAnnotationValueIRI (rawIRIFromText (propertyValueText value))
...   | false =
  rawAnnotationValueLiteral (rawStringLiteral (propertyValueText value))

rawPropertyValueWarnings : PropertyValue → List RawAnnotation
rawPropertyValueWarnings value with propertyValueType value
... | absent =
  []
... | present valueType with propertyValueTypeIsAnyURI valueType
...   | true =
  []
...   | false =
  rawTextAnnotation ffImportWarning valueType ∷ []

rawPropertyValueAnnotation : PropertyValue → RawAnnotation
rawPropertyValueAnnotation value =
  rawAnnotation (rawPropertyValueWarnings value)
    (rawIRIFromText (propertyPredicate value))
    (rawPropertyValueValue value)

deprecatedAnnotations : Bool → List RawAnnotation
deprecatedAnnotations true =
  rawTextAnnotation owlDeprecated "true" ∷ []
deprecatedAnnotations false =
  []

metaRawAnnotations : Meta → List RawAnnotation
metaRawAnnotations m =
  map (rawTextAnnotation iaoDefinition) (toList (definition m))
  ++ map (rawTextAnnotation rdfsComment) (comments m)
  ++ map (rawTextAnnotation oboHasDbXref) (xrefs m)
  ++ map (rawTextAnnotation oboInSubset) (subsets m)
  ++ map
       (λ s → rawTextAnnotation (synonymPredicate s) (synonymValue s))
       (synonyms m)
  ++ map rawPropertyValueAnnotation (basicPropertyValues m)
  ++ deprecatedAnnotations (deprecated m)
  ++ map (rawTextAnnotation ffImportWarning) (unsupported m)

rawAnnotationPropertyDeclaration : String → RawAnnotated RawAxiom
rawAnnotationPropertyDeclaration property =
  rawAnnotated []
    (rawDeclaration
      (rawEntity rawAnnotationProperty (rawIRIFromText property)))

deprecatedAnnotationPropertyDeclarations :
  Bool →
  List (RawAnnotated RawAxiom)
deprecatedAnnotationPropertyDeclarations true =
  rawAnnotationPropertyDeclaration owlDeprecated ∷ []
deprecatedAnnotationPropertyDeclarations false =
  []

rawPropertyValueWarningDeclarations :
  PropertyValue →
  List (RawAnnotated RawAxiom)
rawPropertyValueWarningDeclarations value with propertyValueType value
... | absent =
  []
... | present valueType with propertyValueTypeIsAnyURI valueType
...   | true =
  []
...   | false =
  rawAnnotationPropertyDeclaration ffImportWarning ∷ []

metaAnnotationPropertyDeclarations :
  Meta →
  List (RawAnnotated RawAxiom)
metaAnnotationPropertyDeclarations m =
  map (λ _ → rawAnnotationPropertyDeclaration iaoDefinition)
      (toList (definition m))
  ++ map (λ _ → rawAnnotationPropertyDeclaration rdfsComment) (comments m)
  ++ map (λ _ → rawAnnotationPropertyDeclaration oboHasDbXref) (xrefs m)
  ++ map (λ _ → rawAnnotationPropertyDeclaration oboInSubset) (subsets m)
  ++ map
       (λ s → rawAnnotationPropertyDeclaration (synonymPredicate s))
       (synonyms m)
  ++ map
       (λ p → rawAnnotationPropertyDeclaration (propertyPredicate p))
       (basicPropertyValues m)
  ++ concatMap rawPropertyValueWarningDeclarations (basicPropertyValues m)
  ++ deprecatedAnnotationPropertyDeclarations (deprecated m)
  ++ map (λ _ → rawAnnotationPropertyDeclaration ffImportWarning)
         (unsupported m)

nodeLabelRawAnnotations : Node → List RawAnnotation
nodeLabelRawAnnotations n =
  map (rawTextAnnotation rdfsLabel) (toList (nodeLabel n))

nodeRawAnnotations : Node → List RawAnnotation
nodeRawAnnotations n =
  nodeLabelRawAnnotations n ++ metaRawAnnotations (nodeMeta n)

nodeLabelAnnotationPropertyDeclarations :
  Node →
  List (RawAnnotated RawAxiom)
nodeLabelAnnotationPropertyDeclarations n =
  map
    (λ _ → rawAnnotationPropertyDeclaration rdfsLabel)
    (toList (nodeLabel n))

nodeAnnotationPropertyDeclarations :
  Node →
  List (RawAnnotated RawAxiom)
nodeAnnotationPropertyDeclarations n =
  nodeLabelAnnotationPropertyDeclarations n ++
  metaAnnotationPropertyDeclarations (nodeMeta n)

edgeRawAnnotations : Edge → List RawAnnotation
edgeRawAnnotations e =
  metaRawAnnotations (edgeMeta e)

edgeAnnotationPropertyDeclarations :
  Edge →
  List (RawAnnotated RawAxiom)
edgeAnnotationPropertyDeclarations e =
  metaAnnotationPropertyDeclarations (edgeMeta e)

rawXSDStringDeclaration : RawAnnotated RawAxiom
rawXSDStringDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawDatatype rawXSDStringIRI))

rawAnnotationValueUsesStringDatatype : RawAnnotationValue → Bool
rawAnnotationValueUsesStringDatatype (rawAnnotationValueIRI iri) =
  false
rawAnnotationValueUsesStringDatatype (rawAnnotationValueAnonymous name) =
  false
rawAnnotationValueUsesStringDatatype (rawAnnotationValueLiteral literal) =
  true

mutual
  rawAnnotationUsesStringDatatype : RawAnnotation → Bool
  rawAnnotationUsesStringDatatype (rawAnnotation annotations property value) =
    if rawAnnotationsUseStringDatatype annotations then true else
    rawAnnotationValueUsesStringDatatype value

  rawAnnotationsUseStringDatatype : List RawAnnotation → Bool
  rawAnnotationsUseStringDatatype [] =
    false
  rawAnnotationsUseStringDatatype (annotation ∷ annotations) =
    if rawAnnotationUsesStringDatatype annotation then true else
    rawAnnotationsUseStringDatatype annotations

metadataStringDatatypeDeclarations :
  List RawAnnotation →
  List (RawAnnotated RawAxiom)
metadataStringDatatypeDeclarations annotations with
  rawAnnotationsUseStringDatatype annotations
... | true =
  rawXSDStringDeclaration ∷ []
... | false =
  []

graphRawAnnotations : Graph → List RawAnnotation
graphRawAnnotations g =
  metaRawAnnotations (graphMeta g)

graphRawAnnotationPayload : Graph → List RawAnnotation
graphRawAnnotationPayload g =
  graphRawAnnotations g ++
  concatMap nodeRawAnnotations (nodes g) ++
  concatMap edgeRawAnnotations (edges g)

graphAnnotationPropertyDeclarations :
  Graph →
  List (RawAnnotated RawAxiom)
graphAnnotationPropertyDeclarations g =
  metaAnnotationPropertyDeclarations (graphMeta g) ++
  concatMap nodeAnnotationPropertyDeclarations (nodes g) ++
  concatMap edgeAnnotationPropertyDeclarations (edges g)

metadataSupportAxiomsFromGraph : Graph → List (RawAnnotated RawAxiom)
metadataSupportAxiomsFromGraph g =
  metadataStringDatatypeDeclarations (graphRawAnnotationPayload g) ++
  graphAnnotationPropertyDeclarations g

rawEntityKindFromPropertyType : Optional PropertyType → RawEntityKind
rawEntityKindFromPropertyType (present objectProperty) =
  rawObjectProperty
rawEntityKindFromPropertyType (present annotationProperty) =
  rawAnnotationProperty
rawEntityKindFromPropertyType (present dataProperty) =
  rawDataProperty
rawEntityKindFromPropertyType (present unknownProperty) =
  rawUnknownEntityKind
rawEntityKindFromPropertyType absent =
  rawUnknownEntityKind

rawEntityKindFromNode : Node → RawEntityKind
rawEntityKindFromNode n with nodeType n
... | classNode =
  rawClass
... | individualNode =
  rawIndividual
... | propertyNode =
  rawEntityKindFromPropertyType (nodePropertyType n)
... | unknownNode =
  rawUnknownEntityKind

rawDeclarationFromNode : Node → RawAnnotated RawAxiom
rawDeclarationFromNode n =
  rawAnnotated (nodeRawAnnotations n)
    (rawDeclaration
      (rawEntity (rawEntityKindFromNode n) (rawIRIFromText (nodeId n))))

lookupNodeById : String → List Node → Optional Node
lookupNodeById text [] =
  absent
lookupNodeById text (n ∷ ns) with primStringEquality text (nodeId n)
... | true =
  present n
... | false =
  lookupNodeById text ns

rawUnsupportedAxiomFromEdge : Edge → RawAnnotated RawAxiom
rawUnsupportedAxiomFromEdge e =
  rawAnnotated (edgeRawAnnotations e) (rawUnsupportedAxiom (edgePredicate e))

rawAnnotatedEdgeAxiom : Edge → RawAxiom → RawAnnotated RawAxiom
rawAnnotatedEdgeAxiom e axiom =
  rawAnnotated (edgeRawAnnotations e) axiom

rawTypeAxiomFromNodes :
  Edge →
  Node →
  Node →
  RawAnnotated RawAxiom
rawTypeAxiomFromNodes e subject object with nodeType subject | nodeType object
... | individualNode | classNode =
  rawAnnotatedEdgeAxiom e
    (rawClassAssertion
      (rawNamedClass (rawIRIFromText (edgeObject e)))
      (rawNamedIndividual (rawIRIFromText (edgeSubject e))))
... | _ | _ =
  rawUnsupportedAxiomFromEdge e

rawTypeAxiomFromEdge : List Node → Edge → RawAnnotated RawAxiom
rawTypeAxiomFromEdge ns e with
  lookupNodeById (edgeSubject e) ns |
  lookupNodeById (edgeObject e) ns
... | present subject | present object =
  rawTypeAxiomFromNodes e subject object
... | _ | _ =
  rawUnsupportedAxiomFromEdge e

rawRelationAxiomFromNodes :
  Edge →
  Node →
  Node →
  Node →
  RawAnnotated RawAxiom
rawRelationAxiomFromNodes e subject predicate object with
  nodeType subject | nodeType predicate | nodePropertyType predicate |
  nodeType object
... | classNode | propertyNode | present objectProperty | classNode =
  rawAnnotatedEdgeAxiom e
    (rawSubClassOf
      (rawNamedClass (rawIRIFromText (edgeSubject e)))
      (rawObjectSomeValuesFrom
        (rawObjectProperty (rawIRIFromText (edgePredicate e)))
        (rawNamedClass (rawIRIFromText (edgeObject e)))))
... | individualNode | propertyNode | present objectProperty | individualNode =
  rawAnnotatedEdgeAxiom e
    (rawObjectPropertyAssertion
      (rawObjectProperty (rawIRIFromText (edgePredicate e)))
      (rawNamedIndividual (rawIRIFromText (edgeSubject e)))
      (rawNamedIndividual (rawIRIFromText (edgeObject e))))
... | _ | _ | _ | _ =
  rawUnsupportedAxiomFromEdge e

rawRelationAxiomFromEdge : List Node → Edge → RawAnnotated RawAxiom
rawRelationAxiomFromEdge ns e with
  lookupNodeById (edgeSubject e) ns |
  lookupNodeById (edgePredicate e) ns |
  lookupNodeById (edgeObject e) ns
... | present subject | present predicate | present object =
  rawRelationAxiomFromNodes e subject predicate object
... | _ | _ | _ =
  rawUnsupportedAxiomFromEdge e

rawAxiomFromEdge : List Node → Edge → RawAnnotated RawAxiom
rawAxiomFromEdge ns e with primStringEquality (edgePredicate e) "is_a"
... | true =
  rawAnnotatedEdgeAxiom e
    (rawSubClassOf
      (rawNamedClass (rawIRIFromText (edgeSubject e)))
      (rawNamedClass (rawIRIFromText (edgeObject e))))
... | false with primStringEquality (edgePredicate e) "type"
...   | true =
  rawTypeAxiomFromEdge ns e
...   | false =
  rawRelationAxiomFromEdge ns e

rawAllValuesFromAxiomFromEdge : Edge → RawAnnotated RawAxiom
rawAllValuesFromAxiomFromEdge e =
  rawAnnotatedEdgeAxiom e
    (rawSubClassOf
      (rawNamedClass (rawIRIFromText (edgeSubject e)))
      (rawObjectAllValuesFrom
        (rawObjectProperty (rawIRIFromText (edgePredicate e)))
        (rawNamedClass (rawIRIFromText (edgeObject e)))))

rawAxiomsFromAllValuesFromEdges :
  List Edge → List (RawAnnotated RawAxiom)
rawAxiomsFromAllValuesFromEdges [] =
  []
rawAxiomsFromAllValuesFromEdges (e ∷ edges) =
  rawAllValuesFromAxiomFromEdge e ∷
  rawAxiomsFromAllValuesFromEdges edges

rawAxiomsFromDomainRangeAxiom :
  DomainRangeAxiom → List (RawAnnotated RawAxiom)
rawAxiomsFromDomainRangeAxiom axiom with
  domainClassIds axiom | rangeClassIds axiom
... | [] | [] =
  rawAxiomsFromAllValuesFromEdges (allValuesFromEdges axiom)
... | _ | _ =
  []

rawAxiomsFromDomainRangeAxioms :
  List DomainRangeAxiom → List (RawAnnotated RawAxiom)
rawAxiomsFromDomainRangeAxioms [] =
  []
rawAxiomsFromDomainRangeAxioms (axiom ∷ axioms) =
  rawAxiomsFromDomainRangeAxiom axiom ++
  rawAxiomsFromDomainRangeAxioms axioms

rawAxiomsFromGraph : Graph → List (RawAnnotated RawAxiom)
rawAxiomsFromGraph g =
  metadataSupportAxiomsFromGraph g ++
  map rawDeclarationFromNode (nodes g) ++
  map (rawAxiomFromEdge (nodes g)) (edges g) ++
  rawAxiomsFromDomainRangeAxioms (domainRangeAxioms g)

rawAxiomsFromGraphs : List Graph → List (RawAnnotated RawAxiom)
rawAxiomsFromGraphs [] =
  []
rawAxiomsFromGraphs (g ∷ gs) =
  rawAxiomsFromGraph g ++ rawAxiomsFromGraphs gs

rawAnnotationsFromGraphs : List Graph → List RawAnnotation
rawAnnotationsFromGraphs [] =
  []
rawAnnotationsFromGraphs (g ∷ gs) =
  graphRawAnnotations g ++ rawAnnotationsFromGraphs gs

rawIRIFromOptionalText : Optional String → Optional RawIRI
rawIRIFromOptionalText absent =
  absent
rawIRIFromOptionalText (present text) =
  present (rawIRIFromText text)

ontologyIRIFromDocument : GraphDocument → Optional RawIRI
ontologyIRIFromDocument (graphDocument []) =
  absent
ontologyIRIFromDocument (graphDocument (g ∷ [])) =
  rawIRIFromOptionalText (graphId g)
ontologyIRIFromDocument (graphDocument (g ∷ h ∷ gs)) =
  absent

versionIRIFromDocument : GraphDocument → Optional RawIRI
versionIRIFromDocument (graphDocument []) =
  absent
versionIRIFromDocument (graphDocument (g ∷ [])) =
  rawIRIFromOptionalText (graphVersion g)
versionIRIFromDocument (graphDocument (g ∷ h ∷ gs)) =
  absent

rawOntologyFromOBOGraph : GraphDocument → RawOntology
rawOntologyFromOBOGraph doc =
  rawOntology
    obographSource
    (ontologyIRIFromDocument doc)
    (versionIRIFromDocument doc)
    []
    (rawAnnotationsFromGraphs (graphs doc))
    (rawAxiomsFromGraphs (graphs doc))

nodeSupportDiagnostics : Node → Diagnostics
nodeSupportDiagnostics n with nodeType n
... | unknownNode =
  singleDiagnostic (unsupportedNodeTypeDiagnostic n)
... | classNode =
  noDiagnostics
... | individualNode =
  noDiagnostics
... | propertyNode =
  noDiagnostics

nodesSupportDiagnostics : List Node → Diagnostics
nodesSupportDiagnostics [] =
  noDiagnostics
nodesSupportDiagnostics (n ∷ ns) =
  nodeSupportDiagnostics n ++ nodesSupportDiagnostics ns

isAEndpointDiagnostics : List Node → Edge → String → Diagnostics
isAEndpointDiagnostics ns e text with lookupNodeById text ns
... | absent =
  noDiagnostics
... | present n with nodeType n
...   | classNode =
  noDiagnostics
...   | individualNode =
  singleDiagnostic (isANonClassEndpointDiagnostic text e)
...   | propertyNode =
  singleDiagnostic (isANonClassEndpointDiagnostic text e)
...   | unknownNode =
  singleDiagnostic (isANonClassEndpointDiagnostic text e)

isAEdgeDiagnostics : List Node → Edge → Diagnostics
isAEdgeDiagnostics ns e =
  isAEndpointDiagnostics ns e (edgeSubject e) ++
  isAEndpointDiagnostics ns e (edgeObject e)

typeEdgeSupportDiagnosticsFromNodes :
  Edge →
  Node →
  Node →
  Diagnostics
typeEdgeSupportDiagnosticsFromNodes e subject object with
  nodeType subject | nodeType object
... | individualNode | classNode =
  noDiagnostics
... | _ | _ =
  singleDiagnostic (unsupportedTypeEdgeDiagnostic e)

typeEdgeSupportDiagnostics : List Node → Edge → Diagnostics
typeEdgeSupportDiagnostics ns e with
  lookupNodeById (edgeSubject e) ns |
  lookupNodeById (edgeObject e) ns
... | present subject | present object =
  typeEdgeSupportDiagnosticsFromNodes e subject object
... | _ | _ =
  noDiagnostics

relationEdgeSupportDiagnosticsFromNodes :
  Edge →
  Node →
  Node →
  Node →
  Diagnostics
relationEdgeSupportDiagnosticsFromNodes e subject predicate object with
  nodeType subject | nodeType predicate | nodePropertyType predicate |
  nodeType object
... | classNode | propertyNode | present objectProperty | classNode =
  noDiagnostics
... | individualNode | propertyNode | present objectProperty | individualNode =
  noDiagnostics
... | _ | _ | _ | _ =
  singleDiagnostic (unsupportedEdgeDiagnostic e)

relationEdgeSupportDiagnostics : List Node → Edge → Diagnostics
relationEdgeSupportDiagnostics ns e with
  lookupNodeById (edgeSubject e) ns |
  lookupNodeById (edgePredicate e) ns |
  lookupNodeById (edgeObject e) ns
... | present subject | present predicate | present object =
  relationEdgeSupportDiagnosticsFromNodes e subject predicate object
... | _ | _ | _ =
  noDiagnostics

edgeSupportDiagnostics : List Node → Edge → Diagnostics
edgeSupportDiagnostics ns e with primStringEquality (edgePredicate e) "is_a"
... | true =
  isAEdgeDiagnostics ns e
... | false with primStringEquality (edgePredicate e) "type"
...   | true =
  typeEdgeSupportDiagnostics ns e
...   | false =
  relationEdgeSupportDiagnostics ns e

edgesSupportDiagnostics : List Node → List Edge → Diagnostics
edgesSupportDiagnostics ns [] =
  noDiagnostics
edgesSupportDiagnostics ns (e ∷ es) =
  edgeSupportDiagnostics ns e ++ edgesSupportDiagnostics ns es

allValuesFromEdgeSupportDiagnosticsFromNodes :
  Edge →
  Node →
  Node →
  Node →
  Diagnostics
allValuesFromEdgeSupportDiagnosticsFromNodes e subject predicate object with
  nodeType subject | nodeType predicate | nodePropertyType predicate |
  nodeType object
... | classNode | propertyNode | present objectProperty | classNode =
  noDiagnostics
... | _ | _ | _ | _ =
  singleDiagnostic unsupportedDomainRangeDiagnostic

allValuesFromEdgeSupportDiagnostics : List Node → Edge → Diagnostics
allValuesFromEdgeSupportDiagnostics ns e with
  lookupNodeById (edgeSubject e) ns |
  lookupNodeById (edgePredicate e) ns |
  lookupNodeById (edgeObject e) ns
... | present subject | present predicate | present object =
  allValuesFromEdgeSupportDiagnosticsFromNodes e subject predicate object
... | _ | _ | _ =
  noDiagnostics

allValuesFromEdgesSupportDiagnostics :
  List Node → List Edge → Diagnostics
allValuesFromEdgesSupportDiagnostics ns [] =
  noDiagnostics
allValuesFromEdgesSupportDiagnostics ns (e ∷ es) =
  allValuesFromEdgeSupportDiagnostics ns e ++
  allValuesFromEdgesSupportDiagnostics ns es

domainRangeAxiomSupportDiagnostics :
  List Node → DomainRangeAxiom → Diagnostics
domainRangeAxiomSupportDiagnostics ns axiom with
  domainClassIds axiom | rangeClassIds axiom
... | [] | [] =
  allValuesFromEdgesSupportDiagnostics ns (allValuesFromEdges axiom)
... | _ | _ =
  singleDiagnostic unsupportedDomainRangeDiagnostic

domainRangeAxiomsSupportDiagnostics :
  List Node → List DomainRangeAxiom → Diagnostics
domainRangeAxiomsSupportDiagnostics ns [] =
  noDiagnostics
domainRangeAxiomsSupportDiagnostics ns (axiom ∷ axioms) =
  domainRangeAxiomSupportDiagnostics ns axiom ++
  domainRangeAxiomsSupportDiagnostics ns axioms

nonEmptyDiagnostic :
  ∀ {ℓ} {A : Type ℓ} →
  Diagnostic →
  List A →
  Diagnostics
nonEmptyDiagnostic d [] =
  noDiagnostics
nonEmptyDiagnostic d (_ ∷ _) =
  singleDiagnostic d

graphSupportDiagnostics : Graph → Diagnostics
graphSupportDiagnostics g =
  nodesSupportDiagnostics (nodes g) ++
  edgesSupportDiagnostics (nodes g) (edges g) ++
  nonEmptyDiagnostic
    unsupportedEquivalentNodesDiagnostic
    (equivalentNodesSets g) ++
  nonEmptyDiagnostic
    unsupportedLogicalDefinitionsDiagnostic
    (logicalDefinitionAxioms g) ++
  domainRangeAxiomsSupportDiagnostics (nodes g) (domainRangeAxioms g) ++
  nonEmptyDiagnostic
    unsupportedPropertyChainsDiagnostic
    (propertyChainAxioms g) ++
  nonEmptyDiagnostic
    unsupportedGraphPayloadDiagnostic
    (graphUnsupported g)

graphsSupportDiagnostics : List Graph → Diagnostics
graphsSupportDiagnostics [] =
  noDiagnostics
graphsSupportDiagnostics (g ∷ gs) =
  graphSupportDiagnostics g ++ graphsSupportDiagnostics gs

missingReferenceDiagnostics : List Ref.MissingNodeReference → Diagnostics
missingReferenceDiagnostics [] =
  noDiagnostics
missingReferenceDiagnostics (missing ∷ missingRefs) =
  singleDiagnostic (missingNodeReferenceDiagnostic missing) ++
  missingReferenceDiagnostics missingRefs

obographRawDiagnostics : ImportPolicy → GraphDocument → Diagnostics
obographRawDiagnostics policy doc =
  policyDiagnostics policy doc ++
  missingReferenceDiagnostics (Ref.missingNodeReferencesInDocument doc) ++
  graphsSupportDiagnostics (graphs doc)

record ImportsOBOGraphToRaw
  (doc : GraphDocument)
  (raw : RawOntology)
  : Type₀ where
  constructor importsOBOGraphToRaw
  field
    rawMatchesTranslation :
      raw ≡ rawOntologyFromOBOGraph doc

open ImportsOBOGraphToRaw public

OBOGraphRawImportResult : Type₀
OBOGraphRawImportResult =
  CheckResult
    GraphDocument
    (λ _ → RawOntology)
    ImportsOBOGraphToRaw

obographRawEvidence? :
  ImportPolicy →
  GraphDocument →
  Diagnostics →
  Optional RawOntology
obographRawEvidence? policy doc [] =
  present (rawOntologyFromOBOGraph doc)
obographRawEvidence? policy doc (_ ∷ _) =
  absent

obographRawCleanEvidence :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  (diagnostics : Diagnostics) →
  CleanDiagnostics diagnostics →
  Present (obographRawEvidence? policy doc diagnostics)
obographRawCleanEvidence policy doc [] clean =
  presentWitness (rawOntologyFromOBOGraph doc)
obographRawCleanEvidence policy doc (_ ∷ _) ()

obographRawSound :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  (diagnostics : Diagnostics) →
  (proof : Present (obographRawEvidence? policy doc diagnostics)) →
  ImportsOBOGraphToRaw doc (presentValue proof)
obographRawSound policy doc [] (presentWitness raw) =
  importsOBOGraphToRaw refl
obographRawSound policy doc (_ ∷ _) ()

importOBOGraphRaw :
  ImportPolicy →
  GraphDocument →
  OBOGraphRawImportResult
importOBOGraphRaw policy doc =
  let diagnostics = obographRawDiagnostics policy doc in
  record
    { input =
        doc
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        obographRawEvidence? policy doc diagnostics
    ; cleanEvidence =
        obographRawCleanEvidence policy doc diagnostics
    ; sound =
        obographRawSound policy doc diagnostics
    }

importOBOGraphRawStrict : GraphDocument → OBOGraphRawImportResult
importOBOGraphRawStrict =
  importOBOGraphRaw strictPolicy

importOBOGraphRawCompatibility : GraphDocument → OBOGraphRawImportResult
importOBOGraphRawCompatibility =
  importOBOGraphRaw compatibilityPolicy

obographRawImportSucceeded :
  (result : OBOGraphRawImportResult) →
  EvidenceAvailable result →
  RawOntology
obographRawImportSucceeded result evidence =
  evidenceValue result evidence

rawImportSucceeded :
  (result : OBOGraphRawImportResult) →
  EvidenceAvailable result →
  RawOntology
rawImportSucceeded =
  obographRawImportSucceeded