Introduce len for ADTs to be used as a termination measure

[jcp19]

This PR introduces support for expressions of the form len(e), where e is an expression of an ADT type. This computes the rank of e, as defined in Paul Dahlke's thesis, which is a useful termination measure for functions defined by structural recursion on an ADT instance.

Arguably, it is bad style to overload len here for this measure but I would argue that this is consistent with the other overloads of len in Go and Gobra, e.g. for things like channels, maps (part of Go) and sets (part of Gobra). Nonetheless, I could introduce a new node if the majority dislikes this design, although this would introduce a new reserved keyword.

[Felalolf]

I think the design mixes the idea of a len and rank function, which has drawbacks on both sides. For a rank function, the axiomatization can be improved as described in my comment. For a len function, I am not sure the current behavior makes sense. For instance, given a pair and list adt (with the obvious constructors), len(cons(pair(1,2), cons(pair(3,4), nil())) is 5 and not the length of the list or the number of constructors of the list. In particular, the rank function mixes lengths of different composed ADTs, which I think might be suprising for users.

I had the idea that we could instead support adt values directly as measures. I.e. instead of a measure len(x) you can use directly x which is then encoded to an application of the rank function. A problem of this design is that you cannot support measures that use the rank function as part of a more complex measure, e.g. rank(x) - 5 (it can be supported, but makes the typing more complex, as an adt value would be treated differently depending on the context).

[jcp19]

• As I said, the idea for overloading len was more to be consistent with Go, but I will likely introduce a node for the rank function (EDIT: strike-through after talking to Felix)
• As for using an adt instance as a termination measure, it was my original idea (see Add support for ADTs as termination measures #588) but I decided against it because you may at some point need to write assertions that mention directly len(t), for some t of adt type in order to deal with a solver incompletness, e.g., the function testSubSubList in the test file src/test/resources/regressions/features/adts/termination-success1.gobra : even though the asserts there are not strictly required, you may in similar examples actually need to do sth like this. Ofc we could have an hybrid approach where you still provide access to the rank function in the source language but interpret an adt in a decreases clause as a call to rank.
• I will change rank such that I use the weaker axioms instead of a specific "implementation".