Properly scoped iteration ops for IL

[rossberg]

This PR generalises IL iteration expressions to proper parallel maps, as proposed in the meeting the other day. That is, the IL expression form

e*{x1, ... ,xN}

becomes

e*{x1<-e1, ... ,xN<-eN}

where x1...xN are locally scoped variables. For each ei of type ti*, xi iterates over its elements of type ti. In other words, this simply is an n-ary mapN (λ x1 ... xN. e) e1 ... eN. All ei must evaluate to lists of the same length. Likewise for options.

• Unlike the previous form, this is closed under substitution, and hence allows reduction.
• The notion of variable dimensions is no longer needed in the IL, ordinary list and option types suffice.

Both make for a simpler and cleaner IL semantics overall. Dimensions still exist in the EL, but are elaborated away by introducing separate variables for each nesting level. For example, EL

def $f(x*, y*) = (x + y)*

elaborates to IL

def $f(xs, ys) = (x + y)*{x<-xs, y<-ys}

(In reality, xs and ys will currently be named "x*" and "y*" internally.)

This will require adapting the IL2AL translation, and possibly changes to the AL itself, to handle the more general form. I made some obvious minor changes to get it to compile again. But I'm not sure what the right changes are to support prose rendering in the best manner. @f52985, can I once more leave that part to you?

(I note that this form also matches more closely the manually written prose, where the equivalent is expressed as "for each xi in x [and corresponding yi in y] do e", etc. Perhaps this change could even simplify generating such prose?)

[f52985]

Now the algorithmic backends support the new IterE.

It took a bit longer than I initially expected, mainly due the the case where IterE appears as the binding target, (i.e. Let x = ...) which made the inference of identifier binding (a.k.a. animation) a bit tricky. (Previously, we ignored all of the "iters" when infering the identifier binding, so all of x = ..., `x = ...,x* = ..., were all simply treated as the "binding to the variable namedx". But now, we have to keep track of what are the actual variables that are bound by this equation, i.e., "binding to the variable namedx,x, andx**`" respectively.)

Now it's all resolved anyway, and all the tests are passing again!

(I note that this form also matches more closely the manually written prose, where the equivalent is expressed as "for each xi in x [and corresponding yi in y] do e", etc. Perhaps this change could even simplify generating such prose?)

Yes, that would be possible. Although the generated prose still uses a bit implicit notation to express such cases, we are in the process of figuring out the difference of the manually written prose and the generated prose and trying to minify the difference, and this PR would be indeed useful during that process.

[rossberg]

Cool, thank you very much! I'll land this then.