Fix wildcard let bindings and add body-less let syntax

Ix/Aiur/Compile.lean

@@ -295,6 +295,9 @@ partial def toIndex
   | .let (.var var) val bod => do
     let val ← toIndex layoutMap bindings val
     toIndex layoutMap (bindings.insert var val) bod
+  | .let .wildcard val bod => do
+    let _ ← toIndex layoutMap bindings val
+    toIndex layoutMap bindings bod
   | .let .. => throw "Should not happen after simplifying"
   | .add a b => do
     let a ← expectIdx a
@@ -502,6 +505,9 @@ partial def TypedTerm.compile
   | .let (.var var) val bod => do
     let val ← toIndex layoutMap bindings val
     bod.compile returnTyp layoutMap (bindings.insert var val)
+  | .let .wildcard val bod => do
+    let _ ← toIndex layoutMap bindings val
+    bod.compile returnTyp layoutMap bindings
   | .let .. => throw "Should not happen after simplifying"
   | .debug label term ret => do
     let term ← term.mapM (toIndex layoutMap bindings)

Ix/Aiur/Meta.lean

@@ -103,6 +103,8 @@ syntax "[" trm (", " trm)* "]"                                : trm
 syntax "[" trm "; " num "]"                                   : trm
 syntax "return " trm                                          : trm
 syntax "let " pattern (":" typ)? " = " trm "; " trm           : trm
+syntax "let " pattern (":" typ)? " = " trm ";"                : trm
+syntax "let " pattern (":" typ)? " = " trm                    : trm
 syntax "match " trm " { " (pattern " => " trm ", ")+ " }"     : trm
 syntax ("." noWs)? ident "(" ")"                              : trm
 syntax ("." noWs)? ident "(" trm (", " trm)* ")"              : trm
@@ -173,6 +175,16 @@ partial def elabTrm : ElabStxCat `trm
     | some ty => do
       let t ← mkAppM ``Term.ann #[← elabTyp ty, ← elabTrm t]
       mkAppM ``Term.let #[← elabPattern p, t, ← elabTrm t']
+  | `(trm| let $p:pattern $[: $ty:typ]? = $t:trm;) => match ty with
+    | none => do mkAppM ``Term.let #[← elabPattern p, ← elabTrm t, mkConst ``Term.unit]
+    | some ty => do
+      let t ← mkAppM ``Term.ann #[← elabTyp ty, ← elabTrm t]
+      mkAppM ``Term.let #[← elabPattern p, t, mkConst ``Term.unit]
+  | `(trm| let $p:pattern $[: $ty:typ]? = $t:trm) => match ty with
+    | none => do mkAppM ``Term.let #[← elabPattern p, ← elabTrm t, mkConst ``Term.unit]
+    | some ty => do
+      let t ← mkAppM ``Term.ann #[← elabTyp ty, ← elabTrm t]
+      mkAppM ``Term.let #[← elabPattern p, t, mkConst ``Term.unit]
   | `(trm| match $t:trm {$[$ps:pattern => $ts:trm,]*}) => do
     let mut prods := Array.mkEmpty (ps.size + 1)
     for (p, t) in ps.zip ts do
@@ -294,6 +306,12 @@ where
       let t ← replaceToken old new t
       let t' ← replaceToken old new t'
       `(trm| let $p $[: $ty]? = $t; $t')
+    | `(trm| let $p:pattern $[: $ty]? = $t:trm;) => do
+      let t ← replaceToken old new t
+      `(trm| let $p $[: $ty]? = $t;)
+    | `(trm| let $p:pattern $[: $ty]? = $t:trm) => do
+      let t ← replaceToken old new t
+      `(trm| let $p $[: $ty]? = $t)
     | `(trm| match $t:trm {$[$ps:pattern => $ts:trm,]*}) => do
       let t ← replaceToken old new t
       let ts ← ts.mapM $ replaceToken old new

Ix/Aiur/Simple.lean

@@ -11,9 +11,7 @@ private abbrev tmpVar := Local.idx 0
 
 partial def simplifyTerm (decls : Decls) : Term → Term
   | .let var@(.var _) val body => .let var (recr val) (recr body)
-  -- NOTE: This would not be safe in case Aiur allows side-effects.
-  -- A sequencing operation would be needed.
-  | .let .wildcard _ body => recr body
+  | .let .wildcard val body => .let .wildcard (recr val) (recr body)
   | .let pat val body =>
     let mtch := .match (.var tmpVar) [(pat, body)]
     .let (.var tmpVar) (recr val) (recr mtch)

