Aiur grammar: statement sequencing t; rest (#475)

Add `syntax:0 aiur_trm "; " (aiur_trm)?` — `f(x); rest` elaborates to
`let _ = f(x); rest` (wildcard let, value discarded); trailing `f(x);`
closes the block with `()`. Unit-returning calls sit in statement
position without the `let _ =` boilerplate.

The sequencing rule is the grammar's only prec-0 rule; positions where
an expression can end right before a `;` are bumped to prec 1 so it
can't leak into expression operands: `let` right-hand sides, `+`/`-`
right operands, `return`, array elements/replicate. Without the binop
guard, `let x = a - 1; rest` reparses as `a - (1; rest)` — caught only
at `ix codegen` scope-check (`unboundGlobal`), not by `lake build`,
since elaboration builds Source.Term without checking. All other
argument positions are bounded by closing tokens and can't precede a
`;`. Since prec-51 positions accept every leading form, default rule
prec ≥ 51 and the :1 annotations exclude only the sequencing rule.

Rewrite all 113 `let _ = call(...);` sites in Ix/IxVM and the 3
`let _ = store(...)` sites in Tests/Aiur to the new form, and drop the
4 redundant explicit `()` continuations after trailing `assert_eq!`
(an omitted continuation already elaborates to unit). Generated kernel
is byte-identical after `lake exe ix codegen` (identical IR by
construction — no FFT shift), and `lake test -- aiur-cross` passes
with the new syntax exercised.

Author: arthurpaulino

Ix/Aiur/Meta.lean

@@ -135,12 +135,21 @@ syntax ("." noWs)? ident                                                      :
 syntax num                                                                    : aiur_trm
 syntax "(" ")"                                                                : aiur_trm
 syntax "(" aiur_trm (", " aiur_trm)* ")"                                    : aiur_trm
-syntax "[" aiur_trm (", " aiur_trm)* "]"                                    : aiur_trm
-syntax "[" aiur_trm "; " num "]"                                             : aiur_trm
-syntax "return " aiur_trm                                                    : aiur_trm
-syntax "let " aiur_pattern (":" aiur_typ)? " = " aiur_trm "; " aiur_trm   : aiur_trm
-syntax "let " aiur_pattern (":" aiur_typ)? " = " aiur_trm ";"              : aiur_trm
-syntax "let " aiur_pattern (":" aiur_typ)? " = " aiur_trm                  : aiur_trm
+-- Array elements and `return` operands parse at prec 1: it keeps the
+-- statement-sequencing rule (prec 0, below `let`) out of expression
+-- positions and keeps `[t; n]` replicate vs `[t]` list unambiguous.
+syntax "[" aiur_trm:1 (", " aiur_trm:1)* "]"                                : aiur_trm
+syntax "[" aiur_trm:1 "; " num "]"                                           : aiur_trm
+syntax "return " aiur_trm:1                                                  : aiur_trm
+-- `let` right-hand sides parse at prec 1 so the statement-sequencing rule
+-- (prec 0, below) can't swallow the `let`'s own `;` and continuation.
+syntax "let " aiur_pattern (":" aiur_typ)? " = " aiur_trm:1 "; " aiur_trm  : aiur_trm
+syntax "let " aiur_pattern (":" aiur_typ)? " = " aiur_trm:1 ";"            : aiur_trm
+syntax "let " aiur_pattern (":" aiur_typ)? " = " aiur_trm:1                : aiur_trm
+-- Statement sequencing: `t; rest` discards `t`'s value (elaborates to
+-- `let _ = t; rest`); trailing `t;` closes the block with `()`. Lets
+-- unit-returning calls sit in statement position without `let _ =`.
+syntax:0 aiur_trm "; " (aiur_trm)?                                          : aiur_trm
 syntax "match " aiur_trm " { "
        (aiur_pattern " => " aiur_trm ", ")+ " }"                            : aiur_trm
 syntax ("." noWs)? ident "(" ")"                                              : aiur_trm
@@ -156,8 +165,11 @@ syntax "#" noWs ident "‹" aiur_typ (", " aiur_typ)* "›" "(" aiur_trm
 syntax ident "‹" aiur_typ (", " aiur_typ)* "›" "." noWs ident "(" ")"       : aiur_trm
 syntax ident "‹" aiur_typ (", " aiur_typ)* "›" "." noWs ident
        "(" aiur_trm (", " aiur_trm)* ")"                                    : aiur_trm
