Skip to content

Commit

Permalink
Merge pull request #681 from tweag/rec-let
Browse files Browse the repository at this point in the history
Recursive let
  • Loading branch information
yannham authored Apr 27, 2022
2 parents 6815dbf + f4a15f7 commit c2e378f
Show file tree
Hide file tree
Showing 23 changed files with 222 additions and 65 deletions.
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 {
}
}

/// 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)]
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

0 comments on commit c2e378f

Please sign in to comment.