-
Notifications
You must be signed in to change notification settings - Fork 47
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
allow generic calls within forloop #189
base: main
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very nice PR!
Left a comment on what I think is a small bug.
Another thing: shouldn't this behavior be implemented also for method calls?
|
||
// rewalk the observed arg expression | ||
// it should throw an error if the arg contains generic vars relating to the variables in the forloop scope | ||
self.compute_type(observed_arg, &mut forbidden_env)?; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think there is a small bug in the handling of the for loop variables. Take this code (just modifying one of the examples)
fn clone(const LEN: Field, val: Field) -> [Field; LEN] {
let mut arr = [0; LEN];
for idx in 0..LEN {
arr[idx] = val;
}
return arr;
}
fn main(pub xx: Field) {
let mut arr3 = [[0; 2]; 2];
for idx in 0..2 {
let cloned = clone(2, xx + idx);
arr3[idx] = cloned;
}
let fst = arr3[0];
let snd = arr3[1];
assert_eq(fst[0], 0);
assert_eq(fst[1], 0);
assert_eq(snd[0], 1);
assert_eq(snd[1], 1);
}
I would expect that adding a nested loop of one iteration inside the one defined do not change any of the emitted constraints, and indeed it works.
for idx in 0..2 {
for unused in 0..1 {
let cloned = clone(2, xx + idx);
arr3[idx] = cloned;
}
}
However, if the LEN
argument is replaced with the outer loop variable
for idx in 0..2 {
for unused in 0..1 {
let cloned = clone(idx, xx + idx);
arr3[idx] = cloned;
}
}
then the nice error about the call of generic function is not returned anymore and instead there is this panic
thread 'main' panicked at src/parser/types.rs:800:14:
generic value not assigned
I'm not really sure what is going on, but a bit of debugging shows that this compute_type
call at this line of code does not return an error in the latter case (maybe it should?).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great spot. I have't thought about this case. Will check it out. Thanks!
This PR is to allow calling generic functions within forloops while preventing it from running into the case of unrolling.
For example, we want to allow generic function calls:
Because the argument LEN is not relating to the variables inside the for loop scope, it is allowed to call the generic function.
But if it is the following case, it won't be allowed:
The checking logic relies on the states of
TypedFnEnv
. When it processes theExpr::Variable
case during type check,TypedFnEnv
will throw error if the condition isn't allowed to load the variable for a generic function call: