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

Implementing let blocks, adding non-regression test #504

Closed
wants to merge 2 commits into from

Conversation

litchipi
Copy link
Contributor

@litchipi litchipi commented Dec 13, 2021

Implementation of let blocks in the form:

let foo = 3,
    bar : Num = 2,
    message = "Hello World",
    f = fun x => x,
    f2 : Num -> Bool = fun x => x == 2,
in

Adds a new node LetBlock in the AST that basically mimic all actions from simple Let term, simply looping through all the definitions and adding them to the environment before passing the environment to the final term.

Made for feature request #494
Waiting for PR #502 and #470 to be merged.
Requesting reviews on the regression test to be sure to cover edge cases.

Copy link
Member

@yannham yannham left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The overall changes look reasonable (it misses the grammar but I imagine it's because it's still draft), but this doesn't implement the semantics of #494 that states let-blocks should be mutually recursive, as for record, and not just equivalent to a series of simple lets. See the corresponding comments.

Also, tagging @ysndr as this may need additional support in the LSP.

src/eval.rs Show resolved Hide resolved
src/eval.rs Outdated
Term::LetBlock(defs, rest) => {
let mut data = vec![];
for (id, term) in defs.iter() {
data.push((id.clone(), subst_(term.clone(), global_env, env, Cow::Borrowed(bound.as_ref()))));
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same remark about cloning.

src/parser/utils.rs Outdated Show resolved Hide resolved
src/term.rs Outdated Show resolved Hide resolved
let ty_let = binding_type(term.as_ref(), &mut env, global, state.table, strict);
type_check_(state, global, lin, linearizer.scope(ScopeId::Left), strict, term, Closure::new(ty_let.clone(), env.clone()))?;
env.insert(id.clone(), Closure::new(ty_let, env.clone()));
}
Copy link
Member

@yannham yannham Dec 13, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same thing as with evaluation, you need to typecheck this in a recursive environment. You can look at the RecRecord case to see how to do it. We may even separate this typechecking of mutually recursive bindings in a separate helper as I expect the code to be almost the same for let blocks and recursive records.

Signed-off-by: Litchi Pi <litchi.pi@protonmail.com>
@litchipi litchipi force-pushed the timcer/block_let branch 2 times, most recently from 5d21c40 to e42ce33 Compare December 13, 2021 13:26
@github-actions github-actions bot temporarily deployed to pull request December 13, 2021 13:34 Inactive
Signed-off-by: Litchi Pi <litchi.pi@protonmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants