Thorin scoping rules mean PE specialization doesn't work the way programmers think it should

[Hugobros3]

Thorin uses implicit scoping, where functions and continuations have a scope that corresponds to the live, transitive users of their parameters. This has interesting consequences: in the example below, in the body of the for loop in the foo function, the statements after the function call to square belong in a continuation that is not in the scope of the for loop body at all.

#[export]
fn foo(a: i32) -> i32 {
    for i in unroll(0, 4) {
        if (a == i) {
            let b = unsquare(i * i);
            let c = b();
            // pe_info("i:", i);
            return (c)
        }
    }
    69
}

This is perhaps clearer at the IR level:

// enclosing foo and for loop scopes removed for brevity
fn loop_body(m0: mem, i: i32, continue: fn(mem)) {
  br (a == i, if_true, if_join)

  fn if_true(m1: mem) {
    unsquare(i * i, cont0)
  }

  fn if_join(m1: mem) {
    continue(m1)
  }
}

// no parameters from loop_body used here
fn cont0(m2: mem, b: fn(i32) -> i32) {
  b(m2, return)
}

This leads to the example not being specialized as intended: this pattern of unroll + if should allow for specialized branches where i is fully known, but because cont0 is not in the scope of loop_body, only the calls to unsquare are specialized and, and control-flow joins back at the original cont0 which has not been specialized, and so the b(); call cannot be partially evaluated because b is still a parameter in a continuation with multiple predecessors.

Adding the commented-out pe_info statement gets around the problem by forcefully including the previous statements in the scope of loop_body. However, this behavior is extremely surprising to programmers who are used to reason in terms of structured programming.

We should, at a minimum, educate AnyDSL users about this behavior. A better long-term solution is to have the compiler insert some sort of intrinsic to "tie" continuations in a block to the structured programming scope it appears to belong to, at least until PE completes and then we could remove them to allow for more optimizations.

---

Full example:

#[export]
fn foo(a: i32) -> i32 {
    for i in unroll(0, 4) {
        if (a == i) {
            let b = unsquare(i * i);
            let c = b();
            // pe_info("i:", i);
            return (c)
        }
    }
    69
}

fn @unsquare(a: i32) -> fn() -> i32 {
    match (a) {
        1 => { return(@ || { 1 }) },
        4 => { return(@ || { 2 }) },
        9 => { return(@ || { 3 }) },
        _ => { return(@ || { 0 }) },
    }
}

// irrelevant to the issue
#[import(cc = "thorin")]
fn pe_info[T](_src: &[u8], _val: T) -> ();
fn @unroll(body: fn(i32) -> ()) = @|lower: i32, upper: i32| unroll_step(body)(lower, upper, 1);
fn @unroll_step(body: fn(i32) -> ()) {
    fn @(?beg & ?end & ?step) loop(beg: i32, end: i32, step: i32) -> () {
        if beg < end {
            @body(beg);
            loop(beg + step, end, step)
        }
    }
    loop
}