Skip to content

Commit

Permalink
Get rid of most generated variables (#1679)
Browse files Browse the repository at this point in the history
* add Closure node to AST

* Implement non-looping partial eq for Term

* Fix contracts app

* Use closure within records as well everywhere

* Fix double closurization

* Fix subst to update closurized attrs

* Fix type eq for closures

* More typecheck eq

* More work + formatting

* Get rid of share normal form + move Closurize to dedicated mod

* Accept new snapshots (error msg less noisy)

* Fix compilation warnings

* Fix various small TODOs left

* Cleaning comments and debug println

* Update documentation for new closurize approach

* Apply suggestions from code review

Co-authored-by: jneem <joeneeman@gmail.com>

* Update core/src/closurize.rs

Co-authored-by: jneem <joeneeman@gmail.com>

* Fix various code comments

* Post-rebase fixup

* Formatting + post-rebase fixup

* Restore array contract dedup fix messed up by rebases

---------

Co-authored-by: jneem <joeneeman@gmail.com>
  • Loading branch information
yannham and jneem authored Oct 16, 2023
1 parent 859293a commit 2a727ba
Show file tree
Hide file tree
Showing 27 changed files with 999 additions and 998 deletions.
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
3std.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
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
3std.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
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
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

0 comments on commit 2a727ba

Please sign in to comment.