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

module OWL2.OBOGraph.Decode where

open import Agda.Builtin.Nat using (zero; suc)
open import Agda.Builtin.String using (primShowNat; primStringAppend)

open import OWL2.Prelude
open import OWL2.OBOGraph.Syntax
open import FF.Json.Base using (atom; array; object)
open import FF.Json.Native using (JsonValue; string; boolean)

infixl  _>>=_
infixr  _<>_

_<>_ : String → String → String
_<>_ =
  primStringAppend

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

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

fromMaybe : ∀ {ℓ} {A : Type ℓ} → A → Optional A → A
fromMaybe fallback absent =
  fallback
fromMaybe fallback (present x) =
  x

showNat : ℕ → String
showNat =
  primShowNat

indexPath : String → ℕ → String
indexPath path n =
  path <> "[" <> showNat n <> "]"

lookupField : String → List (String × JsonValue) → Optional JsonValue
lookupField key [] =
  absent
lookupField key ((name , value) ∷ fields) with primStringEquality key name
... | true =
  present value
... | false =
  lookupField key fields

asString : JsonValue → Optional String
asString (atom string text) =
  present text
asString _ =
  absent

asBool : JsonValue → Optional Bool
asBool (atom boolean b) =
  present b
asBool _ =
  absent

asArray : JsonValue → Optional (List JsonValue)
asArray (array xs) =
  present xs
asArray _ =
  absent

asObject : JsonValue → Optional (List (String × JsonValue))
asObject (object fields) =
  present fields
asObject _ =
  absent

fieldString : String → List (String × JsonValue) → Optional String
fieldString key fields =
  lookupField key fields >>= asString

fieldBoolDefault : String → Bool → List (String × JsonValue) → Bool
fieldBoolDefault key fallback fields =
  fromMaybe fallback (lookupField key fields >>= asBool)

fieldArrayDefault :
  String → List (String × JsonValue) → List JsonValue
fieldArrayDefault key fields =
  fromMaybe [] (lookupField key fields >>= asArray)

fieldObjectDefault :
  String → List (String × JsonValue) → List (String × JsonValue)
fieldObjectDefault key fields =
  fromMaybe [] (lookupField key fields >>= asObject)

stringIn : String → List String → Bool
stringIn key [] =
  false
stringIn key (candidate ∷ candidates) with primStringEquality key candidate
... | true =
  true
... | false =
  stringIn key candidates

unknownFieldMessages :
  String → String → List String → List (String × JsonValue) → List String
unknownFieldMessages path label known [] =
  []
unknownFieldMessages path label known ((key , value) ∷ fields) with stringIn key known
... | true =
  unknownFieldMessages path label known fields
... | false =
  (path <> ": ignored " <> label <> " field " <> key) ∷
  unknownFieldMessages path label known fields

unknownRawFieldMessages :
  String → List String → List (String × JsonValue) → List String
unknownRawFieldMessages path known [] =
  []
unknownRawFieldMessages path known ((key , value) ∷ fields) with stringIn key known
... | true =
  unknownRawFieldMessages path known fields
... | false =
  (path <> ": ignored field " <> key) ∷
  unknownRawFieldMessages path known fields

hasField : String → List (String × JsonValue) → Bool
hasField key fields with lookupField key fields
... | present _ =
  true
... | absent =
  false

appendIf : Bool → String → List String → List String
appendIf true message messages =
  messages ++ (message ∷ [])
appendIf false message messages =
  messages

decodeList : ∀ {ℓ} {A : Type ℓ} →
             (JsonValue → Optional A) → List JsonValue → List A
decodeList f [] =
  []
decodeList f (x ∷ xs) with f x
... | present y =
  y ∷ decodeList f xs
... | absent =
  decodeList f xs

decodeListAt : ∀ {ℓ} {A : Type ℓ} →
               (ℕ → JsonValue → Optional A) → ℕ → List JsonValue → List A
decodeListAt f n [] =
  []
