Stream: Elpi users & devs

Topic: Flexible term outside pattern fragment

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:

• strictly give every type annotation everywhere in the term, but for some cases it is tedious;
• put a dummy eigenvariable and replace it with fresh variables everytime anything external is needed (e.g. typechecking), but it is a lot of bureaucracy.

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: Oct 13 2024 at 01:02 UTC