From 3a6c746fd6bd424b7e5e69ded0972a14f45057da Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Wed, 15 May 2024 12:24:43 +0200 Subject: [PATCH] [sc-684] Disable forwarding of free vars in ask terms --- src/fun/{builtins.hvm => builtins.bend} | 0 src/fun/builtins.rs | 2 +- src/fun/transform/desugar_do_blocks.rs | 14 +++------- .../examples__bitonic_sort.bend.snap | 2 +- .../run_file__recursive_bind.bend.snap | 28 ++++++++++++++++++- 5 files changed, 33 insertions(+), 13 deletions(-) rename src/fun/{builtins.hvm => builtins.bend} (100%) diff --git a/src/fun/builtins.hvm b/src/fun/builtins.bend similarity index 100% rename from src/fun/builtins.hvm rename to src/fun/builtins.bend diff --git a/src/fun/builtins.rs b/src/fun/builtins.rs index f82ea9bc..29f24be1 100644 --- a/src/fun/builtins.rs +++ b/src/fun/builtins.rs @@ -1,7 +1,7 @@ use super::{parser::TermParser, Book, Name, Num, Pattern, Term}; use crate::maybe_grow; -const BUILTINS: &str = include_str!(concat!(env!("CARGO_MANIFEST_DIR"), "/src/fun/builtins.hvm")); +const BUILTINS: &str = include_str!(concat!(env!("CARGO_MANIFEST_DIR"), "/src/fun/builtins.bend")); pub const LIST: &str = "List"; pub const LCONS: &str = "List/cons"; diff --git a/src/fun/transform/desugar_do_blocks.rs b/src/fun/transform/desugar_do_blocks.rs index 5eff4313..46d5036c 100644 --- a/src/fun/transform/desugar_do_blocks.rs +++ b/src/fun/transform/desugar_do_blocks.rs @@ -1,6 +1,6 @@ use crate::{ diagnostics::Diagnostics, - fun::{Ctx, Name, Pattern, Term}, + fun::{Ctx, Name, Term}, maybe_grow, }; use std::collections::HashSet; @@ -41,15 +41,9 @@ impl Term { let fun = make_fun_name(typ); if def_names.contains(&fun) { - let mut fvs = nxt.free_vars(); - pat.binds().flatten().for_each(|bind| _ = fvs.remove(bind)); - let fvs = fvs.into_keys().collect::>(); - let nxt = fvs - .iter() - .fold(*nxt.clone(), |nxt, nam| Term::lam(Pattern::Var(Some(nam.clone())), nxt.clone())); - let nxt = Term::lam(*pat.clone(), nxt); - let term = Term::call(Term::Ref { nam: fun.clone() }, [*val.clone(), nxt]); - *self = Term::call(term, fvs.into_iter().map(|nam| Term::Var { nam })); + // TODO: come up with a strategy for forwarding free vars to prevent infinite recursion. + let nxt = Term::lam(*pat.clone(), std::mem::take(nxt)); + *self = Term::call(Term::Ref { nam: fun.clone() }, [*val.clone(), nxt]); } else { return Err(format!("Could not find definition {} for type {}.", fun, typ)); } diff --git a/tests/snapshots/examples__bitonic_sort.bend.snap b/tests/snapshots/examples__bitonic_sort.bend.snap index 95766bcb..f4de5189 100644 --- a/tests/snapshots/examples__bitonic_sort.bend.snap +++ b/tests/snapshots/examples__bitonic_sort.bend.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: examples/bitonic_sort.bend --- -523776 +16515072 diff --git a/tests/snapshots/run_file__recursive_bind.bend.snap b/tests/snapshots/run_file__recursive_bind.bend.snap index bcfeb884..75419ceb 100644 --- a/tests/snapshots/run_file__recursive_bind.bend.snap +++ b/tests/snapshots/run_file__recursive_bind.bend.snap @@ -2,4 +2,30 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/recursive_bind.bend --- -λa (a 0) +Errors: +The following functions contain recursive cycles incompatible with HVM's strict evaluation: + * Foo -> Foo + +The greedy eager evaluation of HVM may cause infinite loops. +Refactor these functions to use lazy references instead of direct function calls. +A reference is strict when it's being called ('(Foo x)') or when it's used non-linearly ('let x = Foo; (x x)'). +It is lazy when it's an argument ('(x Foo)') or when it's used linearly ('let x = Foo; (x 0)'). + +Try one of these strategies: +- Use pattern matching with 'match', 'fold', and 'bend' to automatically lift expressions to lazy references. +- Replace direct calls with combinators. For example, change: + 'Foo = λa λb (b (λc (Foo a c)) a)' + to: + 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)' + which is lifted to: + 'Foo = λa λb (b Foo__C1 Foo_C2 a)' +- Replace non-linear 'let' expressions with 'use' expressions. For example, change: + 'Foo = λf let x = Foo; (f x x)' + to: + 'Foo = λf use x = Foo; (f x x)' + which inlines to: + 'Foo = λf (f Foo Foo)' +- If disabled, re-enable the default 'float-combinators' and 'linearize-matches' compiler options. + +For more information, visit: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md. +To disable this check, use the "-Arecursion-cycle" compiler option.