Browse Source

ISLE: add support for implicit `=x` variable matchers. (#4074)

Currently, a variable can be named in two different ways in an ISLE
pattern. One can write a pattern like `(T x y)` that binds the two
args of `T` with the subpatterns `x` and `y`, each of which match
anything and capture the value as a bound variable. Or, one can write
a pattern like `(T x =x)`, where the first arg pattern `x` captures
the value in `x` and the second arg pattern `=x` matches only the same
value that was already captured.

It turns out (thanks to @fitzgen for this insight here [1]) that this
distinction can actually be inferred easily: if `x` isn't bound, then
mentioning it binds it; otherwise, it matches only the already-bound
variable. There's no concern about ordering (one mention binding
vs. the other) because (i) the value is equal either way, and (ii) the
types at both sites must be the same.

This language tweak seems like it should simplify things nicely! We
can remove the `=x` syntax later if we want, but this PR doesn't do
so.

[1] https://github.com/bytecodealliance/wasmtime/pull/4071#discussion_r859111513
pull/4078/head
Chris Fallin 3 years ago
committed by GitHub
parent
commit
b69fede72f
No known key found for this signature in database GPG Key ID: 4AEE18F83AFDEB23
  1. 7
      cranelift/isle/isle/isle_examples/fail/bound_var_type_mismatch.isle
  2. 6
      cranelift/isle/isle/isle_examples/pass/bound_var.isle
  3. 27
      cranelift/isle/isle/src/ast.rs
  4. 10
      cranelift/isle/isle/src/parser.rs
  5. 55
      cranelift/isle/isle/src/sema.rs

7
cranelift/isle/isle/isle_examples/fail/bound_var_type_mismatch.isle

@ -0,0 +1,7 @@
(type u32 (primitive u32))
(type u64 (primitive u64))
(decl A (u32 u64) u32)
(rule 1 (A x x) x)
(rule 0 (A x _) 0)

6
cranelift/isle/isle/isle_examples/pass/bound_var.isle

@ -0,0 +1,6 @@
(type u32 (primitive u32))
(decl A (u32 u32) u32)
(rule 1 (A x x) x)
(rule 0 (A x _) 0)

27
cranelift/isle/isle/src/ast.rs

@ -93,15 +93,22 @@ pub struct Extractor {
/// A pattern: the left-hand side of a rule.
#[derive(Clone, PartialEq, Eq, Debug)]
pub enum Pattern {
/// An operator that binds a variable to a subterm and match the
/// A mention of a variable.
///
/// Equivalent either to a binding (which can be emulated with
/// `BindPattern` with a `Pattern::Wildcard` subpattern), if this
/// is the first mention of the variable, in order to capture its
/// value; or else a match of the already-captured value. This
/// disambiguation happens when we lower `ast` nodes to `sema`
/// nodes as we resolve bound variable names.
Var { var: Ident, pos: Pos },
/// An operator that binds a variable to a subterm and matches the
/// subpattern.
BindPattern {
var: Ident,
subpat: Box<Pattern>,
pos: Pos,
},
/// A variable that has already been bound (`=x` syntax).
Var { var: Ident, pos: Pos },
/// An operator that matches a constant integer value.
ConstInt { val: i64, pos: Pos },
/// An operator that matches an external constant value.
@ -180,6 +187,13 @@ impl Pattern {
subpat: Box::new(subpat.make_macro_template(macro_args)),
pos,
},
&Pattern::Var { ref var, pos } => {
if let Some(i) = macro_args.iter().position(|arg| arg.0 == var.0) {
Pattern::MacroArg { index: i, pos }
} else {
self.clone()
}
}
&Pattern::And { ref subpats, pos } => {
let subpats = subpats
.iter()
@ -203,10 +217,9 @@ impl Pattern {
}
}
&Pattern::Var { .. }
| &Pattern::Wildcard { .. }
| &Pattern::ConstInt { .. }
| &Pattern::ConstPrim { .. } => self.clone(),
&Pattern::Wildcard { .. } | &Pattern::ConstInt { .. } | &Pattern::ConstPrim { .. } => {
self.clone()
}
&Pattern::MacroArg { .. } => unreachable!(),
}
}

10
cranelift/isle/isle/src/parser.rs

@ -412,6 +412,10 @@ impl<'a> Parser<'a> {
} else if self.is_sym() {
let s = self.symbol()?;
if s.starts_with("=") {
// Deprecated `=x` syntax. This will go away once we
// change all uses to just `x`, which we can do
// because we disambiguate whether a mention of `x` is
// a binding or a matching of the already-bound value.
let s = &s[1..];
let var = self.str_to_ident(pos, s)?;
Ok(Pattern::Var { var, pos })
@ -422,11 +426,7 @@ impl<'a> Parser<'a> {
let subpat = Box::new(self.parse_pattern()?);
Ok(Pattern::BindPattern { var, subpat, pos })
} else {
Ok(Pattern::BindPattern {
var,
subpat: Box::new(Pattern::Wildcard { pos }),
pos,
})
Ok(Pattern::Var { var, pos })
}
}
} else if self.is_lparen() {

55
cranelift/isle/isle/src/sema.rs

@ -1543,36 +1543,51 @@ impl TermEnv {
Some((Pattern::BindPattern(ty, id, Box::new(subpat)), ty))
}
&ast::Pattern::Var { ref var, pos } => {
// Look up the variable; it must already have been bound.
// Look up the variable; if it has already been bound,
// then this becomes a `Var` node (which matches the
// existing bound value), otherwise it becomes a
// `BindPattern` with a wildcard subpattern to capture
// at this location.
let name = tyenv.intern_mut(var);
let bv = match bindings.vars.iter().rev().find(|bv| bv.name == name) {
match bindings.vars.iter().rev().find(|bv| bv.name == name) {
None => {
tyenv.report_error(
pos,
format!(
"Unknown variable '{}' in bound-var pattern '={}'",
var.0, var.0
),
);
return None;
let ty = match expected_ty {
Some(ty) => ty,
None => {
tyenv.report_error(
pos,
format!("Variable pattern '{}' not allowed in context without explicit type", var.0),
);
return None;
}
};
let id = VarId(bindings.next_var);
bindings.next_var += 1;
log::trace!("binding var {:?}", var.0);
bindings.vars.push(BoundVar { name, id, ty });
Some((
Pattern::BindPattern(ty, id, Box::new(Pattern::Wildcard(ty))),
ty,
))
}
Some(bv) => bv,
};
let ty = match expected_ty {
None => bv.ty,
Some(expected_ty) if expected_ty == bv.ty => bv.ty,
Some(expected_ty) => {
tyenv.report_error(
Some(bv) => {
let ty = match expected_ty {
None => bv.ty,
Some(expected_ty) if expected_ty == bv.ty => bv.ty,
Some(expected_ty) => {
tyenv.report_error(
pos,
format!(
"Mismatched types: pattern expects type '{}' but already-bound var '{}' has type '{}'",
tyenv.types[expected_ty.index()].name(tyenv),
var.0,
tyenv.types[bv.ty.index()].name(tyenv)));
bv.ty // Try to keep going for more errors.
bv.ty // Try to keep going for more errors.
}
};
Some((Pattern::Var(ty, bv.id), ty))
}
};
Some((Pattern::Var(ty, bv.id), ty))
}
}
&ast::Pattern::Term {
ref sym,

Loading…
Cancel
Save