From 7c2b5573739a4734fb3c73c1ab08723a6a96b72e Mon Sep 17 00:00:00 2001 From: Erin van der Veen Date: Wed, 6 Apr 2022 14:08:26 +0200 Subject: [PATCH 1/4] Parse rec keyword after let --- src/grammar.lalrpop | 7 +++++-- src/parser/lexer.rs | 2 ++ src/term.rs | 2 +- tests/contracts_fail.rs | 2 +- tests/pass/contracts.ncl | 2 +- 5 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop index 8730a2dfc7..8b6ffea9c9 100644 --- a/src/grammar.lalrpop +++ b/src/grammar.lalrpop @@ -166,7 +166,7 @@ UniTerm: UniTerm = { InfixExpr, AnnotatedInfixExpr, AsUniTerm, - "let" ?> + "let" ?> "=" "in" => { let t1 = if let Some(mut meta) = meta { @@ -178,7 +178,9 @@ UniTerm: UniTerm = { t1 }; - UniTerm::from(mk_term::let_pat(pat.0, pat.1, t1, t2)) + let is_rec = recursive.is_some(); + + UniTerm::from(mk_term::let_pat(is_rec, pat.0, pat.1, t1, t2)) }, "fun" "=>" => { let pos = mk_pos(src_id, l, r); @@ -781,6 +783,7 @@ extern { "forall" => Token::Normal(NormalToken::Forall), "in" => Token::Normal(NormalToken::In), "let" => Token::Normal(NormalToken::Let), + "rec" => Token::Normal(NormalToken::Rec), "switch" => Token::Normal(NormalToken::Switch), "null" => Token::Normal(NormalToken::Null), diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs index 704d6f29ba..54a9ef2d7e 100644 --- a/src/parser/lexer.rs +++ b/src/parser/lexer.rs @@ -68,6 +68,8 @@ pub enum NormalToken<'input> { In, #[token("let")] Let, + #[token("rec")] + Rec, #[token("switch")] Switch, diff --git a/src/term.rs b/src/term.rs index f683bd1d4d..2f921580dd 100644 --- a/src/term.rs +++ b/src/term.rs @@ -1355,7 +1355,7 @@ pub mod make { Term::Let(id.into(), t1.into(), t2.into(), BindingType::Normal).into() } - pub fn let_pat(id: Option, pat: D, t1: T1, t2: T2) -> RichTerm + pub fn let_pat(rec: bool, id: Option, pat: D, t1: T1, t2: T2) -> RichTerm where T1: Into, T2: Into, diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs index a435eb19b8..39d97a5f04 100644 --- a/tests/contracts_fail.rs +++ b/tests/contracts_fail.rs @@ -127,7 +127,7 @@ fn records_contracts_poly() { (forall b. {a: Num, b: Num ; b} -> { a: Num ; b}) -> {a: Num ; a} -> { ; a} - = fun f rec => %record_remove% \"b\" (%record_remove% \"a\" (f rec)) in + = fun f r => %record_remove% \"b\" (%record_remove% \"a\" (f r)) in f (fun x => x) {a = 1, b = true, c = 3}" ); } diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl index a459965357..2cbab5c795 100644 --- a/tests/pass/contracts.ncl +++ b/tests/pass/contracts.ncl @@ -81,7 +81,7 @@ let Assert = fun l x => x || %blame% l in (remove (extend {}) == {} | Assert) && (extend (remove {foo = 2}) == {foo =1} | Assert) && (let f | forall a b. {f: a -> a, arg: a ; b} -> a = - fun rec => rec.f (rec.arg) in + fun r => r.f (r.arg) in f { f = fun x => x ++ " suffix", arg = "foo" } == "foo suffix" | Assert) From 686d87643fd9770201c337baa7b51830e947e31e Mon Sep 17 00:00:00 2001 From: Erin van der Veen Date: Thu, 7 Apr 2022 10:58:12 +0200 Subject: [PATCH 2/4] Implement let rec --- examples/fibonacci/README.md | 3 -- examples/fibonacci/fibonacci.ncl | 10 ++--- lsp/nls/src/linearization/mod.rs | 10 ++--- src/error.rs | 15 +++++++ src/eval/mod.rs | 20 ++++++---- src/grammar.lalrpop | 8 ++-- src/parser/error.rs | 3 ++ src/parser/utils.rs | 38 ++++++++++++++++++ src/term.rs | 54 ++++++++++++++++++-------- src/transform/desugar_destructuring.rs | 10 ++--- src/transform/free_vars.rs | 9 ++++- src/transform/share_normal_form.rs | 23 +++++++++-- src/typecheck/mod.rs | 11 ++++-- 13 files changed, 156 insertions(+), 58 deletions(-) diff --git a/examples/fibonacci/README.md b/examples/fibonacci/README.md index b63e6e0532..13d63a1711 100644 --- a/examples/fibonacci/README.md +++ b/examples/fibonacci/README.md @@ -3,9 +3,6 @@ This is a basic example of a recursive function: fibonnacci. This is the naive, exponential version of fibonacci: don't call it on a big value! -Currently, only record bindings are recursive. To use a recursive function, one -has to use a record. - ## Run ``` diff --git a/examples/fibonacci/fibonacci.ncl b/examples/fibonacci/fibonacci.ncl index 8c6644e25d..6cfc9c64b2 100644 --- a/examples/fibonacci/fibonacci.ncl +++ b/examples/fibonacci/fibonacci.ncl @@ -1,15 +1,11 @@ -# Currently, only record bindings are recursive. To use a recursive function, -# one has to use a record. - # This is the naive, exponential version of fibonacci: don't call it on a big # value! -let fibonacci = { - f = fun n => +let rec fibonacci = fun n => if n == 0 then 0 else if n == 1 then 1 else - f (n - 1) + f (n - 2) -}.f in + fibonacci (n - 1) + fibonacci (n - 2) +in fibonacci 10 diff --git a/lsp/nls/src/linearization/mod.rs b/lsp/nls/src/linearization/mod.rs index 8a59c57c84..3d73ce83ea 100644 --- a/lsp/nls/src/linearization/mod.rs +++ b/lsp/nls/src/linearization/mod.rs @@ -161,11 +161,11 @@ impl Linearizer for AnalysisHost { Term::LetPattern(ident, destruct, ..) | Term::FunPattern(ident, destruct, _) => { if let Some(ident) = ident { let value_ptr = match term { - Term::LetPattern(_, _, _, _) => { + Term::LetPattern(..) => { self.let_binding = Some(id); ValueState::Unknown } - Term::FunPattern(_, _, _) => { + Term::FunPattern(..) => { // stub object lin.push(LinearizationItem { id: id_gen.get_and_advance(), @@ -218,13 +218,13 @@ impl Linearizer for AnalysisHost { }); } } - Term::Let(ident, _, _, _) | Term::Fun(ident, _) => { + Term::Let(ident, ..) | Term::Fun(ident, ..) => { let value_ptr = match term { - Term::Let(_, _, _, _) => { + Term::Let(..) => { self.let_binding = Some(id); ValueState::Unknown } - Term::Fun(_, _) => { + Term::Fun(..) => { // stub object lin.push(LinearizationItem { id: id_gen.get_and_advance(), diff --git a/src/error.rs b/src/error.rs index 4d2265ee0a..642ec38636 100644 --- a/src/error.rs +++ b/src/error.rs @@ -306,6 +306,9 @@ pub enum ParseError { RawSpan, /* tail position */ RawSpan, /* whole record position */ ), + /// A recursive let pattern was encountered. They are not currently supported because we + /// decided it was too involved to implement them. + RecursiveLetPattern(RawSpan), } /// An error occurring during the resolution of an import. @@ -462,6 +465,9 @@ impl ParseError { InternalParseError::InvalidUniRecord(illegal_pos, tail_pos, pos) => { ParseError::InvalidUniRecord(illegal_pos, tail_pos, pos) } + InternalParseError::RecursiveLetPattern(pos) => { + ParseError::RecursiveLetPattern(pos) + } }, } } @@ -1220,6 +1226,15 @@ impl ToDiagnostic for ParseError { String::from("Using a polymorphic tail in a record `{ ..; a}` requires the rest of the record to be only composed of type annotations, of the form `: `."), String::from("Value assignements, such as ` = `, metadata, etc. are forbidden."), ]), + ParseError::RecursiveLetPattern(span) => Diagnostic::error() + .with_message(format!("recursive destructuring is not supported")) + .with_labels(vec![ + primary(span), + ]) + .with_notes(vec![ + String::from("A destructuring let-binding can't be recursive. Try removing the `rec` from `let rec`."), + String::from("Note: you can reference other fields of a record recursively from within a field, so you might not need the recursive let."), + ]), }; vec![diagnostic] diff --git a/src/eval/mod.rs b/src/eval/mod.rs index 1a39286135..3d0a9d6f32 100644 --- a/src/eval/mod.rs +++ b/src/eval/mod.rs @@ -95,8 +95,8 @@ use crate::{ identifier::Ident, match_sharedterm, mk_app, term::{ - make as mk_term, BinaryOp, BindingType, MetaValue, RichTerm, SharedTerm, StrChunk, Term, - UnaryOp, + make as mk_term, BinaryOp, BindingType, LetAttrs, MetaValue, RichTerm, SharedTerm, + StrChunk, Term, UnaryOp, }, }; @@ -225,7 +225,7 @@ where use crate::transform::fresh_var; let var = fresh_var(); - // Desugar to let x = term in deepSeq x x + // Desugar to let x = term in %deep_seq% x x let wrapper = mk_term::let_in( var.clone(), t0, @@ -357,19 +357,25 @@ where env, } } - Term::Let(x, s, t, btype) => { + Term::Let(x, s, t, LetAttrs { binding_type, rec }) => { let closure = Closure { body: s.clone(), env: env.clone(), }; - let thunk = match btype { + let mut thunk = match binding_type { BindingType::Normal => Thunk::new(closure, IdentKind::Let), BindingType::Revertible(deps) => { Thunk::new_rev(closure, IdentKind::Let, deps.clone()) } }; + // Patch the environment with the (x <- closure) binding + if *rec { + let thunk_ = thunk.clone(); + thunk.borrow_mut().env.insert(x.clone(), thunk_); + } + env.insert(x.clone(), thunk); Closure { body: t.clone(), @@ -692,11 +698,11 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT | v @ Term::Enum(_) | v @ Term::Import(_) | v @ Term::ResolvedImport(_) => RichTerm::new(v, pos), - Term::Let(id, t1, t2, btype) => { + Term::Let(id, t1, t2, attrs) => { let t1 = subst_(t1, global_env, env, Cow::Borrowed(bound.as_ref())); let t2 = subst_(t2, global_env, env, bound); - RichTerm::new(Term::Let(id, t1, t2, btype), pos) + RichTerm::new(Term::Let(id, t1, t2, attrs), pos) } p @ Term::LetPattern(..) => panic!("Pattern {:?} has not been transformed before evaluation", p), p @ Term::FunPattern(..) => panic!("Pattern {:?} has not been transformed before evaluation", p), diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop index 8b6ffea9c9..1ffefed365 100644 --- a/src/grammar.lalrpop +++ b/src/grammar.lalrpop @@ -166,9 +166,9 @@ UniTerm: UniTerm = { InfixExpr, AnnotatedInfixExpr, AsUniTerm, - "let" ?> + "let" ?> "=" - "in" => { + "in" =>? { let t1 = if let Some(mut meta) = meta { let pos = t1.pos; meta.value = Some(t1); @@ -178,9 +178,7 @@ UniTerm: UniTerm = { t1 }; - let is_rec = recursive.is_some(); - - UniTerm::from(mk_term::let_pat(is_rec, pat.0, pat.1, t1, t2)) + Ok(UniTerm::from(mk_let(recursive.is_some(), pat.0, pat.1, t1, t2, mk_span(src_id, l, r))?)) }, "fun" "=>" => { let pos = mk_pos(src_id, l, r); diff --git a/src/parser/error.rs b/src/parser/error.rs index a7cd46f4a5..ab79be265a 100644 --- a/src/parser/error.rs +++ b/src/parser/error.rs @@ -33,4 +33,7 @@ pub enum ParseError { RawSpan, /* tail position */ RawSpan, /* whole record position */ ), + /// A recursive let pattern was encountered. They are not currently supported because we + /// decided it was too involved to implement them. + RecursiveLetPattern(RawSpan), } diff --git a/src/parser/utils.rs b/src/parser/utils.rs index 21d09f57bb..3f172bd3ba 100644 --- a/src/parser/utils.rs +++ b/src/parser/utils.rs @@ -7,7 +7,10 @@ use std::rc::Rc; use codespan::FileId; +use super::error::ParseError; + use crate::{ + destruct::Destruct, identifier::Ident, label::Label, mk_app, mk_fun, @@ -314,6 +317,41 @@ pub fn mk_label(types: Types, src_id: FileId, l: usize, r: usize) -> Label { } } +/// Generate a `Let` or a `LetPattern` (depending on `pat` being empty or not) from a the parsing +/// of a let definition. This function fails if the definition has both a non-empty pattern and +/// is recursive (`pat != Destruct::Empty && rec`), because recursive let-patterns are currently +/// not supported. +pub fn mk_let( + rec: bool, + id: Option, + pat: Destruct, + t1: RichTerm, + t2: RichTerm, + span: RawSpan, +) -> Result { + let result = match pat.into() { + d @ (Destruct::Record { .. } | Destruct::Array { .. }) => { + if rec { + return Err(ParseError::RecursiveLetPattern(span)); + } + mk_term::let_pat(id, d, t1, t2) + } + Destruct::Empty => { + if let Some(id) = id { + if rec { + mk_term::let_rec_in(id, t1, t2) + } else { + mk_term::let_in(id, t1, t2) + } + } else { + panic!("unexpected let-binding without pattern or identifier") + } + } + }; + + Ok(result) +} + /// Determine the minimal level of indentation of a multi-line string. /// /// The result is determined by computing the minimum indentation level among all lines, where the diff --git a/src/term.rs b/src/term.rs index 2f921580dd..e3ff97f795 100644 --- a/src/term.rs +++ b/src/term.rs @@ -69,7 +69,7 @@ pub enum Term { /// A let binding. #[serde(skip)] - Let(Ident, RichTerm, RichTerm, BindingType), + Let(Ident, RichTerm, RichTerm, LetAttrs), /// A destructuring let-binding. #[serde(skip)] LetPattern(Option, Destruct, RichTerm, RichTerm), @@ -185,6 +185,15 @@ pub struct RecordAttrs { pub open: bool, } +/// The attributes of a let binding. +#[derive(Debug, Default, Eq, PartialEq, Clone)] +pub struct LetAttrs { + /// The type of a let binding. See the documentation of [`BindingType`]. + pub binding_type: BindingType, + /// A recursive let binding adds its binding to the environment of the expression. + pub rec: bool, +} + impl RecordAttrs { pub fn merge(attrs1: RecordAttrs, attrs2: RecordAttrs) -> RecordAttrs { RecordAttrs { @@ -1002,11 +1011,11 @@ impl RichTerm { pos, ) }, - Term::Let(id, t1, t2, btype) => { + Term::Let(id, t1, t2, attrs) => { let t1 = t1.traverse(f, state, order)?; let t2 = t2.traverse(f, state, order)?; RichTerm::new( - Term::Let(id, t1, t2, btype), + Term::Let(id, t1, t2, attrs), pos, ) }, @@ -1346,34 +1355,45 @@ pub mod make { Term::Var(v.into()).into() } + fn let_in_(rec: bool, id: I, t1: T1, t2: T2) -> RichTerm + where + T1: Into, + T2: Into, + I: Into, + { + let attrs = LetAttrs { + binding_type: BindingType::Normal, + rec, + }; + Term::Let(id.into(), t1.into(), t2.into(), attrs).into() + } + pub fn let_in(id: I, t1: T1, t2: T2) -> RichTerm where T1: Into, T2: Into, I: Into, { - Term::Let(id.into(), t1.into(), t2.into(), BindingType::Normal).into() + let_in_(false, id, t1, t2) } - pub fn let_pat(rec: bool, id: Option, pat: D, t1: T1, t2: T2) -> RichTerm + pub fn let_rec_in(id: I, t1: T1, t2: T2) -> RichTerm + where + T1: Into, + T2: Into, + I: Into, + { + let_in_(true, id, t1, t2) + } + + pub fn let_pat(id: Option, pat: D, t1: T1, t2: T2) -> RichTerm where T1: Into, T2: Into, D: Into, I: Into, { - match pat.into() { - d @ (Destruct::Record { .. } | Destruct::Array { .. }) => { - Term::LetPattern(id.map(|i| i.into()), d, t1.into(), t2.into()).into() - } - Destruct::Empty => { - if let Some(id) = id { - let_in(id, t1, t2) - } else { - Term::Null.into() - } - } - } + Term::LetPattern(id.map(|i| i.into()), pat.into(), t1.into(), t2.into()).into() } #[cfg(test)] diff --git a/src/transform/desugar_destructuring.rs b/src/transform/desugar_destructuring.rs index fef3b6bf1f..4b767f4e8b 100644 --- a/src/transform/desugar_destructuring.rs +++ b/src/transform/desugar_destructuring.rs @@ -34,9 +34,7 @@ use crate::destruct::{Destruct, Match}; use crate::identifier::Ident; use crate::match_sharedterm; use crate::term::make::{op1, op2}; -use crate::term::{ - BinaryOp::DynRemove, BindingType, MetaValue, RichTerm, Term, UnaryOp::StaticAccess, -}; +use crate::term::{BinaryOp::DynRemove, MetaValue, RichTerm, Term, UnaryOp::StaticAccess}; /// Entry point of the patterns desugaring. /// It desugar a `RichTerm` if possible (the term is a let pattern or a function with patterns in @@ -117,7 +115,7 @@ pub fn desugar(rt: RichTerm) -> RichTerm { x.clone(), t_, destruct_term(x.clone(), &pat, bind_open_field(x, &pat, body)), - BindingType::Normal, + Default::default(), ), pos, ) @@ -161,7 +159,7 @@ fn bind_open_field(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm { } }), body, - BindingType::Normal, + Default::default(), ) .into() } @@ -177,7 +175,7 @@ fn destruct_term(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm { id.clone(), op1(StaticAccess(id.clone()), Term::Var(x.clone())), t, - BindingType::Normal, + Default::default(), ), pos, ), diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs index afc5972da5..22248f3c63 100644 --- a/src/transform/free_vars.rs +++ b/src/transform/free_vars.rs @@ -53,10 +53,15 @@ fn collect_free_vars(rt: &mut RichTerm, free_vars: &mut HashSet) { free_vars.extend(fresh); } - Term::Let(id, t1, t2, _) => { + Term::Let(id, t1, t2, attrs) => { let mut fresh = HashSet::new(); - collect_free_vars(t1, free_vars); + if attrs.rec { + collect_free_vars(t1, &mut fresh); + } else { + collect_free_vars(t1, free_vars); + } + collect_free_vars(t2, &mut fresh); fresh.remove(id); diff --git a/src/transform/share_normal_form.rs b/src/transform/share_normal_form.rs index c187687292..dbb3d710e9 100644 --- a/src/transform/share_normal_form.rs +++ b/src/transform/share_normal_form.rs @@ -32,7 +32,7 @@ use crate::{ identifier::Ident, match_sharedterm, position::TermPos, - term::{BindingType, RichTerm, Term}, + term::{BindingType, LetAttrs, RichTerm, Term}, }; use std::{collections::HashSet, rc::Rc}; @@ -165,7 +165,11 @@ pub fn transform_one(rt: RichTerm) -> RichTerm { meta.value .replace(RichTerm::new(Term::Var(fresh_var.clone()), t.pos)); let inner = RichTerm::new(Term::MetaValue(meta), pos); - RichTerm::new(Term::Let(fresh_var, t, inner, BindingType::Normal), pos) + let attrs = LetAttrs { + binding_type: BindingType::Normal, + rec : false, + }; + RichTerm::new(Term::Let(fresh_var, t, inner, attrs), pos) } } else rt } @@ -203,6 +207,19 @@ fn with_bindings( ) -> RichTerm { bindings.into_iter().fold( RichTerm::new(body, pos.into_inherited()), - |acc, (id, t, btype)| RichTerm::new(Term::Let(id, t, acc, btype), pos), + |acc, (id, t, binding_type)| { + RichTerm::new( + Term::Let( + id, + t, + acc, + LetAttrs { + binding_type, + rec: false, + }, + ), + pos, + ) + }, ) } diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs index 5ad80466cc..cf260635ad 100644 --- a/src/typecheck/mod.rs +++ b/src/typecheck/mod.rs @@ -391,8 +391,12 @@ fn type_check_( unify(state, strict, ty, mk_typewrapper::dynamic()) .map_err(|err| err.into_typecheck_err(state, rt.pos)) } - Term::Let(x, re, rt, _) => { + Term::Let(x, re, rt, attrs) => { let ty_let = binding_type(re.as_ref(), &envs, state.table, strict, state.resolver); + if attrs.rec { + envs.insert(x.clone(), ty_let.clone()); + } + linearizer.retype_ident(lin, x, ty_let.clone()); type_check_( state, @@ -404,8 +408,9 @@ fn type_check_( ty_let.clone(), )?; - // TODO move this up once lets are rec - envs.insert(x.clone(), ty_let); + if !attrs.rec { + envs.insert(x.clone(), ty_let); + } type_check_(state, envs, lin, linearizer, strict, rt, ty) } Term::LetPattern(x, pat, re, rt) => { From 6151e2058624d41cb9b2a361980282adb922cfe7 Mon Sep 17 00:00:00 2001 From: Erin van der Veen Date: Wed, 20 Apr 2022 12:15:36 +0200 Subject: [PATCH 3/4] Recursive let tests --- benches/numeric/fibonacci.ncl | 14 +++++++------- tests/free_vars.rs | 16 ++++++++++++++++ tests/pass.rs | 5 +++++ tests/pass/recursive_let.ncl | 7 +++++++ tests/pass/typechecking.ncl | 9 +++++++++ tests/typecheck_fail.rs | 7 +++++++ 6 files changed, 51 insertions(+), 7 deletions(-) create mode 100644 tests/pass/recursive_let.ncl diff --git a/benches/numeric/fibonacci.ncl b/benches/numeric/fibonacci.ncl index 1cc55f6ffc..1971b4bdd8 100644 --- a/benches/numeric/fibonacci.ncl +++ b/benches/numeric/fibonacci.ncl @@ -1,9 +1,9 @@ { - run = { - f = fun n => - if n == 0 || n == 1 then - 1 - else - f (n - 1) + f (n - 2) - }.f + run = + let rec f = fun n => + if n == 0 || n == 1 then + 1 + else + f (n - 1) + f (n - 2) + in f } diff --git a/tests/free_vars.rs b/tests/free_vars.rs index a8d6106948..3066252083 100644 --- a/tests/free_vars.rs +++ b/tests/free_vars.rs @@ -163,3 +163,19 @@ fn nested_records() { HashMap::from([("a", vec!["c"]), ("b", vec!["a", "c"]), ("c", vec!["b"]),]) )); } + +#[test] +fn recursive_let() { + assert!(check_stat_vars( + "{ + a = let rec b = b + a + h in b, + b = let rec a = a + b in f (a + 1) z, + c = let rec foo = b in let rec bar = c in if a.r then [b] else {foo = c} + }", + HashMap::from([ + ("a", vec!["a"]), + ("b", vec!["b"]), + ("c", vec!["a", "b", "c"]) + ]) + )); +} diff --git a/tests/pass.rs b/tests/pass.rs index a2b15a9799..91b51ec9ad 100644 --- a/tests/pass.rs +++ b/tests/pass.rs @@ -117,3 +117,8 @@ fn importing() { fn overriding() { check_file("overriding.ncl"); } + +#[test] +fn recursive_let() { + check_file("recursive_let.ncl"); +} diff --git a/tests/pass/recursive_let.ncl b/tests/pass/recursive_let.ncl new file mode 100644 index 0000000000..1cb46f4e91 --- /dev/null +++ b/tests/pass/recursive_let.ncl @@ -0,0 +1,7 @@ +let Assert = fun l x => x || %blame% l in + +[ + let rec f = fun n => if n == 0 then n else f (n - 1) in f 10 == 0, + let rec fib = fun n => if n == 0 || n == 1 then 1 else fib (n - 1) + fib (n - 2) in fib 5 == 8, +] +|> array.foldl (fun x y => (x | Assert) && y) true diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl index 12b8aa0d34..9ffe18a8a0 100644 --- a/tests/pass/typechecking.ncl +++ b/tests/pass/typechecking.ncl @@ -74,6 +74,15 @@ let typecheck = [ fun x => switch {`blo => `bla, `ble => `bli, _ => `bla} x in f `bli, + # recursive let bindings + let rec f : forall a. a -> Num -> a = fun x n => + if n == 0 then x else if f "0" n == "1" then f x (n - 1) else f x (f 1 n) in + (f "0" 2 : Str), + let rec f : Num -> Num = fun x => if x == 0 then x else f (x - 1) in + (f 10 : Num), + let rec repeat : forall a. Num -> a -> Array a = fun n x => + if n <= 0 then [] else repeat (n - 1) x @ [x] in (repeat 3 "foo" : Array Str), + # static records ({bla = 1} : {bla : Num}), ({blo = true, bla = 1} : {bla : Num, blo : Bool}), diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs index 165e633f9f..08c62f3442 100644 --- a/tests/typecheck_fail.rs +++ b/tests/typecheck_fail.rs @@ -230,3 +230,10 @@ fn piecewise_signature() { Err(TypecheckError::TypeMismatch(..)) ); } +#[test] +fn recursive_let() { + assert_matches!( + type_check_expr("let rec f : Num -> Num = fun x => f \"hoi\" in null"), + Err(TypecheckError::TypeMismatch(..)) + ); +} From f4a15f738bb35685539920aca00f88d1e240bece Mon Sep 17 00:00:00 2001 From: Erin van der Veen Date: Wed, 20 Apr 2022 13:04:40 +0200 Subject: [PATCH 4/4] Update manual section on let to include rec --- doc/manual/syntax.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/doc/manual/syntax.md b/doc/manual/syntax.md index 8e747f1cc4..96a3b749fb 100644 --- a/doc/manual/syntax.md +++ b/doc/manual/syntax.md @@ -328,7 +328,8 @@ Examples: ``` ### Let-In -Let-in allows the binding of an expression. It is used as `let = in `. +Let-in allows the binding of an expression. It is used as `let = in `. +The `rec` keyword in Let-in constructs allows the let binding to become recursive, enabling the use of the `` within the first ``. Examples: ``` @@ -340,6 +341,15 @@ true > let a = 1 in let b = 2 in a + b 3 + +> let rec f = fun n => if n == 0 then n else n + f (n - 1) in f 10 +55 + +> let rec fib = fun n => if n <= 2 then 1 else fib (n - 1) + fib (n - 2) in fib 9 +34 + +> let rec repeat = fun n x => if n <= 0 then [] else repeat (n - 1) x @ [x] in repeat 3 "foo" +["foo", "foo", "foo"] ``` ## Functions