#!/usr/bin/env bash
# run.sh — build and run the native-interruptibility proof.
#
# Concatenates runtime/swarm.el + proof.el into one translation unit (the El
# multi-file strategy — elc does not resolve cross-directory imports), compiles
# via the canonical elc, links against el_runtime.c, and runs.
#
# A tiny forward-declaration prelude is prepended to the generated C for the
# __channel_* seed primitives (they are defined in el_runtime.c but not declared
# in el_runtime.h). This touches nothing shared — it is local to this build.

set -uo pipefail
cd "$(dirname "$0")"

EL_HOME="${EL_HOME:-$(cd ../.. && pwd)}"
ELC="${EL_HOME}/dist/platform/elc"
RT="${EL_HOME}/el-compiler/runtime"
SWARM="${EL_HOME}/runtime/swarm.el"

OSSL="$(brew --prefix openssl@3 2>/dev/null || brew --prefix openssl 2>/dev/null || echo /usr/local)"
LDF=(); [ -d "${OSSL}/lib" ] && LDF=(-L"${OSSL}/lib")

BUILD="$(mktemp -d -t swarmproof.XXXXXX)"
trap 'rm -rf "${BUILD}"' EXIT

if [ ! -x "${ELC}" ]; then echo "elc not found at ${ELC}" >&2; exit 1; fi

# 1. Concatenate library + proof into one .el
cat "${SWARM}" proof.el > "${BUILD}/combined.el"

# 2. elc emit -> C
if ! "${ELC}" "${BUILD}/combined.el" > "${BUILD}/body.c" 2>"${BUILD}/elc.err"; then
    echo "elc FAILED:"; sed 's/^/  /' "${BUILD}/elc.err"; exit 1
fi

# 3. Prepend forward-decl prelude for the __channel_* seed primitives
cat > "${BUILD}/prog.c" <<'PRELUDE'
#include <stdint.h>
typedef int64_t el_val_t;
el_val_t __channel_new(el_val_t);
el_val_t __channel_send(el_val_t, el_val_t);
el_val_t __channel_recv(el_val_t);
el_val_t __channel_try_recv(el_val_t);
el_val_t __channel_close(el_val_t);
PRELUDE
cat "${BUILD}/body.c" >> "${BUILD}/prog.c"

# 4. cc link
if ! cc -O2 -Wno-implicit-function-declaration -I "${RT}" "${LDF[@]}" \
        "${BUILD}/prog.c" "${RT}/el_runtime.c" \
        -lcurl -lssl -lcrypto -lpthread -lm -o "${BUILD}/proof" 2>"${BUILD}/cc.err"; then
    echo "cc FAILED:"; tail -20 "${BUILD}/cc.err"; exit 1
fi

# 5. run
"${BUILD}/proof"