Numeric constraint disjunctions

[rybla]

As a generalization of #701, a signature's constraints could be allowed to include up to one numeric constraint disjunction. A numeric constraint disjunction has the form

(c, ..., c) \/ ... \/ (c, ..., c)

where each disjunct is a conjunction of numeric constraints that are not disjunctions.

The implementation of a function that has a numeric constraint disjunction in its signature needs to include a branch for each disjunct (i.e. case) of the disjunction. For example, as well as some proposed syntax, the following declares a function bar which requires n to either be 1 or divisible by 2.

bar : {n} {fin n, n == 1 \/ n % 2 == 0) => [n] -> [n]
bar `(n == 1) [x] = ...
bar `(n % 2 == 0) xs = ...

Each case of such a declaration can be type checked by including the case's disjunct into the assumed constraints and then typechecking the body of the case as usual.

There need not be any exhaustivity or exclusivity check over the disjunction. In the case of overlapping cases, the first matching case will be chosen at runtime, but nothing at typecheck-time is affected.

This feature generalizes #701 since that feature is the same as the feature proposed here, except with an additional requirement of exhaustivity (and perhaps also exclusivity) as the entire disjunction encoded by the pattern matching is assumed to always be satisfiable, since the domain of the disjunction cannot be specified in the top-level type of the declaration.

#701 gives some justifications for why constraint-aware conditioning can be useful, and this proposal allows for conditioning on disjunctions of constraints which may not be exhaustive.

• If a function requires a size from a discrete set, then this set can be specified as a disjunction of equalities e.g. foo : {n} (n == 128 \/ n == 256 \/ n == 512) [n] -> [n].
• If a function requires a size from a discontinuous set, then this set can be specified as a disjunction of constraints e.g. foo : {n} (n == 0 \/ n == 2 \/ n >= 4) [n] -> [n].
• TODO: actual use cases in example implementations