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

module Spartan6.Import.Json where

open import Spartan6.Prelude

import FF.Json as JSON
import FF.Json.Native as Native
import Spartan6.Validation.Diagnostic as Diagnostic

open import Agda.Builtin.String
  using (primShowNat; primStringAppend; primStringEquality)

infixr  _<>_

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

JsonValue : Type₀
JsonValue = Native.JsonValue

ObjectFields : Type₀
ObjectFields = List (String × JsonValue)

data PathSegment : Type₀ where
  keySegment   : String → PathSegment
  indexSegment : ℕ → PathSegment

JsonPath : Type₀
JsonPath = List PathSegment

root : JsonPath
root = []ᴸ

fieldAt : JsonPath → String → JsonPath
fieldAt path name = path ++ᴸ (keySegment name ∷ᴸ []ᴸ)

indexAt : JsonPath → ℕ → JsonPath
indexAt path number = path ++ᴸ (indexSegment number ∷ᴸ []ᴸ)

renderPathFrom : String → JsonPath → String
renderPathFrom prefix []ᴸ = prefix
renderPathFrom prefix (keySegment name ∷ᴸ path) =
  renderPathFrom (prefix <> "." <> name) path
renderPathFrom prefix (indexSegment number ∷ᴸ path) =
  renderPathFrom (prefix <> "[" <> primShowNat number <> "]") path

renderPath : JsonPath → String
renderPath = renderPathFrom "$"

singleton : Diagnostic.Diagnostic → Diagnostic.Diagnostics
singleton problem = problem ∷ᴸ []ᴸ

malformedAt : JsonPath → String → String → String → Diagnostic.Diagnostics
malformedAt path expected observed detail =
  singleton
    (Diagnostic.diagnostic
      Diagnostic.malformedImport
      Diagnostic.reject
      (renderPath path)
      expected
      observed
      detail)

jsonShape : JsonValue → String
jsonShape (JSON.atom Native.string value) = "string"
jsonShape (JSON.atom Native.number value) = "natural number"
jsonShape (JSON.atom Native.boolean value) = "boolean"
jsonShape (JSON.atom Native.null value) = "null"
jsonShape (JSON.array values) = "array"
jsonShape (JSON.object fields) = "object"

containsField : String → ObjectFields → Bool
containsField name []ᴸ = false
containsField name ((candidate , value) ∷ᴸ fields) =
  primStringEquality name candidate or containsField name fields

firstDuplicateField : ObjectFields → Maybe String
firstDuplicateField []ᴸ = nothing
firstDuplicateField ((name , value) ∷ᴸ fields) =
  if containsField name fields
  then just name
  else firstDuplicateField fields

expectUniqueObject : JsonPath → JsonValue
                   → Diagnostic.CheckResult ObjectFields
expectUniqueObject path (JSON.object fields) with firstDuplicateField fields
... | nothing = Diagnostic.accepted fields
... | just name =
  Diagnostic.rejected
    (malformedAt
      (fieldAt path name)
      "a unique object field"
      "a duplicate field"
      "Duplicate JSON object fields are rejected; source order never assigns precedence.")
expectUniqueObject path value =
  Diagnostic.rejected
    (malformedAt path "an object" (jsonShape value)
      "This Yosys schema position requires a JSON object.")

matchingFields : String → ObjectFields → List JsonValue
matchingFields name []ᴸ = []ᴸ
matchingFields name ((candidate , value) ∷ᴸ fields) =
  if primStringEquality name candidate
  then value ∷ᴸ matchingFields name fields
  else matchingFields name fields

requiredField : JsonPath → String → ObjectFields
              → Diagnostic.CheckResult JsonValue
requiredField path name fields with matchingFields name fields
... | []ᴸ =
  Diagnostic.rejected
    (malformedAt
      (fieldAt path name)
      "one required field"
      "a missing field"
      "The selected Yosys schema requires this field.")
... | value ∷ᴸ []ᴸ = Diagnostic.accepted value
... | first ∷ᴸ second ∷ᴸ rest =
  Diagnostic.rejected
    (malformedAt
      (fieldAt path name)
      "one required field"
      "multiple fields with the same name"
      "Required fields must be unique; no duplicate wins by position.")

expectArray : JsonPath → JsonValue → Diagnostic.CheckResult (List JsonValue)
expectArray path (JSON.array values) = Diagnostic.accepted values
expectArray path value =
  Diagnostic.rejected
    (malformedAt path "an array" (jsonShape value)
      "This Yosys schema position requires a JSON array.")

expectString : JsonPath → JsonValue → Diagnostic.CheckResult String
expectString path (JSON.atom Native.string value) = Diagnostic.accepted value
expectString path value =
  Diagnostic.rejected
    (malformedAt path "a string" (jsonShape value)
      "This Yosys schema position requires a JSON string.")

expectNatural : JsonPath → JsonValue → Diagnostic.CheckResult ℕ
expectNatural path (JSON.atom Native.number value) = Diagnostic.accepted value
expectNatural path value =
  Diagnostic.rejected
    (malformedAt path "a natural number" (jsonShape value)
      "The native ff-json universe represents only non-negative integral numbers.")

prependResult : ∀ {A : Type₀}
              → Diagnostic.CheckResult A
              → Diagnostic.CheckResult (List A)
              → Diagnostic.CheckResult (List A)
prependResult (Diagnostic.accepted value) (Diagnostic.accepted values) =
  Diagnostic.accepted (value ∷ᴸ values)
prependResult (Diagnostic.rejected problems) (Diagnostic.accepted values) =
  Diagnostic.rejected problems
prependResult (Diagnostic.accepted value) (Diagnostic.rejected problems) =
  Diagnostic.rejected problems
prependResult (Diagnostic.rejected first) (Diagnostic.rejected rest) =
  Diagnostic.rejected (first ++ᴸ rest)

decodeArrayFrom : ∀ {A : Type₀}
                → (JsonPath → JsonValue → Diagnostic.CheckResult A)
                → JsonPath → ℕ → List JsonValue
                → Diagnostic.CheckResult (List A)
decodeArrayFrom decoder path next-index []ᴸ = Diagnostic.accepted []ᴸ
decodeArrayFrom decoder path next-index (value ∷ᴸ values) =
  prependResult
    (decoder (indexAt path next-index) value)
    (decodeArrayFrom decoder path (suc next-index) values)

decodeArray : ∀ {A : Type₀}
            → (JsonPath → JsonValue → Diagnostic.CheckResult A)
            → JsonPath → List JsonValue
            → Diagnostic.CheckResult (List A)
decodeArray decoder path = decodeArrayFrom decoder path zero

decodeObjectFields : ∀ {A : Type₀}
                   → (JsonPath → String → JsonValue
                      → Diagnostic.CheckResult A)
                   → JsonPath → ObjectFields
                   → Diagnostic.CheckResult (List A)
decodeObjectFields decoder path []ᴸ = Diagnostic.accepted []ᴸ
decodeObjectFields decoder path ((name , value) ∷ᴸ fields) =
  prependResult
    (decoder (fieldAt path name) name value)
    (decodeObjectFields decoder path fields)

record AcceptedResult {A : Type₀}
                      (result : Diagnostic.CheckResult A) : Type₀ where
  constructor acceptedResult
  field
    acceptedValue    : A
    acceptedEquality : result ≡ Diagnostic.accepted acceptedValue

open AcceptedResult public

extractAccepted : ∀ {A : Type₀} {result : Diagnostic.CheckResult A}
                → AcceptedResult result → A
extractAccepted evidence = acceptedValue evidence