Frontend.Dim assertion failure

[zilinc]

def $f(nat**): nat*
def $f((n^(i<k))^j) = l^j  -- (if l = |n^k|)^j

results in a crash:

./spectec: uncaught exception File "src/frontend/dim.ml", line 504, characters 8-14: Assertion failed

Backtrace:
Raised at Frontend__Dim.annot_iterexp.(fun) in file "src/frontend/dim.ml", line 504, characters 8-55
Called from Stdlib__List.filter_map in file "list.ml", line 280, characters 12-15
Called from Frontend__Dim.annot_iterexp in file "src/frontend/dim.ml", line 500, characters 4-281
Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19
Called from Frontend__Dim.annot_iter in file "src/frontend/dim.ml", line 365, characters 12-114
Called from Frontend__Dim.annot_iterexp in file "src/frontend/dim.ml", line 498, characters 32-51
Called from Frontend__Dim.annot_exp in file "src/frontend/dim.ml", line 433, characters 26-60
Called from Frontend__Dim.annot_exp in file "src/frontend/dim.ml", line 432, characters 24-40
Called from Frontend__Dim.annot_arg in file "src/frontend/dim.ml", line 549, characters 23-38
Called from Frontend__Dim.annot_top in file "src/frontend/dim.ml", line 581, characters 19-32
Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19
Called from Frontend__Elab.elab_def in file "src/frontend/elab.ml", line 2584, characters 14-48
Called from Stdlib__List.concat_map in file "list.ml", line 286, characters 32-37
Called from Stdlib__List.prepend_concat_map in file "list.ml", line 290, characters 20-46
Called from Frontend__Elab.elab in file "src/frontend/elab.ml", line 2722, characters 12-45
Called from Dune__exe__Main in file "src/exe-spectec/main.ml", line 180, characters 23-44

Workaround is to change the iterator from n^(i<k) to n^k.

[rossberg]

I fixed the assertion failure. However, the example will probably still not work as expected: due to limitations of the interpreter backend, the frontend cannot currently introduce iteration variables of higher dimension. Thus it infers

def $f{`n**` : nat**, `k*` : nat*, `i*` : nat*, j : nat, `l*` : nat*}
  (n^(i<k){i <- `i*`, n <- `n*`}^j{k <- `k*`, `n*` <- `n**`}) = l^j{l <- `l*`}
    -- (if (l = |n^k{n <- `n*`}|))^j{k <- `k*`, l <- `l*`, `n*` <- `n**`}

which isn't very useful. What we'd really want is

def $f{`n**` : nat**, `k*` : nat*, `i**` : nat*, j : nat, `l*` : nat*}
  (n^(i<k){i <- `i*`, n <- `n*`}^j{k <- `k*`, `n*` <- `n**`, `i*` <- `i**`}) = l^j{l <- `l*`}
    -- (if (l = |n^k{n <- `n*`}|))^j{k <- `k*`, l <- `l*`, `n*` <- `n**`}

but then the interpreter crashes because i** appears to be unbound in the outer iteration.

(Unfortunately, changing the frontend to at least infer the more general dimension will also make the interpreter crash on parts of the actual Wasm spec, which just happen to work with the lower dimension.)