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

module OWL2.OBOGraph.ToPortable where

open import OWL2.Prelude
open import OWL2.OBOGraph.Syntax
import OWL2.Portable.Syntax as P

private
  maybeMap : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
             (A → B) → Optional A → Optional B
  maybeMap f absent =
    absent
  maybeMap f (present x) =
    present (f x)

rdfsLabel rdfsComment rdfType owlDeprecated iaoDefinition
  oboHasDbXref oboInSubset ffImportWarning ffRepresentativeNodeId : String
rdfsLabel =
  "http://www.w3.org/2000/01/rdf-schema#label"
rdfsComment =
  "http://www.w3.org/2000/01/rdf-schema#comment"
rdfType =
  "http://www.w3.org/1999/02/22-rdf-syntax-ns#type"
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"
ffRepresentativeNodeId =
  "https://ff-owl.local/obograph#representativeNodeId"

iri : String → P.IRI
iri =
  P.iri

name : String → P.Name
name text =
  P.named (iri text)

className : String → P.ClassName
className =
  name

objectPropertyName : String → P.ObjectPropertyName
objectPropertyName =
  name

dataPropertyName : String → P.DataPropertyName
dataPropertyName =
  name

datatypeName : String → P.DatatypeName
datatypeName =
  name

annotationPropertyName : String → P.AnnotationPropertyName
annotationPropertyName =
  iri

classExpression : String → P.ClassExpression
classExpression text =
  P.namedClass (className text)

objectPropertyExpression : String → P.ObjectPropertyExpression
objectPropertyExpression text =
  P.objectProperty (objectPropertyName text)

dataPropertyExpression : String → P.DataPropertyExpression
dataPropertyExpression text =
  P.dataProperty (dataPropertyName text)

individual : String → P.Individual
individual text =
  P.namedIndividual (iri text)

subject : String → P.AnnotationSubject
subject text =
  P.annotationSubjectIRI (iri text)

literalValue : String → P.AnnotationValue
literalValue text =
  P.annotationValueLiteral (P.stringLiteral text)

annotation : String → String → P.Annotation
annotation pred value =
  P.annotation [] (annotationPropertyName pred) (literalValue value)

axiom : P.Axiom → P.Annotated P.Axiom
axiom body =
  P.annotated [] body

annotatedAxiom : List P.Annotation → P.Axiom → P.Annotated P.Axiom
annotatedAxiom anns body =
  P.annotated anns body

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

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

twoOrMoreFromList : ∀ {ℓ} {A : Type ℓ} → List A → Optional (P.TwoOrMore A)
twoOrMoreFromList [] =
  absent
twoOrMoreFromList (x ∷ []) =
  absent
twoOrMoreFromList (x ∷ y ∷ xs) =
  present (P.twoOrMore x y xs)

classIntersectionFromList : List P.ClassExpression → Optional P.ClassExpression
classIntersectionFromList [] =
  absent
classIntersectionFromList (x ∷ []) =
  present x
classIntersectionFromList (x ∷ y ∷ xs) =
  present (P.objectIntersectionOf (P.twoOrMore x y xs))

sameString : String → String → Bool
sameString =
  primStringEquality

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

isClassNodeType : NodeType → Bool
isClassNodeType classNode =
  true
isClassNodeType individualNode =
  false
isClassNodeType propertyNode =
  false
isClassNodeType unknownNode =
  false

isIndividualNodeType : NodeType → Bool
isIndividualNodeType individualNode =
  true
isIndividualNodeType classNode =
  false
isIndividualNodeType propertyNode =
  false
isIndividualNodeType unknownNode =
  false

isPropertyNodeType : NodeType → Bool
isPropertyNodeType propertyNode =
  true
isPropertyNodeType classNode =
  false
isPropertyNodeType individualNode =
  false
isPropertyNodeType unknownNode =
  false

isClassId : String → List Node → Bool
isClassId text nodes with lookupNode text nodes
... | present n =
  isClassNodeType (nodeType n)
... | absent =
  true

isIndividualId : String → List Node → Bool
isIndividualId text nodes with lookupNode text nodes
... | present n =
  isIndividualNodeType (nodeType n)
... | absent =
  false

isPropertyId : String → List Node → Bool
isPropertyId text nodes with lookupNode text nodes
... | present n =
  isPropertyNodeType (nodeType n)
... | absent =
  false

data ResolvedPropertyKind : Type₀ where
  objectPropertyKind dataPropertyKind annotationPropertyKind
    unknownPropertyKind nonPropertyKind : ResolvedPropertyKind

propertyTypeKind : Optional PropertyType → ResolvedPropertyKind
propertyTypeKind (present objectProperty) =
  objectPropertyKind
propertyTypeKind (present dataProperty) =
  dataPropertyKind
