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.

Sign up for GitHub

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

Jump to bottom

Non-recursive definitions #3138

Merged
merged 9 commits into from
Nov 4, 2024
Merged

Non-recursive definitions #3138

merged 9 commits into from
Nov 4, 2024

Conversation

lukaszcz
Copy link
Collaborator

@lukaszcz lukaszcz commented Oct 31, 2024 •
edited
Loading

  • Closes Handling of record field names is inconsistent: different for record creation and record update #2968
  • Implements detection of function-like definitions, which either:
    • have some arguments on the left of :, or
    • have at least one clause.
  • Only function-like definitions are recursive.
  • Non-recursive definitions are not mutually recursive either, and can be used only after their definition. This necessitates rearranging some definitions in existing Juvix code.
  • Changes the scoping of identifiers in record updates. Now field names on the right side don't refer to the old values of the record fields but to identifiers in scope defined outside the record update. To refer to old values, one needs to explicitly use record projections, e.g.
r@Rec{x := Rec.x r}

@lukaszcz lukaszcz added enhancement New feature or request parsing syntax labels Oct 31, 2024
@lukaszcz lukaszcz added this to the 0.6.7 milestone Oct 31, 2024
@lukaszcz lukaszcz self-assigned this Oct 31, 2024
@lukaszcz lukaszcz mentioned this pull request Nov 4, 2024
Merged
@lukaszcz lukaszcz mentioned this pull request Nov 4, 2024
Merged
@lukaszcz lukaszcz marked this pull request as ready for review November 4, 2024 12:14
@lukaszcz lukaszcz requested review from janmasrovira and paulcadman and removed request for janmasrovira November 4, 2024 12:14
janmasrovira
janmasrovira previously approved these changes Nov 4, 2024
View reviewed changes
@lukaszcz lukaszcz requested a review from janmasrovira November 4, 2024 15:03
@lukaszcz lukaszcz merged commit a1037be into main Nov 4, 2024
4 checks passed
@lukaszcz lukaszcz deleted the record-fields branch November 4, 2024 15:31
janmasrovira pushed a commit that referenced this pull request Nov 4, 2024
@lukaszcz @janmasrovira
Non-recursive definitions (#3138)
3030196 
* Closes #2968 
* Implements detection of function-like definitions, which either:
  - have some arguments on the left of `:`, or
  - have at least one clause.
* Only function-like definitions are recursive.
* Non-recursive definitions are not mutually recursive either, and can
be used only after their definition. This necessitates rearranging some
definitions in existing Juvix code.
* Changes the scoping of identifiers in record updates. Now field names
on the right side don't refer to the old values of the record fields but
to identifiers in scope defined outside the record update. To refer to
old values, one needs to explicitly use record projections, e.g.
```
r@Rec{x := Rec.x r}
```
janmasrovira pushed a commit that referenced this pull request Nov 4, 2024
@lukaszcz @janmasrovira
Non-recursive definitions (#3138)
84786a2 
* Closes #2968 
* Implements detection of function-like definitions, which either:
  - have some arguments on the left of `:`, or
  - have at least one clause.
* Only function-like definitions are recursive.
* Non-recursive definitions are not mutually recursive either, and can
be used only after their definition. This necessitates rearranging some
definitions in existing Juvix code.
* Changes the scoping of identifiers in record updates. Now field names
on the right side don't refer to the old values of the record fields but
to identifiers in scope defined outside the record update. To refer to
old values, one needs to explicitly use record projections, e.g.
```
r@Rec{x := Rec.x r}
```
janmasrovira pushed a commit that referenced this pull request Nov 4, 2024
@lukaszcz @janmasrovira
Non-recursive definitions (#3138)
ff7dc6d 
* Closes #2968 
* Implements detection of function-like definitions, which either:
  - have some arguments on the left of `:`, or
  - have at least one clause.
* Only function-like definitions are recursive.
* Non-recursive definitions are not mutually recursive either, and can
be used only after their definition. This necessitates rearranging some
definitions in existing Juvix code.
* Changes the scoping of identifiers in record updates. Now field names
on the right side don't refer to the old values of the record fields but
to identifiers in scope defined outside the record update. To refer to
old values, one needs to explicitly use record projections, e.g.
```
r@Rec{x := Rec.x r}
```
@lukaszcz lukaszcz mentioned this pull request Nov 5, 2024
Closed
paulcadman added a commit to anoma/juvix-arm-specs that referenced this pull request Nov 5, 2024
@paulcadman
Update juvix-stdlib dependency
1f5be35 
After the Juvix record update syntax change the Juvix stdlib must be
updated.

anoma/juvix#3138
@paulcadman paulcadman mentioned this pull request Nov 5, 2024
Merged
heueristik pushed a commit to anoma/juvix-arm-specs that referenced this pull request Nov 5, 2024
@paulcadman
chore: update juvix-stdlib dependency (#24)
94af3f3 
After the Juvix record update syntax change the Juvix stdlib must be
updated.

anoma/juvix#3138
@lukaszcz lukaszcz mentioned this pull request Nov 6, 2024
Closed
paulcadman pushed a commit to anoma/juvix-stdlib that referenced this pull request Nov 6, 2024
@lukaszcz
Record updates new syntax (#134)
0080b11 
* Adapts to anoma/juvix#3138
@lukaszcz lukaszcz mentioned this pull request Nov 29, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@janmasrovira janmasrovira janmasrovira approved these changes

@paulcadman paulcadman Awaiting requested review from paulcadman

Assignees

@lukaszcz lukaszcz

Labels
enhancement New feature or request parsing syntax
Projects
None yet
Milestone
0.6.7
Development

Successfully merging this pull request may close these issues.

Handling of record field names is inconsistent: different for record creation and record update
2 participants
@lukaszcz @janmasrovira