struct literal expressions. we might then prohibit changing one of the parameter members of a "dependent struct" without updating the dependent members at the same time.
verification of index bounds (suggests moving to a more robust verifier, such as Z3)
a <- b currently does not verify that overwriting a will not invalidate the computation of b (for instance, a[:,:] <- a*a generates incorrect code). the easiest immediate fix would be to always store b in a temp if it involves vectors.
(a#b) <- c; -- this works when (a#b) is passed as an out variable, but is invalid (syntactically) in the given form
polymorphism over base types, for instance: reverse {a, n} (x :: a[n]) :: a[n]
a <- b
currently does not verify that overwritinga
will not invalidate the computation ofb
(for instance,a[:,:] <- a*a
generates incorrect code). the easiest immediate fix would be to always storeb
in a temp if it involves vectors.(a#b) <- c;
-- this works when(a#b)
is passed as an out variable, but is invalid (syntactically) in the given formreverse {a, n} (x :: a[n]) :: a[n]