propertyTypeKind (present annotationProperty) =
  annotationPropertyKind
propertyTypeKind (present unknownProperty) =
  unknownPropertyKind
propertyTypeKind absent =
  unknownPropertyKind

nodePropertyKind : Node → ResolvedPropertyKind
nodePropertyKind n with nodeType n
... | propertyNode =
  propertyTypeKind (nodePropertyType n)
... | classNode =
  nonPropertyKind
... | individualNode =
  nonPropertyKind
... | unknownNode =
  nonPropertyKind

lookupPropertyKind : String → List Node → Optional ResolvedPropertyKind
lookupPropertyKind text nodes with lookupNode text nodes
... | present n =
  present (nodePropertyKind n)
... | absent =
  absent

isKnownObjectPropertyId : String → List Node → Bool
isKnownObjectPropertyId text nodes with lookupPropertyKind text nodes
... | present objectPropertyKind =
  true
... | present dataPropertyKind =
  false
... | present annotationPropertyKind =
  false
... | present unknownPropertyKind =
  false
... | present nonPropertyKind =
  false
... | absent =
  false

isClassEquivalentNodeType : NodeType → Bool
isClassEquivalentNodeType classNode =
  true
isClassEquivalentNodeType unknownNode =
  true
isClassEquivalentNodeType individualNode =
  false
isClassEquivalentNodeType propertyNode =
  false

isClassEquivalentId : String → List Node → Bool
isClassEquivalentId text nodes with lookupNode text nodes
... | present n =
  isClassEquivalentNodeType (nodeType n)
... | absent =
  true

isObjectPropertyEquivalentPropertyType : Optional PropertyType → Bool
isObjectPropertyEquivalentPropertyType (present dataProperty) =
  false
isObjectPropertyEquivalentPropertyType (present annotationProperty) =
  false
isObjectPropertyEquivalentPropertyType (present objectProperty) =
  true
isObjectPropertyEquivalentPropertyType (present unknownProperty) =
  true
isObjectPropertyEquivalentPropertyType absent =
  true

isObjectPropertyEquivalentNode : Node → Bool
isObjectPropertyEquivalentNode n with nodeType n
... | propertyNode =
  isObjectPropertyEquivalentPropertyType (nodePropertyType n)
... | classNode =
  false
... | individualNode =
  false
... | unknownNode =
  false

isObjectPropertyEquivalentId : String → List Node → Bool
isObjectPropertyEquivalentId text nodes with lookupNode text nodes
... | present n =
  isObjectPropertyEquivalentNode n
... | absent =
  false

isDataPropertyEquivalentPropertyType : Optional PropertyType → Bool
isDataPropertyEquivalentPropertyType (present dataProperty) =
  true
isDataPropertyEquivalentPropertyType (present annotationProperty) =
  false
isDataPropertyEquivalentPropertyType (present objectProperty) =
  false
isDataPropertyEquivalentPropertyType (present unknownProperty) =
  false
isDataPropertyEquivalentPropertyType absent =
  false

isDataPropertyEquivalentNode : Node → Bool
isDataPropertyEquivalentNode n with nodeType n
... | propertyNode =
  isDataPropertyEquivalentPropertyType (nodePropertyType n)
... | classNode =
  false
... | individualNode =
  false
... | unknownNode =
  false

isDataPropertyEquivalentId : String → List Node → Bool
isDataPropertyEquivalentId text nodes with lookupNode text nodes
... | present n =
  isDataPropertyEquivalentNode n
... | absent =
  false

allBy : (String → Bool) → List String → Bool
allBy p [] =
  true
allBy p (x ∷ xs) =
  if p x then allBy p xs else false

metaAnnotations : Meta → List P.Annotation
metaAnnotations m =
  map (annotation iaoDefinition) (optionalToList (definition m))
  ++ map (annotation rdfsComment) (comments m)
  ++ map (annotation oboHasDbXref) (xrefs m)
  ++ map (annotation oboInSubset) (subsets m)
  ++ map (λ s → annotation (synonymPredicate s) (synonymValue s)) (synonyms m)
  ++ map (λ p → annotation (propertyPredicate p) (propertyValueText p))
         (basicPropertyValues m)
  ++ deprecatedAnnotation (deprecated m)
  ++ map (annotation ffImportWarning) (unsupported m)
  where
  deprecatedAnnotation : Bool → List P.Annotation
  deprecatedAnnotation true =
    annotation owlDeprecated "true" ∷ []
  deprecatedAnnotation false =
    []

