search

gmalecha / template-coq

Reflection library for Coq
MIT License
12 stars 0 forks source link

Allow [Eval] in [Quote Definition], or make a [Quote Unfolded Definition] #12

Closed JasonGross closed 9 years ago

JasonGross commented 9 years ago

I want to do something like

Quote Definition foo := Eval unfold bar in bar.

This is useful when bar is built by tactics, or by Eval simpl in baz, etc, and the definition is too long to write out manually. I can mimic this with Quote Recursively, and then pulling out the right constant, but this is slower, especially if there are many dependencies.

gmalecha commented 9 years ago

The code for this exists (https://github.com/gmalecha/template-coq/blob/coq-8.5/src/reify.ml4#L623), but for some reason it isn't being invoked. This is probably due to the fact that both rules occur in the same VERNAC COMMAND EXTEND

JasonGross commented 9 years ago

I will also note that

Quote Definition foo := 1 + 1.

does not work (last I checked), while

Quote Definition foo := (1 + 1).

does work. This might have something to do with it, given that 

Definition foo := (Eval compute in 1 + 1).

is not valid in general.

gmalecha commented 9 years ago

@JasonGross This is fixed in the 8.5 branch (by splitting the definition) but

Quote Definition foo := 1 + 1.

still does not work. I'm not sure how to make it work b/c I don't entirely understand the way the parser works. This seems pretty similar to the rules in parsing/g_vernac.ml4 (as much as I can understand).

@maximedenes: Do you know what I'm missing here? (the code is https://github.com/gmalecha/template-coq/blob/coq-8.5/src/reify.ml4#L629)

gmalecha commented 9 years ago

This is fixed in the 8.5 branch. The solution is to use lconstr rather than constr.