Stream: Elpi users & devs

Topic: Support for fixpoints

Enzo Crance (Feb 17 2022 at 17:04):

Hello. I got this error today while trying to print a Coq term:
https://github.com/LPCIC/coq-elpi/blob/ee3c88373d6c0e0ef7bbb9de85a081c48dd88427/src/coq_elpi_glob_quotation.ml#L310

What is this case exactly? Is it because the fixpoint I wanted to quote has several arguments?

IIUC, Coq has 3 ASTs, one for parsing, the global AST is the second one, with names elaborated to their full paths and notations resolved, and the constr thing is the fully-typed one in the kernel. So I wanted to ask why do we need this gterm2lp API? As we already have constr2lp. I thought that one might just let Coq do the first parsing phase then only implement the quote and unquote operations on constr.

Enrico Tassi (Feb 17 2022 at 17:10):

Terms passed to an elpi command are not typechecked yet, unlike the ones you pull from the env.

Enrico Tassi (Feb 17 2022 at 17:11):

You probably passed a fix with no struct annotation (saying which the recursive argument is).

Enrico Tassi (Feb 17 2022 at 17:11):

A more descriptive error message would be better I guess.

Enrico Tassi (Feb 17 2022 at 17:17):

FTR Coq has 3 AST:

• constrexpr is the parsed one
• globterm has notations unfolded, implicit arguments inserted, and name/binder analysis done
• constr is typechecked/typecheckable

Elpi only gives you one, hence g(lob)term2lp and contr2lp

Enrico Tassi (Feb 17 2022 at 17:18):

I believe it is a mistake to have globterms even in Coq, but it is hard to get rid of foe technical reasons

Enrico Tassi (Feb 17 2022 at 17:19):

In particular the "elborator" (pretyper) goes from glob -> constr, which makes it not compose with itself, so we have another typechecker from constr -> constr which you use after the first step...

Enzo Crance (Feb 17 2022 at 17:20):

Thanks for the information.

Enrico Tassi (Feb 17 2022 at 17:21):

I do want elpi commands to take raw (un-elaborated) terms to give them more freedom:

• you can call elaborate-skeleton if you want
• or you can manipualte the terms before that (essential in hierarchy builder for example)

Enzo Crance (Feb 17 2022 at 17:23):

I added the struct annotation and the problem is solved. Now it's the match that fails. But it's not a big deal, I just wanted to see what a term looked like in Elpi in order to learn how fix and match are implemented in HOAS. I'll have a look somewhere else or with a simpler term.

Enrico Tassi (Feb 17 2022 at 17:32):

The match must be simple, on one term and not deep

Enrico Tassi (Feb 17 2022 at 17:34):

fetch Nat.plus for the env and print it, it is what I do in the tutorials

Last updated: Apr 18 2024 at 17:02 UTC