metaAnnotationAxioms : P.AnnotationSubject → Meta → List (P.Annotated P.Axiom)
metaAnnotationAxioms target m =
  concatMap (λ text →
    axiom (P.annotationAssertion (annotationPropertyName iaoDefinition) target (literalValue text)) ∷ [])
    (optionalToList (definition m))
  ++ map (λ text →
    axiom (P.annotationAssertion (annotationPropertyName rdfsComment) target (literalValue text)))
    (comments m)
  ++ map (λ text →
    axiom (P.annotationAssertion (annotationPropertyName oboHasDbXref) target (literalValue text)))
    (xrefs m)
  ++ map (λ text →
    axiom (P.annotationAssertion (annotationPropertyName oboInSubset) target (literalValue text)))
    (subsets m)
  ++ map (λ s →
    axiom (P.annotationAssertion (annotationPropertyName (synonymPredicate s)) target (literalValue (synonymValue s))))
    (synonyms m)
  ++ map (λ p →
    axiom (P.annotationAssertion (annotationPropertyName (propertyPredicate p)) target (literalValue (propertyValueText p))))
    (basicPropertyValues m)
  ++ deprecatedAxioms (deprecated m)
  ++ map (λ text →
    axiom (P.annotationAssertion (annotationPropertyName ffImportWarning) target (literalValue text)))
    (unsupported m)
  where
  deprecatedAxioms : Bool → List (P.Annotated P.Axiom)
  deprecatedAxioms true =
    axiom (P.annotationAssertion (annotationPropertyName owlDeprecated) target (literalValue "true")) ∷ []
  deprecatedAxioms false =
    []

annotationPropertyDeclaration : String → P.Annotated P.Axiom
annotationPropertyDeclaration text =
  axiom (P.declaration (P.annotationPropertyEntity (annotationPropertyName text)))

metaAnnotationPropertyDeclarations : Meta → List (P.Annotated P.Axiom)
metaAnnotationPropertyDeclarations m =
  map (λ _ → annotationPropertyDeclaration iaoDefinition)
      (optionalToList (definition m))
  ++ map (λ _ → annotationPropertyDeclaration rdfsComment) (comments m)
  ++ map (λ _ → annotationPropertyDeclaration oboHasDbXref) (xrefs m)
  ++ map (λ _ → annotationPropertyDeclaration oboInSubset) (subsets m)
  ++ map (λ s → annotationPropertyDeclaration (synonymPredicate s))
         (synonyms m)
  ++ map (λ p → annotationPropertyDeclaration (propertyPredicate p))
         (basicPropertyValues m)
  ++ deprecatedDeclaration (deprecated m)
  ++ map (λ _ → annotationPropertyDeclaration ffImportWarning)
         (unsupported m)
  where
  deprecatedDeclaration : Bool → List (P.Annotated P.Axiom)
  deprecatedDeclaration true =
    annotationPropertyDeclaration owlDeprecated ∷ []
  deprecatedDeclaration false =
    []

propertyDeclaration : String → Optional PropertyType → P.Annotated P.Axiom
propertyDeclaration text (present annotationProperty) =
  axiom (P.declaration (P.annotationPropertyEntity (annotationPropertyName text)))
propertyDeclaration text (present dataProperty) =
  axiom (P.declaration (P.dataPropertyEntity (dataPropertyName text)))
propertyDeclaration text (present objectProperty) =
  axiom (P.declaration (P.objectPropertyEntity (objectPropertyName text)))
propertyDeclaration text (present unknownProperty) =
  axiom (P.declaration (P.objectPropertyEntity (objectPropertyName text)))
propertyDeclaration text absent =
  axiom (P.declaration (P.objectPropertyEntity (objectPropertyName text)))

nodeDeclaration : Node → P.Annotated P.Axiom
nodeDeclaration n with nodeType n
... | classNode =
  axiom (P.declaration (P.classEntity (className (nodeId n))))
... | individualNode =
  axiom (P.declaration (P.namedIndividualEntity (iri (nodeId n))))
... | propertyNode =
  propertyDeclaration (nodeId n) (nodePropertyType n)
... | unknownNode =
  axiom (P.declaration (P.classEntity (className (nodeId n))))

nodeLabelAxioms : Node → List (P.Annotated P.Axiom)
nodeLabelAxioms n =
  map
    (λ text →
      axiom
        (P.annotationAssertion
          (annotationPropertyName rdfsLabel)
          (subject (nodeId n))
          (literalValue text)))
    (optionalToList (nodeLabel n))

nodeLabelAnnotationPropertyDeclarations : Node → List (P.Annotated P.Axiom)
nodeLabelAnnotationPropertyDeclarations n =
  map
    (λ _ → annotationPropertyDeclaration rdfsLabel)
    (optionalToList (nodeLabel n))

nodeAxioms : Node → List (P.Annotated P.Axiom)
nodeAxioms n =
  nodeDeclaration n ∷
  nodeLabelAnnotationPropertyDeclarations n ++
  metaAnnotationPropertyDeclarations (nodeMeta n) ++
  nodeLabelAxioms n ++
  metaAnnotationAxioms (subject (nodeId n)) (nodeMeta n)