Ix/IxVM/Blake3.lean

@@ -21,7 +21,7 @@ def blake3 := ⟦
     let key = [num_hashes_pred];
     let (idx, len) = io_get_info(key);
     let byte_stream = read_byte_stream(idx, len);
-    let _x = blake3(byte_stream);
+    let _ = blake3(byte_stream);
     match num_hashes_pred {
       0 => 0,
       _ => blake3_bench(num_hashes_pred),

Ix/IxVM/Kernel.lean

@@ -1073,7 +1073,7 @@ def kernel := ⟦
         },
 
       KExpr.Lam(&ty, &body) =>
-        let _x = k_ensure_sort(ty, types, env, depth, top, nat_idx, str_idx);
+        let _ = k_ensure_sort(ty, types, env, depth, top, nat_idx, str_idx);
         let dom_val = k_eval(ty, env, top);
         let fvar = KVal.FVar(depth, store(dom_val), store(KValList.Nil));
         let types2 = KValList.Cons(store(dom_val), store(types));
@@ -1093,7 +1093,7 @@ def kernel := ⟦
         KVal.Srt(store(result_level)),
 
       KExpr.Let(&ty, &val, &body) =>
-        let _x = k_ensure_sort(ty, types, env, depth, top, nat_idx, str_idx);
+        let _ = k_ensure_sort(ty, types, env, depth, top, nat_idx, str_idx);
         let ty_val = k_eval(ty, env, top);
         let val_type = k_infer(val, types, env, depth, top, nat_idx, str_idx);
         let let_eq = k_is_def_eq(val_type, ty_val, depth, top, nat_idx, str_idx);
@@ -1884,21 +1884,20 @@ def kernel := ⟦
   fn k_check_const(ci: KConstantInfo, top: KConstList, nat_idx: G, str_idx: G) {
     match ci {
       KConstantInfo.Axiom(_, &ty, _) =>
-        let _x = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
-        (),
+        let _ = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx),
 
       KConstantInfo.Defn(_, &ty, &value, _, _) =>
-        let _x = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
+        let _ = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
         let ty_val = k_eval(ty, KValEnv.Nil, top);
         k_check(value, ty_val, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx),
 
       KConstantInfo.Thm(_, &ty, &value) =>
-        let _x = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
+        let _ = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
         let ty_val = k_eval(ty, KValEnv.Nil, top);
         k_check(value, ty_val, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx),
 
       KConstantInfo.Opaque(_, &ty, &value, is_unsafe) =>
-        let _x = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
+        let _ = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
         match is_unsafe {
           1 => (),
           0 =>
@@ -1907,20 +1906,16 @@ def kernel := ⟦
         },
 
       KConstantInfo.Quot(_, &ty, _) =>
-        let _x = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
-        (),
+        let _ = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx),
 
       KConstantInfo.Induct(_, &ty, _, _, _, _, _, _) =>
-        let _x = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
-        (),
+        let _ = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx),
 
       KConstantInfo.Ctor(_, &ty, _, _, _, _, _) =>
-        let _x = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
-        (),
+        let _ = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx),
 
       KConstantInfo.Rec(_, &ty, _, _, _, _, _, _, _) =>
-        let _x = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx);
-        (),
+        let _ = k_ensure_sort(ty, KValList.Nil, KValEnv.Nil, 0, top, nat_idx, str_idx),
     }
   }
 
@@ -1935,7 +1930,7 @@ def kernel := ⟦
     match consts {
       KConstList.Nil => (),
       KConstList.Cons(&ci, &rest) =>
-        let _x = k_check_const(ci, top, nat_idx, str_idx);
+        let _ = k_check_const(ci, top, nat_idx, str_idx);
         k_check_all_go(rest, top, nat_idx, str_idx, idx + 1),
     }
   }

Ix/IxVM/Sha256.lean

@@ -21,7 +21,7 @@ def sha256 := ⟦
     let key = [num_hashes_pred];
     let (idx, len) = io_get_info(key);
     let byte_stream = read_byte_stream(idx, len);
-    let _x = sha256(byte_stream);
+    let _ = sha256(byte_stream);
     match num_hashes_pred {
       0 => 0,
       _ => sha256_bench(num_hashes_pred),