module Generic.Unsafe.PrimAtom.Macro where

-- Unsafe interactive value construction for generics over `PrimAtoms`.
--
-- The safe library can describe and JSON-encode generic specifications. This
-- module crosses Agda's trust boundary: it uses `AGDATCMEXEC` to run a Node.js
-- program, lets the user construct a value in a browser UI, and fills the Agda
-- hole after validating and decoding the returned generic-code JSON.

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
    ; normalise
    ; quoteTC
    ; returnTC
    ; strErr
    ; typeError
    ; unquoteTC
    ; unify
    )
open import Agda.Builtin.Sigma using (Σ; _,_)
open import Agda.Builtin.String
  using
    ( String
    ; primStringAppend
    )
open import Agda.Builtin.Unit using (⊤)

open import Cubical.Data.Maybe.Base using (Maybe; just; nothing)

open import Generic.Core hiding (natAtom; stringAtom; boolAtom)
open import Generic.Certified
open import Generic.NativeJson
open import Generic.PrimAtom
open import Generic.PrimAtom.WebEditor public
  using
    ( primAtomJsonString
    ; primAtomJsonNumber
    ; primAtomJsonTrue
    ; primAtomJsonFalse
    ; primAtomJsonNull
    ; primAtomJsonArrayNil
    ; primAtomJsonArrayCons
    ; editorProtocolJSON
    ; rootSource
    ; certifiedEditorSourceFromValue
    )
import FF.Json as Json

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