data EdgeKind : Type₀ where
  classIsAEdge objectPropertyIsAEdge dataPropertyIsAEdge
    annotationPropertyIsAEdge unsupportedPropertyIsAEdge
    typeEdge objectSubPropertyEdge dataSubPropertyEdge
    annotationSubPropertyEdge unsupportedSubPropertyEdge
    inverseEdge unsupportedInverseEdge unsupportedRelationEdge
    individualRelationEdge classRelationEdge : EdgeKind

hierarchyEdgeKind :
  ResolvedPropertyKind → Optional ResolvedPropertyKind → EdgeKind
hierarchyEdgeKind objectPropertyKind (present objectPropertyKind) =
  objectPropertyIsAEdge
hierarchyEdgeKind dataPropertyKind (present dataPropertyKind) =
  dataPropertyIsAEdge
hierarchyEdgeKind annotationPropertyKind (present annotationPropertyKind) =
  annotationPropertyIsAEdge
hierarchyEdgeKind objectPropertyKind _ =
  unsupportedPropertyIsAEdge
hierarchyEdgeKind dataPropertyKind _ =
  unsupportedPropertyIsAEdge
hierarchyEdgeKind annotationPropertyKind _ =
  unsupportedPropertyIsAEdge
hierarchyEdgeKind unknownPropertyKind _ =
  unsupportedPropertyIsAEdge
hierarchyEdgeKind nonPropertyKind _ =
  classIsAEdge

subPropertyEdgeKind :
  Optional ResolvedPropertyKind → Optional ResolvedPropertyKind → EdgeKind
subPropertyEdgeKind (present objectPropertyKind) (present objectPropertyKind) =
  objectSubPropertyEdge
subPropertyEdgeKind (present dataPropertyKind) (present dataPropertyKind) =
  dataSubPropertyEdge
subPropertyEdgeKind (present annotationPropertyKind) (present annotationPropertyKind) =
  annotationSubPropertyEdge
subPropertyEdgeKind _ _ =
  unsupportedSubPropertyEdge

inversePropertyEdgeKind :
  Optional ResolvedPropertyKind → Optional ResolvedPropertyKind → EdgeKind
inversePropertyEdgeKind (present objectPropertyKind) (present objectPropertyKind) =
  inverseEdge
inversePropertyEdgeKind _ _ =
  unsupportedInverseEdge

relationEdgeKind :
  Optional ResolvedPropertyKind → Bool → EdgeKind
relationEdgeKind (present dataPropertyKind) subjectIsIndividual =
  unsupportedRelationEdge
relationEdgeKind (present annotationPropertyKind) subjectIsIndividual =
  unsupportedRelationEdge
relationEdgeKind (present nonPropertyKind) subjectIsIndividual =
  unsupportedRelationEdge
relationEdgeKind (present objectPropertyKind) true =
  individualRelationEdge
relationEdgeKind (present objectPropertyKind) false =
  classRelationEdge
relationEdgeKind (present unknownPropertyKind) true =
  individualRelationEdge
relationEdgeKind (present unknownPropertyKind) false =
  classRelationEdge
relationEdgeKind absent true =
  individualRelationEdge
relationEdgeKind absent false =
  classRelationEdge

edgeKind : List Node → Edge → EdgeKind
edgeKind nodes e =
  if sameString (edgePredicate e) "is_a"
  then
    isAEdgeKind (lookupPropertyKind (edgeSubject e) nodes)
  else
    if sameString (edgePredicate e) "type"
    then typeEdge
    else
      if sameString (edgePredicate e) "subPropertyOf"
      then
        subPropertyEdgeKind
          (lookupPropertyKind (edgeSubject e) nodes)
          (lookupPropertyKind (edgeObject e) nodes)
      else
        if sameString (edgePredicate e) "inverseOf"
        then
          inversePropertyEdgeKind
            (lookupPropertyKind (edgeSubject e) nodes)
            (lookupPropertyKind (edgeObject e) nodes)
        else
          relationEdgeKind
            (lookupPropertyKind (edgePredicate e) nodes)
            (isIndividualId (edgeSubject e) nodes)
  where
  isAEdgeKind : Optional ResolvedPropertyKind → EdgeKind
  isAEdgeKind absent =
    classIsAEdge
  isAEdgeKind (present nonPropertyKind) =
    classIsAEdge
  isAEdgeKind (present k) =
    hierarchyEdgeKind k (lookupPropertyKind (edgeObject e) nodes)

warningAxiom : String → String → P.Annotated P.Axiom
warningAxiom target text =
  axiom
    (P.annotationAssertion
      (annotationPropertyName ffImportWarning)
      (subject target)
      (literalValue text))

