Skip to content
BANG

Frontend / language role lab

This role lab is generated from the shared four-stage contract. Page identity, route, prerequisites, first-edit seams, and gates are manifest-owned; prose, checks, the fixture, and additional seams are content-owned.

Prerequisites

1. Retrieve and predict

Retrieve the language and CLI contracts before editing. Read the formatter, query, rewrite, and impact surfaces as one workflow: the formatter changes presentation; the read model must keep reporting the same declarations, reference edges, effects, impact closure, and result.

Retrieve:

  • Locate the syntax and type-check seams named by this route.
  • Locate the language/CLI reference for fmt, check --json, query, impact, and rewrite fmt.

Predict before running:

  • Predict the three declarations and their inferred types before running a query.
  • Predict the direct double → quad edge and transitive double → quad → main impact.
  • Predict the program result before formatting the source.

2. Trace the seam

Trace a frontend change from surface parsing through elaboration and its focused executable gates. Start at the manifest-owned seams, then inspect the CLI entry and query/rewrite tests that expose the user-visible boundary.

Checks:

  • Explain which seam owns parsing and which owns elaboration/type checking.
  • Name the focused gate that can falsify the intended frontend change before the full gate.

Tracked seams:

3. Practise in isolation

Create this intentionally noncanonical program in a disposable full-clone lane. Observe its facts first, prove rewrite diff mode does not mutate it, then apply formatting with -w. Do not rename a declaration: this lab isolates the formatting boundary.

Start from the clean, ready checkout used for the common journey. The project helper creates an independent full clone at its exact commit; all writes and gates below happen there.

set -euo pipefail
root="$(git rev-parse --show-toplevel)"
test -z "$(git -C "$root" status --porcelain)"
base="$(git -C "$root" rev-parse HEAD)"
parent="$(mktemp -d)"
lane="$parent/repo"
branch="practice/frontend-language-$(date +%s)-$$"
"$root/tools/new-worktree.sh" "$lane" "$branch" "$base"
cd "$lane"
practice="$lane/main.bang"
bang="$root/.lake/build/bin/bang"
cat > "$practice" <<'BANG'
let rec double : Int -> Int = fun n => n+n
let quad = {fun n => $double ($double n)}
let main = $quad 3
BANG

Run every step in order:

nix develop --command lake build Bang.Frontend.TypeCheck
"$bang" fmt "$practice"
"$bang" check --json "$practice"
"$bang" query dump "$practice"
"$bang" query symbols "$practice"
"$bang" query type "$practice" double
"$bang" query effects double "$practice"
"$bang" query def double "$practice"
"$bang" query refs double "$practice"
"$bang" impact "$practice" double
"$bang" run "$practice"
"$bang" rewrite fmt "$practice"
"$bang" rewrite fmt "$practice" -w
test "$(cat "$practice")" = "$("$bang" fmt "$practice")"
"$bang" check --json "$practice"
"$bang" query dump "$practice"
"$bang" impact "$practice" double
"$bang" run "$practice"

Bounded outcome: Only formatting changes: declarations, types, effects, reference edges, impact, and result remain equal.

4. Inspect evidence and select live work

Treat the before/after observations as evidence, not a transcript to copy. After the narrow and full gates pass, select current work by querying the live issue tracker read-only and matching labels or descriptions to the traced frontend seams.

Evidence checks:

  • Record the formatter output computed from the current binary; do not compare with a stored golden.
  • Compare parsed before/after query facts and the observed result.
  • Confirm rewrite diff mode left the disposable file byte-identical and write mode reached formatter content; fmt stdout adds one terminal newline that rewrite -w does not store.
  • Run the route narrow gate, then the full gate, without treating a skipped step as a pass.
  • Confirm the practice stayed in the disposable lane and made no push or GitHub mutation.

Narrow gate:

nix develop --command just check Bang/Frontend/TypeCheck.lean

Full gate:

nix develop --command just verify

Read-only issue selection:

Run gh issue list --repo phibkro/bang --state open --search "frontend OR parser OR type checker"; set issue=<candidate-number> and inspect it with gh issue view "$issue" --repo phibkro/bang. This only supports a recommendation: do not claim, comment on, or mutate the issue.