Read stdout from Agda's interaction mode (JSON/Emacs)

agda-stdout-reader.js

/** Given chunks as iov, truncate the prompt if possible.
 * @param {string[]} chunks
 * @param {string} prompt
 */
function truncatePrompt(chunks, prompt) {
  /** Does the iov start with the given prefix? Return the end position [x, y] if yes, null if no.
   * @param {string[]} chunks
   * @param {string} target
   */
  function chunksStartWithPrefix(chunks, target) {
    let accuLen = 0
    let chunkIdx = 0
    let toCheck = 0
    while (accuLen < target.length) {
      if (chunkIdx >= chunks.length) return null
      toCheck = Math.min(chunks[chunkIdx].length, target.length - accuLen)
      if (chunks[chunkIdx].slice(0, toCheck) != target.slice(accuLen, accuLen + toCheck)) {
        return null
      }
      accuLen += toCheck
      chunkIdx++
    }
    return [chunkIdx, toCheck]
  }

  const pos = chunksStartWithPrefix(chunks, prompt)
  if (pos == null) return false
  const [x, y] = pos
  for (let i = 0; i < x; i++) chunks.shift()
  if (chunks.length)
    chunks[0] = chunks[0].slice(y)
  return true
}

/** An async iterator intended for reading output from Agda. */
export class AgdaStdoutReader {
  /** @param {ReadableStreamDefaultReader<Uint8Array>} reader */
  constructor(reader) {
    /** @type {typeof reader} */
    this.reader = reader
    /** @type {TextDecoder} */
    this.decoder = new TextDecoder()
    /** @type {string[]} */
    this.chunks = []
  }

  async readOnce() {
    const { value, done } = await this.reader.read()
    return done ? null : this.decoder.decode(value)
  }

  /** Reads until a newline appears. return a non-empty array of complete lines with prompt trimmed or null on EOF.
   * @param {string | null} prompt */
  async read(prompt) {
    /** @type {string[]} */
    const lines = []
    let chunksCheckedPrompt = false

    let step
    // I know I know, the stream itself IS async iterable
    while (step = await this.reader.read(), !step.done) {
      let str = this.decoder.decode(step.value, { stream: true })
      let idx
      while (idx = str.indexOf('\n'), idx >= 0) {
        const line = this.chunks.join('') + str.slice(0, idx)
        this.chunks.length = 0
        chunksCheckedPrompt = false
        if (prompt != null) {
          const luni = [line]
          truncatePrompt(luni, prompt)
          lines.push(luni[0])
        } else {
          lines.push(line)
        }
        str = str.slice(idx + 1)
      }

      if (str != '') {
        this.chunks.push(str)
      }

      // try to truncate prompt
      if (prompt && !chunksCheckedPrompt) {
        if (truncatePrompt(this.chunks, prompt)) {
          chunksCheckedPrompt = true
          lines.push('')
        }
      }

      // read more if no line is available
      if (lines.length) {
        return lines
      }
    }
    return null
  }

  async* iterate() {
    let buf
    let prompt = null
    // assume prompt is always flushed at once
    while (buf = await this.readOnce()) {
      // startup error may appear before the prompt
      if (buf[0] == '(' || buf[0] == '{') {
        const moreLines = await this.read(null)
        if (moreLines == null) {
          yield buf
        } else {
          // always non-empty
          moreLines[0] = buf + moreLines[0]
          for (const ln of moreLines) yield ln
        }
      } else {
        prompt = buf
        break
      }
    }
    if (prompt == null) {
      throw new Error('unexpected end')
    }
    yield ''

    let lines
    while (lines = await this.read(prompt), lines != null) {
      yield* lines
    }
    const lastLine = this.chunks.join('')
    if (lastLine) yield lastLine
  }

  async* [Symbol.asyncIterator]() {
    try {
      yield* this.iterate()
    } catch (err) {
      throw err
    } finally {
      this.dispose()
    }
  }

  dispose() {
    this.chunks.length = 0
    this.reader.releaseLock()
  }
}