Skip to content

Commit

Permalink
Merge pull request #244 from HigherOrderCO/bug/sc-527/recursion-check…
Browse files Browse the repository at this point in the history
…-incorrectly-displays-some

[sc-527] Recursion check incorrectly displays some generated functions
  • Loading branch information
imaqtkatt authored Mar 25, 2024
2 parents 175a6f6 + 4bdf93e commit a341acc
Show file tree
Hide file tree
Showing 5 changed files with 78 additions and 5 deletions.
37 changes: 34 additions & 3 deletions src/hvmc_net/mutual_recursion.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
use crate::diagnostics::{Diagnostics, WarningType, ERR_INDENT_SIZE};
use crate::{
diagnostics::{Diagnostics, WarningType, ERR_INDENT_SIZE},
term::transform::definition_merge::MERGE_SEPARATOR,
};
use hvmc::ast::{Book, Tree};
use indexmap::{IndexMap, IndexSet};
use std::fmt::Debug;
Expand All @@ -17,17 +20,19 @@ pub fn check_cycles(book: &Book, diagnostics: &mut Diagnostics) -> Result<(), Di
let cycles = graph.cycles();

if !cycles.is_empty() {
let msg = format!(include_str!("mutual_recursion.message"), cycles = show_cycles(&cycles));
let msg = format!(include_str!("mutual_recursion.message"), cycles = show_cycles(cycles));
diagnostics.add_book_warning(msg.as_str(), WarningType::MutualRecursionCycle);
}

diagnostics.fatal(())
}

fn show_cycles(cycles: &[Vec<Ref>]) -> String {
fn show_cycles(mut cycles: Vec<Vec<Ref>>) -> String {
let tail = &format!("\n{:ERR_INDENT_SIZE$}* ...", "");
let tail = if cycles.len() > 5 { tail } else { "" };

cycles = cycles.into_iter().flat_map(combinations_from_merges).collect::<Vec<_>>();

let mut cycles = cycles
.iter()
.take(5)
Expand Down Expand Up @@ -151,3 +156,29 @@ impl Debug for Graph {
write!(f, "Graph{:?}", self.0)
}
}

fn combinations_from_merges(cycle: Vec<Ref>) -> Vec<Vec<Ref>> {
let mut combinations: Vec<Vec<Ref>> = vec![vec![]];
for r#ref in cycle {
if let Some(index) = r#ref.find(MERGE_SEPARATOR) {
let (left, right) = r#ref.split_at(index);
let right = &right[MERGE_SEPARATOR.len() ..]; // skip merge separator
let mut new_combinations = Vec::new();
for combination in &combinations {
let mut left_comb = combination.clone();
left_comb.push(left.to_string());
new_combinations.push(left_comb);

let mut right_comb = combination.clone();
right_comb.push(right.to_string());
new_combinations.push(right_comb);
}
combinations = new_combinations;
} else {
for combination in &mut combinations {
combination.push(r#ref.clone());
}
}
}
combinations
}
4 changes: 3 additions & 1 deletion src/term/transform/definition_merge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ use indexmap::{IndexMap, IndexSet};
use itertools::Itertools;
use std::collections::BTreeMap;

pub const MERGE_SEPARATOR: &str = "_$_";

impl Book {
/// Merges definitions that have the same structure into one definition.
/// Expects variables to be linear.
Expand All @@ -28,7 +30,7 @@ impl Book {

for (term, equal_defs) in equal_terms {
// def1_$_def2_$_def3
let new_name = Name::new(equal_defs.iter().join("_$_"));
let new_name = Name::new(equal_defs.iter().join(MERGE_SEPARATOR));

// Builtin origin takes precedence
let builtin = equal_defs.iter().any(|nam| self.defs[nam].builtin);
Expand Down
4 changes: 3 additions & 1 deletion tests/golden_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -349,7 +349,9 @@ fn mutual_recursion() {
..DiagnosticsConfig::new(Severity::Allow, true)
};
let mut book = do_parse_book(code, path)?;
let res = compile_book(&mut book, CompileOpts::light(), diagnostics_cfg, None)?;
let mut opts = CompileOpts::light();
opts.merge = true;
let res = compile_book(&mut book, opts, diagnostics_cfg, None)?;
Ok(format!("{}{}", res.diagnostics, res.core_book))
})
}
7 changes: 7 additions & 0 deletions tests/golden_tests/mutual_recursion/merged.hvm
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
(X x) = (Rec x)
(Y x) = (Rec x)

(Rec x) = (X x)
(Rec2 x) = (X x)

(Main) = (Y 0)
31 changes: 31 additions & 0 deletions tests/snapshots/mutual_recursion__merged.hvm.snap
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/mutual_recursion/merged.hvm
---
Errors:
Seems like you're trying to run some recursive function(s) on strict-mode.
The following recursive cycles are not compatible with strict-mode the way these functions were written:
* Rec -> X -> Rec
* Rec -> Y -> Rec
* Rec2 -> X -> Rec2
* Rec2 -> Y -> Rec2

Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
If the float-combinators optimization is not on, we recommend activating it.

You have 2 options:

1. Easy Fix: use lazy-mode.

Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.

2. Hard Fix: refactor the program to use lazy references.

When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')

For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')

See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.

0 comments on commit a341acc

Please sign in to comment.