-
Notifications
You must be signed in to change notification settings - Fork 58
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
Multiple lookups, simpler rec environment #996
Multiple lookups, simpler rec environment #996
Conversation
587e376
to
e14b268
Compare
e14b268
to
43a4ed2
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The better use of tags is great, I left a question, mostly geared at maintenability.
src/lem/eval.rs
Outdated
// This is a hack to signal that the binding came from a letrec | ||
Expr::Thunk => { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
- How much more expensive would it be to add a proper case in the environment?
- If the answer is "quite a bit", could we document this special meaning in the definition of the
Thunk
variant in the enum declaration?
I also wouldn't mind removing the mention of "hack" here, and renaming the "Thunk" variant to ThunkOrRecSym
(or something more evocative).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@huitseeker not expensive at all, I think it would just add 1 constraint and 1 auxiliary. I just didn't do it because I'd have to add a bunch of cases in a bunch of files. I think I will add a new tag "FrozenVar", since it is a frozen computation that the variable refers to. I'll replace the comment as well
43a4ed2
to
997557e
Compare
847d520
to
3a5c7e7
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The specialized RecVar
looks great, the cycle counts going down also looks nice. I'd love for @arthurpaulino and / or @porcuquine to have quick look, but this LGTM
My review is summarized in this Zulip thread. The first bullet point is solved with the specialized On the second bullet point, I'd like us to, at least, plan for a solution for mutual recursion which makes us all content, as the syntactical manipulation mentioned in the PR description doesn't satisfy me completely (at least not yet). |
!gpu-benchmark |
Benchmark for 753bf71Click to view benchmark
|
…)" This reverts commit 2efe6ec for a suspected perf regression.
* two lookups per step * let/letrec refactor * recursive enviroments simplified * fixed eval/proof iterations * New tag for recursive variables * fixed lurk-lib and demo tests
* two lookups per step * let/letrec refactor * recursive enviroments simplified * fixed eval/proof iterations * New tag for recursive variables * fixed lurk-lib and demo tests
* two lookups per step * let/letrec refactor * recursive enviroments simplified * fixed eval/proof iterations * New tag for recursive variables * fixed lurk-lib and demo tests
This PR simplifies recursive environments. Now, instead of it taking an environment itself, the tag for the symbol is changed to denote a recursive variable. Although we can't get mutual recursion like this, there's a possible fix:
(letrec ((f A) (g B)) C)
can be transformed into
while reducing, which will achieve mutual recursion. This will, however, add some overhead to non-mutually recursive functions. But again, this can be mitigated if we take the memoset approach to
letrec
.Now, because of the simplification, it is possible to do 3 lookups per step without adding any slots. This greatly increases performance.
(fib 20)
goes from 613 iterations to 390, almost half the number of iterations