Adding subtraction to constant expressions

[sadministrator]

When needing to index through a vector with a constant generic length >= 0, you can't transmute the index variable to a type that allows indexing of that vector because the compiler thinks the length could be zero even if it's explicitly ruled out (e.g. with an if statement).

You can obviously fix this by having the compiler check if $n == 0 has already been ruled out but I think adding subtraction to constant expressions is more useful because it will make the language more versatile in other situations as well.

Contrived examples:

def add1_or_fail<$n>(vec: [Nat; $n], offset: {0..$n}) = 
if $n == 0 then fail! else vec[0] + 1

/home/marco/dev/bridge-covenants/proof.melo:37: error: type [Nat; $n] cannot be indexed into
    if $n == 0 then fail! else vec[0] + 1
                               ^~~~~~

def looper(vec: [Nat; $n], offset: {$o}) =
  let accum = [] :: [Nat;] in
  loop $n - $o do
    accum <- accum + vec[offset];
    offset <- offset + 1 :! {0..$n - 1}
  return accum

[nullchinchilla]

Subtraction in const-expressions is very problematic because it then becomes hard to guarantee that the const-expression as a whole can never be negative.

In your case, you probably want to do something like

add1_or_fail<$n>(vec: [Nat; $n+1], offset: {0..$n}) = 

In fact, your original code was subtly wrong because {0..$n} is inclusive :)

[sadministrator]

Yeah that's how I get around it now but it makes it so you can't accept empty vectors which I guess is not a huge deal in the long run.

Should we close this issue then?

[nullchinchilla]

No; I think subtraction might make sense and is indeed useful --- if we can figure out the semantics.

In general I am not very happy with const generics semantics in Melodeon; it's a little messy and my current model of using polynomials and polynomial math might not be the best, since polynomials are a continuous thing and const-generics are fundamentally integer-based and encode discrete structure. Instead, we might go the Peano arithmetic / structural recursion route for bounding computation, which should also make Coq-like bounded recursion etc expressable