decodeListAt f n (x ∷ xs) with f n x
... | present y =
  y ∷ decodeListAt f (suc n) xs
... | absent =
  decodeListAt f (suc n) xs

decodeStringList : List JsonValue → List String
decodeStringList =
  decodeList asString

decodeXref : JsonValue → Optional String
decodeXref (atom string text) =
  present text
decodeXref (object fields) =
  fieldString "val" fields
decodeXref _ =
  absent

decodePropertyValue : JsonValue → Optional PropertyValue
decodePropertyValue (object fields) =
  fieldString "pred" fields >>= λ pred →
  fieldString "val" fields >>= λ val →
  present (propertyValue pred val (fieldString "valType" fields))
decodePropertyValue _ =
  absent

propertyValueUnsupported : String → JsonValue → List String
propertyValueUnsupported path (object fields) with fieldString "pred" fields
... | absent =
  (path <> ": ignored property value without string pred/val") ∷ []
... | present pred with fieldString "val" fields
...   | absent =
  (path <> ": ignored property value without string pred/val") ∷ []
...   | present val =
  appendIf
    (hasField "meta" fields)
    (path <> ": ignored nested property value metadata")
    (unknownFieldMessages path "property value" ("pred" ∷ "val" ∷ "xrefs" ∷ "meta" ∷ "valType" ∷ []) fields)
propertyValueUnsupported path _ =
  (path <> ": ignored non-object property value") ∷ []

decodePropertyValuesAt : String → ℕ → List JsonValue → List PropertyValue
decodePropertyValuesAt path n [] =
  []
decodePropertyValuesAt path n (x ∷ xs) with decodePropertyValue x
... | present value =
  value ∷ decodePropertyValuesAt path (suc n) xs
... | absent =
  decodePropertyValuesAt path (suc n) xs

propertyValuesUnsupportedAt : String → ℕ → List JsonValue → List String
propertyValuesUnsupportedAt path n [] =
  []
propertyValuesUnsupportedAt path n (x ∷ xs) =
  propertyValueUnsupported (indexPath path n) x ++
  propertyValuesUnsupportedAt path (suc n) xs

decodeSynonym : JsonValue → Optional Synonym
decodeSynonym (object fields) =
  fieldString "val" fields >>= λ val →
  present (synonym (fromMaybe "hasRelatedSynonym" (fieldString "pred" fields)) val)
decodeSynonym _ =
  absent

synonymUnsupported : String → JsonValue → List String
synonymUnsupported path (object fields) with fieldString "val" fields
... | absent =
  (path <> ": ignored synonym without string val") ∷ []
... | present val =
  appendIf
    (hasField "meta" fields)
    (path <> ": ignored nested synonym metadata")
    []
synonymUnsupported path _ =
  (path <> ": ignored non-object synonym") ∷ []

decodeSynonymsAt : String → ℕ → List JsonValue → List Synonym
decodeSynonymsAt path n [] =
  []
decodeSynonymsAt path n (x ∷ xs) with decodeSynonym x
... | present value =
  value ∷ decodeSynonymsAt path (suc n) xs
... | absent =
  decodeSynonymsAt path (suc n) xs

synonymsUnsupportedAt : String → ℕ → List JsonValue → List String
synonymsUnsupportedAt path n [] =
  []
synonymsUnsupportedAt path n (x ∷ xs) =
  synonymUnsupported (indexPath path n) x ++
  synonymsUnsupportedAt path (suc n) xs

decodeDefinition : JsonValue → Optional String
decodeDefinition (atom string text) =
  present text
decodeDefinition (object fields) =
  fieldString "val" fields
decodeDefinition _ =
  absent

definitionXrefs : JsonValue → List String
definitionXrefs (object fields) =
  decodeList decodeXref (fieldArrayDefault "xrefs" fields)
definitionXrefs _ =
  []

definitionXrefsFromField : List (String × JsonValue) → List String
definitionXrefsFromField fields with lookupField "definition" fields
... | absent =
  []
... | present value =
  definitionXrefs value

