fac :: Int -> Int
fac n | n == 0 = 1
| n > 0 = n * fac (n - 1)
--fac'nonfail :: Int -> Bool
--fac'nonfail n = n >= 0
{-
FlatCurry representation:
fac :: Int -> Int
fac v1 = case (v1 _impl#==#Prelude.Eq#Prelude.Int 0) of
True -> 1
False -> case (((_impl#>#Prelude.Ord#Prelude.Int) v1) 0) of
True -> v1 _impl#*#Prelude.Num#Prelude.Int (fac (v1 _impl#-#Prelude.Num#Prelude.Int 1))
False -> failed
fac :: Int -> Int
fac v1 = case (v1 == 0) of
True -> 1
False -> case (v1 > 0) of
True -> v1 * (fac (v1 - 1))
False -> failed (*)
Collect information about non-variable cases at (*):
(v1 == 0) = False /\ (v1 > 0) = False
Since "False" is the non-fail condition of failed, a successful proof
should ensure
((v1 == 0) = False /\ (v1 > 0) = False) => False
This is equivalent to
not ((v1 == 0) = False /\ (v1 > 0) = False) \/ False
or
(v1 == 0) = True \/ (v1 > 0) = True
Add this as a non-fail condition to fac and verify again.
Now we have to (*) the following collected information:
((v1 == 0) = True \/ (v1 > 0) = True) /\ (v1 == 0) = False /\ (v1 > 0) = False
This is SMT equivalent to
v1 >= 0 /\ v1 /= 0 /\ v1 <= 0
and, thus, unsatisfiable. Hence, the branch is unreachable.
Furthermore, the precondition at the recursive call to fac is
((v1 == 0) = False /\ (v1 > 0) = True)
This implies
(v1 - 1) >= 0
so that the non-fail conditions holds.
Description of the inference method:
------------------------------------
Operations have call types as well as call conditions (Boolean expressions
over the arguments). The latter are initially `True`.
1. Collect non-type representable information in addition to abstract type.
In particular, if the case discriminator is not a variable.
2. If some non-fail condition does not hold, add it to the current
non-fail condition (only if arguments are involved?).
3. Try the proof again.
Call conditions for predefined predicates:
div, mod,...: v2 /= 0
Advantages:
- Improve code by not checking unreachabel branches, i.e., translate
fac n | n == 0 = 1
| n > 0 = n * fac (n - 1)
(after verification) into
fac n | n == 0 = 1
| otherwise = n * fac (n - 1)
-}