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

Get rid of most generated variables #1679

Merged
merged 21 commits into from
Oct 16, 2023
Merged

Get rid of most generated variables #1679

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
8ad1227
add Closure node to AST
yannham Sep 27, 2023
08a2ba4
Implement non-looping partial eq for Term
yannham Oct 4, 2023
1d105ef
Fix contracts app
yannham Oct 4, 2023
4894518
Use closure within records as well everywhere
yannham Oct 4, 2023
23cbe94
Fix double closurization
yannham Oct 6, 2023
a1d9367
Fix subst to update closurized attrs
yannham Oct 6, 2023
ccc5896
Fix type eq for closures
yannham Oct 6, 2023
ae0784e
More typecheck eq
yannham Oct 6, 2023
5f35327
More work + formatting
yannham Oct 6, 2023
5349d1c
Get rid of share normal form + move Closurize to dedicated mod
yannham Oct 12, 2023
66511de
Accept new snapshots (error msg less noisy)
yannham Oct 12, 2023
c4e7c71
Fix compilation warnings
yannham Oct 13, 2023
44e5e88
Fix various small TODOs left
yannham Oct 13, 2023
6a92fb0
Cleaning comments and debug println
yannham Oct 13, 2023
b0e85d5
Update documentation for new closurize approach
yannham Oct 13, 2023
2b1a00c
Apply suggestions from code review
yannham Oct 16, 2023
eaefc58
Update core/src/closurize.rs
yannham Oct 16, 2023
03be479
Fix various code comments
yannham Oct 16, 2023
d2557aa
Post-rebase fixup
yannham Oct 16, 2023
2870517
Formatting + post-rebase fixup
yannham Oct 16, 2023
8fcc151
Restore array contract dedup fix messed up by rebases
yannham Oct 16, 2023
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
5 changes: 0 additions & 5 deletions cli/tests/snapshot/snapshots/snapshot__eval_stderr_array_at_empty_array.ncl.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,6 @@ error: contract broken by the caller of `at`: invalid array indexing
3 │ std.array.at 0 []
│ -- evaluated to this expression
│
┌─ <unknown> (generated by evaluation):1:1
│
1 │ [ ]
│ ---- evaluated to this value
│
= Can't index into an empty array

note:
Expand Down
5 changes: 0 additions & 5 deletions cli/tests/snapshot/snapshots/snapshot__eval_stderr_array_at_out_of_bound.ncl.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,6 @@ error: contract broken by the caller of `at`: invalid array indexing
3 │ std.array.at 2 [1]
│ --- evaluated to this expression
│
┌─ <unknown> (generated by evaluation):1:1
│
1 │ [ %262 ]
│ -------- evaluated to this value
│
= Expected an array index between 0 and 0 (included), got 2

note:
Expand Down
5 changes: 0 additions & 5 deletions cli/tests/snapshot/snapshots/snapshot__eval_stderr_destructuring_closed_fail.ncl.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,6 @@ error: contract broken by a value: extra field `b`
│ │
│ expected type
│
┌─ <unknown> (generated by evaluation):1:1
│
1 │ { a = 1, b = 2, }
│ ----------------- evaluated to this value
│
= Have you misspelled a field?
= The record contract might also be too strict. By default, record contracts exclude any field which is not listed.
Append `, ..` at the end of the record contract, as in `{some_field | SomeContract, ..}`, to make it accept extra fields.
Expand Down
5 changes: 0 additions & 5 deletions ...ests/snapshot/snapshots/snapshot__eval_stderr_record_forall_constraints_contract.ncl.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,6 @@ error: contract broken by the caller: field not allowed in tail: `x`
│ ------- --------- evaluated to this expression
│ │
│ expected type of the argument provided by the caller
│
┌─ <unknown> (generated by evaluation):1:1
│
1 │ { x = 0, }
│ ---------- evaluated to this value

note:
┌─ [INPUTS_PATH]/errors/record_forall_constraints_contract.ncl:3:58
Expand Down
Loading