tweaks for Lean: order of decls need toposort, plus minor parentheses

tools/src/lean-emit.ts

@@ -464,8 +464,13 @@ function emitExpr(e: Expr, parentPrec?: number): string {
       // Same unsupported-real story as the `real` type case in tyToLean.
       throw new Error("real arithmetic is not supported by the Lean backend (needs noncomputable ℝ / Mathlib).");
 
-    case "index":
-      return `${emitExpr(e.arr)}[${emitExpr(e.idx)}]!`;
+    case "index": {
+      const arr = emitExpr(e.arr);
+      // Parenthesize a low-precedence array expr (e.g. a function application)
+      // so the index binds to the whole thing, not its last token.
+      const wrap = e.arr.kind === "app" || e.arr.kind === "binop" || e.arr.kind === "methodCall" || e.arr.kind === "if" || e.arr.kind === "let" || e.arr.kind === "unop";
+      return `${wrap ? `(${arr})` : arr}[${emitExpr(e.idx)}]!`;
+    }
 
     case "record": {
       const fields = e.fields.map(f => `${escapeName(f.name)} := ${emitExpr(f.value)}`);
@@ -644,6 +649,48 @@ function emitStmt(s: Stmt, indent: number): string {
 
 // ── Declaration emission ─────────────────────────────────────
 
+/** Collect every function/variable name an IR tree references (stripping any
+ *  `Pure.` qualifier), via a generic walk over `app`/`var` nodes. */
+function collectRefNames(node: unknown, into: Set<string>): void {
+  if (node === null || typeof node !== "object") return;
+  if (Array.isArray(node)) { for (const x of node) collectRefNames(x, into); return; }
+  const n = node as { kind?: string; fn?: unknown; name?: unknown };
+  if (n.kind === "app" && typeof n.fn === "string") into.add(n.fn.replace(/^Pure\./, ""));
+  if (n.kind === "var" && typeof n.name === "string") into.add(n.name.replace(/^Pure\./, ""));
+  for (const k of Object.keys(node)) collectRefNames((node as Record<string, unknown>)[k], into);
+}
+
+/** Lean requires definition-before-use: order sibling decls so one that
+ *  references another is emitted after it. Cycles are left in place (they would
+ *  need a `mutual` block). Bails to the original order if any decl is unnamed. */
+function orderDeclsByDeps(decls: Decl[]): Decl[] {
+  const named = decls.filter((d): d is Decl & { name: string } => typeof (d as { name?: unknown }).name === "string");
+  if (named.length !== decls.length) return decls;
+  const names = new Set(named.map(d => d.name));
+  const byName = new Map(named.map(d => [d.name, d]));
+  const deps = new Map<string, string[]>();
+  for (const d of named) {
+    const refs = new Set<string>();
+    collectRefNames(d, refs);
+    refs.delete(d.name);
+    deps.set(d.name, [...refs].filter(r => names.has(r)));
+  }
+  const sorted: Decl[] = [];
+  const done = new Set<string>();
+  const onStack = new Set<string>();
+  const visit = (name: string) => {
+    if (done.has(name) || onStack.has(name)) return;
+    onStack.add(name);
+    for (const dep of deps.get(name) ?? []) visit(dep);
+    onStack.delete(name);
+    done.add(name);
+    const def = byName.get(name);
+    if (def) sorted.push(def);
+  };
+  for (const d of named) visit(d.name);
+  return sorted;
+}
+
 function emitDecl(d: Decl): string {
   switch (d.kind) {
     case "inductive": {
@@ -725,7 +772,7 @@ function emitDecl(d: Decl): string {
 
     case "namespace": {
       const lines = [`namespace ${d.name}`];
-      for (const inner of d.decls) lines.push("", emitDecl(inner));
+      for (const inner of orderDeclsByDeps(d.decls)) lines.push("", emitDecl(inner));
       lines.push("", `end ${d.name}`);
       return lines.join("\n");
     }
@@ -748,8 +795,10 @@ function emitDecl(d: Decl): string {
       if (d.requires.length === 0 && d.ensures.length === 0) return sig;
       // Spec axiom: ∀ params, req1 → … → (ens1 ∧ … ∧ ensN). Tagged `@[grind]` so
       // the proof automation can use it, matching the ghost-function convention.
-      const hyps = d.requires.map(emitExpr);
-      const concl = d.ensures.map(emitExpr).join(" ∧ ");
+      // Parenthesize each clause: an unwrapped `∀ k, P` would otherwise swallow
+      // the following ` ∧ …` conjuncts into its body.
+      const hyps = d.requires.map(e => `(${emitExpr(e)})`);
+      const concl = d.ensures.map(e => `(${emitExpr(e)})`).join(" ∧ ");
       const axBody = [...hyps, concl].join(" → ");
       const axiom = `@[grind] axiom ${escapeName(d.name)}_spec${params ? ` ${params}` : ""} : ${axBody}`;
       return `${sig}\n${axiom}`;

tools/src/transform.ts

@@ -192,6 +192,14 @@ let _opts: TransformOptions = DAFNY_OPTIONS;
 /** Type declarations — set once per module transform for discriminated union handling. */
 let _typeDecls: TypeDeclInfo[] = [];
 
+/** Names of functions that get a `Pure.` mirror (Lean). A bare reference to one
+ *  in a higher-order position resolves to the monadic method, so it must be
+ *  redirected to the pure mirror. Set once per module transform. */
+let _pureDefNames: Set<string> = new Set();
+
+/** Array methods that take a function argument. */
+const HOF_METHODS = new Set(["map", "filter", "every", "some", "find", "findLast", "findIndex", "findLastIndex", "reduce"]);
+
 /** Prefix match-bound field names to avoid capturing user variables.
  *  When prefix is given (the scrutinee name), include it to avoid
  *  collisions in nested matches on different variables. `freshName` closes
@@ -774,8 +782,15 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
       if (e.fn.kind === "field") {
         const recv = lowerExpr(e.fn.obj, binds);
         let method = e.fn.field;
+        const isHOF = e.fn.obj.ty.kind === "array" && HOF_METHODS.has(method);
         const args = e.args.map((a, i) => {
           const lowered = lowerExpr(a, binds);
+          // Lean: a pure fn passed to a HOF by name resolves to the monadic
+          // method; redirect to its pure `Pure.` mirror.
+          if (_opts.backend === "lean" && isHOF &&
+              lowered.kind === "var" && _pureDefNames.has(lowered.name)) {
+            return { kind: "var" as const, name: `Pure.${lowered.name}` };
+          }
           // Array index args must be nat in Lean: `with`'s index (0), includes/indexOf `from` (1).
           const isArrIdxArg = e.fn.kind === "field" && e.fn.obj.ty.kind === "array" &&
             ((e.fn.field === "with" && i === 0) || ((e.fn.field === "includes" || e.fn.field === "indexOf") && i === 1));
@@ -2191,6 +2206,7 @@ export function transformModule(mod: TModule, specImport?: string, moduleBaseOve
   _forofCounters.clear();
   _liftCounter = 0;
   _typeDecls = mod.typeDecls;
+  _pureDefNames = new Set(mod.functions.filter(f => f.isPure).map(f => f.name));
   const typeDecls = mod.typeDecls.map(transformTypeDecl);
 
   // Module-level constants