Hi all -- is there any way to set the reduction flags manually for the reduction operators like nf_betaiotazeta
and friends in Reductionops? Specifically, we'd like to be able to make a specific list of constants treated as opaque, sort of like the cbv delta -[<list of constants we don't want to unfold>]
tactic. We're looking at the reduction flags in CClosure but not sure where to start. We're specifically on Coq 8.16.1 but any advice would be welcome.
So, I'm on the same project as Audrey so this is more of a continuation of the question than an answer, but my guess was something like this:
let normalize_term ?(opaques=[]) env trm sigma =
let red = all in
let red = red_add_transparent red (Conv_oracle.get_transp_state (Environ.oracle env)) in
let red =
List.fold_right
(fun v red -> RedFlags.red_sub red (make_flag_constant v))
opaques
red
in Reductionops.clos_norm_flags red env sigma trm
I don't know if that's the right idea? before i waste any time trying to get the right opaques list
clos_norm_flags is lazy, did you want cbv?
let red = red_add_transparent red (Conv_oracle.get_transp_state (Environ.oracle env)) in
IIRC this makes it so that any constant marked globally Opaque won't be unfolded even if it's not in your list, is that what you want?
style nitpicks:
env sigma trm
not env trm sigma
Gaëtan Gilbert said:
clos_norm_flags is lazy, did you want cbv?
let red = red_add_transparent red (Conv_oracle.get_transp_state (Environ.oracle env)) in
IIRC this makes it so that any constant marked globally Opaque won't be unfolded even if it's not in your list, is that what you want?
style nitpicks:
- always use List.fold_left instead of List.fold_right if you don't care about the order (fold_left is tailrec)
- conventional order of arguments would be
env sigma trm
notenv trm sigma
Yeah that sounds like the right behavior I think. re:style, env trm sigma
makes things work nicely with the state monad while the other order doesn't
Last updated: Oct 13 2024 at 01:02 UTC