|
| 1 | +#!/usr/bin/env bash |
| 2 | +# SPDX-License-Identifier: MPL-2.0 |
| 3 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 4 | +# |
| 5 | +# Every Haec example lowers to a well-formed Trope IR document. Pure bash + jq, |
| 6 | +# no Python. Self-contained: structural checks against the vendored IR contract. |
| 7 | +# The full round-trip (verdicts) runs when the sibling trope-checker is present. |
| 8 | +set -uo pipefail |
| 9 | + |
| 10 | +ROOT="$(cd "$(dirname "$0")/.." && pwd)" |
| 11 | +EX="$ROOT/examples" |
| 12 | +SIB="$ROOT/../trope-checker" |
| 13 | +G="\033[32m"; R="\033[31m"; Y="\033[33m"; O="\033[0m" |
| 14 | +fail=0 |
| 15 | +command -v jq >/dev/null || { echo "jq is required"; exit 2; } |
| 16 | + |
| 17 | +# 1. structural: each *.ir.json is well-formed and has the required IR shape. |
| 18 | +for f in "$EX"/*.ir.json; do |
| 19 | + if ! jq -e '.version and .profile and .nodes and .edges and .use_model' "$f" >/dev/null 2>&1; then |
| 20 | + echo -e "${R}FAIL${O} $(basename "$f"): not a well-formed Trope IR document"; fail=1 |
| 21 | + fi |
| 22 | +done |
| 23 | + |
| 24 | +# 2. every example in the manifest pairs a program with its IR. |
| 25 | +while read -r e; do |
| 26 | + prog=$(jq -r '.program' <<<"$e"); ir=$(jq -r '.ir' <<<"$e") |
| 27 | + [ -f "$EX/$prog" ] || { echo -e "${R}FAIL${O} missing program $prog"; fail=1; } |
| 28 | + [ -f "$EX/$ir" ] || { echo -e "${R}FAIL${O} missing IR $ir"; fail=1; } |
| 29 | + [ "$fail" = 0 ] && echo -e "${G}ok${O} $prog → $ir (well-formed IR, expects $(jq -r '.expect' <<<"$e"))" |
| 30 | +done < <(jq -c '.examples[]' "$EX/EXAMPLES.json") |
| 31 | + |
| 32 | +# 3. drift guard: the vendored IR schema must match the canonical one if present. |
| 33 | +if [ -f "$SIB/schemas/trope-ir.schema.json" ]; then |
| 34 | + if diff -q "$ROOT/design/trope-ir.schema.json" "$SIB/schemas/trope-ir.schema.json" >/dev/null; then |
| 35 | + echo -e "${G}ok${O} vendored design/trope-ir.schema.json matches the canonical checker schema" |
| 36 | + else |
| 37 | + echo -e "${R}FAIL${O} vendored IR schema has drifted from trope-checker/schemas/trope-ir.schema.json"; fail=1 |
| 38 | + fi |
| 39 | +else |
| 40 | + echo -e "${Y}note${O} sibling trope-checker not checked out; skipping schema-drift guard" |
| 41 | +fi |
| 42 | + |
| 43 | +# 4. full round-trip: verdicts via the sibling Idris2 checker, if built. |
| 44 | +BIN="$SIB/src/idris2/build/exec/tropecheck" |
| 45 | +if [ -x "$BIN" ]; then |
| 46 | + while read -r e; do |
| 47 | + ir=$(jq -r '.ir' <<<"$e"); exp=$(jq -r '.expect' <<<"$e") |
| 48 | + got=$("$BIN" "$EX/$ir" | awk '{print $1}') |
| 49 | + if [ "$got" = "$exp" ]; then echo -e "${G}ok${O} round-trip $ir → $got" |
| 50 | + else echo -e "${R}FAIL${O} round-trip $ir: got $got, expected $exp"; fail=1; fi |
| 51 | + done < <(jq -c '.examples[]' "$EX/EXAMPLES.json") |
| 52 | +else |
| 53 | + echo -e "${Y}note${O} sibling tropecheck binary not built; skipping verdict round-trip (run 'just trope-build' in ../trope-checker)" |
| 54 | +fi |
| 55 | + |
| 56 | +if [ "$fail" = 0 ]; then echo -e "\n${G}examples: all lower to valid Trope IR${O}"; else echo -e "\n${R}examples: failures${O}"; fi |
| 57 | +exit "$fail" |
0 commit comments