Merge pull request #232 from HigherOrderCO/feature/sc-500/add-simple-infinite-expansion-check-to-eagerly

[sc-500] Add mutual recursion cycle check

cspell.json

@@ -36,6 +36,7 @@
     "interner",
     "itertools",
     "lcons",
+    "linearization",
     "linearizes",
     "linearizing",
     "lnet",

docs/lazy-definitions.md

@@ -17,36 +17,46 @@ Nat.add = (Y λaddλaλb match a {
 main = (Nat.add (S (S (S Z))) (S Z))
 ```
 
-Because of that, is recommended to use [supercombinator](https://en.wikipedia.org/wiki/Supercombinator) formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.
+Because of that, its recommended to use a [supercombinator](https://en.wikipedia.org/wiki/Supercombinator) formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.
 
-Supercombinators are simply closed terms. Supercombinator formulation is writing the program as a composition of supercombinators. In this case, `Nat.add` can be a supercombinator.
+The `Nat.add` definition below can be a supercombinator if linearized.
 
 ```rs
-data Nat = Z | (S p)
-
 Nat.add = λaλb match a {
 	Z: b
 	(S p): (S (Nat.add p b))
 }
+```
 
-main = (Nat.add (S (S (S Z))) (S Z))
+```rs
+// Linearized Nat.add
+Nat.add = λa match a {
+	Z: λb b
+	(S p): λb (S (Nat.add p b))
+}
 ```
 
 This code will work as expected, because `Nat.add` is unrolled lazily only when it is used as an argument to a lambda.
 
 ### Automatic optimization
 
-HVM-lang carries out an optimization automatically:
+HVM-lang carries out [match linearization](compiler-options#linearize-matches) and [combinator floating](compiler-options#float-combinators) optimizations, enabled through the CLI, which are active by default in strict mode.
 
 Consider the code below:
+
 ```rs
 Zero = λf λx x
 Succ = λn λf λx (f n)
 ToMachine = λn (n λp (+ 1 (ToMachine p)) 0)
 ```
+
 The lambda terms without free variables are extracted to new definitions.
+
 ```rs
 ToMachine0 = λp (+ 1 (ToMachine p))
 ToMachine = λn (n ToMachine0 0)
 ```
+
 Definitions are lazy in the runtime. Floating lambda terms into new definitions will prevent infinite expansion.
+
+It's important to note that preventing infinite expansion through simple mutual recursion doesn't imply that a program lacks infinite expansion entirely or that it will terminate.

src/hvmc_net/mod.rs

@@ -1 +1,2 @@
+pub mod mutual_recursion;
 pub mod prune;

src/hvmc_net/mutual_recursion.rs

@@ -0,0 +1,143 @@
+use hvmc::ast::{Book, Tree};
+use indexmap::{IndexMap, IndexSet};
+use std::fmt::Debug;
+
+type Ref = String;
+type Stack<T> = Vec<T>;
+type RefSet = IndexSet<Ref>;
+
+#[derive(Default)]
+pub struct Graph(IndexMap<Ref, RefSet>);
+
+pub fn check_cycles(book: &Book) -> Result<(), String> {
+  let graph = Graph::from(book);
+  let cycles = graph.cycles();
+
+  if cycles.is_empty() {
+    Ok(())
+  } else {
+    Err(format!(
+      "{}\n{}\n{}\n{}",
+      "Mutual recursion cycle detected in compiled functions:",
+      pretty_print_cycles(&cycles),
+      "This program will expand infinitely in strict evaluation mode.",
+      "Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information."
+    ))
+  }
+}
+
+fn pretty_print_cycles(cycles: &[Vec<Ref>]) -> String {
+  cycles
+    .iter()
+    .enumerate()
+    .map(|(i, cycle)| {
+      let cycle_str = cycle.iter().chain(cycle.first()).cloned().collect::<Vec<_>>().join(" -> ");
+      format!("Cycle {}: {}", 1 + i, cycle_str)
+    })
+    .collect::<Vec<String>>()
+    .join("\n")
+}
+
+impl Graph {
+  pub fn cycles(&self) -> Vec<Vec<Ref>> {
+    let mut cycles = Vec::new();
+    let mut stack = Stack::new();
+    let mut visited = RefSet::new();
+
+    for r#ref in self.0.keys() {
+      if !visited.contains(r#ref) {
+        self.find_cycles(r#ref, &mut visited, &mut stack, &mut cycles);
+      }
+    }
+
+    cycles
+  }
+
+  fn find_cycles(
+    &self,
+    r#ref: &Ref,
+    visited: &mut RefSet,
+    stack: &mut Stack<Ref>,
+    cycles: &mut Vec<Vec<Ref>>,
+  ) {
+    // Check if the current ref is already in the stack, which indicates a cycle.
+    if let Some(cycle_start) = stack.iter().position(|n| n == r#ref) {
+      // If found, add the cycle to the cycles vector.
+      cycles.push(stack[cycle_start ..].to_vec());
+      return;
+    }
+
+    // If the ref has not been visited yet, mark it as visited.
+    if visited.insert(r#ref.clone()) {
+      // Add the current ref to the stack to keep track of the path.
+      stack.push(r#ref.clone());
+
+      // Get the dependencies of the current ref.
+      if let Some(dependencies) = self.get(r#ref) {
+        // Search for cycles from each dependency.
+        for dep in dependencies {
+          self.find_cycles(dep, visited, stack, cycles);
+        }
+      }
+
+      stack.pop();
+    }
+  }
+}
+
+fn collect_refs(current: Ref, tree: &Tree, graph: &mut Graph) {
+  match tree {
+    Tree::Ref { nam } => graph.add(current, nam.clone()),
+    Tree::Ctr { box lft, rgt, .. } => {
+      if let Tree::Ref { nam } = lft {
+        graph.add(current.clone(), nam.clone());
+      }
+      collect_refs(current, rgt, graph);
+    }
+    Tree::Op { rhs: fst, out: snd, .. } | Tree::Mat { sel: fst, ret: snd } => {
+      collect_refs(current.clone(), fst, graph);
+      collect_refs(current, snd, graph);
+    }
+    Tree::Era | Tree::Num { .. } | Tree::Var { .. } => (),
+  }
+}
+
+impl From<&Book> for Graph {
+  fn from(book: &Book) -> Self {
+    let mut graph = Self::new();
+
+    for (r#ref, net) in book.iter() {
+      // Collect active refs from root.
+      collect_refs(r#ref.clone(), &net.root, &mut graph);
+      for (left, _) in net.redexes.iter() {
+        // If left is an active reference, add to the graph.
+        if let Tree::Ref { nam } = left {
+          graph.add(r#ref.clone(), nam.clone());
+        }
+      }
+    }
+
+    graph
+  }
+}
+
+impl Graph {
+  pub fn new() -> Self {
+    Self::default()
+  }
+
+  pub fn add(&mut self, r#ref: Ref, dependency: Ref) {
+    self.0.entry(r#ref).or_default().insert(dependency.clone());
+    self.0.entry(dependency).or_default();
+  }
+
+  pub fn get(&self, r#ref: &Ref) -> Option<&RefSet> {
+    self.0.get(r#ref)
+  }
+}
+
+impl Debug for Graph {
+  fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+    write!(f, "Graph{:?}", self.0)
+  }
+}

src/lib.rs

@@ -9,7 +9,7 @@ use hvmc::{
   run::{DynNet, Heap, Rewrites},
   stdlib::LogDef,
 };
-use hvmc_net::prune::prune_defs;
+use hvmc_net::{mutual_recursion, prune::prune_defs};
 use net::{hvmc_to_net::hvmc_to_net, net_to_hvmc::nets_to_hvmc};
 use std::{
   str::FromStr,
@@ -82,12 +82,13 @@ pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, adt_encoding: AdtEncodi
 pub fn check_book(book: &mut Book) -> Result<(), Info> {
   // TODO: Do the checks without having to do full compilation
   // TODO: Shouldn't the check mode show warnings?
-  compile_book(book, CompileOpts::light(), None)?;
+  compile_book(book, true, CompileOpts::light(), None)?;
   Ok(())
 }
 
 pub fn compile_book(
   book: &mut Book,
+  lazy_mode: bool,
   opts: CompileOpts,
   args: Option<Vec<Term>>,
 ) -> Result<CompileResult, Info> {
@@ -101,6 +102,9 @@ pub fn compile_book(
   if opts.prune {
     prune_defs(&mut core_book, book.hvmc_entrypoint().to_string());
   }
+  if !lazy_mode {
+    mutual_recursion::check_cycles(&core_book)?;
+  }
   Ok(CompileResult { core_book, labels, warns })
 }
 
@@ -180,7 +184,8 @@ pub fn run_book(
   compile_opts: CompileOpts,
   args: Option<Vec<Term>>,
 ) -> Result<(Term, RunInfo), Info> {
-  let CompileResult { core_book, labels, warns } = compile_book(&mut book, compile_opts, args)?;
+  let CompileResult { core_book, labels, warns } =
+    compile_book(&mut book, run_opts.lazy_mode, compile_opts, args)?;
 
   // Turn the book into an Arc so that we can use it for logging, debugging, etc.
   // from anywhere else in the program

src/main.rs

@@ -199,7 +199,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Info> {
       }
 
       let mut book = load_book(&path)?;
-      let compiled = compile_book(&mut book, opts, None)?;
+      let compiled = compile_book(&mut book, lazy_mode, opts, None)?;
       println!("{}", compiled.display_with_warns(warning_opts)?);
     }
     Mode::Desugar { path, comp_opts, lazy_mode } => {

tests/golden_tests.rs

@@ -119,7 +119,7 @@ fn compile_term() {
 fn compile_file_o_all() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut book = do_parse_book(code, path)?;
-    let compiled = compile_book(&mut book, CompileOpts::heavy(), None)?;
+    let compiled = compile_book(&mut book, true /*ignore check_cycles*/, CompileOpts::heavy(), None)?;
     Ok(format!("{:?}", compiled))
   })
 }
@@ -127,7 +127,7 @@ fn compile_file_o_all() {
 fn compile_file() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut book = do_parse_book(code, path)?;
-    let compiled = compile_book(&mut book, CompileOpts::light(), None)?;
+    let compiled = compile_book(&mut book, true /*ignore check_cycles*/, CompileOpts::light(), None)?;
     Ok(format!("{:?}", compiled))
   })
 }
@@ -301,7 +301,7 @@ fn compile_entrypoint() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut book = do_parse_book(code, path)?;
     book.entrypoint = Some(Name::from("foo"));
-    let compiled = compile_book(&mut book, CompileOpts::light(), None)?;
+    let compiled = compile_book(&mut book, true /*ignore check_cycles*/, CompileOpts::light(), None)?;
     Ok(format!("{:?}", compiled))
   })
 }
@@ -335,3 +335,12 @@ fn cli() {
     Ok(format_output(output))
   })
 }
+
+#[test]
+fn mutual_recursion() {
+  run_golden_test_dir(function_name!(), &|code, path| {
+    let mut book = do_parse_book(code, path)?;
+    let compiled = compile_book(&mut book, false, CompileOpts::light(), None)?;
+    Ok(format!("{:?}", compiled))
+  })
+}

tests/golden_tests/mutual_recursion/a_b_c.hvm

@@ -0,0 +1,5 @@
+(A) = (B)
+(B) = (C)
+(C) = (A)
+
+(Main) = (A)

tests/golden_tests/mutual_recursion/len.hvm

@@ -0,0 +1,4 @@
+(Len []) = 0
+(Len (List.cons _ tail)) = (+ 1 (Len tail))
+
+(Main) = (Len [* * * * * *])

tests/golden_tests/mutual_recursion/multiple.hvm

@@ -0,0 +1,12 @@
+(A) = (B)
+(B) = (C)
+(C) = (A)
+
+(H) = (I)
+(I) = (H)
+
+(N x) = (x (N x))
+
+(M) = (M)
+
+(Main) = *

tests/golden_tests/mutual_recursion/odd_even.hvm

@@ -0,0 +1,9 @@
+data Bool = True | False
+
+(if 0 then else) = else
+(if _ then else) = then
+
+(isOdd  n) = (if (== n 0) False (isEven (- n 1)))
+(isEven n) = (if (== n 0) True  (isOdd  (- n 1)))
+
+(Main) = (isOdd 4)

tests/snapshots/mutual_recursion__a_b_c.hvm.snap

@@ -0,0 +1,8 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/mutual_recursion/a_b_c.hvm
+---
+Mutual recursion cycle detected in compiled functions:
+Cycle 1: A -> B -> C -> A
+This program will expand infinitely in strict evaluation mode.
+Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information.

tests/snapshots/mutual_recursion__len.hvm.snap

@@ -0,0 +1,19 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/mutual_recursion/len.hvm
+---
+@Len = ({2 @Len$S1 {2 #0 a}} a)
+@Len$S0 = {2 a b}
+& #1 ~ <+ c b>
+& @Len ~ (a c)
+@Len$S1 = {2 * @Len$S0}
+@List.cons = (a (b {2 {2 a {2 b c}} {2 * c}}))
+@List.nil = {2 * {2 a a}}
+@main = a
+& @Len ~ (b a)
+& @List.cons ~ (* (c b))
+& @List.cons ~ (* (d c))
+& @List.cons ~ (* (e d))
+& @List.cons ~ (* (f e))
+& @List.cons ~ (* (g f))
+& @List.cons ~ (* (@List.nil g))

tests/snapshots/mutual_recursion__multiple.hvm.snap

@@ -0,0 +1,11 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/mutual_recursion/multiple.hvm
+---
+Mutual recursion cycle detected in compiled functions:
+Cycle 1: A -> B -> C -> A
+Cycle 2: H -> I -> H
+Cycle 3: M -> M
+Cycle 4: N -> N
+This program will expand infinitely in strict evaluation mode.
+Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information.

tests/snapshots/mutual_recursion__odd_even.hvm.snap

@@ -0,0 +1,8 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/mutual_recursion/odd_even.hvm
+---
+Mutual recursion cycle detected in compiled functions:
+Cycle 1: isEven -> isOdd -> isEven
+This program will expand infinitely in strict evaluation mode.
+Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information.