call_auto.sh

#!/usr/bin/env bash

set -euo pipefail

# just some sanity checks to make sure the arguments make sense
if ! test -f "${1}"; then
  echo "usage: ${0} <file>"
  exit 1
fi
file="${1}"

# if agda isn't executable and the user didn't specify it tell them that
# they can
if (! type agda &>/dev/null) && [ "\0${AGDA}" == "\0" ]; then
  echo "usage: env AGDA=<path to agda> ${0} \"${file}\""
  exit 1
fi

# if we can't run agda then tell the user that
if ! ${AGDA:-agda} --version &>/dev/null; then
  echo "agda executable ${AGDA:-agda} is not executable"
  exit 1
fi

# the interaction protocol is undocumented and unstable, and basically
# tied to your agda/agda-mode versions. these commands probably work for
# 2.8.0 and will keep working for 2.9.0.
#
# note that the messages basically need to be valid haskell, so e.g. if
# the file name has a stray quote this won't work.
# please don't do that
#
# this is its own thing just because heredocs and escaping line ends
# works badly
msg () {
  cat <<EOF
IOTCM "${file}" None Indirect (Cmd_load "${file}" [])
IOTCM "${file}" None Indirect (Cmd_autoAll AsIs)
EOF
}

# agda will report the unsolved interaction points twice, once when the
# file is loaded, once after it's done telling us what the solutions
# are.
# we only want to print the latter because those are the ones auto
# didn't solve. just using a "boolean" so we don't have to track more
# state.
state=0

# we use the json interaction mode because jq makes that much easier to
# mangle than s-expressions (emacs interaction).
#
# agda will send a bunch of different messages because it thinks it's
# communicating with a text editor. we only care about two, the one that
# tells us where the goals are and the one that tells us the solution
# for a goal
#
# finally, agda will print a prompt indicating that it's ready to
# receive a command, but we don't care because we're not a text editor.
# (we're just printing all our commands upfront.)
# most of the time this is in its own line, but not always so remove it
# from the stream, so we can jq without a thought
msg | ${AGDA:-agda} --interaction-json | grep -E '(InteractionPoints|GiveAction)' | sed -re 's/JSON>//' | \
  while IFS='' read -r line; do

    # helpfully, mimer will report the solution to each goal
    # individually, so we don't have to do a nested loop.
    # also if you have a type called GiveAction this won't work either.
    if echo "${line}" | grep 'GiveAction' >/dev/null; then
      state=1
      echo "${line}" | jq -r '  "auto ?\(.interactionPoint.id) := \(.giveResult.str)"'
    fi

    # if we're receiving the InteractionPoints message after the
    # GiveAction message, they are the ones auto couldn't solve, so we
    # should report them.
    # these *are* in an array, so we have to do some more jq'ing to get
    # at them.
    if [ "${state}" -eq 1 ] && ( echo "${line}" | grep 'InteractionPoints' >/dev/null ); then
      echo -e "\nstill open:"

      # this horrible jq string interpolation computes a C-style printf
      # format string with a single marker for the file name, because
      # dealing with the escaping of having it in the interpolating
      # string is way too annoying. the rest of the data can just go in
      # literally
      echo "${line}" \
        | jq -r '.interactionPoints .[] | "goal ?\(.id) at %s:\(.range[0].start.line):\(.range[0].start.col)\\n"' \
        | while IFS='' read -r goal; do printf "  ${goal}" "${file}"; done
    fi
  done