elaboration/type inference while unquoting

[aa755]

It would be great to not have to provide implicit arguments while unquoting. Any ideas on how this can be achieved? Should the input of (a version of) the unquoting function be a Coq equivalent of a Glob_term.glob_constr?

What is the purpose of Ast.tUnknown? Can it be used to stand for implicit arguments that need be inferred by the unquoting function?

[gmalecha]

Ast.tUnknown was used predominantly as a debugging mechanism. It should probably be removed.

I like the idea of going through elaboration, but I'm not sure that we should re-use Ast.tUnknown. In particular, I'm wondering if we should support repeated unification variables, i.e. the ability to put something akin to ?1 in multiple places. The argument against this is that you could always let-bind the unification variables which is probably more efficient.

The other question is how should it be exposed? Should all denotations go through elaboration? Just some?

[aa755]

The denote_term in function in reify.ml4 could keep track of whether it encountered any hole (unification variable) and at the end, call the elaboration to fill them. This would suffice for my use cases.

Is Ast.tMeta desined to denote unification variables? If so, is there an OCaml function of type Term.constr -> Term.constr that takes a term containing occurrences of Term.mkMeta and fill those holes?

[aa755]

I accidentally discovered that the current unquoting already supports inference of implicit arguments. The implementation of unquote first calls Constrextern.extern_constr and passes the result to Command.do_definition. During the process, it seems that implicit arguments are erased and rediscovered. Thus, even garbage Ast.terms are accepted at implicit positions -- see the example below. This is also a bug because, in one instance, unqoting failed with an error saying that Coq was unable to infer implicit arguments, even when I had painfully produced all the implicit arguments. The current workaround for the bug is to clear implicits for the problematic definitions. Perhaps we can have two unqote functions. It would be even better to have only one unquote function that only erases and rediscovers occurrences of a designated subterm, e.g. a new Ast.inferThis in Ast.term

Require Import Template.Template.

Quote Definition xx_syntax := (existT _ 0 (@eq_refl nat 0)).

Make Definition xx := 
(Ast.tApp (Ast.tConstruct (Ast.mkInd "Coq.Init.Specif.sigT" 0) 0)
  [Ast.tInd (Ast.mkInd "THIS.is.now.garbage.no.other.change.in.xx_syntax" 0);
  Ast.tApp (Ast.tInd (Ast.mkInd "Coq.Init.Logic.eq" 0))
    [Ast.tInd (Ast.mkInd "Coq.Init.Datatypes.nat" 0);
    Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0];
  Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0;
  Ast.tApp (Ast.tConstruct (Ast.mkInd "Coq.Init.Logic.eq" 0) 0)
    [Ast.tInd (Ast.mkInd "Coq.Init.Datatypes.nat" 0);
    Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0]]).
(* xx is defined *)

Arguments existT : clear implicits.
Make Definition xxFailed := 
(Ast.tApp (Ast.tConstruct (Ast.mkInd "Coq.Init.Specif.sigT" 0) 0)
  [Ast.tInd (Ast.mkInd "THIS.is.now.garbage.no.other.change.in.xx_syntax" 0);
  Ast.tApp (Ast.tInd (Ast.mkInd "Coq.Init.Logic.eq" 0))
    [Ast.tInd (Ast.mkInd "Coq.Init.Datatypes.nat" 0);
    Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0];
  Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0;
  Ast.tApp (Ast.tConstruct (Ast.mkInd "Coq.Init.Logic.eq" 0) 0)
    [Ast.tInd (Ast.mkInd "Coq.Init.Datatypes.nat" 0);
    Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0]]).
(* Anomaly: Uncaught exception Not_found. Please report. *)