Message delimiter for Agda's interaction mode

agda-stdout-decoder.ts

import chp from 'child_process'
import { Readable } from 'stream'
import { inspect } from 'util'

enum DecoderState {
  Initial,
  // Agda used to (until 2.7.0.1) emit error when the data dir is not found before the very first prompt;
  // this has now (v2.8.0) become a runtime error message to stderr;
  // in v2.9.0 nightly (2026/7/22) the stacktrace is printed to stdout???
  StartupMessage,
  Message,
  Prompt,
}

const RESPONSE_END = Symbol('RESPONSE_END')
type RESPONSE_END = typeof RESPONSE_END

class AgdaStdoutDecoder implements Transformer<string, string | RESPONSE_END> {
  state = DecoderState.Initial
  buffer = ''
  // is any message emitted after the last prompt? as a safe check for messed-up messages
  canEndResponse = false

  transform(chunk: string, controller: TransformStreamDefaultController<string | RESPONSE_END>) {
    // console.log('--- MSG', JSON.stringify(chunk))
    let idx = 0
    chunk = this.buffer + chunk

    while (idx < chunk.length) {
      switch (this.state) {
      case DecoderState.Initial:
        if (chunk[idx] == '(' || chunk[idx] == '{') {
          this.state = DecoderState.StartupMessage
        } else {
          controller.enqueue(RESPONSE_END)
          this.state = DecoderState.Prompt
        }
        continue
      case DecoderState.Prompt: {
        const regex = /(?:Agda2|JSON)> /g
        regex.lastIndex = idx
        const found = regex.exec(chunk)
        if (found) {
          idx = regex.lastIndex
          this.state = DecoderState.Message
          this.canEndResponse = false
          continue
        } else {
          return
        }
      }
      case DecoderState.Message:
      case DecoderState.StartupMessage: {
        // XXX: 'c' for "cannot read: ..."
        if (!(chunk[idx] == '(' || chunk[idx] == '{' || chunk[idx] == 'c')) {
          if (!this.canEndResponse) {
            controller.error(
              new Error('No message is sent between two prompts, this should not happen: ' + JSON.stringify(chunk.slice(idx))))
          }
          controller.enqueue(RESPONSE_END)
          this.state = DecoderState.Prompt
          continue
        }
        const found = chunk.indexOf('\n', idx)
        if (found >= 0) {
          controller.enqueue(chunk.slice(idx, found))
          this.canEndResponse = true
          idx = found + 1
          continue
        } else {
          return
        }
      }
      default:
        this.state satisfies never; throw new Error('unreachable')
      }
    }

    this.buffer = chunk.slice(idx)
  }

  flush(controller: TransformStreamDefaultController) {
    if (this.buffer) {
      controller.error(new Error('trailing data: [' + this.buffer + ']'))
    }
  }
}

const proc = chp.spawn('./agda', ['--interaction-json'], { stdio: ['pipe', 'pipe', 'inherit'] })
proc.stdin.write('IOTCM "a.agda" NonInteractive Direct (Cmd_load "a.agda" [])\n')
proc.stdin.write('IOTCM "a.agda" NonInteractive Direct (Cmd_goal_type_context AsIs 0 noRange "")\n')

const ts = new TransformStream(new AgdaStdoutDecoder)

const bufferReadable = Readable.toWeb(proc.stdout) as ReadableStream<unknown>
const rs = bufferReadable.pipeThrough(new TextDecoderStream).pipeThrough<string | RESPONSE_END>(ts)

setImmediate(() => {
  proc.stdin.end()
})

for await (const x of rs) {
  if (x === RESPONSE_END) {
    console.log('END')
  } else if (x.startsWith('cannot read: ')) {
    console.log('ERR', x)
  } else {
    console.log('OUT', inspect(JSON.parse(x), { colors: true, depth: 999 }))
  }
}