Support constants

[yannbolliger]

For example something like this:

const DEFAULT_PORT: u64 = 1000;

Currently, this fails with: error: Unsupported tree: Other kind of item

[yannbolliger]

Currently, we serialise a triple of (FunDef, ClassDef, ADTSort) to give to the Stainless backend. This leaves no room for top-level constants. A solution could be to scope the constants inside of some ADT.

[romac]

Can we just extract them as FunDefs and rewrite mentions to constants to function calls?

ie.

const DEFAULT_PORT: u64 = 1000;

fn test() {
  let x = DEFAULT_PORT;
}

would be extracted as

def DEFAULT_PORT(): U64 = 1000;

def test(): Unit = {
  val x = DEFAULT_PORT();
}

We may also want to add a @inline annotation to the extracted FunDef to eventually erase them in the Stainless pipeline.