definitionUnsupported : String → JsonValue → List String
definitionUnsupported path (atom string text) =
  []
definitionUnsupported path (object fields) =
  appendIf
    (hasField "meta" fields)
    (path <> ".definition: ignored nested metadata")
    (unknownRawFieldMessages (path <> ".definition") ("val" ∷ "xrefs" ∷ "meta" ∷ []) fields)
definitionUnsupported path _ =
  (path <> ": ignored malformed definition") ∷ []

definitionUnsupportedFromField : String → List (String × JsonValue) → List String
definitionUnsupportedFromField path fields with lookupField "definition" fields
... | absent =
  []
... | present value =
  definitionUnsupported path value

metaKnownFields : List String
metaKnownFields =
  "definition" ∷ "comments" ∷ "xrefs" ∷ "subsets" ∷ "synonyms" ∷
  "basicPropertyValues" ∷ "deprecated" ∷ []

graphMetaKnownFields : List String
graphMetaKnownFields =
  "definition" ∷ "comments" ∷ "xrefs" ∷ "subsets" ∷ "synonyms" ∷
  "basicPropertyValues" ∷ "version" ∷ "deprecated" ∷ []

decodeMetaFieldsAt : String → List String → List (String × JsonValue) → Meta
decodeMetaFieldsAt path knownFields fields =
  meta
    (lookupField "definition" fields >>= decodeDefinition)
    (decodeStringList (fieldArrayDefault "comments" fields))
    (definitionXrefsFromField fields ++
     decodeList decodeXref (fieldArrayDefault "xrefs" fields))
    (decodeStringList (fieldArrayDefault "subsets" fields))
    (decodeSynonymsAt (path <> ".synonyms") zero (fieldArrayDefault "synonyms" fields))
    (decodePropertyValuesAt
      (path <> ".basicPropertyValues")
      zero
      (fieldArrayDefault "basicPropertyValues" fields))
    (fieldBoolDefault "deprecated" false fields)
    (definitionUnsupportedFromField path fields ++
     synonymsUnsupportedAt (path <> ".synonyms") zero (fieldArrayDefault "synonyms" fields) ++
     propertyValuesUnsupportedAt
       (path <> ".basicPropertyValues")
       zero
       (fieldArrayDefault "basicPropertyValues" fields) ++
     unknownFieldMessages path "meta" knownFields fields)

decodeMetaAt : String → JsonValue → Optional Meta
decodeMetaAt path (object fields) =
  present (decodeMetaFieldsAt path metaKnownFields fields)
decodeMetaAt path _ =
  present
    (meta absent [] [] [] [] [] false
      ((path <> ": ignored non-object meta") ∷ []))

decodeGraphMetaAt : String → JsonValue → Optional Meta
decodeGraphMetaAt path (object fields) =
  present (decodeMetaFieldsAt path graphMetaKnownFields fields)
decodeGraphMetaAt path _ =
  present
    (meta absent [] [] [] [] [] false
      ((path <> ": ignored non-object meta") ∷ []))

decodeMeta : JsonValue → Optional Meta
decodeMeta =
  decodeMetaAt "meta"

fieldMetaDefault : String → List (String × JsonValue) → Meta
fieldMetaDefault key fields =
  fromMaybe emptyMeta (lookupField key fields >>= decodeMeta)

fieldMetaDefaultAt : String → String → List (String × JsonValue) → Meta
fieldMetaDefaultAt key path fields with lookupField key fields
... | absent =
  emptyMeta
... | present value =
  fromMaybe emptyMeta (decodeMetaAt path value)

fieldGraphMetaDefaultAt : String → String → List (String × JsonValue) → Meta
fieldGraphMetaDefaultAt key path fields with lookupField key fields
... | absent =
  emptyMeta
... | present value =
  fromMaybe emptyMeta (decodeGraphMetaAt path value)

fieldGraphVersionDefault : String → List (String × JsonValue) → Optional String
fieldGraphVersionDefault key fields with lookupField key fields
... | absent =
  absent
