Let premise introduction pass

[DCupello1]

It probably is a good time to make use of the let premise in efforts to make function definitions more translatable.

This pass goes through all list of premises, and if there is a LHS that has a variable that has not been declared before, then it introduces a let premise.

Due to this approach, this pass relies on the ordering of the premises. Perhaps there is a way to remove this restriction but for now this naive approach should work fine.

Valid LHS are:
VarE, StrE (records), CaseE, IterE (only allows identity iteration), TupE

In the validator, there are some RHS that need to be inferred, but some expressions are not possible to have their type inferred.

So, the RHS not allowed are:
OptE, StrE

For the most part, this works well. However due to some of the restrictions above, (and uncaseE appearing in unfortunate locations) it sometimes just does not introduce the let premise.

Example from Wasm 3.0:

rec {
def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*)
  def $minus_recs([], []) = ([], [])
  def $minus_recs{n : n, `tv*` : typevar*, tu_1 : typeuse, `tu*` : typeuse*}([REC_typevar(n)] ++ tv*{tv <- `tv*`}, [tu_1] ++ tu*{tu <- `tu*`}) = $minus_recs(tv*{tv <- `tv*`}, tu*{tu <- `tu*`})
  def $minus_recs{x : idx, `tv*` : typevar*, tu_1 : typeuse, `tu*` : typeuse*, `tv'*` : typevar*, `tu'*` : typeuse*}([_IDX_typevar(x)] ++ tv*{tv <- `tv*`}, [tu_1] ++ tu*{tu <- `tu*`}) = ([_IDX_typevar(x)] ++ tv'*{tv' <- `tv'*`}, [tu_1] ++ tu'*{tu' <- `tu'*`})
    -- if ((tv'*{tv' <- `tv'*`}, tu'*{tu' <- `tu'*`}) = $minus_recs(tv*{tv <- `tv*`}, tu*{tu <- `tu*`}))
}

to

rec {
def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*)
  def $minus_recs([], []) = ([], [])
  def $minus_recs{n : nat, `tv*` : typevar*, tu_1 : typeuse, `tu*` : typeuse*}([REC_typevar(n)] ++ tv*{tv <- `tv*`}, [tu_1] ++ tu*{tu <- `tu*`}) = $minus_recs(tv*{tv <- `tv*`}, tu*{tu <- `tu*`})
  def $minus_recs{x : uN(32), `tv*` : typevar*, tu_1 : typeuse, `tu*` : typeuse*, `tv'*` : typevar*, `tu'*` : typeuse*}([_IDX_typevar(x)] ++ tv*{tv <- `tv*`}, [tu_1] ++ tu*{tu <- `tu*`}) = ([_IDX_typevar(x)] ++ tv'*{tv' <- `tv'*`}, [tu_1] ++ tu'*{tu' <- `tu'*`})
    -- where (tv'*{tv' <- `tv'*`}, tu'*{tu' <- `tu'*`}) = $minus_recs(tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) {tu', `tu'*`, tv', `tv'*`}
}

Based off #198 so need to merge that one first.

Some limitations of this pass:

• The premise must be of the exact right shape (according to the valid LHS and RHS noted above) and ordering to introduce lets. If it is not ordered properly, it leaves the if premise untouched.
• It does not try to do any dependency analysis nor does it introduce any new variables, making it quite weak compared to Zilin's pass. Regardless, most if premises are in the right shape so this should not introduce a problem.

[DCupello1]

Its probably a good time to start merging down most of the passes. @rossberg could you take a look? This should be in line with the semantics you made for let premises, though please let me know if I missed something

[rossberg]

This makes sense to me, although my question is how much this overlaps with one of @zilinc's animation passes, which does something very similar, but including dependency analysis and reordering.

@zilinc, first of all, you're the expert, can you review this PR? Second, how modular is your pass? What's your thought on whether both these lines can (and should) somehow be refactored and/or integrated to avoid duplication?

[zilinc]

My immediate thought is that we can possibly apply my animation pass to selected functions that you want to introduce let. My animation pass is more aggressive in introducing intermediate variables (A-normalisation) to avoid evaluating the same expression multiple times in the meta-interpreter. If this normalisation is not desirable, I think it can be configured to be optional. Another difference is that I'm more restrictive in what is allowed to appear in LHS, for OCaml extraction, which is not necessary in an IL-to-IL pass. There are a couple of gaps that I haven't closed, e.g. the output AST is currently not strictly IL (should be relatively easy to fix); the output IL doesn't not typecheck (hopefully not too troublesome), But I'll read the code in more detail to give an informed opinion.

[zilinc]

Why do you not need to restrict args to be valid LHS?

[DCupello1]

I don't think I restrict args in any way, do I? I only restrict the LHS of the let premise to be valid (in terms of whether its feasible for ITPs to be able to capture the variable through their version of let).

[zilinc]

No you don't. But I thought you needed to restrict them, because they are essentially LHS (i.e. patterns). Is it because the functions that you're concerned with happen to have arguments that are already valid LHSes?

[DCupello1]

Ah I see what you mean with this. I'm more concerned with LHS for functions being valid in the deftorel pass, as then if its not valid I could turn them into relations.

So in the let-intro pass, I don't really care as much if the function is actually valid. It makes it so the let-intro pass is very focused: it only focuses on let premises. Hope that makes sense!

[zilinc]