edgeAxiom : List Node → Edge → P.Annotated P.Axiom
edgeAxiom nodes e with edgeKind nodes e
... | objectPropertyIsAEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subObjectPropertyOf
      (P.subObjectProperty (objectPropertyExpression (edgeSubject e)))
      (objectPropertyExpression (edgeObject e)))
... | dataPropertyIsAEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subDataPropertyOf
      (dataPropertyExpression (edgeSubject e))
      (dataPropertyExpression (edgeObject e)))
... | annotationPropertyIsAEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subAnnotationPropertyOf
      (annotationPropertyName (edgeSubject e))
      (annotationPropertyName (edgeObject e)))
... | unsupportedPropertyIsAEdge =
  warningAxiom (edgeSubject e) "unsupported or mismatched is_a property edge"
... | classIsAEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subClassOf (classExpression (edgeSubject e)) (classExpression (edgeObject e)))
... | typeEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.classAssertion (classExpression (edgeObject e)) (individual (edgeSubject e)))
... | objectSubPropertyEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subObjectPropertyOf
      (P.subObjectProperty (objectPropertyExpression (edgeSubject e)))
      (objectPropertyExpression (edgeObject e)))
... | dataSubPropertyEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subDataPropertyOf
      (dataPropertyExpression (edgeSubject e))
      (dataPropertyExpression (edgeObject e)))
... | annotationSubPropertyEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subAnnotationPropertyOf
      (annotationPropertyName (edgeSubject e))
      (annotationPropertyName (edgeObject e)))
... | unsupportedSubPropertyEdge =
  warningAxiom (edgeSubject e) "unsupported or mismatched subPropertyOf edge"
... | inverseEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.inverseObjectProperties
      (objectPropertyExpression (edgeSubject e))
      (objectPropertyExpression (edgeObject e)))
... | unsupportedInverseEdge =
  warningAxiom (edgeSubject e) "unsupported non-object inverseOf edge"
... | unsupportedRelationEdge =
  warningAxiom (edgeSubject e) "unsupported non-object relation edge"
... | individualRelationEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.objectPropertyAssertion
      (objectPropertyExpression (edgePredicate e))
      (individual (edgeSubject e))
      (individual (edgeObject e)))
... | classRelationEdge =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subClassOf
      (classExpression (edgeSubject e))
      (P.objectSomeValuesFrom
        (objectPropertyExpression (edgePredicate e))
        (classExpression (edgeObject e))))

edgeAnnotationPropertyDeclarations :
  List Node → Edge → List (P.Annotated P.Axiom)
edgeAnnotationPropertyDeclarations nodes e with edgeKind nodes e
... | objectPropertyIsAEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | dataPropertyIsAEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | annotationPropertyIsAEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | unsupportedPropertyIsAEdge =
  annotationPropertyDeclaration ffImportWarning ∷ []
... | classIsAEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | typeEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | objectSubPropertyEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | dataSubPropertyEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | annotationSubPropertyEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | unsupportedSubPropertyEdge =
  annotationPropertyDeclaration ffImportWarning ∷ []
... | inverseEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | unsupportedInverseEdge =
  annotationPropertyDeclaration ffImportWarning ∷ []
... | unsupportedRelationEdge =
  annotationPropertyDeclaration ffImportWarning ∷ []
... | individualRelationEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | classRelationEdge =
  metaAnnotationPropertyDeclarations (edgeMeta e)

edgeAxioms : List Node → Edge → List (P.Annotated P.Axiom)
edgeAxioms nodes e =
  edgeAnnotationPropertyDeclarations nodes e
  ++ edgeAxiom nodes e ∷ []

allValuesFromEdgeAxiom : Edge → P.Annotated P.Axiom
allValuesFromEdgeAxiom e =
  annotatedAxiom (metaAnnotations (edgeMeta e))
    (P.subClassOf
      (classExpression (edgeSubject e))
      (P.objectAllValuesFrom
        (objectPropertyExpression (edgePredicate e))
        (classExpression (edgeObject e))))

unsupportedAllValuesFromEdgeAxiom : Edge → P.Annotated P.Axiom
unsupportedAllValuesFromEdgeAxiom e =
  warningAxiom
    (edgePredicate e)
    "unsupported allValuesFromEdge for non-object property"

allValuesFromEdgeToPortable :
  List Node → Edge → List (P.Annotated P.Axiom)
allValuesFromEdgeToPortable nodes e with lookupPropertyKind (edgePredicate e) nodes
... | present objectPropertyKind =
  allValuesFromEdgeAxiom e ∷ []
... | present dataPropertyKind =
  unsupportedAllValuesFromEdgeAxiom e ∷ []
... | present annotationPropertyKind =
  unsupportedAllValuesFromEdgeAxiom e ∷ []
