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

module Spartan6.Import.Source where

open import Spartan6.Prelude

import FF.Json as JSON
import FF.Json.Native as Native

-- These pure names intentionally match the expressions emitted by ff-json's
-- external Node generator.  Generated safe modules import this module, not
-- the ff-json-unsafe macro/exec wrapper.

genString : String → Native.JsonValue
genString = Native.jstring

genNumber : ℕ → Native.JsonValue
genNumber = Native.jnumber

genTrue : Native.JsonValue
genTrue = Native.jbool true

genFalse : Native.JsonValue
genFalse = Native.jbool false

genNull : Native.JsonValue
genNull = Native.jnull

genArrayNil : Native.JsonValue
genArrayNil = Native.jarray []ᴸ

genArrayCons : Native.JsonValue → Native.JsonValue → Native.JsonValue
genArrayCons value (JSON.array values) = Native.jarray (value ∷ᴸ values)
genArrayCons value tail = Native.jarray (value ∷ᴸ []ᴸ)

genObjectNil : Native.JsonValue
genObjectNil = Native.jobject []ᴸ

genObjectCons : String → Native.JsonValue → Native.JsonValue
              → Native.JsonValue
genObjectCons key value (JSON.object fields) =
  Native.jobject ((key , value) ∷ᴸ fields)
genObjectCons key value tail =
  Native.jobject ((key , value) ∷ᴸ []ᴸ)

generated-shape-example :
  genObjectCons "ok" genTrue
    (genObjectCons "items"
      (genArrayCons (genNumber ) genArrayNil)
      genObjectNil)
  ≡ Native.jobject
      ( ("ok" , Native.jbool true)
      ∷ᴸ ("items" , Native.jarray (Native.jnumber  ∷ᴸ []ᴸ))
      ∷ᴸ []ᴸ )
generated-shape-example = refl