-syntax:50 aiur_trm " + " aiur_trm                                           : aiur_trm
-syntax:50 aiur_trm " - " aiur_trm                                           : aiur_trm
+-- Right operands parse at prec 1 (not 0) so the statement-sequencing rule
+-- can't swallow `<binop-expr>; rest` from inside the right operand. All
+-- other rules have prec ≥ 50, so associativity/precedence are unchanged.
+syntax:50 aiur_trm " + " aiur_trm:1                                         : aiur_trm
+syntax:50 aiur_trm " - " aiur_trm:1                                         : aiur_trm
 syntax aiur_trm " * " aiur_trm:51                                           : aiur_trm
 syntax "eq_zero" "(" aiur_trm ")"                                            : aiur_trm
 syntax "proj" "(" aiur_trm ", " num ")"                                      : aiur_trm
@@ -240,6 +252,9 @@ partial def elabTrm : ElabStxCat `aiur_trm
     | some ty => do
       let t ← mkAppM ``Source.Term.ann #[← elabTyp ty, ← elabTrm t]
       mkAppM ``Source.Term.let #[← elabPattern p, t, mkConst ``Source.Term.unit]
+  | `(aiur_trm| $t:aiur_trm; $[$t':aiur_trm]?) => do
+    mkAppM ``Source.Term.let
+      #[mkConst ``Pattern.wildcard, ← elabTrm t, ← elabRet t']
   | `(aiur_trm| match $t:aiur_trm {$[$ps:aiur_pattern => $ts:aiur_trm,]*}) => do
     let mut prods := Array.mkEmpty (ps.size + 1)
     for (p, t) in ps.zip ts do
@@ -570,6 +585,10 @@ where
       let body ← if v.getId = old then pure body
         else replaceToken old new body
       `(aiur_trm| fold($i .. $j, $init, |$acc, @$v| $body))
+    | `(aiur_trm| $t:aiur_trm; $[$t':aiur_trm]?) => do
+      let t ← replaceToken old new t
+      let t' ← t'.mapM $ replaceToken old new
+      `(aiur_trm| $t; $[$t']?)
     | stx => pure stx
 
 declare_syntax_cat                                aiur_constructor

Ix/IxVM/Blake3.lean

@@ -21,7 +21,7 @@ def blake3 := ⟦
     let key = [num_hashes_pred];
     let (idx, len) = io_get_info(0, key);
     let byte_stream = #read_byte_stream(0, idx, len);
-    let _ = blake3(byte_stream);
+    blake3(byte_stream);
     match num_hashes_pred {
       0 => 0,
       _ => blake3_bench(num_hashes_pred),
@@ -60,7 +60,6 @@ def blake3 := ⟦
        h[6][0], h[6][1], h[6][2], h[6][3],
        h[7][0], h[7][1], h[7][2], h[7][3]],
       expected);
-    ()
   }
 
   -- Hash `bytes` and intern the digest into the Store. Returned pointer is

Ix/IxVM/Ingress.lean

@@ -49,7 +49,7 @@ def ingress := ⟦
     let raw = load(addr);
     let (idx, len) = io_get_info(2, raw);
     let bytes = #read_byte_stream(2, idx, len);
-    let _ = verify_bytes_against(bytes, raw);
+    verify_bytes_against(bytes, raw);
     let (constant, rest) = get_constant(bytes);
     assert_eq!(load(rest), ListNode.Nil);
     constant
@@ -61,7 +61,7 @@ def ingress := ⟦
     let raw = load(addr);
     let (idx, len) = io_get_info(5, raw);
     let bytes = #read_byte_stream(5, idx, len);
-    let _ = verify_bytes_against(bytes, raw);
+    verify_bytes_against(bytes, raw);
     bytes
   }
 

Ix/IxVM/Kernel/CanonicalCheck.lean

@@ -766,7 +766,7 @@ def canonicalCheck := ⟦
             check_canonical_block_sort_walk(rest, ba, list_snoc(cur_members, pos),
                                              pos + 1, top),
           0 =>
-            let _ = validate_block_if_nonzero(cur_ba, cur_members, top);
+            validate_block_if_nonzero(cur_ba, cur_members, top);
             let new_members = init_block_members(ba, pos);
             check_canonical_block_sort_walk(rest, ba, new_members, pos + 1, top),
         },

Ix/IxVM/Kernel/Check.lean

@@ -93,10 +93,10 @@ def check := ⟦
       KLevelNode.Zero => (),
       KLevelNode.Succ(inner) => validate_univ_params_seen(inner, bound),
       KLevelNode.Max(a, b) =>
-        let _ = validate_univ_params_seen(a, bound);
+        validate_univ_params_seen(a, bound);
         validate_univ_params_seen(b, bound),
       KLevelNode.IMax(a, b) =>
-        let _ = validate_univ_params_seen(a, bound);
+        validate_univ_params_seen(a, bound);
         validate_univ_params_seen(b, bound),
       KLevelNode.Param(i) =>
         assert_eq!(u32_less_than(i, bound), 1);
@@ -108,7 +108,7 @@ def check := ⟦
     match load(lvls) {
       ListNode.Nil => (),
       ListNode.Cons(u, rest) =>
-        let _ = validate_univ_params_seen(u, bound);
+        validate_univ_params_seen(u, bound);
         validate_univ_params_list(rest, bound),
     }
   }
