Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Recursive let #681

Merged
merged 4 commits into from
Apr 27, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions benches/numeric/fibonacci.ncl
Original file line number Diff line number Diff line change
@@ -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
}
12 changes: 11 additions & 1 deletion doc/manual/syntax.md
Original file line number Diff line number Diff line change
Expand Up @@ -328,7 +328,8 @@ Examples:
```

### Let-In
Let-in allows the binding of an expression. It is used as `let <ident> = <expr> in <expr>`.
Let-in allows the binding of an expression. It is used as `let <rec?> <ident> = <expr> in <expr>`.
The `rec` keyword in Let-in constructs allows the let binding to become recursive, enabling the use of the `<ident>` within the first `<expr>`.

Examples:
```
Expand All @@ -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
Expand Down
3 changes: 0 additions & 3 deletions examples/fibonacci/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

```
Expand Down
10 changes: 3 additions & 7 deletions examples/fibonacci/fibonacci.ncl
Original file line number Diff line number Diff line change
@@ -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
10 changes: 5 additions & 5 deletions lsp/nls/src/linearization/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
Expand Down Expand Up @@ -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(),
Expand Down
15 changes: 15 additions & 0 deletions src/error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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)
}
},
}
}
Expand Down Expand Up @@ -1220,6 +1226,15 @@ impl ToDiagnostic<FileId> 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 `<field>: <type>`."),
String::from("Value assignements, such as `<field> = <expr>`, 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]
Expand Down
20 changes: 13 additions & 7 deletions src/eval/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
},
};

Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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(),
Expand Down Expand Up @@ -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),
Expand Down
7 changes: 4 additions & 3 deletions src/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -166,9 +166,9 @@ UniTerm: UniTerm = {
InfixExpr,
AnnotatedInfixExpr,
AsUniTerm<Forall>,
"let" <pat:Pattern> <meta: Annot<FixedType>?>
"let" <l: @L> <recursive:"rec"?> <r: @R> <pat:Pattern> <meta: Annot<FixedType>?>
"=" <t1: Term>
"in" <t2: Term> => {
"in" <t2: Term> =>? {
let t1 = if let Some(mut meta) = meta {
let pos = t1.pos;
meta.value = Some(t1);
Expand All @@ -178,7 +178,7 @@ UniTerm: UniTerm = {
t1
};

UniTerm::from(mk_term::let_pat(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))?))
},
<l: @L> "fun" <pats: Pattern+> "=>" <t: Term> <r: @R> => {
let pos = mk_pos(src_id, l, r);
Expand Down Expand Up @@ -781,6 +781,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),
Expand Down
3 changes: 3 additions & 0 deletions src/parser/error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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),
}
2 changes: 2 additions & 0 deletions src/parser/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,8 @@ pub enum NormalToken<'input> {
In,
#[token("let")]
Let,
#[token("rec")]
Rec,
#[token("switch")]
Switch,

Expand Down
38 changes: 38 additions & 0 deletions src/parser/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -314,6 +317,41 @@ pub fn mk_label(types: Types, src_id: FileId, l: usize, r: usize) -> Label {
}
}

ErinvanderVeen marked this conversation as resolved.
Show resolved Hide resolved
/// 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<Ident>,
pat: Destruct,
t1: RichTerm,
t2: RichTerm,
span: RawSpan,
) -> Result<RichTerm, ParseError> {
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
Expand Down
52 changes: 36 additions & 16 deletions src/term.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<Ident>, Destruct, RichTerm, RichTerm),
Expand Down Expand Up @@ -185,6 +185,15 @@ pub struct RecordAttrs {
pub open: bool,
}

/// The attributes of a let binding.
#[derive(Debug, Default, Eq, PartialEq, Clone)]
ErinvanderVeen marked this conversation as resolved.
Show resolved Hide resolved
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 {
Expand Down Expand Up @@ -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,
)
},
Expand Down Expand Up @@ -1346,13 +1355,35 @@ pub mod make {
Term::Var(v.into()).into()
}

fn let_in_<I, T1, T2>(rec: bool, id: I, t1: T1, t2: T2) -> RichTerm
where
T1: Into<RichTerm>,
T2: Into<RichTerm>,
I: Into<Ident>,
{
let attrs = LetAttrs {
binding_type: BindingType::Normal,
rec,
};
Term::Let(id.into(), t1.into(), t2.into(), attrs).into()
}

pub fn let_in<I, T1, T2>(id: I, t1: T1, t2: T2) -> RichTerm
where
T1: Into<RichTerm>,
T2: Into<RichTerm>,
I: Into<Ident>,
{
Term::Let(id.into(), t1.into(), t2.into(), BindingType::Normal).into()
let_in_(false, id, t1, t2)
}

pub fn let_rec_in<I, T1, T2>(id: I, t1: T1, t2: T2) -> RichTerm
where
T1: Into<RichTerm>,
T2: Into<RichTerm>,
I: Into<Ident>,
{
let_in_(true, id, t1, t2)
}

pub fn let_pat<I, D, T1, T2>(id: Option<I>, pat: D, t1: T1, t2: T2) -> RichTerm
Expand All @@ -1362,18 +1393,7 @@ pub mod make {
D: Into<Destruct>,
I: Into<Ident>,
{
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)]
Expand Down
Loading