Fix linearization of unscoped vars in adt matches

This commit is contained in:
Nicolas Abril 2024-01-24 18:16:10 +01:00
parent 9cd2bac3d0
commit 8f780f1b28
6 changed files with 32 additions and 5 deletions

View File

@ -503,7 +503,7 @@ impl Term {
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
go(fst, decls, uses);
go(snd, uses, decls);
go(snd, decls, uses);
}
Term::Lam { bod, .. } => {
go(bod, decls, uses);

View File

@ -387,7 +387,7 @@ fn insert_string_cons(app: &mut Term, term: Term) {
fn string_app(val: &str, arg: Term) -> Term {
let str_term = match val.len() {
0 => return arg,
1 => Term::Num { val: val.chars().nth(0).unwrap().try_into().unwrap() },
1 => Term::Num { val: val.chars().next().unwrap().try_into().unwrap() },
_ => Term::Str { val: val.to_owned() },
};

View File

@ -414,10 +414,11 @@ fn linearize_match_unscoped_vars(match_term: &mut Term) -> Result<&mut Term, Mat
return Err(MatchError::Linearize(Name(format!("λ${var}"))));
}
// Change unscoped var to normal scoped var if it references something outside this match arm.
for var in uses.difference(&decls) {
let arm_free_vars = uses.difference(&decls);
for var in arm_free_vars.clone() {
arm.subst_unscoped(var, &Term::Var { nam: Name(format!("%match%unscoped%{var}")) });
}
free_vars.extend(uses);
free_vars.extend(arm_free_vars.cloned());
}
// Add lambdas to the arms

View File

@ -276,7 +276,7 @@ fn make_dup_tree(nam: &Name, nxt: &mut Term, uses: Val, mut dup_body: Option<&mu
let make_name = |uses| {
let dup_name = dup_name(nam, uses);
free_vars.contains_key(&dup_name).then(|| dup_name)
free_vars.contains_key(&dup_name).then_some(dup_name)
};
for i in (1 .. uses).rev() {

View File

@ -0,0 +1,7 @@
// Test that we don't mess up with that unscoped lambda/var
data bool = T | F
main = @x match x {
T: @$x $x
F: @x x
}

View File

@ -0,0 +1,19 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_in_arm.hvm
---
(main) = λx (main$match$1 x)
(T) = #bool λT #bool λF T
(F) = #bool λT #bool λF F
(main$match$1) = λx #bool (x main$match$1$PT main$match$1$PF)
(main$match$1$R0) = λ$x $x
(main$match$1$R1) = λx x
(main$match$1$PT) = main$match$1$R0
(main$match$1$PF) = main$match$1$R1