import stainless.annotation.*
object LawAndOrder:
def sign(i: Int): Int =
if i > 0 then 1
else
if i < 0 then -1 else 0
sealed trait Ordering[T]:
def compare(x: T, y: T): Int
@law
def inverse(x: T, y: T): Boolean =
sign(compare(x, y)) == -sign(compare(y, x))
/*
@law
def transitive(x: T, y: T, z: T): Boolean =
!(compare(x, y) > 0 && compare(y, z) > 0) || (compare(x, z) > 0)
@law
def consistent(x: T, y: T, z: T): Boolean =
!(compare(x, y) == 0) || (sign(compare(x, z)) == sign(compare(y, z)))
*/
end Ordering
val IntOrder = new Ordering[Int]:
def compare(x: Int, y: Int) =
if x == y then 0
else if x < y then -1
else 1
def LexOrder[A,B](ordA: Ordering[A], ordB: Ordering[B]): Ordering[(A,B)] =
new Ordering[(A,B)] {
def compare(x: (A, B), y: (A, B)): Int =
val compA = ordA.compare(x._1, y._1)
if compA == 0 then ordB.compare(x._2, y._2)
else compA
override def inverse(x: (A,B), y: (A,B)): Boolean =
ordA.inverse(x._1, y._1) && ordB.inverse(x._2,y._2) &&
sign(compare(x, y)) == -sign(compare(y, x))
}
end LawAndOrder
in two consecutive runs reports returns different error message:
kuncak@kuncak-x1yog6: (main)~/software/stainless/tmp$ stainless LawAndOrder.scala --timeout=10
[ Info ] Finished compiling
[ Info ] Preprocessing finished
[ Info ] Finished lowering the symbols
[ Info ] Generating VCs for 17 functions...
[ Fatal ] LawAndOrder.scala:13:23: Variable T 43 is not defined in context:
[ Fatal ] Kind: argument types (call isOrdering(x, T))
[ Fatal ] Check SAT: false
[ Fatal ] Emit VCs: true
[ Fatal ] Functions: isOrdering, choose$0, IntAbsToBigInt, ObjectPrimitiveSize, BigIntAbs, compare, choose$2, is$anon
[ Fatal ] ADTs: Object
[ Fatal ] Type Variables:
[ Fatal ] Term Variables:
[ Fatal ] A: (Object) => Boolean
[ Fatal ] B: (Object) => Boolean
[ Fatal ] thiss: { x: Object | (is$anon(x, A, B)): @dropConjunct }
[ Fatal ] x: ({ x: Object | (A(x)): @dropConjunct }, { x: Object | (B(x)): @dropConjunct })
[ Fatal ] y: ({ x: Object | (A(x)): @dropConjunct }, { x: Object | (B(x)): @dropConjunct })
[ Fatal ] T: (Object) => Boolean
[ Fatal ] T == A
[ Fatal ] thiss.isInstanceOf[$anon]
[ Fatal ] x: Object
[ Fatal ] x == thiss.ordA
[ Fatal ] x: Object
[ Fatal ] x == x
[ Fatal ]
def inverse(x: T, y: T): Boolean =
^
[ Error ] Stainless terminated with an error.
[ Error ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error ] You may use --debug=stack to have the stack trace displayed in the output.
kuncak@kuncak-x1yog6: (main)~/software/stainless/tmp$ stainless LawAndOrder.scala --timeout=10
[ Info ] Finished compiling
[ Info ] Preprocessing finished
[ Info ] Finished lowering the symbols
[ Info ] Generating VCs for 17 functions...
[ Fatal ] LawAndOrder.scala:36:21: Call to function compare is not allowed here, because it is mutually recursive with the current function compare
val compA = ordA.compare(x._1, y._1)
^^^^^^^^^^^^^^^^^^^^^^^^
[ Error ] Stainless terminated with an error.
[ Error ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error ] You may use --debug=stack to have the stack trace displayed in the output.
Maybe depending on the solver the termination checker takes different paths and some of them trigger the bug.
The ability to handle the example may need some assumptions about well-formedness on type arguments that do not necessarily hold in the presence of polymorphic recursion (which we don't handle, but the termination checker is not using that fact either).
On Version: 0.9.8.7-14-g7fd69e2 this code
in two consecutive runs reports returns different error message:
Maybe depending on the solver the termination checker takes different paths and some of them trigger the bug.
The ability to handle the example may need some assumptions about well-formedness on type arguments that do not necessarily hold in the presence of polymorphic recursion (which we don't handle, but the termination checker is not using that fact either).