Stream: Coq users

Topic: Number of unfoldings


view this post on Zulip Pierre Vial (Oct 05 2020 at 12:57):

Hello,
Side effects are bad, but I'm in the following situation

let foo .... :=
   let fix bar ... (fun_aux : ....) :=...
   end in let fix foo_aux ... := ...
  end in bar .... foo_aux.

i.e., the function bar takes foo_aux as a parameter.
foo_aux is actually used only once while executing foo but I would like to know how many times it is unfolded as a fixpoint.
I would like to avoid introducing an extra-parameter just for that purpose, because I would need to modify foo (Coq seemingly cannot infer the type of fun_aux if I do not specify it explicitly).

In practice, for the examples I'm considering, foo_aux should be unfolded less thant 10 times, so that would be great to just print "unfold foo_aux" each time it is unfolded

view this post on Zulip Gaëtan Gilbert (Oct 05 2020 at 13:09):

what evaluation strategy?
look into https://github.com/coq-community/reduction-effects/ i guess

view this post on Zulip Pierre Vial (Oct 05 2020 at 13:15):

Cbv and cbn but I don't think it matter that much.
Thanks !


Last updated: Oct 13 2024 at 01:02 UTC