Yeah it makes sense, and thanks for the clarification. I think I'm missing the big picture here a bit, possibly rooted in the deftorel pass. Could you give (or point to) a high-level summary of the design, as of what functions should remain as functions and what need to be turned into relations? I saw in #206 there are some discussion, and combining with what I learned from this PR, I sense that you are preserving those SpecTec definitions that are already functions in a PL sense. Are there more nuances to it that I'm missing?

[DCupello1]

(Sorry for the late reply!) I updated the description in #206 that shows more the design of the pass, but it has kind of made me realize that this pass is way too complex to even explain. I am going to see if there is a better way to handle this pass.

[zilinc]

There are a few more differences between my animation pass and this let-intro pass:

• It looks the code here only turns IfPr into LetPr if the LHS and RHS are already in the right shapes. But my animation tries to move things around to create opportunities to transform to LetPr. Besides -- if lhs = rhs premises, a membership if-premise may become an equality. They are all parts of the monolithic animation engine. It's not very obvious how to separate them, if they are not desirable.
• It also does a rel-to-def along the way, which is the opposite direction to what we want.
• It's currently done as a backend instead of a middle-end pass. Some significant code reshuffling is warranted, to resolve circular imports.

[DCupello1]

There are a few more differences between my animation pass and this let-intro pass:

• It looks the code here only turns IfPr into LetPr if the LHS and RHS are already in the right shapes. But my animation tries to move things around to create opportunities to transform to LetPr. Besides -- if lhs = rhs premises, a membership if-premise may become an equality. They are all parts of the monolithic animation engine. It's not very obvious how to separate them, if they are not desirable.
• It also does a rel-to-def along the way, which is the opposite direction to what we want.
• It's currently done as a backend instead of a middle-end pass. Some significant code reshuffling is warranted, to resolve circular imports.

Yes, you are right. This pass is much less aggressive when it comes to introducing lets, as it only makes sure that it is in the right shape. If not, it just leaves it untouched.

So, from what I can see, having your version of let be a middlend pass is pretty hard since there are a lot of dependencies and assumptions made specifically for the animation backend. In that case, I think its maybe fine to have two versions of let introduction, maybe having their names be more explicit for what backend they are useful for?

[DCupello1]

Changed the name of the pass to specify that this is for mechanization backends, and rebased to main to resolve testing conflicts

[rossberg]

Mh, I'm still a bit confused, to be honest. If I understand correctly, this pass misbehaves (i.e., silently produces an ill-typed program) when applied to premises that are not already ordered, and where not every if's l.h.s. actually is meant as a pattern.

For the simplest example, consider a case like if x = y. It looks like this would unconditionally turn into let, but that might easily be plain wrong if x is already defined and this purely is a comparison. (OTOH, such an if might actually define y!) Similar cases could arise with composed literals (if (x,y) = (a,b)), although those are probably rarer.

Do you envision a separate pass normalising the if premises (or at least checking the preconditions) beforehand? Or how else is it ensured that nothing goes wrong when running this pass?

My understanding is that Zilin's animation transformation for function premises is a generalisation of this pass (or a composition) that can handle these and other cases — and moreover, report cases it cannot handle. Isn't such a generalisation desirable/necessary to have, even for mechanisation backends?

[DCupello1]

Mh, I'm still a bit confused, to be honest. If I understand correctly, this pass misbehaves (i.e., silently produces an ill-typed program) when applied to premises that are not already ordered, and where not every if's l.h.s. actually is meant as a pattern.

For the simplest example, consider a case like if x = y. It looks like this would unconditionally turn into let, but that might easily be plain wrong if x is already defined and this purely is a comparison. (OTOH, such an if might actually define y!) Similar cases could arise with composed literals (if (x,y) = (a,b)), although those are probably rarer.

Do you envision a separate pass normalising the if premises (or at least checking the preconditions) beforehand? Or how else is it ensured that nothing goes wrong when running this pass?

My understanding is that Zilin's animation transformation for function premises is a generalisation of this pass (or a composition) that can handle these and other cases — and moreover, report cases it cannot handle. Isn't such a generalisation desirable/necessary to have, even for mechanisation backends?

I believe for a case if x = y, if x is already defined, then it leaves it as a comparison. In fact, if x is defined and y is not, then it defines y using let! I.e. it would turn into let y {y : T} = x. (Though do let me know if there is a counterexample, because then it would be a bug!) If both are defined then again it just leaves it as an if.

The pass I have made actually tries to be as safe as possible, since whenever it can't find a way to have let in the right shape and conditions, it just leaves it as it is. This is actually already enough for many of the functions actually. It does not report the cases it cannot handle (though it should not be hard to do if we want to honestly).

Of course, this does miss some cases i.e. when it is not ordered as you said. But again, if this is the case, then it would just leave it as it is.

My understanding of Zilin's pass (Zilin correct me if I am wrong!) is that it does some transformations that might not be desirable as they are too aggressive for mechanization.

[rossberg]

Ah, okay, sorry, I misread what's going on. Thanks for the explanation.

In an ideal world, I would hope that Zilin's pass can be decomposed such that this pass becomes one part of it. But that may be not be worth the trouble at this point, so I'm fine with landing this.

It might be worth documenting the limitations in the MLI, though.

[DCupello1]

Ah, okay, sorry, I misread what's going on. Thanks for the explanation.

In an ideal world, I would hope that Zilin's pass can be decomposed such that this pass becomes one part of it. But that may be not be worth the trouble at this point, so I'm fine with landing this.

It might be worth documenting the limitations in the MLI, though.

No worries! I should have made it more clear in the PR.

I agree, I would think that in the future we can attempt to merge both passes, but at the moment it seems too much work.

I put the limitations for this pass in the PR comment!