Typechecking blocks in continuation-passing style

[leo-leesco]

Because of typing issues arising during some Laurel-to-Laurel passes, well-typedness was not always preserved. The main observed cause is the typing rule for blocks that is too generic. We propose to typecheck blocks using continuation-passing style ideas :

1. we case analyze on the list of statements that constitute a block

• [] <= A is always true
• [stmtExpr] <= A gets stmtExpr <= A
• hd ; tl <= A :

2. we case analyze on hd :

• another block, propagate hd <= A and tl <= A
• anything else, apply the usual rule that matches this given constructor, for instance :
  • exit label : check that label is indeed in context (this is the usual exit rule)
  • return e : e <= function return type (those are the usual return rules)
  • x := e : x is in context and e <= typeof(x)
  • literals simply get synthesized and discarded ; similarly for operators (fixes EliminateIncrDecr pass)
  • etc…