... | present unknownPropertyKind =
  allValuesFromEdgeAxiom e ∷ []
... | present nonPropertyKind =
  unsupportedAllValuesFromEdgeAxiom e ∷ []
... | absent =
  allValuesFromEdgeAxiom e ∷ []

allValuesFromEdgesToPortable :
  List Node → DomainRangeAxiom → List (P.Annotated P.Axiom)
allValuesFromEdgesToPortable nodes a =
  concatMap (allValuesFromEdgeToPortable nodes) (allValuesFromEdges a)

domainRangeAxiomsToPortable :
  List Node → DomainRangeAxiom → List (P.Annotated P.Axiom)
domainRangeAxiomsToPortable nodes a with
  lookupPropertyKind (domainRangePredicate a) nodes
... | present objectPropertyKind =
  map
    (λ c →
      axiom
        (P.objectPropertyDomain
          (objectPropertyExpression (domainRangePredicate a))
          (classExpression c)))
    (domainClassIds a)
  ++
  map
    (λ c →
      axiom
        (P.objectPropertyRange
          (objectPropertyExpression (domainRangePredicate a))
          (classExpression c)))
    (rangeClassIds a)
  ++ allValuesFromEdgesToPortable nodes a
... | present dataPropertyKind =
  map
    (λ c →
      axiom
        (P.dataPropertyDomain
          (dataPropertyExpression (domainRangePredicate a))
          (classExpression c)))
    (domainClassIds a)
  ++
  map
    (λ c →
      axiom
        (P.dataPropertyRange
          (dataPropertyExpression (domainRangePredicate a))
          (P.datatype (datatypeName c))))
    (rangeClassIds a)
  ++ allValuesFromEdgesToPortable nodes a
... | present annotationPropertyKind =
  map
    (λ c →
      axiom
        (P.annotationPropertyDomain
          (annotationPropertyName (domainRangePredicate a))
          (iri c)))
    (domainClassIds a)
  ++
  map
    (λ c →
      axiom
        (P.annotationPropertyRange
          (annotationPropertyName (domainRangePredicate a))
          (iri c)))
    (rangeClassIds a)
  ++ allValuesFromEdgesToPortable nodes a
... | present unknownPropertyKind =
  warningAxiom (domainRangePredicate a) "unsupported domain/range axiom for unknown property kind" ∷
  allValuesFromEdgesToPortable nodes a
... | present nonPropertyKind =
  warningAxiom (domainRangePredicate a) "unsupported domain/range axiom for non-property node" ∷
  allValuesFromEdgesToPortable nodes a
... | absent =
  warningAxiom (domainRangePredicate a) "unsupported domain/range axiom for unresolved property" ∷
  allValuesFromEdgesToPortable nodes a

allValuesFromEdgeAnnotationPropertyDeclarations :
  List Node → Edge → List (P.Annotated P.Axiom)
allValuesFromEdgeAnnotationPropertyDeclarations nodes e with
  lookupPropertyKind (edgePredicate e) nodes
... | present objectPropertyKind =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | present dataPropertyKind =
  annotationPropertyDeclaration ffImportWarning ∷ []
... | present annotationPropertyKind =
  annotationPropertyDeclaration ffImportWarning ∷ []
... | present unknownPropertyKind =
  metaAnnotationPropertyDeclarations (edgeMeta e)
... | present nonPropertyKind =
  annotationPropertyDeclaration ffImportWarning ∷ []
... | absent =
  metaAnnotationPropertyDeclarations (edgeMeta e)

allValuesFromEdgesAnnotationPropertyDeclarations :
  List Node → DomainRangeAxiom → List (P.Annotated P.Axiom)
allValuesFromEdgesAnnotationPropertyDeclarations nodes a =
  concatMap
    (allValuesFromEdgeAnnotationPropertyDeclarations nodes)
    (allValuesFromEdges a)

domainRangeAnnotationPropertyDeclarations :
  List Node → DomainRangeAxiom → List (P.Annotated P.Axiom)
domainRangeAnnotationPropertyDeclarations nodes a with
  lookupPropertyKind (domainRangePredicate a) nodes
... | present objectPropertyKind =
  allValuesFromEdgesAnnotationPropertyDeclarations nodes a
... | present dataPropertyKind =
  allValuesFromEdgesAnnotationPropertyDeclarations nodes a
... | present annotationPropertyKind =
  allValuesFromEdgesAnnotationPropertyDeclarations nodes a
... | present unknownPropertyKind =
  annotationPropertyDeclaration ffImportWarning ∷
  allValuesFromEdgesAnnotationPropertyDeclarations nodes a
... | present nonPropertyKind =
  annotationPropertyDeclaration ffImportWarning ∷
  allValuesFromEdgesAnnotationPropertyDeclarations nodes a