... | present (object metaFields) =
  fieldString "version" metaFields
... | present _ =
  absent

appendMetaUnsupported : Meta → List String → Meta
appendMetaUnsupported m messages =
  meta
    (definition m)
    (comments m)
    (xrefs m)
    (subsets m)
    (synonyms m)
    (basicPropertyValues m)
    (deprecated m)
    (unsupported m ++ messages)

nodeTypeFromString : String → NodeType
nodeTypeFromString text with primStringEquality text "CLASS"
... | true =
  classNode
... | false with primStringEquality text "INDIVIDUAL"
...   | true =
  individualNode
...   | false with primStringEquality text "PROPERTY"
...     | true =
  propertyNode
...     | false =
  unknownNode

propertyTypeFromString : String → PropertyType
propertyTypeFromString text with primStringEquality text "OBJECT"
... | true =
  objectProperty
... | false with primStringEquality text "ANNOTATION"
...   | true =
  annotationProperty
...   | false with primStringEquality text "DATA"
...     | true =
  dataProperty
...     | false =
  unknownProperty

decodeNodeAt : ℕ → JsonValue → Optional Node
decodeNodeAt n (object fields) =
  fieldString "id" fields >>= λ nodeId →
  present
    (node
      nodeId
      (fieldString "lbl" fields)
      (nodeTypeFromString (fromMaybe "CLASS" (fieldString "type" fields)))
      (maybeMap propertyTypeFromString (fieldString "propertyType" fields))
      (appendMetaUnsupported
        (fieldMetaDefaultAt "meta" (indexPath "nodes" n <> ".meta") fields)
        (unknownFieldMessages
          (indexPath "nodes" n)
          "node"
          ("id" ∷ "lbl" ∷ "type" ∷ "propertyType" ∷ "meta" ∷ [])
          fields)))
decodeNodeAt n _ =
  absent

decodeNode : JsonValue → Optional Node
decodeNode =
  decodeNodeAt zero

edgeSubjectField : List (String × JsonValue) → Optional String
edgeSubjectField fields with lookupField "sub" fields
... | present value =
  asString value
... | absent =
  fieldString "subj" fields

decodeEdgeAtPath : String → ℕ → JsonValue → Optional Edge
decodeEdgeAtPath path n (object fields) =
  edgeSubjectField fields >>= λ sub →
  fieldString "pred" fields >>= λ pred →
  fieldString "obj" fields >>= λ obj →
  present
    (edge
      sub
      pred
      obj
      (appendMetaUnsupported
        (fieldMetaDefaultAt "meta" (indexPath path n <> ".meta") fields)
        (unknownFieldMessages
          (indexPath path n)
          "edge"
          ("sub" ∷ "subj" ∷ "pred" ∷ "obj" ∷ "meta" ∷ [])
          fields)))
decodeEdgeAtPath path n _ =
  absent

decodeEdgeAt : ℕ → JsonValue → Optional Edge
decodeEdgeAt =
  decodeEdgeAtPath "edges"

decodeEdge : JsonValue → Optional Edge
decodeEdge =
  decodeEdgeAt zero

decodeDomainRangeAxiomAt : ℕ → JsonValue → Optional DomainRangeAxiom
decodeDomainRangeAxiomAt n (object fields) =
  fieldString "predicateId" fields >>= λ pred →
  present
    (domainRangeAxiom
      pred
      (decodeStringList (fieldArrayDefault "domainClassIds" fields))
      (decodeStringList (fieldArrayDefault "rangeClassIds" fields))
      (decodeListAt
        (decodeEdgeAtPath (indexPath "domainRangeAxioms" n <> ".allValuesFromEdges"))
        zero
        (fieldArrayDefault "allValuesFromEdges" fields))
      (fieldMetaDefaultAt
        "meta"
        (indexPath "domainRangeAxioms" n <> ".meta")
        fields))
decodeDomainRangeAxiomAt n _ =
  absent

decodeDomainRangeAxiom : JsonValue → Optional DomainRangeAxiom
decodeDomainRangeAxiom =
  decodeDomainRangeAxiomAt zero

