Stream: Coq devs & plugin devs

Topic: Setting reduction flags for custom normalization


view this post on Zulip Audrey Seo (Mar 12 2024 at 19:47):

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.

view this post on Zulip Talia Ringer (Mar 12 2024 at 22:31):

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

view this post on Zulip Talia Ringer (Mar 12 2024 at 22:32):

I don't know if that's the right idea? before i waste any time trying to get the right opaques list

view this post on Zulip Gaëtan Gilbert (Mar 12 2024 at 22:44):

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:

view this post on Zulip Talia Ringer (Mar 12 2024 at 23:05):

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:

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