Call expand_generated for succ_term

src/fun/net_to_term.rs

@@ -19,6 +19,7 @@ pub fn net_to_term(
     net,
     labels,
     book,
+    recursive_defs: &book.recursive_defs(),
     dup_paths: if linear { None } else { Some(Default::default()) },
     scope: Default::default(),
     seen_fans: Default::default(),
@@ -72,6 +73,8 @@ pub struct Reader<'a> {
   seen_fans: Scope,
   seen: HashSet<Port>,
   errors: Vec<ReadbackError>,
+  //
+  recursive_defs: &'a BTreeSet<Name>,
 }
 
 impl Reader<'_> {
@@ -140,6 +143,8 @@ impl Reader<'_> {
 
             let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1)));
             let mut succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2)));
+            // Call expand_generated in case of succ_term be a lifted term
+            succ_term.expand_generated(&self.book, &self.recursive_defs);
 
             // Succ term should be a lambda
             let (zero, succ) = match &mut succ_term {

src/lib.rs

@@ -191,8 +191,8 @@ pub fn readback_hvm_net(
   let mut diags = Diagnostics::default();
   let net = hvm_to_net(net);
   let mut term = net_to_term(&net, book, labels, linear, &mut diags);
-  let recursive_cycles = book.recursive_defs();
-  term.expand_generated(book, &recursive_cycles);
+  let recursive_defs = book.recursive_defs();
+  term.expand_generated(book, &recursive_defs);
   term.resugar_strings(adt_encoding);
   term.resugar_lists(adt_encoding);
   (term, diags)

tests/snapshots/run_file__linearize_match.bend.snap

@@ -3,15 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/linearize_match.bend
 ---
 NumScott:
-Warnings:
-During readback:
-  Encountered an invalid 'switch'.
-
-λa switch a = a { 0: λb b; _: λa λb (+ a b); }
+λa switch a = a { 0: λb b; _: λb (+ a-1 b); }
 
 Scott:
-Warnings:
-During readback:
-  Encountered an invalid 'switch'.
-
-λa switch a = a { 0: λb b; _: λa λb (+ a b); }
+λa switch a = a { 0: λb b; _: λb (+ a-1 b); }

tests/snapshots/run_file__match_mult_linearization.bend.snap

@@ -3,15 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/match_mult_linearization.bend
 ---
 NumScott:
-Warnings:
-During readback:
-  Encountered an invalid 'switch'.
-
-λa switch a = a { 0: λa λb λc (+ (+ a b) c); _: λa λb λc λd (+ (+ (+ a b) c) d); }
+λa switch a = a { 0: λa λb λc (+ (+ a b) c); _: λb λc λd (+ (+ (+ a-1 b) c) d); }
 
 Scott:
-Warnings:
-During readback:
-  Encountered an invalid 'switch'.
-
-λa switch a = a { 0: λa λb λc (+ (+ a b) c); _: λa λb λc λd (+ (+ (+ a b) c) d); }
+λa switch a = a { 0: λa λb λc (+ (+ a b) c); _: λb λc λd (+ (+ (+ a-1 b) c) d); }