Add mutual recursion check for strict mode

This commit is contained in:
imaqtkatt 2024-03-12 10:10:43 -03:00
parent f79817ce68
commit 4e7c204697
11 changed files with 199 additions and 7 deletions

View File

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

View File

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

View File

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

View File

@ -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 } => {

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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