Stream: Elpi users & devs

Topic: Support for fixpoints


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Feb 17 2022 at 17:11):

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

view this post on Zulip Enrico Tassi (Feb 17 2022 at 17:11):

A more descriptive error message would be better I guess.

view this post on Zulip Enrico Tassi (Feb 17 2022 at 17:17):

FTR Coq has 3 AST:

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Enzo Crance (Feb 17 2022 at 17:20):

Thanks for the information.

view this post on Zulip Enrico Tassi (Feb 17 2022 at 17:21):

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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Feb 17 2022 at 17:32):

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

view this post on Zulip 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: Feb 05 2023 at 14:02 UTC