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

Support for trait clause bounds #11

Merged
merged 69 commits into from
Jun 3, 2024
Merged

Support for trait clause bounds #11

Show file tree
Hide file tree
Changes from 17 commits
Commits
Show all changes
69 commits
Select commit Hold shift + click to select a range
bfd890c
Checkpoint
protz May 10, 2024
d7d40e5
More regularity in the binding structure.
protz May 13, 2024
5bced73
WIP: extend binding logic to handle clause method binders
protz May 13, 2024
559fde5
Implement dictionary-passing style. Numerous tiny refactors
protz May 13, 2024
7ebcee7
WIP: passing trait method impls at call-site
protz May 15, 2024
5df6d8a
It translates, but does not type-check
protz May 15, 2024
037b789
Fix code-gen of opaque function signatures to receive trait implement…
protz May 15, 2024
97d84f9
Down to two errors on the minimal example
protz May 15, 2024
5323c3d
Fix silly copy-paste
protz May 15, 2024
9caf19f
Refactor -- lookup_fun was not taking into account trait clauses
protz May 15, 2024
0e382ac
Simple test case works!
protz May 15, 2024
872024a
Avoid silly issue for now
protz May 15, 2024
ed12caa
Minor refactoring to avoid duplicating signature type computation logic
protz May 18, 2024
2776c37
Cleanup + bugfix
protz May 18, 2024
633ad43
Comments, refactor, add a blocklist for trait methods that are handle…
protz May 18, 2024
a7f1bfe
Fix some matching logic, comments about things that should be handled…
protz May 18, 2024
1d26324
One last bug and one more blocklist entry, and now old Kyber works
protz May 18, 2024
7d91be1
Fix comments
msprotz May 20, 2024
01435a8
Merge remote-tracking branch 'refs/remotes/origin/protz_trait_clauses…
msprotz May 20, 2024
0db1baa
WIP
protz May 20, 2024
7a3c021
Support for parent clauses. Fix substitutions that were inside-out in…
msprotz May 21, 2024
efecc6e
Proper support for string literals
msprotz May 21, 2024
5fd335d
Merge branch 'protz_trait_clauses' of pro.github.com:aeneasverif/eury…
msprotz May 21, 2024
89b6ee3
Better testcase, wip
msprotz May 22, 2024
38a23b1
Trait impls that do not feature the trait decl's const generics shoul…
msprotz May 22, 2024
6e85f4e
WIP trying to bring everything in alignment
msprotz May 22, 2024
1af3af6
Different substitution strategy
msprotz May 22, 2024
9c49a5b
nix voodoo
msprotz May 22, 2024
48c6527
WIP, relying on krml changes
msprotz May 22, 2024
aa633ca
Down to a single error
msprotz May 22, 2024
c9f0ac0
Passes first round of type-checking
msprotz May 22, 2024
cfbfb3d
Fix post-monomorphization casts
msprotz May 23, 2024
bdea3e1
Down to nine errors for mlkem
msprotz May 23, 2024
5b8ca63
snapshot
msprotz May 23, 2024
aadfa2b
Band-aid until a proper fix for higher-rank cg-polymorphism arrives
msprotz May 23, 2024
0157d13
A few test cases related to higher-order cg polymorphism
msprotz May 23, 2024
8e32aa6
Enable tests...
msprotz May 23, 2024
1ee910f
Trigger the substitution issue
msprotz May 23, 2024
4e30dab
Introduce type schemes in all the right places to avoid substitution …
msprotz May 24, 2024
a46b42c
Squash a couple final bugs
msprotz May 24, 2024
297f49a
Forgot to resolve subtituted type application to monomorphized instance
msprotz May 24, 2024
c55d67f
New flag: library
msprotz May 27, 2024
97f8169
WIP: support for relocating monomorphized functions to another file
msprotz May 28, 2024
f5a0a59
WIP extending the config language
msprotz May 28, 2024
a337a9c
More tweaks to the config language, remove an assumption related to d…
msprotz May 28, 2024
0cd41f9
Don't keel over in the presence of Debug attributes -- minimal type-c…
msprotz May 28, 2024
584ee76
A test for the partial eq issue reported by Lucas
msprotz May 28, 2024
31c6888
Resurrect a commit from branch protz_misc and add support for multidi…
msprotz May 28, 2024
d67e413
A tweak for representing closures in the AST (until they are inlined …
msprotz May 29, 2024
93a683e
For now, leaving what I think should be the correct behavior, barring…
msprotz May 29, 2024
bf24c3b
Two good repros (but broken)
msprotz May 29, 2024
d3da56c
Settle on normalizing all 1-uples to avoid discrepancies on the LLBC …
msprotz May 29, 2024
c895ea9
Generalize treatment of array::from_fn to state-capturing closures
msprotz May 29, 2024
19ddd07
This perhaps fixes #13
msprotz May 29, 2024
4fbc12a
A fix for the unit mismatch
msprotz May 29, 2024
62f9d8d
And another topological sort
msprotz May 29, 2024
dbdbc9c
Change the semantics of include to be early; more stubs
msprotz May 29, 2024
443c6a2
Upstream missing definitions
msprotz May 29, 2024
24b384b
Tweaks
msprotz May 29, 2024
7d1f0f0
And another topological sort
msprotz May 30, 2024
749fb6c
update eurydice_glue.h
franziskuskiefer May 30, 2024
c236816
Possibly fix slices
msprotz May 30, 2024
df95260
And enable loop unrolling
msprotz May 30, 2024
545e6af
Almost entirely overhaul config language
msprotz May 31, 2024
25decac
Another complete rewrite of the bundling system to be more precise
msprotz May 31, 2024
6e86974
Bump Terminal version. This fixes #10
msprotz May 31, 2024
cb24adf
Some nix magic
msprotz Jun 3, 2024
b8705ac
Catch up on upstream Charon
msprotz Jun 3, 2024
fcc0213
Allow customizing funroll-loops to work around a silly bug
msprotz Jun 3, 2024
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
Loading
Loading