@@ -129,17 +129,17 @@ def check := ⟦
         assert_eq!(list_length(lvls), expected);
         validate_univ_params_list(lvls, bound),
       KExprNode.App(f, a) =>
-        let _ = validate_expr_well_scoped(f, depth, bound, top);
+        validate_expr_well_scoped(f, depth, bound, top);
         validate_expr_well_scoped(a, depth, bound, top),
       KExprNode.Lam(t, b) =>
-        let _ = validate_expr_well_scoped(t, depth, bound, top);
+        validate_expr_well_scoped(t, depth, bound, top);
         validate_expr_well_scoped(b, depth + 1, bound, top),
       KExprNode.Forall(t, b) =>
-        let _ = validate_expr_well_scoped(t, depth, bound, top);
+        validate_expr_well_scoped(t, depth, bound, top);
         validate_expr_well_scoped(b, depth + 1, bound, top),
       KExprNode.Let(t, v, b) =>
-        let _ = validate_expr_well_scoped(t, depth, bound, top);
-        let _ = validate_expr_well_scoped(v, depth, bound, top);
+        validate_expr_well_scoped(t, depth, bound, top);
+        validate_expr_well_scoped(v, depth, bound, top);
         validate_expr_well_scoped(b, depth + 1, bound, top),
       KExprNode.Lit(_) => (),
       KExprNode.Proj(_, _, val) =>
