Fix deferrals #1402
Fix deferrals #1402
Conversation
src/haz3lcore/dynamics/Elaborator.re
Outdated
|
|
||
| let remaining_arg_ty = | ||
| List.length(remaining_args) == 1 | ||
| ? snd(List.hd(remaining_args)) | ||
| : Prod(List.map(snd, remaining_args)) |> Typ.temp; | ||
| DeferredAp(f'', args'') |
There was a problem hiding this comment.
This seems right to me. I don't think we always want the remaining function to be from a product.
There was a problem hiding this comment.
The code still works without this in my test though. So TODO
src/haz3lcore/dynamics/Transition.re
Outdated
| let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) | ||
| and. d1' = | ||
| req_value(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) | ||
| req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) |
There was a problem hiding this comment.
I still don't have a strong sense as to why this needs to be req_final but it remains indet otherwise.
There was a problem hiding this comment.
@Negabinary not sure I understand what req_value was doing here since we still need to handle casts? are casts considered values?
In any case, deferredap should be treated as if it were a lambda, so it should be a value.
Let's chat briefly about this with @7h3kk1d at the beginning of our meeting tomorrow.
There was a problem hiding this comment.
@cyrus- Oh I see, yeah I guess if you still want to do the function cast rules when the function is indet then you do need that to be req_final
There was a problem hiding this comment.
I got all of the cases I can think of working. I'm struggling to find a case that req_final catches that req_value doesn't though. There might be something wrong with Constructor
Before
After