Improve determinism analysis

[pschachte]

Wybe issues an error message if you call a test procedure or function outside of a test context. So code like

if { lst = [] :: ?z = y
    | else :: ?z = [head(lst) | append(tail(lst), y)]
    }

causes an error, because the calls to head and tailare tests. However, because they appear in a context in which we know lst is not [], they actually can be guaranteed to succeed.

Because determinism errors are detected and reported during type/mode analysis, this must be addressed prior to transformation to LPVM, and since LPVM code is strictly deterministic, determinism errors need to be handled at the AST state, which makes the analysis messier.

I believe the easiest way to handle this would be to maintain sets of mutually exclusive calls, and sets of exhaustive tests. Initially, all the constructors of each type would be recorded as both mutually exclusive and exhaustive. Additionally, we should allow users to declare these sets. For example, the int type would include declarations that <= and > are mutually exclusive and exhaustive, likewise <, =, and >.

Given this information, when compiling code that follows success of a test, we can know that none of the calls that are mutually exclusive with it can succeed. When compiling code that follows failure of a test, we can know that one of the calls it is exhaustive with must succeed. When that set is a singleton, we can record that it must succeed. Thus in the example code above, because we know that and head(lst,?tmp) are exhaustive, in the else branch in that example, because has failed, then the call to head must succeed, and similarly for tail.

[pschachte]

An alternative, which is probably more generally useful, would be to implement a declaration of a disjunction of tests which is promised to be true. For example:

promise x:int < y:int | x = y | x > y
promise lst:list(_) = [] | lst = [_|_]

When mode checking conditionals and disjunction, when one of these tests is seen, we remember that one of the remaining tests in the disjunction must be true in the rest of the disjunction. When we have seen all but one of them in past disjuncts, the final one will be considered to be deterministic, and the Boolean success code returned by the call should not be tested.