epfl-lara/leon — pull request #52 by colder (2014-02-03 13:41:16+00:00)
Title: Implement generics for functions and ADTs

- Calling functions are now typed, FunctionInvokation takes a
TypedFunDef which is basically a FunDef with type parameters' values.
Instantiation of types within the signature/body is done on demand
through this wrapper class.

- Operations on ADTs are now taking a *ClassType instead of *ClassDef.
Similarly, Case/AbstractClassType takes values for type parameters.

- Introduces a GenericValue tree for models targeting abstract types.
e.g. foo[T](a: T, b: T) { a == b } ensuring (_) will find a model with
{ a -> T#1, b -> T#2 }

- Only "simple" hierarchies allowed with type parameters. All members of
the hierarchy must define the same number of type parameters and
correctly pass them to parent classes.

- Type parameters are invariant.