Il-to-Il pass: Eliminate the ! operator equationally #13
Conversation
|
I did some mildly nasty things to |
|
CI is only red because github is stupid and tries to merge before running CI, instead of testing the latest commit. This can be fixed in the github workflow file, maybe I should open a PR for that later. Will merge later (need to handle the |
|
Should we just annotate every node in the IL AST with its type? |
|
Yes, probably. As a Source.note as in Motoko? Maybe make it a |
|
Yes, that's what I was thinking. And then we can remove all type annotations inside exp constructors. Not sure about making it optional, is there indication that it might be difficult in places? |
|
Not yet, we can try without option and I'll complain if it's hard somewhere. |
|
Or we could do what GHC does: only annotate enough leafs (variables and functions, I assume) so that one can infer the type for all expressions without context. A bit less bookkeeping, and performance is not super critical here. |
|
Okay, I implemented this (i.e., types in all expression nodes). Also removed the now redundant annotations on DotE, CaseE, and DotP again. It was slightly painful to construct the types in the sideconditions phase, because that required a variable environment. We can make them optional if that turns out to be too dreadful in the future. |
|
Cool, will update this pass accordingly in a few days (unless someone beats me to it) |
|
Updated to use the type information in the AST annotations. |
| let rec t_exp n e : eqns * exp = | ||
| (* Descend first using t_exp2, and then see if we have to pull out the current expression *) | ||
| let eqns, e' = t_exp2 n e in | ||
| match e.it with |
There was a problem hiding this comment.
@nomeata - Was this supposed to be e'.it instead of e.it?
There was a problem hiding this comment.
Oh, quite likely. We probably don’t have nested the so far. Thanks for spotting!
Merge with WebAssembly/spec and WebAssembly/gc
This pass can go before the sideconditions pass #9, to do something more clever with option projection. Here is an example:
Before it would introduce
!= nullconstraints and leave!(e)in place, which is correct, but typically hard to work with in a formalization. With this pass before, it introduces a fresh variableo0and asserts that the partial expression is= ?o0.This is a separate pass because maybe only some backends will prefer this (and because it’s slightly complicated).