ISLE: Allow shadowing in let expressions (#4562)

* Support shadowing in isle

* Re-run the isle build.rs if the examples change

* Print error messages when isle tests fail

* Move run tests

* Refactor `let` uses that don't need to introduce unique names
This commit is contained in:
Trevor Elliott
2022-08-01 14:10:28 -07:00
committed by GitHub
parent 25782b527e
commit 586ec95c11
10 changed files with 153 additions and 86 deletions

View File

@@ -2,6 +2,7 @@ use std::fmt::Write;
fn main() {
println!("cargo:rerun-if-changed=build.rs");
println!("cargo:rerun-if-changed=isle_examples");
let out_dir = std::path::PathBuf::from(
std::env::var_os("OUT_DIR").expect("The OUT_DIR environment variable must be set"),

View File

@@ -0,0 +1,38 @@
(type u64 (primitive u64))
(decl foo (u64) u64)
(rule (foo x) x)
;; Shadowing of a global name
(decl test1 (u64) u64)
(rule (test1 x)
(let ((foo u64 x))
foo))
;; Shadowing of a parameter
(decl test2 (u64) u64)
(rule (test2 x)
(let ((x u64 x))
x))
;; Shadowing of this binding's name
(decl test3 (u64) u64)
(rule (test3 x)
(let ((test3 u64 x))
test3))
;; Shadowing another let-bound name
(decl test4 (u64) u64)
(rule (test4 x)
(let ((val u64 x)
(val u64 23))
val))
;; Shadowing a global with a parameter name
(decl test5 (u64) u64)
(rule (test5 foo) foo)
;; Using a previously shadowed global
(decl test6 (u64) u64)
(rule (test6 x) (foo x))

View File

@@ -0,0 +1,27 @@
mod let_shadowing;
struct Context;
impl let_shadowing::Context for Context {}
fn main() {
let mut ctx = Context;
assert_eq!(Some(20), let_shadowing::constructor_test1(&mut ctx, 20));
assert_eq!(Some(97), let_shadowing::constructor_test1(&mut ctx, 97));
assert_eq!(Some(20), let_shadowing::constructor_test2(&mut ctx, 20));
assert_eq!(Some(97), let_shadowing::constructor_test2(&mut ctx, 97));
assert_eq!(Some(20), let_shadowing::constructor_test3(&mut ctx, 20));
assert_eq!(Some(97), let_shadowing::constructor_test3(&mut ctx, 97));
assert_eq!(Some(23), let_shadowing::constructor_test4(&mut ctx, 20));
assert_eq!(Some(23), let_shadowing::constructor_test4(&mut ctx, 97));
assert_eq!(Some(20), let_shadowing::constructor_test5(&mut ctx, 20));
assert_eq!(Some(97), let_shadowing::constructor_test5(&mut ctx, 97));
assert_eq!(Some(20), let_shadowing::constructor_test6(&mut ctx, 20));
assert_eq!(Some(97), let_shadowing::constructor_test6(&mut ctx, 97));
}

View File

@@ -1951,9 +1951,6 @@ impl TermEnv {
for def in defs {
// Check that the given variable name does not already exist.
let name = tyenv.intern_mut(&def.var);
if bindings.vars.iter().any(|bv| bv.name == name) {
tyenv.report_error(pos, format!("Variable '{}' already bound", def.var.0));
}
// Look up the type.
let tysym = match tyenv.intern(&def.ty) {

View File

@@ -11,11 +11,15 @@ fn build(filename: &str) -> Result<String> {
}
pub fn run_pass(filename: &str) {
assert!(build(filename).is_ok());
if let Err(err) = build(filename) {
panic!("pass test failed:\n{}", err);
}
}
pub fn run_fail(filename: &str) {
assert!(build(filename).is_err());
if build(filename).is_ok() {
panic!("test {} passed unexpectedly", filename);
}
}
fn build_and_link_isle(isle_filename: &str) -> (tempfile::TempDir, std::path::PathBuf) {