Add mutual recursion check for strict mode

src/hvmc_net/mod.rs

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

src/hvmc_net/mutual_recursion.rs

@@ -0,0 +1,130 @@
+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(pprint_cycles(&cycles)) }
+}
+
+fn pprint_cycles(cycles: &[Vec<Ref>]) -> String {
+  cycles
+    .iter()
+    .enumerate()
+    .map(|(i, cycles)| format!("Cycle {}: {}", 1 + i, cycles.join(" -> ")))
+    .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_insert_with(RefSet::new).insert(dependency.clone());
+    self.0.entry(dependency).or_insert_with(RefSet::new);
+  }
+
+  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,15 +119,15 @@ 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))
   })
 }
 #[test]
 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/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,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/mutual_recursion/a_b_c.hvm
+---
+Cycle 1: A -> B -> C

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__odd_even.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/mutual_recursion/odd_even.hvm
+---
+Cycle 1: isEven -> isOdd