... | absent =
  annotationPropertyDeclaration ffImportWarning ∷
  allValuesFromEdgesAnnotationPropertyDeclarations nodes a

knownObjectPropertyChain : List Node → PropertyChainAxiom → Bool
knownObjectPropertyChain nodes a =
  if isKnownObjectPropertyId (chainPredicateId a) nodes
  then allBy (λ text → isKnownObjectPropertyId text nodes) (chainPredicateIds a)
  else false

propertyChainWithKnown :
  PropertyChainAxiom →
  P.TwoOrMore P.ObjectPropertyExpression →
  Bool →
  List (P.Annotated P.Axiom)
propertyChainWithKnown a chain true =
  axiom
    (P.subObjectPropertyOf
      (P.subObjectPropertyChain (P.objectPropertyChain chain))
      (objectPropertyExpression (chainPredicateId a)))
  ∷ []
propertyChainWithKnown a chain false =
  warningAxiom (chainPredicateId a) "unsupported property chain with unresolved or non-object property" ∷ []

propertyChainAxiomToPortable :
  List Node → PropertyChainAxiom → List (P.Annotated P.Axiom)
propertyChainAxiomToPortable nodes a with
  twoOrMoreFromList (map objectPropertyExpression (chainPredicateIds a))
... | present chain =
  propertyChainWithKnown a chain (knownObjectPropertyChain nodes a)
... | absent =
  warningAxiom (chainPredicateId a) "unsupported property chain shorter than two properties" ∷ []

propertyChainAnnotationPropertyDeclarations :
  List Node → PropertyChainAxiom → List (P.Annotated P.Axiom)
propertyChainAnnotationPropertyDeclarations nodes a with
  twoOrMoreFromList (map objectPropertyExpression (chainPredicateIds a))
... | present chain with knownObjectPropertyChain nodes a
...   | true =
  []
...   | false =
  annotationPropertyDeclaration ffImportWarning ∷ []
propertyChainAnnotationPropertyDeclarations nodes a | absent =
  annotationPropertyDeclaration ffImportWarning ∷ []

restrictionExpression : ExistentialRestriction → P.ClassExpression
restrictionExpression r =
  P.objectSomeValuesFrom
    (objectPropertyExpression (restrictionPropertyId r))
    (classExpression (restrictionFillerId r))

logicalDefinitionAxiomToPortable :
  LogicalDefinitionAxiom → List (P.Annotated P.Axiom)
logicalDefinitionAxiomToPortable a with
  classIntersectionFromList
    (map classExpression (genusIds a)
     ++ map restrictionExpression (restrictions a))
... | present rhs =
  axiom
    (P.equivalentClasses
      (P.twoOrMore (classExpression (definedClassId a)) rhs []))
  ∷ []
... | absent =
  []

representativeAnnotation : Optional String → List P.Annotation
representativeAnnotation absent =
  []
representativeAnnotation (present text) =
  annotation ffRepresentativeNodeId text ∷ []

firstString : List String → Optional String
firstString [] =
  absent
firstString (x ∷ xs) =
  present x

equivalentClassesSetToPortable :
  List P.Annotation → List String → List (P.Annotated P.Axiom)
equivalentClassesSetToPortable anns ids with
  twoOrMoreFromList (map classExpression ids)
... | present classes =
  annotatedAxiom
    anns
    (P.equivalentClasses classes)
  ∷ []
... | absent =
  []

equivalentObjectPropertiesSetToPortable :
  List P.Annotation → List String → List (P.Annotated P.Axiom)
equivalentObjectPropertiesSetToPortable anns ids with
  twoOrMoreFromList (map objectPropertyExpression ids)
... | present properties =
  annotatedAxiom
    anns
    (P.equivalentObjectProperties properties)
  ∷ []
... | absent =
  []

equivalentDataPropertiesSetToPortable :
  List P.Annotation → List String → List (P.Annotated P.Axiom)
equivalentDataPropertiesSetToPortable anns ids with
  twoOrMoreFromList (map dataPropertyExpression ids)
... | present properties =
  annotatedAxiom
    anns
    (P.equivalentDataProperties properties)
  ∷ []
... | absent =
  []

sameIndividualsSetToPortable :
  List P.Annotation → List String → List (P.Annotated P.Axiom)
sameIndividualsSetToPortable anns ids with
  twoOrMoreFromList (map individual ids)
... | present individuals =
  annotatedAxiom
    anns
    (P.sameIndividual individuals)
  ∷ []
... | absent =
  []

unsupportedEquivalentNodesSetToPortable :
  EquivalentNodesSet → List (P.Annotated P.Axiom)
unsupportedEquivalentNodesSetToPortable s with firstString (nodeIds s)
... | present text =
  axiom
    (P.annotationAssertion
      (annotationPropertyName ffImportWarning)
      (subject text)
      (literalValue "unsupported equivalentNodesSet node kinds"))
  ∷ []
