Louise Dubois de Prisque (Nov 08 2021 at 15:40): Louise Dubois de Prisque (Nov 08 2021 at 15:40):Hello everyone,
Is there a way to let the unquote mechanism infer implicit types ? For instance, if I quote the term eq I will get a reified term applied to a tEvar but using this reified evar leads me to an error message if I try to unquote an refied equality which uses it :
MetaCoq Quote Definition eq_reif := eq.
MetaCoq Quote Definition one_reif := 1.
Definition mkEq u v := tApp eq_reif [u; v].
Definition foo_reif := mkEq one_reif one_reif.
MetaCoq Unquote Definition foo := (mkEq one_reif one_reif). (* Anomaly "Evar ?X135 was not declared." Please report at http://coq.inria.fr/bugs/.*)
Thanks in advance for your help !
Yannick Forster (Nov 08 2021 at 15:47):Hey Louise! Yes, you can use a hole:
(* Distributed under the terms of the MIT license. *)
From MetaCoq.Template Require Import utils All.
Import MCMonadNotation.
MetaCoq Quote Definition eq_reif := @eq.
MetaCoq Quote Definition one_reif := 1.
Definition mkEq u v := tApp eq_reif [hole; u; v].
Definition foo_reif := mkEq one_reif one_reif.
MetaCoq Unquote Definition foo := (mkEq one_reif one_reif).
Print foo.
Note that I inserted an @ in front of eq in eq_reif
Louise Dubois de Prisque (Nov 08 2021 at 15:48):Thank you very much for your help!
Yannick Forster (Nov 08 2021 at 15:55):The reason for the @ is that eq has an implicit argument (as can be verified using About), and eq is really @eq ?evar with ?evar being an evar of type Type. In general, I would always use @ when quoting constants in MetaCoq, otherwise you can get strange behaviour
Louise Dubois de Prisque (Nov 08 2021 at 16:01):Do you have a pointer to the evar mechanism in MetaCoq since the main article says it was not implemented at that time ? I am curious about knowing precisely why it is not possible to use the reified evar generated while quoting eq (so @eq ?evar) instead of @eq
Théo Winterhalter (Nov 08 2021 at 16:05):Using the evar directly would not be the expected behaviour I think. If in the future we support evar, unquoting a term with evars should just produce a term with evars don't you think?
Yannick Forster (Nov 08 2021 at 16:06):There is no pointer, because evars are still not properly treated. I don't think anything changed w.r.t. the main article: If you end up with a tEvar after an unquote you are stuck. The only way to morally use evars is via hole
Pierre Vial (Nov 08 2021 at 16:07):@Théo Winterhalter What do you mean "by supporting evar" ? You mean that currently, the complex mechanisms of unification for evars are not formalized in MetaCoq and that it's Coq which is used in the example given by Yannick?
Théo Winterhalter (Nov 08 2021 at 16:08):Yes, there is no unification in MetaCoq at all.
But beyond that, we don't even update the evar map (which collects the constraints and instantiations) I think.
Pierre Vial (Nov 08 2021 at 16:10):Is there unification in the kernel of Coq?
Théo Winterhalter (Nov 08 2021 at 16:11):We're going to areas where I'm not an expert but I don't believe unification is part of the kernel but of elaboration.
Louise Dubois de Prisque (Nov 08 2021 at 16:16):So why the evar tEvar fresh_evar_id [] which corresponds to the term hole is treated by the unquote function?
Yannick Forster (Nov 08 2021 at 16:17):Don't look behind the hole :) It's implemented as an evar, but the right slogan to keep in mind is that evars are not implemented properly and are not treated by the quoting and unquoting mechanisms
Louise Dubois de Prisque (Nov 08 2021 at 16:19):Okay, so if one day the evars are treated by the quoting and unquoting mechanism, I guess that hole would also be implemented differently
Yannick Forster (Nov 08 2021 at 16:20):Yes, I would say that once they are treated properly the more ad-hoc solution with holes goes away. You could but an arbitrary evar there and then run tmUnquote in a way such that evars are solved
Meven Lennon-Bertrand (Nov 09 2021 at 13:26):Pierre Vial said:
Is there unification in the kernel of Coq?
No, but there are evars: AFAIK you must be able to type the term without further solving those evars (so for instance the kernel would type-check refl ?evar : ?evar = ?evar but not refl tt : tt = ?evar while the second one would be treated by the elaboration by unifying tt and ?evar).
Gaëtan Gilbert (Nov 09 2021 at 13:29):no, the kernel rejects evars
Gaëtan Gilbert (Nov 09 2021 at 13:29):https://github.com/coq/coq/blob/21e199784cb8330086b815972c3639c18469d497/kernel/typeops.ml#L611
Meven Lennon-Bertrand (Nov 09 2021 at 13:29):Ah, my bad!
Meven Lennon-Bertrand (Nov 09 2021 at 13:31):I mixed it up with what happens/ed in Matita
Pierre-Marie Pédrot (Nov 09 2021 at 16:10):@Gaëtan Gilbert depends on what you call the kernel, to share code we try to be as resilient as possible w.r.t. evars in the kernel API
Pierre-Marie Pédrot (Nov 09 2021 at 16:10):conversion handles them as variables for instance
Enrico Tassi (Nov 12 2021 at 10:23):Does it? It should have a reflexivity rule for them, not sure it does.
Last updated: Apr 20 2024 at 09:01 UTC