@@ -152,7 +152,7 @@ def check := ⟦
   fn validate_const_well_scoped(ci: KConstantInfo, top: List‹&KConstantInfo›) {
     let bound = const_num_lvls(ci);
     let ty = const_type_of(ci);
-    let _ = validate_expr_well_scoped(ty, 0, bound, top);
+    validate_expr_well_scoped(ty, 0, bound, top);
     match ci {
       KConstantInfo.Defn(_, _, val, _, _) =>
         validate_expr_well_scoped(val, 0, bound, top),
@@ -173,7 +173,7 @@ def check := ⟦
       ListNode.Cons(rule, rest) =>
         match rule {
           KRecRule.Mk(_, _, rhs) =>
-            let _ = validate_expr_well_scoped(rhs, 0, bound, top);
+            validate_expr_well_scoped(rhs, 0, bound, top);
             validate_recr_rules(rest, bound, top),
         },
     }
@@ -201,59 +201,59 @@ def check := ⟦
   -- check_const: dispatch per KConstantInfo variant.
   -- ============================================================================
   fn check_const(ci: KConstantInfo, pos: G, top: List‹&KConstantInfo›, addrs: List‹Addr›) {
-    let _ = validate_const_well_scoped(ci, top);
+    validate_const_well_scoped(ci, top);
     let u = is_unsafe_ci(ci);
     match ci {
       KConstantInfo.Axiom(_, ty, _) =>
-        let _ = k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
-        let _ = assert_safety(u, ty, top);
+        k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
+        assert_safety(u, ty, top);
         (),
 
       KConstantInfo.Defn(_, ty, val, _, _) =>
-        let _ = k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
-        let _ = assert_safety(u, ty, top);
-        let _ = assert_safety(u, val, top);
-        let _ = k_check(val, ty, store(ListNode.Nil), top, addrs);
+        k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
+        assert_safety(u, ty, top);
+        assert_safety(u, val, top);
+        k_check(val, ty, store(ListNode.Nil), top, addrs);
         (),
 
       KConstantInfo.Thm(_, ty, val) =>
         -- Mirror: src/ix/kernel/check.rs:135. Theorem type must be Sort 0.
         let lvl = k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
         assert_eq!(level_equal(lvl, store(KLevelNode.Zero)), 1);
-        let _ = assert_safety(u, ty, top);
-        let _ = assert_safety(u, val, top);
-        let _ = k_check(val, ty, store(ListNode.Nil), top, addrs);
+        assert_safety(u, ty, top);
+        assert_safety(u, val, top);
+        k_check(val, ty, store(ListNode.Nil), top, addrs);
         (),
 
       KConstantInfo.Opaque(_, ty, val, is_unsafe) =>
-        let _ = k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
-        let _ = assert_safety(u, ty, top);
-        let _ = assert_safety(u, val, top);
+        k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
+        assert_safety(u, ty, top);
+        assert_safety(u, val, top);
         match is_unsafe {
           1 => (),
           0 =>
-            let _ = k_check(val, ty, store(ListNode.Nil), top, addrs);
+            k_check(val, ty, store(ListNode.Nil), top, addrs);
             (),
         },
 
       KConstantInfo.Quot(num_lvls, ty, kind) =>
-        let _ = k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
-        let _ = assert_safety(u, ty, top);
+        k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
+        assert_safety(u, ty, top);
         -- Mirror: src/ix/kernel/check.rs:606-675 fn check_quot.
         -- Validate kind ↔ address consistency, universe-param count per
         -- variant, and forall-binder count.
         let self_addr = list_lookup(addrs, pos);
-        let _ = check_quot(self_addr, kind, num_lvls, ty, top, addrs);
+        check_quot(self_addr, kind, num_lvls, ty, top, addrs);
         (),
 
       KConstantInfo.Induct(_, ty, n_params, n_indices, _,
                           _, block_addr) =>
-        let _ = k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
-        let _ = assert_safety(u, ty, top);
-        let _ = check_block_peer_param_agreement(pos, ty, n_params, n_indices,
+        k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
+        assert_safety(u, ty, top);
+        check_block_peer_param_agreement(pos, ty, n_params, n_indices,
                                                   block_addr, top, addrs);
         let block_idxs = derive_block_member_idxs(pos, top);
-        let _ = validate_block_auxes(block_idxs, top);
+        validate_block_auxes(block_idxs, top);
         -- The former H1 declared-vs-computed is_rec check is gone with the
         -- Ixon recr flag: there is no declared value to verify. is_rec is
         -- computed on demand (`computed_is_rec_ind`) wherever it matters
@@ -264,29 +264,29 @@ def check := ⟦
       -- Ctor cross-ref + return-type + field-universe + strict-positivity
       -- (positivity walks mutual + nested via derive_block_member_idxs).
       KConstantInfo.Ctor(_, ty, induct_idx, _, num_params, num_fields, _) =>
-        let _ = k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
-        let _ = assert_safety(u, ty, top);
-        let _ = check_ctor_against_inductive_member(pos, ci, top);
+        k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
+        assert_safety(u, ty, top);
+        check_ctor_against_inductive_member(pos, ci, top);
         let ind_ci = load(list_lookup(top, induct_idx));
         match ind_ci {
           KConstantInfo.Induct(ind_num_lvls, ind_ty, ind_n_params, ind_n_indices, _, _, _) =>
             assert_eq!(num_params, ind_n_params);
             -- A1 defense-in-depth: ctor's leading param domains must match
             -- parent inductive's. Mirror src/ix/kernel/inductive.rs:283,393.
-            let _ = check_param_agreement(ind_ty, ty, ind_n_params, top, addrs);
-            let _ = check_ctor_return_type(ty, num_params, ind_n_indices, num_fields,
+            check_param_agreement(ind_ty, ty, ind_n_params, top, addrs);
+            check_ctor_return_type(ty, num_params, ind_n_indices, num_fields,
                                            induct_idx, ind_num_lvls);
             let ind_level = get_result_sort_level(ind_ty, ind_n_params + ind_n_indices);
-            let _ = check_field_universes(ty, num_params, ind_level,
+            check_field_universes(ty, num_params, ind_level,
                                           store(ListNode.Nil), top, addrs);
-            let _ = check_positivity(ty, num_params, induct_idx, store(ListNode.Nil), top, addrs);
+            check_positivity(ty, num_params, induct_idx, store(ListNode.Nil), top, addrs);
             (),
         },
 
       KConstantInfo.Rec(_, ty, _, _, _, _, _, _, _, _) =>
-        let _ = k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
-        let _ = assert_safety(u, ty, top);
-        let _ = check_recursor_member(pos, ci, top, addrs);
+        k_ensure_sort(ty, store(ListNode.Nil), top, addrs);
+        assert_safety(u, ty, top);
+        check_recursor_member(pos, ci, top, addrs);
         (),
     }
   }
@@ -310,7 +310,7 @@ def check := ⟦
         assert_eq!(address_eq(self_addr, quot_lift_addr()), 1);
         -- Mirror: src/ix/kernel/check.rs:651-653. Lift requires Eq type
         -- to be properly formed (Quot.lift uses Eq in its reduction rule).
-        let _ = check_eq_type(top, addrs);
+        check_eq_type(top, addrs);
         (2, 6),
       QuotKind.Ind =>
         assert_eq!(address_eq(self_addr, quot_ind_addr()), 1);
@@ -337,7 +337,7 @@ def check := ⟦
   }
 
   fn check_all(consts: List‹&KConstantInfo›, top: List‹&KConstantInfo›, addrs: List‹Addr›) {
-    let _ = check_canonical_block_sort(top);
+    check_canonical_block_sort(top);
     check_all_iter(consts, top, addrs, 0)
   }
 
@@ -346,7 +346,7 @@ def check := ⟦
     match load(consts) {
       ListNode.Nil => (),
       ListNode.Cons(&ci, rest) =>
-        let _ = check_const(ci, pos, top, addrs);
+        check_const(ci, pos, top, addrs);
         check_all_iter(rest, top, addrs, pos + 1),
     }
   }