... | absent =
  []

equivalentNodesSetAnnotationPropertyDeclarations :
  EquivalentNodesSet → List (P.Annotated P.Axiom)
equivalentNodesSetAnnotationPropertyDeclarations s =
  map
    (λ _ → annotationPropertyDeclaration ffRepresentativeNodeId)
    (optionalToList (representativeNodeId s))
  ++ metaAnnotationPropertyDeclarations (equivalentMeta s)
  ++ annotationPropertyDeclaration ffImportWarning ∷ []

equivalentNodesSetToPortable :
  List Node → EquivalentNodesSet → List (P.Annotated P.Axiom)
equivalentNodesSetToPortable nodes s with
  allBy (λ text → isIndividualId text nodes) (nodeIds s)
... | true =
  sameIndividualsSetToPortable annotations (nodeIds s)
  where
  annotations : List P.Annotation
  annotations =
    representativeAnnotation (representativeNodeId s)
    ++ metaAnnotations (equivalentMeta s)
... | false with
  allBy (λ text → isDataPropertyEquivalentId text nodes) (nodeIds s)
...   | true =
  equivalentDataPropertiesSetToPortable annotations (nodeIds s)
  where
  annotations : List P.Annotation
  annotations =
    representativeAnnotation (representativeNodeId s)
    ++ metaAnnotations (equivalentMeta s)
...   | false with
  allBy (λ text → isObjectPropertyEquivalentId text nodes) (nodeIds s)
...     | true =
  equivalentObjectPropertiesSetToPortable annotations (nodeIds s)
  where
  annotations : List P.Annotation
  annotations =
    representativeAnnotation (representativeNodeId s)
    ++ metaAnnotations (equivalentMeta s)
...     | false with
  allBy (λ text → isClassEquivalentId text nodes) (nodeIds s)
...       | true =
  equivalentClassesSetToPortable annotations (nodeIds s)
  where
  annotations : List P.Annotation
  annotations =
    representativeAnnotation (representativeNodeId s)
    ++ metaAnnotations (equivalentMeta s)
...       | false =
  unsupportedEquivalentNodesSetToPortable s

graphAnnotations : Graph → List P.Annotation
graphAnnotations g =
  metaAnnotations (graphMeta g)
  ++ map (annotation ffImportWarning) (graphUnsupported g)

graphAnnotationPropertyDeclarations : Graph → List (P.Annotated P.Axiom)
graphAnnotationPropertyDeclarations g =
  metaAnnotationPropertyDeclarations (graphMeta g)
  ++ map (λ _ → annotationPropertyDeclaration ffImportWarning)
         (graphUnsupported g)

graphAxioms : Graph → List (P.Annotated P.Axiom)
graphAxioms g =
  graphAnnotationPropertyDeclarations g
  ++ concatMap nodeAxioms (nodes g)
  ++ concatMap (edgeAxioms (nodes g)) (edges g)
  ++ concatMap
       equivalentNodesSetAnnotationPropertyDeclarations
       (equivalentNodesSets g)
  ++ concatMap (equivalentNodesSetToPortable (nodes g)) (equivalentNodesSets g)
  ++ concatMap logicalDefinitionAxiomToPortable (logicalDefinitionAxioms g)
  ++ concatMap
       (domainRangeAnnotationPropertyDeclarations (nodes g))
       (domainRangeAxioms g)
  ++ concatMap (domainRangeAxiomsToPortable (nodes g)) (domainRangeAxioms g)
  ++ concatMap
       (propertyChainAnnotationPropertyDeclarations (nodes g))
       (propertyChainAxioms g)
  ++ concatMap (propertyChainAxiomToPortable (nodes g)) (propertyChainAxioms g)

graphOntologyId : Graph → P.OntologyID
graphOntologyId g with graphId g
... | present text =
  P.ontologyIRI (iri text) (maybeMap iri (graphVersion g))
... | absent =
  P.anonymousOntology

toOntology : Graph → P.Ontology
toOntology g =
  P.ontology
    (graphOntologyId g)
    []
    (graphAnnotations g)
    (graphAxioms g)

toOntologyFromGraphs : List Graph → P.Ontology
toOntologyFromGraphs [] =
  P.emptyOntology
toOntologyFromGraphs (g ∷ gs) =
  P.ontology
    (graphOntologyId g)
    []
    (graphAnnotations g ++ concatMap graphAnnotations gs)
    (graphAxioms g ++ concatMap graphAxioms gs)

toOntologyDocument : GraphDocument → P.OntologyDocument
toOntologyDocument (graphDocument gs) =
  P.ontologyDocument [] (toOntologyFromGraphs gs)