decodePropertyChainAxiomAt : ℕ → JsonValue → Optional PropertyChainAxiom
decodePropertyChainAxiomAt n (object fields) =
  fieldString "predicateId" fields >>= λ pred →
  present
    (propertyChainAxiom
      pred
      (decodeStringList (fieldArrayDefault "chainPredicateIds" fields))
      (fieldMetaDefaultAt
        "meta"
        (indexPath "propertyChainAxioms" n <> ".meta")
        fields))
decodePropertyChainAxiomAt n _ =
  absent

decodePropertyChainAxiom : JsonValue → Optional PropertyChainAxiom
decodePropertyChainAxiom =
  decodePropertyChainAxiomAt zero

decodeRestriction : JsonValue → Optional ExistentialRestriction
decodeRestriction (object fields) =
  fieldString "propertyId" fields >>= λ pred →
  fieldString "fillerId" fields >>= λ filler →
  present (existentialRestriction pred filler)
decodeRestriction _ =
  absent

decodeLogicalDefinitionAxiom : JsonValue → Optional LogicalDefinitionAxiom
decodeLogicalDefinitionAxiom (object fields) =
  fieldString "definedClassId" fields >>= λ defined →
  present
    (logicalDefinitionAxiom
      defined
      (decodeStringList (fieldArrayDefault "genusIds" fields))
      (decodeList decodeRestriction (fieldArrayDefault "restrictions" fields))
      (fieldMetaDefaultAt "meta" "logicalDefinitionAxioms[].meta" fields))
decodeLogicalDefinitionAxiom _ =
  absent

decodeEquivalentNodesSet : JsonValue → Optional EquivalentNodesSet
decodeEquivalentNodesSet (object fields) =
  present
    (equivalentNodesSet
      (fieldString "representativeNodeId" fields)
      (decodeStringList (fieldArrayDefault "nodeIds" fields))
      (fieldMetaDefaultAt "meta" "equivalentNodesSets[].meta" fields))
decodeEquivalentNodesSet _ =
  absent

decodeGraphAt : ℕ → JsonValue → Optional Graph
decodeGraphAt n (object fields) =
  present
    (graph
      (fieldString "id" fields)
      (fieldGraphVersionDefault "meta" fields)
      (fieldGraphMetaDefaultAt "meta" (indexPath "graphs" n <> ".meta") fields)
      (decodeListAt decodeNodeAt zero (fieldArrayDefault "nodes" fields))
      (decodeListAt decodeEdgeAt zero (fieldArrayDefault "edges" fields))
      (decodeList decodeEquivalentNodesSet (fieldArrayDefault "equivalentNodesSets" fields))
      (decodeList decodeLogicalDefinitionAxiom (fieldArrayDefault "logicalDefinitionAxioms" fields))
      (decodeListAt
        decodeDomainRangeAxiomAt
        zero
        (fieldArrayDefault "domainRangeAxioms" fields))
      (decodeListAt
        decodePropertyChainAxiomAt
        zero
        (fieldArrayDefault "propertyChainAxioms" fields))
      (unknownFieldMessages
        (indexPath "graphs" n)
        "graph"
        ("id" ∷ "lbl" ∷ "meta" ∷ "nodes" ∷ "edges" ∷ "equivalentNodesSets" ∷
         "logicalDefinitionAxioms" ∷ "domainRangeAxioms" ∷ "propertyChainAxioms" ∷ [])
        fields))
decodeGraphAt n _ =
  absent

decodeGraph : JsonValue → Optional Graph
decodeGraph =
  decodeGraphAt zero

decodeGraphDocument : JsonValue → Optional GraphDocument
decodeGraphDocument (object fields) with lookupField "graphs" fields
... | absent =
  present (graphDocument [])
... | present value with asArray value
...   | absent =
  absent
...   | present graphs =
  present (graphDocument (decodeListAt decodeGraphAt zero graphs))
decodeGraphDocument _ =
  absent