diff --git a/Ix/Aiur/Compile.lean b/Ix/Aiur/Compile.lean index 1fd26cc9..32a1935d 100644 --- a/Ix/Aiur/Compile.lean +++ b/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) diff --git a/Ix/Aiur/Meta.lean b/Ix/Aiur/Meta.lean index 2f077428..e75b7c94 100644 --- a/Ix/Aiur/Meta.lean +++ b/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 diff --git a/Ix/Aiur/Simple.lean b/Ix/Aiur/Simple.lean index 4e7b780a..050e8a27 100644 --- a/Ix/Aiur/Simple.lean +++ b/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) diff --git a/Ix/IxVM/Blake3.lean b/Ix/IxVM/Blake3.lean index df1a5ca8..e9131f52 100644 --- a/Ix/IxVM/Blake3.lean +++ b/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), diff --git a/Ix/IxVM/Kernel.lean b/Ix/IxVM/Kernel.lean index c530d629..70780a54 100644 --- a/Ix/IxVM/Kernel.lean +++ b/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), } } diff --git a/Ix/IxVM/Sha256.lean b/Ix/IxVM/Sha256.lean index 697d1b72..2a8ae692 100644 --- a/Ix/IxVM/Sha256.lean +++ b/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),