findEndpoint (local to ses) specification is necessary for ses termination check; however, it is not being checked itself because it is behind an assume annotation.
{-@ assume findEndpoint
:: forall <q :: DL -> Bool>.
i : Nat -> j : Nat -> xs : [DL<q>]
-> { m : Maybe {dl : DL<q> | endPoint i j dl}
| m == Nothing => _wfDistanceToGoal i j xs > 0} @-}
findEndpoint :: Int -> Int -> [DL] -> Maybe DL
findEndpoint i j = find (endPoint i j)Completing this issue requires removing this annotation and make the static checks pass, thus completing the termination proof.
A proposed first step can be found in 86159e2. Note findEndpoint is specified using an abstract refinement that would provide whatever predicate was expected from nodes in both preconditions and postconditions. In this commit the abstract predicate is narrowed to the actual requirement: a DLN node.
What's missing are the means for LiquidHaskell (LH) to reason about the Nothing case, as it does not have access to the find unfolding. Solving this means overcoming existing LH limitations on functions with typeclass constraints.
Possible alternatives include:
- Define and use an specialized
find, so that its unfolding is used by PLE.
- Modify
assume reflect upstream to use specialized functions so that we can keep find in the source, while using a local implementation for its unfolding.
- Strenghten
find upstream specification to account for it (not feasable at the moment because it would require something like typeclass conditioned predicates).
Redefining find to an specialized and optimized version is not a desirable solution, as we expect changes improving the static checks to keep code simple and idiomatic.
A solution exists already in 93549e8 , where explicit recursion is used instead of find in findEndpoint, resulting in a simple idiomatic definition. However, I deem this a no-go given the performance penalty this change incurs (see commit description for a benchmark comparison).
findEndpoint(local toses) specification is necessary forsestermination check; however, it is not being checked itself because it is behind anassumeannotation.{-@ assume findEndpoint :: forall <q :: DL -> Bool>. i : Nat -> j : Nat -> xs : [DL<q>] -> { m : Maybe {dl : DL<q> | endPoint i j dl} | m == Nothing => _wfDistanceToGoal i j xs > 0} @-} findEndpoint :: Int -> Int -> [DL] -> Maybe DL findEndpoint i j = find (endPoint i j)Completing this issue requires removing this annotation and make the static checks pass, thus completing the termination proof.
A proposed first step can be found in 86159e2. Note
findEndpointis specified using an abstract refinement that would provide whatever predicate was expected from nodes in both preconditions and postconditions. In this commit the abstract predicate is narrowed to the actual requirement: a DLN node.What's missing are the means for LiquidHaskell (LH) to reason about the
Nothingcase, as it does not have access to thefindunfolding. Solving this means overcoming existing LH limitations on functions with typeclass constraints.Possible alternatives include:
find, so that its unfolding is used by PLE.assume reflectupstream to use specialized functions so that we can keepfindin the source, while using a local implementation for its unfolding.findupstream specification to account for it (not feasable at the moment because it would require something like typeclass conditioned predicates).Redefining
findto an specialized and optimized version is not a desirable solution, as we expect changes improving the static checks to keep code simple and idiomatic.A solution exists already in 93549e8 , where explicit recursion is used instead of
findinfindEndpoint, resulting in a simple idiomatic definition. However, I deem this a no-go given the performance penalty this change incurs (see commit description for a benchmark comparison).