continue not working in while loop

[franziskuskiefer]

It looks like #196 is not fully working. The following example fails to lax.

fn while_continue() {
    let mut attempt = 0;
    let mut value = None;

    while attempt < 5 {
        attempt += 1;

        if attempt < 3 {
            continue;
        }

        value = Some(1);
    }
}

Open this code snippet in the playground

* Error 12 at Playground.fst(40,10-45,19):
  - Expected type
        o:
        (Rust_primitives.Integers.i32 &
          Core.Option.t_Option Rust_primitives.Integers.i32){o << temp_0_}
    but
        Core.Ops.Control_flow.ControlFlow_Continue (attempt, value)
        <:
        Core.Ops.Control_flow.t_ControlFlow (Prims.unit &
            (Rust_primitives.Integers.i32 &
            Core.Option.t_Option Rust_primitives.Integers.i32))
          (Rust_primitives.Integers.i32 &
            Core.Option.t_Option Rust_primitives.Integers.i32)
    has type
        Core.Ops.Control_flow.t_ControlFlow (Prims.unit &
            (Rust_primitives.Integers.i32 &
            Core.Option.t_Option Rust_primitives.Integers.i32))
          (Rust_primitives.Integers.i32 &
            Core.Option.t_Option Rust_primitives.Integers.i32)
1 error was reported (see above)
make[1]: *** [Makefile:79: Playground.fst.checked] Error 1
make: *** [Makefile:12: all] Error 2

[karthikbhargavan]

Not sure how well we support while-loops in general, so this may be part of a larger issue.

[franziskuskiefer]

If this is not supported for while loops, the description of the other issues has been incomplete.

[maximebuyse]

If this is not supported for while loops, the description of the other issues has been incomplete.

While loops should be supported but it seems like the issue described here is a bug in the translation (I am not sure it is specific to while loops by the way). #1204 is also needed to make the translation usable but it is different.