{-# BUILTIN AGDATCMEXEC execTC #-}

-- The executable is deliberately the stable name `node`. Agda checks this
-- against its trusted executable list before the macro can run.
infixr  _++_
infixl  _>>=_

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

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

return : ∀ {A : Set} → A → TC A
return = returnTC

nodeExecutable : String
nodeExecutable = "node"

uiScriptPath : String
uiScriptPath = "/Users/marcin/agdaLibs/ff-generics/unsafe/web/prim-atom-ui.mjs"

uiArgsAtWithMode : String → String → String → List String
uiArgsAtWithMode script mode spec =
  script ∷ "--spec" ∷ spec ∷ "--output-mode" ∷ mode ∷ []

uiArgsWithMode : String → String → List String
uiArgsWithMode = uiArgsAtWithMode uiScriptPath

uiArgs : String → List String
uiArgs = uiArgsWithMode "json-value-source"

sourceUiArgs : String → List String
sourceUiArgs = uiArgsWithMode "agda-source"

mockUiArgs : String → String → List String
mockUiArgs spec value =
  uiScriptPath ∷ "--spec" ∷ spec
  ∷ "--output-mode" ∷ "json-value-source"
  ∷ "--mock-value" ∷ value ∷ []

sourceMockUiArgs : String → String → List String
sourceMockUiArgs spec value =
  uiScriptPath ∷ "--spec" ∷ spec
  ∷ "--output-mode" ∷ "agda-source"
  ∷ "--mock-value" ∷ value ∷ []

uiError : String → String → String → String → String
uiError spec stdout stderr reason =
  "primitive atom generic UI failed: "
  ++ reason
  ++ "\n\nEditor protocol JSON:\n"
  ++ spec
  ++ "\n\nStdout:\n"
  ++ stdout
  ++ "\n\nStderr:\n"
  ++ stderr

decodeJsonError : String → String → String
decodeJsonError spec output =
  "primitive atom generic UI returned JsonValue source that does not decode for this Generic value\n\n"
  ++ "Editor protocol JSON:\n"
  ++ spec
  ++ "\n\nReturned JsonValue source:\n"
  ++ output

jsonValueSourceTC : String → TC JsonValue
jsonValueSourceTC source =
  checkFromStringTC source (def (quote JsonValue) []) >>= normalise >>= unquoteTC

decodeValueTC : ∀ {A : Type₀} →
                Generic PrimAtoms A →
                String → String → Json.JsonValue → TC A
decodeValueTC g spec output value with
  fromNativeJSON
    (Json.FromToJSON'.from (genericFromToNativeJSON primAtomValueCodecs g))
    value
... | nothing =
  typeError (strErr (decodeJsonError spec output) ∷ [])
... | just x = return x

valueSourceTC : ∀ {A : Type₀} → String → TC A
valueSourceTC {A = A} source =
  quoteTC A >>= λ goal →
  checkFromStringTC source goal >>= unquoteTC

decodeOutputTC : ∀ {A : Type₀} →
                 Generic PrimAtoms A →
                 String → String → String → TC A
decodeOutputTC {A = A} g spec stdout stderr =
  jsonValueSourceTC stdout >>= λ value →
  decodeValueTC g spec stdout value >>= λ _ →
  checkedValue (rootSource g value)
  where
  checkedValue : Maybe String → TC A
  checkedValue nothing =
    typeError
      (strErr
        "primitive atom generic UI decoded the returned JSON, but its metadata cannot render the corresponding constructor source"
      ∷ [])
  checkedValue (just source) = valueSourceTC source

decodeSourceOutputTC : ∀ {A : Type₀} →
                       Generic PrimAtoms A →
                       String → String → String → TC A
decodeSourceOutputTC g spec stdout stderr =
  valueSourceTC stdout

fillOutputTC : ∀ {A : Type₀} →
               Generic PrimAtoms A →
               String → String → String → Term → TC ⊤
fillOutputTC g spec stdout stderr hole =
  jsonValueSourceTC stdout >>= λ value →
  decodeValueTC g spec stdout value >>= λ _ →
  inferType hole >>= λ goal →
  checkGeneratedSource goal (rootSource g value) >>= unify hole
  where
  checkGeneratedSource : Term → Maybe String → TC Term
  checkGeneratedSource goal nothing =
    typeError
      (strErr
        ("primitive atom generic UI decoded the returned JSON, but its metadata cannot render the corresponding constructor source")
      ∷ [])
  checkGeneratedSource goal (just source) =
    checkFromStringTC source goal

fillSourceOutputTC : ∀ {A : Type₀} →
                     Generic PrimAtoms A →
                     String → String → String → Term → TC ⊤
fillSourceOutputTC g spec stdout stderr hole =
  inferType hole >>= λ goal →
  checkFromStringTC stdout goal >>= unify hole

fillCertifiedOutputTC : ∀ {A : Type₀} →
                        CertifiedGeneric PrimAtoms A →
                        String → String → String → Term → TC ⊤
fillCertifiedOutputTC certified protocol stdout stderr hole =
  jsonValueSourceTC stdout >>= λ value →
  checkCertified value (certifiedEditorSourceFromValue certified value)
  where
  checkCertified : JsonValue → Maybe String → TC ⊤
  checkCertified value nothing =
    typeError
      (strErr
        "primitive atom generic UI returned JSON that does not decode for the certified Generic value"
      ∷ [])
  checkCertified value (just source) =
    inferType hole >>= λ goal →
    checkFromStringTC source goal >>= unify hole

runPrimAtomValueWithArgsTC : ∀ {A : Type₀} →
                             Generic PrimAtoms A →
                             (String → List String) →
                             (String → String → String → TC A) →
                             TC A
runPrimAtomValueWithArgsTC g argsFor decodeOutput =
  let protocol = editorProtocolJSON g in
  execTC nodeExecutable (argsFor protocol) "" >>= λ where
    (zero , (stdout , stderr)) →
      decodeOutput protocol stdout stderr
    (suc zero , (stdout , stderr)) →
      typeError (strErr (uiError protocol stdout stderr "bad arguments or invalid specification") ∷ [])
    (suc (suc zero) , (stdout , stderr)) →
      typeError (strErr (uiError protocol stdout stderr "user cancelled") ∷ [])
    (suc (suc (suc _)) , (stdout , stderr)) →
      typeError (strErr (uiError protocol stdout stderr "server/runtime failure") ∷ [])

choosePrimAtomValueWithArgsTC : ∀ {A : Type₀} →
                                  Generic PrimAtoms A →
                                  (String → List String) →
                                  TC A
choosePrimAtomValueWithArgsTC g argsFor =
  runPrimAtomValueWithArgsTC g argsFor (decodeOutputTC g)

-- Value-returning helpers are convenient for offline tests. The public macros
-- below use the hole-filling path, because a macro call in Agda source must
-- ultimately unify with the current hole.
choosePrimAtomValueTC : ∀ {A : Type₀} → Generic PrimAtoms A → TC A
choosePrimAtomValueTC g =
  choosePrimAtomValueWithArgsTC g uiArgs

choosePrimAtomValueMockTC : ∀ {A : Type₀} →
                              Generic PrimAtoms A → String → TC A
choosePrimAtomValueMockTC g value =
  choosePrimAtomValueWithArgsTC g (λ spec → mockUiArgs spec value)

choosePrimAtomValueSourceTC : ∀ {A : Type₀} → Generic PrimAtoms A → TC A
choosePrimAtomValueSourceTC g =
  runPrimAtomValueWithArgsTC g sourceUiArgs (decodeSourceOutputTC g)

choosePrimAtomValueSourceMockTC : ∀ {A : Type₀} →
                                    Generic PrimAtoms A → String → TC A
choosePrimAtomValueSourceMockTC g value =
  runPrimAtomValueWithArgsTC g
    (λ protocol → sourceMockUiArgs protocol value)
    (decodeSourceOutputTC g)

runPrimAtomFillWithArgsTC : ∀ {A : Type₀} →
                            Generic PrimAtoms A →
                            (String → List String) →
                            (String → String → String → Term → TC ⊤) →
                            Term → TC ⊤
runPrimAtomFillWithArgsTC g argsFor fillOutput hole =
  let protocol = editorProtocolJSON g in
  execTC nodeExecutable (argsFor protocol) "" >>= λ where
    (zero , (stdout , stderr)) →
      fillOutput protocol stdout stderr hole
    (suc zero , (stdout , stderr)) →
      typeError (strErr (uiError protocol stdout stderr "bad arguments or invalid specification") ∷ [])
    (suc (suc zero) , (stdout , stderr)) →
      typeError (strErr (uiError protocol stdout stderr "user cancelled") ∷ [])
    (suc (suc (suc _)) , (stdout , stderr)) →
      typeError (strErr (uiError protocol stdout stderr "server/runtime failure") ∷ [])

fillPrimAtomValueWithArgsTC : ∀ {A : Type₀} →
                                Generic PrimAtoms A →
                                (String → List String) →
                                Term → TC ⊤
fillPrimAtomValueWithArgsTC g argsFor hole =
  runPrimAtomFillWithArgsTC g argsFor (fillOutputTC g) hole

fillPrimAtomValueSourceWithArgsTC : ∀ {A : Type₀} →
                                    Generic PrimAtoms A →
                                    (String → List String) →
                                    Term → TC ⊤
fillPrimAtomValueSourceWithArgsTC g argsFor hole =
  runPrimAtomFillWithArgsTC g argsFor (fillSourceOutputTC g) hole

macro
  choosePrimAtomValue : ∀ {A : Type₀} → Generic PrimAtoms A → Term → TC ⊤
  choosePrimAtomValue g hole =
    fillPrimAtomValueWithArgsTC g uiArgs hole

  choosePrimAtomValueAt : ∀ {A : Type₀} →
                          String → Generic PrimAtoms A → Term → TC ⊤
  choosePrimAtomValueAt script g hole =
    fillPrimAtomValueWithArgsTC g
      (uiArgsAtWithMode script "json-value-source") hole

  choosePrimAtomValueMock : ∀ {A : Type₀} →
                              Generic PrimAtoms A → String → Term → TC ⊤
  choosePrimAtomValueMock g value hole =
    fillPrimAtomValueWithArgsTC g (λ spec → mockUiArgs spec value) hole

  choosePrimAtomValueSource : ∀ {A : Type₀} → Generic PrimAtoms A → Term → TC ⊤
  choosePrimAtomValueSource g hole =
    fillPrimAtomValueSourceWithArgsTC g sourceUiArgs hole

  choosePrimAtomValueSourceAt : ∀ {A : Type₀} →
                                String → Generic PrimAtoms A → Term → TC ⊤
  choosePrimAtomValueSourceAt script g hole =
    fillPrimAtomValueSourceWithArgsTC g
      (uiArgsAtWithMode script "agda-source") hole

  choosePrimAtomValueSourceMock : ∀ {A : Type₀} →
                                    Generic PrimAtoms A → String → Term → TC ⊤
  choosePrimAtomValueSourceMock g value hole =
    fillPrimAtomValueSourceWithArgsTC g
      (λ spec → sourceMockUiArgs spec value) hole

  chooseCertifiedPrimAtomValue : ∀ {A : Type₀} →
                                 CertifiedGeneric PrimAtoms A → Term → TC ⊤
  chooseCertifiedPrimAtomValue certified hole =
    runPrimAtomFillWithArgsTC
      (base certified) uiArgs (fillCertifiedOutputTC certified) hole

  chooseCertifiedPrimAtomValueAt : ∀ {A : Type₀} →
                                   String → CertifiedGeneric PrimAtoms A →
                                   Term → TC ⊤
  chooseCertifiedPrimAtomValueAt script certified hole =
    runPrimAtomFillWithArgsTC
      (base certified)
      (uiArgsAtWithMode script "json-value-source")
      (fillCertifiedOutputTC certified)
      hole

  chooseCertifiedPrimAtomValueMock : ∀ {A : Type₀} →
                                     CertifiedGeneric PrimAtoms A →
                                     String → Term → TC ⊤
  chooseCertifiedPrimAtomValueMock certified value hole =
    runPrimAtomFillWithArgsTC
      (base certified)
      (λ protocol → mockUiArgs protocol value)
      (fillCertifiedOutputTC certified)
      hole