module OWL2.Unsafe.OBOGraph.Macro 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; inferType; strErr; typeError; unify)
open import Agda.Builtin.Sigma using (Σ; _,_)
open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Builtin.Unit using (⊤)

import OWL2.OBOGraph.Syntax as OG
import OWL2.OBOGraph.Decode as Decode
import OWL2.OBOGraph.ToPortable as OGP
import OWL2.Portable.Syntax as P
import FF.Json.Native as JSON

postulate
  execTC : String → List String → String →
           TC (Σ Nat (λ _ → Σ String (λ _ → String)))

{-# BUILTIN AGDATCMEXEC execTC #-}

infixl  _>>=_
infixr  _++_

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

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

nodeExecutable : String
nodeExecutable =
  "node"

scriptPath : String
scriptPath =
  "../scripts/json_to_agda_value_macro.mjs"

argsFor : String → List String
argsFor path =
  scriptPath ∷ path ∷ []

errorText : String → String → String → String
errorText path stdout stderr =
  "OBOGraph import failed for "
  ++ path
  ++ "\n\nStdout:\n"
  ++ stdout
  ++ "\n\nStderr:\n"
  ++ stderr

jsonValueTermTC : String → TC Term
jsonValueTermTC path =
  execTC nodeExecutable (argsFor path) "" >>= λ where
    (zero , (stdout , stderr)) →
      checkFromStringTC stdout (def (quote JSON.JsonValue) [])
    (suc _ , (stdout , stderr)) →
      typeError (strErr (errorText path stdout stderr) ∷ [])

portableSource : String → String
portableSource jsonSource =
  "OGP.toOntologyDocument "
  ++ "(Decode.fromMaybe (OG.graphDocument []) "
  ++ "(Decode.decodeGraphDocument ("
  ++ jsonSource
  ++ ")))"

fillPortableTC : String → Term → TC ⊤
fillPortableTC path hole =
  execTC nodeExecutable (argsFor path) "" >>= λ where
    (zero , (stdout , stderr)) →
      inferType hole >>= λ goal →
      checkFromStringTC (portableSource stdout) goal >>= unify hole
    (suc _ , (stdout , stderr)) →
      typeError (strErr (errorText path stdout stderr) ∷ [])

fillJsonValueTC : String → Term → TC ⊤
fillJsonValueTC path hole =
  jsonValueTermTC path >>= unify hole

macro
  importOBOGraphJsonValue : String → Term → TC ⊤
  importOBOGraphJsonValue =
    fillJsonValueTC

  importOBOGraphDocument : String → Term → TC ⊤
  importOBOGraphDocument =
    fillPortableTC