module FF.Json.Validate.Jq 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; returnTC; typeError; unify; quoteTC; strErr)
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 (⊤; tt)

infixr  _++_
infixl  _>>=_ _>>_

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

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

_>>_ : ∀ {A B : Set} → TC A → TC B → TC B
ma >> mb = ma >>= λ _ → mb

jqArgs : List String
jqArgs = "-e" ∷ "." ∷ []

jqError : String → String → String → String
jqError input stdout stderr =
  "jq rejected rendered JSON\n\n"
  ++ "Input:\n"
  ++ input
  ++ "\n\nStdout:\n"
  ++ stdout
  ++ "\n\nStderr:\n"
  ++ stderr

validateJsonWithJqTC : String → TC ⊤
validateJsonWithJqTC input =
  execTC "jq" jqArgs input >>= λ where
    (zero , (stdout , stderr)) → returnTC tt
    (suc n , (stdout , stderr)) →
      typeError (strErr (jqError input stdout stderr) ∷ [])

macro
  validateJsonWithJq : String → Term → TC ⊤
  validateJsonWithJq input hole =
    validateJsonWithJqTC input >>
    (quoteTC tt >>= λ tt-term →
     unify hole tt-term)