Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Problems with recursion and numeric constraints #1537

Closed
ramsdell opened this issue Jun 27, 2023 · 5 comments
Closed

Problems with recursion and numeric constraints #1537

ramsdell opened this issue Jun 27, 2023 · 5 comments
Labels
typechecker Issues related to type-checking Cryptol code.

Comments

@ramsdell
Copy link

I am playing with the new numeric constraints. I'm trying to write a very silly version of copy that uses recursive descent. However, the obvious way of using numeric constraints fails to type check. I tried other permutations of type annotations, but they all failed. Here is the function:

/* Silly recursive copy */

cpy : {n, a} (fin n) => [2 ^^ n]a -> [2 ^^ n]a
cpy a | n == 0 => a
      | n > 1 => cpy`{n - 1} # cpy`{n - 1}
@ramsdell
Copy link
Author

The way to write this with without numeric constraints is:

rec : {n, a} (fin n) => [2 ^^ n]a -> [2 ^^ n]a
rec a =
    if `n == 0 then a
    else coerceSize (l' # r')
  where
    l # r = coerceSize a
    l' = rec`{max 1 n - 1} l
    r' = rec`{max 1 n - 1} r

coerceSize : {m, n, a} [m]a -> [n]a
coerceSize xs = [ xs @ i | i <- [0 .. <n]]

@yav
Copy link
Member

yav commented Jun 27, 2023

@ramsdell you are missing the argument to cpy in the recursive calls, you probably meant to write something like this:

cpy : {n, a} (fin n) => [2 ^^ n]a -> [2 ^^ n]a                                   
cpy a                                                                               
  | n == 0 => a                                                                     
  | n > 1  => (cpy`{n - 1} x # cpy`{n - 1} y)                                    
                  where (x # y) = a

This fails because Cryptol doesn't know that 2 * 2 ^^ (n - 1) == 2 ^^ n

#1381 is related to this issule

@yav yav added the typechecker Issues related to type-checking Cryptol code. label Jun 27, 2023
@weaversa
Copy link
Collaborator

Another issue is that you've defined the function for n==0 and n>1, but not for n==1.

@ramsdell
Copy link
Author

Yeah, there was a bit of sloppiness last night. Here is the example that works.

/* Silly recursive copy */

cpy : {n, a} (fin n) => [2 ^^ n]a -> [2 ^^ n]a
cpy a | n == 0 => a
      | n > 0 => coerceSize (l' # r')
                 where
                   l # r = coerceSize a
                   l' = cpy`{max 1 n - 1} l
                   r' = cpy`{max 1 n - 1} r

coerceSize : {m, n, a} [m]a -> [n]a
coerceSize xs = [ xs @ i | i <- [0 .. <n]]

@yav
Copy link
Member

yav commented Aug 10, 2023

I am closing this, as we are tracking the exponentiation issues in #1381 and #704

@yav yav closed this as completed Aug 10, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
typechecker Issues related to type-checking Cryptol code.
Projects
None yet
Development

No branches or pull requests

3 participants