PrincetonUniversity / lucid

MIT License
40 stars 10 forks source link

Function inlining and comprehension unrolling must be done concurrently #7

Closed DKLoehr closed 3 years ago

DKLoehr commented 3 years ago

Currently function calls are expressions which become statements when inlined. This causes a problem during function inlining, because we might have function calls inside vector comprehensions. We can't inline the function first because comprehensions take an expression, and we can't unroll the comprehension prior to inlining because we might not know how long it will be. Currently we get around this by doing both simultaneously, but this is both complicated and prevents us from running inlining as early as we'd like to. Some examples:

We can work around both of these (taking less precise estimates, or duplicating function bodies the same way we do events), but it might be nicest to find a way to decouple inlining and comprehension unrolling. We might do this by creating a new type of expression, e.g. EStmt of stmt * id, which has the semantics of evaluating the statement and then returning the value of the id variable (which may be initialized within the statement). Alternatively, we could create a new type of comprehension which basically inlines this, e.g. EComp2 of (stmt * id) * id * size.