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

Add a merge label #1217

Merged
merged 4 commits into from
Apr 2, 2023
Merged

Add a merge label #1217

merged 4 commits into from
Apr 2, 2023

Conversation

yannham
Copy link
Member

@yannham yannham commented Mar 31, 2023

While working toward fixing #1187, I need to have access to a span when generating the contract.Equal application for arrays (indeed, contract labels don't accept a TermPos, but require a RawSpan, ensuring the position is always defined).

One solution was to relax the restriction that contract labels need a raw span, but this property is nice, because it forces the Nickel implementation to always make the effort of propagating position information when handling contracts (case in point: this restriction led to this PR).

Another solution was to apply this constraint to merge as well, and propagate a span through merge operations. That is, passing around something akin to label::Label when merging values, which would store the original position of the merge operation.

Beside #1187, this approach has value in itself: when merging, only the original merge operation hold a defined position, but recursive submerges don't:

{ foo = {bar = 1} } & { foo = {baz = 1}}
# evaluates to
{ foo = {bar = 1} & {baz = 1}}

Here, {bar = 1} & {baz = 1} doesn't have a position, and for a good reason: it actually comes from several locations, {bar = 1}, {baz = 1}, and the original top-level merge as well, but we can't pick one as "the" right inherited position, so we pick none. If an error is raised by merge, we currently can't point to the location of the merge:

nickel> let value1 = {foo.bar = 1} in
let value2 = {foo.bar = 2} in
value1 & value2

error: non mergeable terms
  ┌─ repl-input-0:1:25
  │
1 │ let value1 = {foo.bar = 1} in
  │                         ^ cannot merge this expression
2 │ let value2 = {foo.bar = 2} in
  │                         ^ with this expression
  │
  = Both values have the same merge priority but they can't be combined

Note how the error is non mergeable terms, but there is no merge in sight, because we lose track of it.

Content

This PR introduces a separate label, called MergeLabel, which carries the span of the original merge operation, as well as a MergeKind context. This label is a parameter of the binary op merge (not an actual Nickel parameter, so the operation is still binary, but as a parameter of the enum variant).

This label is threaded through subsequent merges and is used for error reporting.

Examples

Here is the above example after this PR:

nickel> let value1 = {foo.bar = 1} in
let value2 = {foo.bar = 2} in
value1 & value2
error: non mergeable terms
  ┌─ repl-input-0:1:25
  │
1 │ let value1 = {foo.bar = 1} in
  │                         ^ cannot merge this expression
2 │ let value2 = {foo.bar = 2} in
  │                         ^ with this expression
3 │ value1 & value2
  │ --------------- originally merged here
  │
  = Both values have the same merge priority but they can't be combined

Additionally, we also improve the error reporting of merge conflicts when elaborating a piecewise definition. Before, the error message was like:

nickel> {
  foo = {
    bar = 1,
  },
  baz = 2,
  foo.bar = 2,
}
error: non mergeable terms
  ┌─ repl-input-1:3:11
  │
3 │     bar = 1,
  │           ^ cannot merge this expression
  ·
6 │   foo.bar = 2,
  │             ^ with this expression
  │
  = Both values have the same merge priority but they can't be combined

After this PR, it becomes:

nickel> {
  foo = {
    bar = 1,
  },
  baz = 2,
  foo.bar = 2,
}
error: non mergeable terms
  ┌─ repl-input-4:3:11
  │
3 │     bar = 1,
  │           ^ cannot merge this expression
  ·
6 │   foo.bar = 2,
  │   ---       ^ with this expression
  │   │          
  │   when combining the definitions of this field
  │
  = Both values have the same merge priority but they can't be combined

Add a datatype for merge labels, similar to contract labels, but
threaded through merges. It's not used anywhere yet.
Adds a merge label, which has been defined just before, to the merge
operation. This is used to thread error reporting data throughout merges
(currently, only the span of the original merge).

This commit also makes use of this span for reporting incompatible merge
values.
Add a distinction inside MergeLabel to indicate if a merge was
user-written (or descendent of user-written) or if it was generated by
the parser to combine a piecewise definition. In the latter case, the
error message is adapted.
@github-actions github-actions bot temporarily deployed to pull request March 31, 2023 16:47 Inactive
@github-actions github-actions bot temporarily deployed to pull request April 1, 2023 14:17 Inactive
@yannham yannham merged commit 441e69f into master Apr 2, 2023
4 checks passed
@yannham yannham deleted the task/merge-label branch April 2, 2023 13:01
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.

None yet

2 participants