Numeric Constraint Guards

[rybla]

This PR implements a new feature: numeric constraint guards.

Addresses #701 and (partially) #1369

Numeric constraint guards are like guards (e.g. Haskell) except that the guarding condition is a numeric constraint that is treated as locally assumed (for the sake of type-checking) in the branch it guards.

f : {n} [n] -> [8]
f x | (n == 0) => g1 x
    | (n <= 4) => g2 x
    | (5 <= n) => g3 x

g1 : [0] -> [8]
g1 x = 1

g2 : {n} (n <= 4) => [n] -> [8]
g2 x = 2

g3 : {n} (5 <= n) => [n] -> [8]
g3 x = 3

Without this feature, f would have to be written verbosely and awkwardly like so as f':

f' : {n} fin n => [n] -> [8]
f' x =
  if n == 1 then g1 (take `{0} x) else
  if n <= 4 then g2 (take `{min 4 n} x)
            else g3 (pad `{5} x)
  where
    n = `n

pad : {m, n} (fin m, fin n) => [n] -> [max m n]
pad = ...

For more complicated constraints, this second kind of implementation becomes more and more cumbersome.

Examples

The following function inits computes the concatenation of all initial sequences of a given sequence, using a tail-recursive style.

// tests/constraint-guards/Inits.cry

inits : {n, a} (fin n) => [n]a -> [(n * (n+1))/2]a
inits xs
  | n == 0 => []
  | n >  0 => go xs' x []
    where
      (x : [1]_) # xs' = xs
      
      go : {l, m} (fin l, fin m, l + m == n, m >= 1) =>
        [l]a -> [m]a -> 
        [((m-1) * ((m-1)+1))/2]a ->
        [(n * (n+1))/2]a
      go ys zs acc
        | l == 0 => acc # zs
        | l >  0 => go ys' (zs # y) (acc # zs)
          where 
            (y : [1]_) # ys' = ys


property inits_correct =
  (inits [] == []) &&
  (inits [1] == [1]) &&
  (inits [1,2] == [1,1,2]) &&
  (inits [1,2,3] == [1,1,2,1,2,3]) &&
  (inits [1,2,3,4] == [1,1,2,1,2,3,1,2,3,4]) &&
  (inits [1,2,3,4,5] == [1,1,2,1,2,3,1,2,3,4,1,2,3,4,5])

// tests/constraint-guards/Len.cry

len : {n,a} (fin n) => [n] a -> Integer
len x
  | (n == 0) => 0
  | (n >  0) => 1 + len (drop`{1} x)

// tests/constraint-guards/Mergesort.cry

sort : {n,a} Cmp a => (fin n) => [n]a -> [n]a
sort xs
  | n <= 1 => xs
  | ()     => merge (sort left) (sort right)
              where (left : [n/2] _) # right = xs

merge : {m,n,a} Cmp a => [m]a -> [n]a -> [m+n]a
merge xs ys
  | m == 0  => ys
  | n == 0  => xs
  | (m > 0, n > 0) => if x <= y 
                        then [x] # merge restX ys
                        else [y] # merge xs restY
                      where
                      [x] # restX = xs
                      [y] # restY = ys

// TODO: more cumbersome example

// TODO: practical everyday examples

Implementation

The significance of this feature is that the guarding numeric constraints are introduced as assumptions locally to the guarded expression.

Immediately after parsing (and the NoPat pass), each guarded expression is expanded into an auxiliary top-level declaration that has the same type signature as the declaration the constraint guards appeared in, but with the guarding constraints appended to its signature's constraint. The original guarded expression is replaced with an appropriate reference to this auxiliary definition.

During typechecking, the guarding constraints of each case are assumed locally before typechecking the guarded expression.

During evaluation, the constraint guards are folded over until a constraint evaluates to True (via evalProp), in which case only that constraints's guarded expression is evaluated as the result.

TODO

• Exhaustive guards checking
  • only implemented a partial checker, since its possible to write exhaustive guards that aren't decidable by the SMT-solver powered typechecker. But, it does handle all the numeric constraints (other than prime) and conjunctions. See Cryptol.TypeCheck.Infer.checkSigB for the implementation. Issues a warning if cannot prove exhaustive.
• Exclusivity checking for a declaration's set of guarding constraints
• What kinds of constraints are allowed in the guarding constraints? Currently allowed are:
  • equality of pair of numeric literals
  • non-equality of pair of numeric literals
  • inequality of pair of numeric literals
  • fin-ness of a numeric literal
  • prime-ness of numeric literal

[yav]

I tried these two examples:

len x = propguards
  | (n == 0) => 0
  | (n > 1) => len (drop`{1} x)

len2 : {n,a} (fin n) => [2^^n] a -> Integer
len2 x = propguards
  | (n == 0)  => 1
  | (n > 1)   => (len2 a + len2 b)
                    where (a,b) = splitAt `{n/2} x

The first one type checked correctly, although I got a panic:

 Message:   cannot use this as a guarding constraint: 
             1 <= n`902

Is that because the evaluator is not yet implemented?

The second one also works correctly from the point of view of this extension, but it reveals some additional facts we need to
teach the solver. I'll make separate tickets for them.

[yav]

@Riib11 I don't think we need the propguards keyword. I tried the following variation, and it seems to work OK:

len : {n,a} (fin n) => [n] a -> Integer
len x 
  | (n == 0) => 0
  | (n > 1) => len (drop`{1} x)

This is all I changed:

-  | var apats_indices '=' propguards
-                           { mkIndexedPropGuardsDecl $1 $2 $4 }
+
+  | var apats_indices '|' propguards_cases { mkIndexedPropGuardsDecl $1 $2 $4 }

[rybla]

I tried these two examples:

len x = propguards
  | (n == 0) => 0
  | (n > 1) => len (drop`{1} x)

len2 : {n,a} (fin n) => [2^^n] a -> Integer
len2 x = propguards
  | (n == 0)  => 1
  | (n > 1)   => (len2 a + len2 b)
                    where (a,b) = splitAt `{n/2} x

The first one type checked correctly, although I got a panic:

 Message:   cannot use this as a guarding constraint: 
             1 <= n`902

Is that because the evaluator is not yet implemented?

The second one also works correctly from the point of view of this extension, but it reveals some additional facts we need to teach the solver. I'll make separate tickets for them.

The first example doesn't work because you didn't quantify n in a signature. And, it should have given you an error when you tried to use propguards in a definition that doesn't have an explicit signature. I'll look in to that.

[rybla]

@Riib11 I don't think we need the propguards keyword. I tried the following variation, and it seems to work OK:

len : {n,a} (fin n) => [n] a -> Integer
len x 
  | (n == 0) => 0
  | (n > 1) => len (drop`{1} x)

This is all I changed:

-  | var apats_indices '=' propguards
-                           { mkIndexedPropGuardsDecl $1 $2 $4 }
+
+  | var apats_indices '|' propguards_cases { mkIndexedPropGuardsDecl $1 $2 $4 }

Awesome! I had added that keyword to deal with an issue getting happy to accept my grammar and couldn't find a better way, but looks like you found one.

[yav]

I think we are almost there, just fix up the error stuff