ISLE: add support for extended left-hand sides with if-let clauses. (#4072)

This PR adds support for `if-let` clauses, as proposed in
bytecodealliance/rfcs#21. These clauses augment the left-hand side
(pattern-matching phase) of rules in the ISLE instruction-selection DSL
with sub-patterns matching on sub-expressions. The ability to list
additional match operations to perform, out-of-line from the original
toplevel pattern, greatly simplifies some idioms. See the RFC for more
details and examples of use.

cranelift/isle/docs/language-reference.md

@@ -949,6 +949,118 @@ semantically as important as the core language: they are not
 implementation details, but rather, a well-defined interface by which
 ISLE can interface with the outside world (an "FFI" of sorts).
 
+### If-Let Clauses
+
+As an extension to the basic left-hand-side / right-hand-side rule
+idiom, ISLE allows *if-let clauses* to be used. These add additional
+pattern-matching steps, and can be used to perform additional tests
+and also to use constructors in place of extractors during the match
+phase when this is more convenient.
+
+To introduce the concept, an example follows (this is taken from the
+[RFC](https://github.com/bytecodealliance/rfcs/tree/main/isle-extended-patterns.md)
+that proposed if-lets):
+
+```lisp
+;; `u32_fallible_add` can now be used in patterns in `if-let` clauses
+(decl pure u32_fallible_add (u32 u32) u32)
+(extern constructor u32_fallible_add u32_fallible_add)
+
+(rule (lower (load (iadd addr
+                         (iadd (uextend (iconst k1))
+                               (uextend (iconst k2))))))
+      (if-let k (u32_fallible_add k1 k2))
+      (isa_load (amode_reg_offset addr k)))
+```
+
+The key idea is that we allow a `rule` form to contain the following
+sub-forms:
+
+```lisp
+(rule LHS_PATTERN
+  (if-let PAT2 EXPR2)
+  (if-let PAT3 EXPR3)
+  ...
+  RHS)
+```
+
+The matching proceeds as follows: the main pattern (`LHS_PATTERN`)
+matches against the input value (the term to be rewritten), as
+described in detail above. Then, if this matches, execution proceeds
+to the if-let clauses in the order they are specified. For each, we
+evaluate the expression (`EXPR2` or `EXPR3` above) first. An
+expression in an if-let context is allowed to be "fallible": the
+constructors return `Option<T>` at the Rust level and can return
+`None`, in which case the whole rule application fails and we move on
+to the next rule as if the main pattern had failed to match. (MOre on
+the fallible constructors below.) If the expression evaluation
+succeeds, we match the associated pattern (`PAT2` or `PAT3` above)
+against the resulting value. This too can fail, causing the whole rule
+to fail. If it succeeds, any resulting variable bindings are
+available. Variables bound in the main pattern are available for all
+if-let expressions and patterns, and variables bound by a given if-let
+clause are available for all subsequent clauses. All bound variables
+(from the main pattern and if-let clauses) are available in the
+right-hand side expression.
+
+#### Pure Expressions and Constructors
+
+In order for an expression to be used in an if-let clause, it has to
+be *pure*: it cannot have side-effects. A pure expression is one that
+uses constants and pure constructors only. Enum variant constructors
+are always pure. In general constructors that invoke function calls,
+however (either as internal or external constructor calls), can lead
+to arbitrary Rust code and have side-effects. So, we add a new
+annotation to declarations as follows:
+
+```lisp
+;; `u32_fallible_add` can now be used in patterns in `if-let` clauses
+(decl pure u32_fallible_add (u32 u32) u32)
+
+;; This adds a method
+;; `fn u32_fallible_add(&mut self, _: u32, _: u32) -> Option<u32>`
+;; to the `Context` trait.
+(extern constructor u32_fallible_add u32_fallible_add)
+```
+
+The `pure` keyword here is a declaration that the term, when used as a
+constructor, has no side-effects. Declaring an external constructor on
+a pure term is a promise by the ISLE programmer that the external Rust
+function we are naming (here `u32_fallible_add`) has no side-effects
+and is thus safe to invoke during the match phase of a rule, when we
+have not committed to a given rule yet.
+
+When an internal constructor body is generated for a term that is pure
+(i.e., if we had `(rule (u32_fallible_add x y) ...)` in our program
+after the above declaration instead of the `extern`), the right-hand
+side expression of each rule that rewrites the term is also checked
+for purity.
+
+#### `if` Shorthand
+
+It is a fairly common idiom that if-let clauses are used as predicates
+on rules, such that their only purpose is to allow a rule to match,
+and not to perform any destructuring with a sub-pattern. For example,
+one might want to write:
+
+```lisp
+(rule (lower (special_inst ...))
+      (if-let _ (isa_extension_enabled))
+      (isa_special_inst ...))
+```
+
+where `isa_extension_enabled` is a pure constructor that is fallible,
+and succeeds only when a condition is true.
+
+To enable more succinct expression of this idiom, we allow the
+following shorthand notation using `if` instead:
+
+```lisp
+(rule (lower (special_inst ...))
+      (if (isa_extension_enabled))
+      (isa_special_inst ...))
+```
+
 ### Mapping to Rust: Constructors, Functions, and Control Flow
 
 ISLE was designed to have a simple, easy-to-understand mapping from

cranelift/isle/isle/isle_examples/fail/impure_expression.isle

@@ -0,0 +1,10 @@
+(type u32 (primitive u32))
+
+(decl ctor (u32) u32)
+(rule (ctor x) x)
+
+(decl entry (u32) u32)
+
+(rule (entry x)
+      (if-let y (ctor x))
+      y)

cranelift/isle/isle/isle_examples/fail/impure_rhs.isle

@@ -0,0 +1,15 @@
+(type u32 (primitive u32))
+
+(decl pure ctor (u32) u32)
+(decl impure (u32) u32)
+
+(decl entry (u32) u32)
+
+(rule (entry x)
+      (if-let y (ctor x))
+      y)
+
+(rule (ctor x)
+      (impure x))
+
+(rule (impure x) x)

cranelift/isle/isle/isle_examples/link/borrows.isle

@@ -0,0 +1,15 @@
+(type u32 (primitive u32))
+(type A extern (enum (B (x u32) (y u32))))
+
+(decl get_a (A) u32)
+(extern extractor get_a get_a)
+
+(decl pure u32_pure (u32) u32)
+(extern constructor u32_pure u32_pure)
+
+(decl entry (u32) u32)
+(rule (entry x @ (get_a a1))
+      (if-let (get_a a2) x)
+      (if-let (A.B p q) a1)
+      (if-let r (u32_pure p))
+      r)

cranelift/isle/isle/isle_examples/link/borrows_main.rs

@@ -0,0 +1,21 @@
+mod borrows;
+
+#[derive(Clone)]
+pub enum A {
+    B { x: u32, y: u32 },
+}
+
+struct Context(A);
+impl borrows::Context for Context {
+    fn get_a(&mut self, _: u32) -> Option<A> {
+        Some(self.0.clone())
+    }
+
+    fn u32_pure(&mut self, value: u32) -> Option<u32> {
+        Some(value + 1)
+    }
+}
+
+fn main() {
+    borrows::constructor_entry(&mut Context(A::B { x: 1, y: 2 }), 42);
+}

cranelift/isle/isle/isle_examples/link/iflets.isle

@@ -0,0 +1,29 @@
+(type u32 (primitive u32))
+
+(decl pure A (u32 u32) u32)
+(extern constructor A A)
+
+(decl B (u32 u32) u32)
+(extern extractor B B)
+
+(decl C (u32 u32 u32 u32) u32)
+
+(decl pure predicate () u32)
+(rule (predicate) 1)
+
+(rule (C a b c (B d e))
+      (if-let (B f g) d)
+      (if-let h (A a b))
+      (A h a))
+
+(rule (C a b c d)
+      (if (predicate))
+      42)
+
+(rule (C a b a b)
+      (if-let x (D a b))
+      x)
+
+(decl pure D (u32 u32) u32)
+(rule (D x 0) x)
+(rule (D 0 x) x)

cranelift/isle/isle/isle_examples/link/iflets_main.rs

@@ -0,0 +1,16 @@
+mod iflets;
+
+struct Context;
+impl iflets::Context for Context {
+    fn A(&mut self, a: u32, b: u32) -> Option<u32> {
+        Some(a + b)
+    }
+
+    fn B(&mut self, value: u32) -> Option<(u32, u32)> {
+        Some((value, value + 1))
+    }
+}
+
+fn main() {
+    iflets::constructor_C(&mut Context, 1, 2, 3, 4);
+}

cranelift/isle/isle/src/ast.rs

@@ -69,17 +69,27 @@ pub struct Decl {
     pub term: Ident,
     pub arg_tys: Vec<Ident>,
     pub ret_ty: Ident,
+    /// Whether this term's constructor is pure.
+    pub pure: bool,
     pub pos: Pos,
 }
 
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub struct Rule {
     pub pattern: Pattern,
+    pub iflets: Vec<IfLet>,
     pub expr: Expr,
     pub pos: Pos,
     pub prio: Option<i64>,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub struct IfLet {
+    pub pattern: Pattern,
+    pub expr: Expr,
+    pub pos: Pos,
+}
+
 /// An extractor macro: (A x y) becomes (B x _ y ...). Expanded during
 /// ast-to-sema pass.
 #[derive(Clone, PartialEq, Eq, Debug)]

cranelift/isle/isle/src/codegen.rs

@@ -68,7 +68,7 @@ impl<'a> Codegen<'a> {
         .unwrap();
         writeln!(
             code,
-            "#![allow(unused_imports, unused_variables, non_snake_case)]"
+            "#![allow(unused_imports, unused_variables, non_snake_case, unused_mut)]"
         )
         .unwrap();
         writeln!(code, "#![allow(irrefutable_let_patterns)]").unwrap();
@@ -626,7 +626,7 @@ impl<'a> Codegen<'a> {
                 ref seq, output_ty, ..
             } => {
                 let closure_name = format!("closure{}", id.index());
-                writeln!(code, "{}let {} = || {{", indent, closure_name).unwrap();
+                writeln!(code, "{}let mut {} = || {{", indent, closure_name).unwrap();
                 let subindent = format!("{}    ", indent);
                 let mut subctx = ctx.clone();
                 let mut returns = vec![];

cranelift/isle/isle/src/ir.rs

@@ -628,13 +628,14 @@ impl ExprSequence {
                     }
                     TermKind::Decl {
                         constructor_kind: Some(ConstructorKind::ExternalConstructor { .. }),
+                        pure,
                         ..
                     } => {
                         self.add_construct(
                             &arg_values_tys[..],
                             ty,
                             term,
-                            /* infallible = */ true,
+                            /* infallible = */ !pure,
                         )
                     }
                     TermKind::Decl {
@@ -675,6 +676,23 @@ pub fn lower_rule(
         &mut vars,
     );
 
+    // Lower the `if-let` clauses into the pattern seq, using
+    // `PatternInst::Expr` for the sub-exprs (right-hand sides).
+    for iflet in &ruledata.iflets {
+        let mut subexpr_seq: ExprSequence = Default::default();
+        let subexpr_ret_value = subexpr_seq.gen_expr(tyenv, termenv, &iflet.rhs, &mut vars);
+        subexpr_seq.add_return(iflet.rhs.ty(), subexpr_ret_value);
+        let pattern_value =
+            pattern_seq.add_expr_seq(subexpr_seq, subexpr_ret_value, iflet.rhs.ty());
+        pattern_seq.gen_pattern(
+            ValueOrArgs::Value(pattern_value),
+            tyenv,
+            termenv,
+            &iflet.lhs,
+            &mut vars,
+        );
+    }
+
     // Lower the expression, making use of the bound variables
     // from the pattern.
     let rhs_root_val = expr_seq.gen_expr(tyenv, termenv, &ruledata.rhs, &vars);

cranelift/isle/isle/src/parser.rs

@@ -18,6 +18,14 @@ struct Parser<'a> {
     lexer: Lexer<'a>,
 }
 
+/// Used during parsing a `(rule ...)` to encapsulate some form that
+/// comes after the top-level pattern: an if-let clause, or the final
+/// top-level expr.
+enum IfLetOrExpr {
+    IfLet(IfLet),
+    Expr(Expr),
+}
+
 impl<'a> Parser<'a> {
     /// Construct a new parser from the given lexer.
     pub fn new(lexer: Lexer<'a>) -> Parser<'a> {
@@ -281,6 +289,14 @@ impl<'a> Parser<'a> {
 
     fn parse_decl(&mut self) -> Result<Decl> {
         let pos = self.pos();
+
+        let pure = if self.is_sym_str("pure") {
+            self.symbol()?;
+            true
+        } else {
+            false
+        };
+
         let term = self.parse_ident()?;
 
         self.lparen()?;
@@ -296,6 +312,7 @@ impl<'a> Parser<'a> {
             term,
             arg_tys,
             ret_ty,
+            pure,
             pos,
         })
     }
@@ -304,6 +321,7 @@ impl<'a> Parser<'a> {
         let pos = self.pos();
         if self.is_sym_str("constructor") {
             self.symbol()?;
+
             let term = self.parse_ident()?;
             let func = self.parse_ident()?;
             Ok(Extern::Constructor { term, func, pos })
@@ -387,13 +405,23 @@ impl<'a> Parser<'a> {
             None
         };
         let pattern = self.parse_pattern()?;
-        let expr = self.parse_expr()?;
+        let mut iflets = vec![];
-        Ok(Rule {
+        loop {
+            match self.parse_iflet_or_expr()? {
+                IfLetOrExpr::IfLet(iflet) => {
+                    iflets.push(iflet);
+                }
+                IfLetOrExpr::Expr(expr) => {
+                    return Ok(Rule {
                         pattern,
+                        iflets,
                         expr,
                         pos,
                         prio,
-        })
+                    });
+                }
+            }
+        }
     }
 
     fn parse_pattern(&mut self) -> Result<Pattern> {
@@ -452,31 +480,52 @@ impl<'a> Parser<'a> {
         }
     }
 
+    fn parse_iflet_or_expr(&mut self) -> Result<IfLetOrExpr> {
+        let pos = self.pos();
+        if self.is_lparen() {
+            self.lparen()?;
+            let ret = if self.is_sym_str("if-let") {
+                self.symbol()?;
+                IfLetOrExpr::IfLet(self.parse_iflet()?)
+            } else if self.is_sym_str("if") {
+                // Shorthand form: `(if (x))` desugars to `(if-let _
+                // (x))`.
+                self.symbol()?;
+                IfLetOrExpr::IfLet(self.parse_iflet_if()?)
+            } else {
+                IfLetOrExpr::Expr(self.parse_expr_inner_parens(pos)?)
+            };
+            self.rparen()?;
+            Ok(ret)
+        } else {
+            self.parse_expr().map(|expr| IfLetOrExpr::Expr(expr))
+        }
+    }
+
+    fn parse_iflet(&mut self) -> Result<IfLet> {
+        let pos = self.pos();
+        let pattern = self.parse_pattern()?;
+        let expr = self.parse_expr()?;
+        Ok(IfLet { pattern, expr, pos })
+    }
+
+    fn parse_iflet_if(&mut self) -> Result<IfLet> {
+        let pos = self.pos();
+        let expr = self.parse_expr()?;
+        Ok(IfLet {
+            pattern: Pattern::Wildcard { pos },
+            expr,
+            pos,
+        })
+    }
+
     fn parse_expr(&mut self) -> Result<Expr> {
         let pos = self.pos();
         if self.is_lparen() {
             self.lparen()?;
-            if self.is_sym_str("let") {
+            let ret = self.parse_expr_inner_parens(pos)?;
-                self.symbol()?;
-                self.lparen()?;
-                let mut defs = vec![];
-                while !self.is_rparen() {
-                    let def = self.parse_letdef()?;
-                    defs.push(def);
-                }
             self.rparen()?;
-                let body = Box::new(self.parse_expr()?);
+            Ok(ret)
-                self.rparen()?;
-                Ok(Expr::Let { defs, body, pos })
-            } else {
-                let sym = self.parse_ident()?;
-                let mut args = vec![];
-                while !self.is_rparen() {
-                    args.push(self.parse_expr()?);
-                }
-                self.rparen()?;
-                Ok(Expr::Term { sym, args, pos })
-            }
         } else if self.is_sym_str("#t") {
             self.symbol()?;
             Ok(Expr::ConstInt { val: 1, pos })
@@ -497,6 +546,28 @@ impl<'a> Parser<'a> {
         }
     }
 
+    fn parse_expr_inner_parens(&mut self, pos: Pos) -> Result<Expr> {
+        if self.is_sym_str("let") {
+            self.symbol()?;
+            self.lparen()?;
+            let mut defs = vec![];
+            while !self.is_rparen() {
+                let def = self.parse_letdef()?;
+                defs.push(def);
+            }
+            self.rparen()?;
+            let body = Box::new(self.parse_expr()?);
+            Ok(Expr::Let { defs, body, pos })
+        } else {
+            let sym = self.parse_ident()?;
+            let mut args = vec![];
+            while !self.is_rparen() {
+                args.push(self.parse_expr()?);
+            }
+            Ok(Expr::Term { sym, args, pos })
+        }
+    }
+
     fn parse_letdef(&mut self) -> Result<LetDef> {
         let pos = self.pos();
         self.lparen()?;

cranelift/isle/isle/src/sema.rs

@@ -232,6 +232,8 @@ pub enum TermKind {
     },
     /// A term declared via a `(decl ...)` form.
     Decl {
+        /// Whether the term is marked as `pure`.
+        pure: bool,
         /// The kind of this term's constructor, if any.
         constructor_kind: Option<ConstructorKind>,
         /// The kind of this term's extractor, if any.
@@ -392,13 +394,14 @@ impl Term {
         match &self.kind {
             TermKind::Decl {
                 constructor_kind: Some(ConstructorKind::ExternalConstructor { name }),
+                pure,
                 ..
             } => Some(ExternalSig {
                 func_name: tyenv.syms[name.index()].clone(),
                 full_name: format!("C::{}", tyenv.syms[name.index()]),
                 param_tys: self.arg_tys.clone(),
                 ret_tys: vec![self.ret_ty],
-                infallible: true,
+                infallible: !pure,
             }),
             TermKind::Decl {
                 constructor_kind: Some(ConstructorKind::InternalConstructor { .. }),
@@ -410,6 +413,10 @@ impl Term {
                     full_name: name,
                     param_tys: self.arg_tys.clone(),
                     ret_tys: vec![self.ret_ty],
+                    // Internal constructors are always fallible, even
+                    // if not pure, because ISLE allows partial
+                    // matching at the toplevel (an entry point can
+                    // fail to rewrite).
                     infallible: false,
                 })
             }
@@ -425,6 +432,8 @@ pub struct Rule {
     pub id: RuleId,
     /// The left-hand side pattern that this rule matches.
     pub lhs: Pattern,
+    /// Any subpattern "if-let" clauses.
+    pub iflets: Vec<IfLet>,
     /// The right-hand side expression that this rule evaluates upon successful
     /// match.
     pub rhs: Expr,
@@ -434,6 +443,18 @@ pub struct Rule {
     pub pos: Pos,
 }
 
+/// An `if-let` clause with a subpattern match on an expr after the
+/// main LHS matches.
+#[derive(Clone, Debug)]
+pub struct IfLet {
+    /// The left-hand side pattern that this `if-let` clause matches
+    /// against the expression below.
+    pub lhs: Pattern,
+    /// The right-hand side expression that this pattern
+    /// evaluates. Must be pure.
+    pub rhs: Expr,
+}
+
 /// A left-hand side pattern of some rule.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum Pattern {
@@ -861,6 +882,7 @@ impl TermEnv {
                         kind: TermKind::Decl {
                             constructor_kind: None,
                             extractor_kind: None,
+                            pure: decl.pure,
                         },
                     });
                 }
@@ -1337,6 +1359,18 @@ impl TermEnv {
                         }
                     };
 
+                    let pure = match &self.terms[rule_term.index()].kind {
+                        &TermKind::Decl { pure, .. } => pure,
+                        _ => {
+                            tyenv.report_error(
+                                pos,
+                                "Cannot define a rule on a left-hand-side that is an enum variant"
+                                    .to_string(),
+                            );
+                            continue;
+                        }
+                    };
+
                     let (lhs, ty) = unwrap_or_continue!(self.translate_pattern(
                         tyenv,
                         rule_term,
@@ -1345,17 +1379,25 @@ impl TermEnv {
                         &mut bindings,
                         /* is_root = */ true,
                     ));
+                    let iflets = unwrap_or_continue!(self.translate_iflets(
+                        tyenv,
+                        rule_term,
+                        &rule.iflets[..],
+                        &mut bindings,
+                    ));
                     let rhs = unwrap_or_continue!(self.translate_expr(
                         tyenv,
                         &rule.expr,
-                        ty,
+                        Some(ty),
-                        &mut bindings
+                        &mut bindings,
+                        pure,
                     ));
 
                     let rid = RuleId(self.rules.len());
                     self.rules.push(Rule {
                         id: rid,
                         lhs,
+                        iflets,
                         rhs,
                         prio: rule.prio,
                         pos,
@@ -1829,7 +1871,13 @@ impl TermEnv {
                     return None;
                 }
                 let ty = expected_ty.unwrap();
-                let expr = self.translate_expr(tyenv, expr, expected_ty.unwrap(), bindings)?;
+                let expr = self.translate_expr(
+                    tyenv,
+                    expr,
+                    expected_ty,
+                    bindings,
+                    /* pure = */ true,
+                )?;
                 Some((TermArgPattern::Expr(expr), ty))
             }
         }
@@ -1863,8 +1911,9 @@ impl TermEnv {
         &self,
         tyenv: &mut TypeEnv,
         expr: &ast::Expr,
-        ty: TypeId,
+        ty: Option<TypeId>,
         bindings: &mut Bindings,
+        pure: bool,
     ) -> Option<Expr> {
         log::trace!("translate_expr: {:?}", expr);
         match expr {
@@ -1890,26 +1939,44 @@ impl TermEnv {
                 // are doing an implicit conversion. Report an error
                 // if types don't match and no conversion is possible.
                 let ret_ty = self.terms[tid.index()].ret_ty;
-                let ty = if ret_ty != ty {
+                let ty = if ty.is_some() && ret_ty != ty.unwrap() {
                     // Is there a converter for this type mismatch?
                     if let Some(expanded_expr) =
-                        self.maybe_implicit_convert_expr(tyenv, expr, ret_ty, ty)
+                        self.maybe_implicit_convert_expr(tyenv, expr, ret_ty, ty.unwrap())
                     {
-                        return self.translate_expr(tyenv, &expanded_expr, ty, bindings);
+                        return self.translate_expr(tyenv, &expanded_expr, ty, bindings, pure);
                     }
 
                     tyenv.report_error(
                         pos,
                         format!("Mismatched types: expression expects type '{}' but term has return type '{}'",
-                                tyenv.types[ty.index()].name(tyenv),
+                                tyenv.types[ty.unwrap().index()].name(tyenv),
                                 tyenv.types[ret_ty.index()].name(tyenv)));
 
                     // Keep going, to discover more errors.
                     ret_ty
                 } else {
-                    ty
+                    ret_ty
                 };
 
+                // Check that the term's constructor is pure.
+                match &self.terms[tid.index()].kind {
+                    TermKind::Decl {
+                        pure: ctor_is_pure, ..
+                    } => {
+                        if pure && !ctor_is_pure {
+                            tyenv.report_error(
+                                pos,
+                                format!(
+                                    "Used non-pure constructor '{}' in pure expression context",
+                                    tyenv.syms[name.index()]
+                                ),
+                            );
+                        }
+                    }
+                    _ => {}
+                }
+
                 // Check that we have the correct argument count.
                 if self.terms[tid.index()].arg_tys.len() != args.len() {
                     tyenv.report_error(
@@ -1928,8 +1995,13 @@ impl TermEnv {
                 for (i, arg) in args.iter().enumerate() {
                     let term = unwrap_or_continue!(self.terms.get(tid.index()));
                     let arg_ty = unwrap_or_continue!(term.arg_tys.get(i).copied());
-                    let subexpr =
+                    let subexpr = unwrap_or_continue!(self.translate_expr(
-                        unwrap_or_continue!(self.translate_expr(tyenv, arg, arg_ty, bindings));
+                        tyenv,
+                        arg,
+                        Some(arg_ty),
+                        bindings,
+                        pure
+                    ));
                     subexprs.push(subexpr);
                 }
 
@@ -1947,12 +2019,12 @@ impl TermEnv {
                 };
 
                 // Verify type. Maybe do an implicit conversion.
-                if bv.ty != ty {
+                if ty.is_some() && bv.ty != ty.unwrap() {
                     // Is there a converter for this type mismatch?
                     if let Some(expanded_expr) =
-                        self.maybe_implicit_convert_expr(tyenv, expr, bv.ty, ty)
+                        self.maybe_implicit_convert_expr(tyenv, expr, bv.ty, ty.unwrap())
                     {
-                        return self.translate_expr(tyenv, &expanded_expr, ty, bindings);
+                        return self.translate_expr(tyenv, &expanded_expr, ty, bindings, pure);
                     }
 
                     tyenv.report_error(
@@ -1961,7 +2033,7 @@ impl TermEnv {
                             "Variable '{}' has type {} but we need {} in context",
                             name.0,
                             tyenv.types[bv.ty.index()].name(tyenv),
-                            tyenv.types[ty.index()].name(tyenv)
+                            tyenv.types[ty.unwrap().index()].name(tyenv)
                         ),
                     );
                 }
@@ -1969,6 +2041,15 @@ impl TermEnv {
                 Some(Expr::Var(bv.ty, bv.id))
             }
             &ast::Expr::ConstInt { val, pos } => {
+                if ty.is_none() {
+                    tyenv.report_error(
+                        pos,
+                        "integer literal in a context that needs an explicit type".to_string(),
+                    );
+                    return None;
+                }
+                let ty = ty.unwrap();
+
                 if !tyenv.types[ty.index()].is_prim() {
                     tyenv.report_error(
                         pos,
@@ -1990,19 +2071,19 @@ impl TermEnv {
                         return None;
                     }
                 };
-                if const_ty != ty {
+                if ty.is_some() && const_ty != ty.unwrap() {
                     tyenv.report_error(
                         pos,
                         format!(
                             "Constant '{}' has wrong type: expected {}, but is actually {}",
                             tyenv.syms[val.index()],
-                            tyenv.types[ty.index()].name(tyenv),
+                            tyenv.types[ty.unwrap().index()].name(tyenv),
                             tyenv.types[const_ty.index()].name(tyenv)
                         ),
                     );
                     return None;
                 }
-                Some(Expr::ConstPrim(ty, val))
+                Some(Expr::ConstPrim(const_ty, val))
             }
             &ast::Expr::Let {
                 ref defs,
@@ -2043,20 +2124,24 @@ impl TermEnv {
                     };
 
                     // Evaluate the variable's value.
-                    let val = Box::new(unwrap_or_continue!(
+                    let val = Box::new(unwrap_or_continue!(self.translate_expr(
-                        self.translate_expr(tyenv, &def.val, tid, bindings)
+                        tyenv,
-                    ));
+                        &def.val,
+                        Some(tid),
+                        bindings,
+                        pure
+                    )));
 
                     // Bind the var with the given type.
                     let id = VarId(bindings.next_var);
                     bindings.next_var += 1;
                     bindings.vars.push(BoundVar { name, id, ty: tid });
 
-                    let_defs.push((id, ty, val));
+                    let_defs.push((id, tid, val));
                 }
 
                 // Evaluate the body, expecting the type of the overall let-expr.
-                let body = Box::new(self.translate_expr(tyenv, body, ty, bindings)?);
+                let body = Box::new(self.translate_expr(tyenv, body, ty, bindings, pure)?);
                 let body_ty = body.ty();
 
                 // Pop the bindings.
@@ -2070,6 +2155,45 @@ impl TermEnv {
             }
         }
     }
+
+    fn translate_iflets(
+        &self,
+        tyenv: &mut TypeEnv,
+        rule_term: TermId,
+        iflets: &[ast::IfLet],
+        bindings: &mut Bindings,
+    ) -> Option<Vec<IfLet>> {
+        let mut translated = vec![];
+        for iflet in iflets {
+            translated.push(unwrap_or_continue!(
+                self.translate_iflet(tyenv, rule_term, iflet, bindings)
+            ));
+        }
+        Some(translated)
+    }
+
+    fn translate_iflet(
+        &self,
+        tyenv: &mut TypeEnv,
+        rule_term: TermId,
+        iflet: &ast::IfLet,
+        bindings: &mut Bindings,
+    ) -> Option<IfLet> {
+        // Translate the expr first. Ensure it's pure.
+        let rhs =
+            self.translate_expr(tyenv, &iflet.expr, None, bindings, /* pure = */ true)?;
+        let ty = rhs.ty();
+        let (lhs, _lhs_ty) = self.translate_pattern(
+            tyenv,
+            rule_term,
+            &iflet.pattern,
+            Some(ty),
+            bindings,
+            /* is_root = */ true,
+        )?;
+
+        Some(IfLet { lhs, rhs })
+    }
 }
 
 #[cfg(test)]