Function types depending on booleans in non-trivial ways?

[martinberger]

What is the idiomatic way of making return types of functions dependent on a boolean value? For example, consider this signature:

val f : forall ('n 'm: Int), ('n == 0 | 'n == 1). (int, bits('m)) -> bits ( 2*'m - 32*'n )

Here the size of the return type's bitvector changes depending on the first argument. But there are only two options, so integers seem to be overkill. I'd like to use a boolean (or a bit) instead. What I would like to say is something like:

val f : forall ('b : Bool) ('m: Int). (bool, bits('m)) -> bits ( if b then 2*'m - 32 else 2*'m )

where dependency on an integer, constrained to 0, 1, is replaced by dependency on a boolean value. What is the idiomatic way of doing this? I can't quite figure it out from the examples and the documentation, I apologise if I overlooked something.

[Alasdair]

There's no type-level if-then-else statement, so you need to encode T(if b then x else y) as {'n, (b & 'n == x) | (not(b) & 'n == y). T('n)}. Here's a working example:

default Order dec

$include <prelude.sail>

val f : forall ('b: Bool) 'm, 'm - 16 >= 0. (bool('b), bits('m)) -> {'n, ('b & 'n == 2 * 'm - 32) | (not('b) & 'n == 2 * 'm). bits('n)}

function f(b, bits) = {
    if b then {
        sail_zeros(2 * length(bits) - 32)
    } else {
        sail_zeros(2 * length(bits))
    }
}

val main : unit -> unit

function main() = {
    let x = f(true, 0xFFFF_FFFF);
    let y = f(false, 0xFFFF_FFFF);
    print_bits("x = ", x);
    print_bits("y = ", y)
}

which prints:

x = 0x00000000
y = 0x0000000000000000