Stream: Elpi users & devs

Topic: Flexible term outside pattern fragment


view this post on Zulip Enzo Crance (Mar 08 2023 at 15:06):

I am struggling with this error:

Flexible term outside pattern fragment:
X48 c0 c1 c2 (pglobal (const «...») «...»)

I think it comes from putting variables in a term, then abstracting the term w.r.t. an eigenvariable, then applying the resulting function to a term that is not a variable.

Is there an easy way to remove the non-eigenvariable terms from the scope of the variables? Like an automatic recursive prune operation that would leave only the visible eigenvariables coming from the traversed binders? The only other options I have found to avoid this problem are:

view this post on Zulip Enrico Tassi (Mar 08 2023 at 20:44):

I think you found the root cause, if F is an Elpi function over Coq terms and it contains a unification variable and T is an arbitrary term, then P = F T is a problematic term, it is outside the pattern fragment.

Now, the easiest way to pass a term like P to Coq is to use the @holes! option (it is taken by all APIs taking a term, IIRC).
Another one is to use coq.elaborate. The former prunes, the latter simply ignores the arguments to the hole.

See https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_HOAS.html#outside-the-pattern-fragment and
https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L213-L231


Last updated: May 24 2024 at 21:01 UTC