module FF.Json.Generate.Node where

open import Agda.Primitive
  using (Set)
open import Agda.Builtin.List
  using (List; []; _∷_)
open import Agda.Builtin.Nat
  using (Nat; zero; suc)
open import Agda.Builtin.Reflection
  using
    ( TC
    ; Term
    ; bindTC
    ; checkFromStringTC
    ; def
    ; strErr
    ; typeError
    ; unify
    )
open import Agda.Builtin.Reflection.External
  using (execTC)
open import Agda.Builtin.Sigma
  using (Σ; _,_)
open import Agda.Builtin.String
  using (String; primStringAppend)
open import Agda.Builtin.Unit
  using (⊤)

open import Cubical.Data.Bool.Base
  using (true; false)
open import Cubical.Data.Sigma.Base
  using (_,_)

open import FF.Json

infixr  _++_
infixl  _>>=_

_++_ : String → String → String
_++_ = primStringAppend

_>>=_ : ∀ {A B : Set} → TC A → (A → TC B) → TC B
_>>=_ = bindTC

nodeExecutable : String
nodeExecutable = "node"

scriptPath : String
scriptPath = "/Users/marcin/agdaLibs/ff-json/test/scripts/json-to-agda.js"

genString : String → JsonValue
genString = jstring

genNumber : Nat → JsonValue
genNumber = jnumber

genTrue : JsonValue
genTrue = jbool true

genFalse : JsonValue
genFalse = jbool false

genNull : JsonValue
genNull = jnull

genArrayNil : JsonValue
genArrayNil = jarray []

genArrayCons : JsonValue → JsonValue → JsonValue
genArrayCons value (array values) = jarray (value ∷ values)
genArrayCons value _ = jarray (value ∷ [])

genObjectNil : JsonValue
genObjectNil = jobject []

genObjectCons : String → JsonValue → JsonValue → JsonValue
genObjectCons key value (object fields) = jobject ((key , value) ∷ fields)
genObjectCons key value _ = jobject ((key , value) ∷ [])

codegenError : String → String → String → String
codegenError input stdout stderr =
  "json-to-agda failed\n\n"
  ++ "Input:\n"
  ++ input
  ++ "\n\nStdout:\n"
  ++ stdout
  ++ "\n\nStderr:\n"
  ++ stderr

jsonToAgdaTermTC : String → TC Term
jsonToAgdaTermTC input =
  execTC nodeExecutable (scriptPath ∷ []) input >>= λ where
    (zero , (stdout , stderr)) →
      checkFromStringTC stdout (def (quote JsonValue) [])
    (suc n , (stdout , stderr)) →
      typeError (strErr (codegenError input stdout stderr) ∷ [])

macro
  jsonValueFromNode : String → Term → TC ⊤
  jsonValueFromNode input hole =
    jsonToAgdaTermTC input >>= unify hole