Merge pull request #148 from HigherOrderCO/fix-linearization-unscoped

Fix linearization of unscoped vars in adt matches

src/term/mod.rs

@@ -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);

src/term/net_to_term.rs

@@ -392,7 +392,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() },
   };
 

src/term/transform/desugar_match_expressions.rs

@@ -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

src/term/transform/linearize.rs

@@ -251,7 +251,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() {

tests/golden_tests/encode_pattern_match/match_adt_unscoped_in_arm.hvm

@@ -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
+}

tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap

@@ -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