Georg Stefan Schmid

Experiment: Less duplication, more aggressive let simplification

4

This PR adds let-bindings in favor of duplicating code in two more places (match desugaring and assertions for ADT field selections). Conversely, it also adds an additional let-simplifications step in...

Add erasure of AnyHeapRef-bounded type parameters and better allocator examples

1

This PR improves upon the existing `AllocatorMono` example by a) adding a variant `AllocatorMonoAbstract` that abstracts the implementation and simply gives a model of an allocator that could feasibly be...

Fixes Stainless-side issue of #1135, i.e., `ADTPattern`s should be compared modulo erased type arguments in `RecursiveEvaluator`.

The following example *sometimes* leads to `TypeChecker` complaining about an illegal recursive call: ```scala import stainless.lang._ import stainless.annotation._ import stainless.collection._ import stainless.proof._ object NodeCycleExample { case class Node(var next: Option[Node])...

Evaluator should match against erased pattern types

1

We currently stored non-normalized types in pattern matches. For instance, we might have a case with an ADT pattern ```scala def size[T](xs: List[T]): BigInt = xs match { case Nil...

For `@synthetic` functions we re-assert postconditions at inlined call sites (see https://github.com/epfl-lara/stainless/blob/3da44e47828dd6269131270b76ada1617eb00b6a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala#L114). The particular way in which this is done, i.e., by let-binding the post condition and *then* asserting the...

Checking measure on type-parametric class method leads to invalid context in type checker

1

Ran into this while trying some to prove some laws example on polymorphic lists: ```scala import stainless.lang._ import stainless.collection._ abstract class Equals[A] { def law_refl(x: A): Boolean = true }...

This results in type error ```scala import stainless.lang._ import stainless.collection._ object TypeError { def some_lemma(x: Int, xs: List[Int]): Boolean = { !the_law(xs) || the_law(xs) } def the_law(xs: List[Int]): Boolean =...

Adds a debug section `blocker-graph` that dumps the (non-strict) implication graph among all blocking literals. The current graph is dumped at the end of `checkAssumptions` and saved in `blocker-graphs/*file*-*n*.dot`. Nodes...