Gordon Stewart (Feb 28 2022 at 18:07): Gordon Stewart (Feb 28 2022 at 18:07):I noticed that coq-elpi doesn't appear to implement reification of terms with ltac, conditionals, or some matches yet:
From elpi Require Import locker.
Ltac do_nothing_tac x := exact x.
Fail mlock Definition y (z : nat) := ltac:(do_nothing_tac z).
(* The command has indeed failed with message:
Not Yet Implemented: (glob)HOAS for GHole *)
Fail mlock Definition q (b : bool) := if b then 1 else 0.
(* The command has indeed failed with message:
Not Yet Implemented: (glob)HOAS if-then-else *)
Reification of match works in some cases but not others. For example, the following is fine:
mlock Definition r (b : bool) :=
match b with
| true => 1
| false => 0
end.
but there are other cases that I've run into that fall into this case:
| GCases _ -> nYI "(glob)HOAS complex match expression"
Are any of these issues tracked (reifying ltac-in-terms, conditionals, complex matches) and simple enough for an outside contributor to tackle? I keep asking for features and would like to help implement them to the extent I'm able :-)
Enrico Tassi (Feb 28 2022 at 19:54):for if-then-else it is probably doable, but I did not check carefully.
for the match, the problem is in general hard but in you case simple. Elpi does not type check these terms, but still has to represent them as "constr". The main problem with match is that the type of the scrutinee is not known, but is an integral part of the internal syntax. I bet that if you add in bool then it works. I claim that in general by looking at the branches, one can infer it without typing (the head symbol of the patterns is a constant, eg true which belongs to one and only one inductive. Similarly the if-then-else thing is probably an instance of this.
for tac-in-terms, I really have no clue if this is easy or hard. one would need to delay the "thunk" until typing is in progress, since you can only run a tactic against a goal. But it would be a very nasty Elpi ast, since one has to track z without exposing all ltac syntax...
another thing not supported is double or deep pattern matching. I again claim that one should be able to compile complex match expressions into simpler ones without typing, as above, but the code in Coq is not structured well, so you can't. Refactoring this code is not trivial.
Tracking these limitations is already a good start.
Another possibility is to have a way to tell Elpi to actually elaborate these terms beforehand (this runs ltac, unfolds deep match and so on). It is an important feature that terms are passed "raw", crucial to hierarchy builder, but here it seems counterproductive. So IMO the quickest way to get what you want is to follow this path. One needs to check if the code in coq/vernac/* which elaborates definitions or inductive declarations is accessible, if not make it so, and then find a decent way to signal Elpi that the command mlock wants elaborated inputs (when they are terms).
Gordon Stewart (Mar 07 2022 at 19:57):Thanks, Enrico. I finally got time today to dig into your last suggestion.
There's code in pretyping for elaborating glob_constr to constr:
(** Generic call to the interpreter from glob_constr to constr
In [understand_ltac flags sigma env ltac_env constraint c],
flags: tell how to manage evars
sigma: initial set of existential variables (typically current goals)
ltac_env: partial substitution of variables (used for the tactic language)
constraint: tell if interpreted as a possibly constrained term or a type
*)
val understand_ltac : inference_flags ->
env -> evar_map -> ltac_var_map ->
typing_constraint -> glob_constr -> evar_map * EConstr.t
(** Standard call to get a constr from a glob_constr, resolving
implicit arguments and coercions, and compiling pattern-matching;
the default inference_flags tells to use type classes and
heuristics (but no external tactic solver hook), as well as to
ensure that conversion problems are all solved and that no
unresolved evar remains, expanding evars. *)
val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
...
but it seems like it's not so easy to hook this up to coq-elpi. coq_elpi_glob_quotation.ml appears to quote directly from glob_constr to the coq-elpi HOAS representation.
One needs to check if the code in coq/vernac/* which elaborates definitions or inductive declarations is accessible
I looked around in vernac and found APIs like:
val interp_definition
: program_mode:bool
-> Environ.env
-> Evd.evar_map
-> Constrintern.internalization_env
-> Constrexpr.local_binder_expr list
-> red_expr option
-> constr_expr
-> constr_expr option
-> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicits
but it seems those already operate at the wrong level (constr_expr). Do you have any additional pointers/thoughts?
There's overall not much in vernac related to glob_constr:
vernacentries.ml: let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
vernacentries.ml: Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env sigma))
vernacentries.ml: Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s
vernacentries.ml: Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s
vernacentries.ml: (Constrextern.without_symbols (pr_glob_constr_env env sigma)) ntn sc
prettyp.ml: let c = Notation_ops.glob_constr_of_notation_constr a in
prettyp.ml: [Notation_term.AbbrevRule kn] (pr_glob_constr_env env (Evd.from_env env)) c)
comInductive.ml: let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
starting at constr expr is fine. I do convert into glob constr in elpi by myself in the code handling arguments' hoas iirc. I'll give you a better pointer tomorrow, I'm not on my PC
Enrico Tassi (Mar 08 2022 at 16:49):It is a bit more involved than what I thought. I'll open a PR ASAP, I think it is better if I start the work.
Gordon Stewart (Mar 08 2022 at 17:12):You're definitely much more qualified :-) My main concern, and the reason I offered to try to help, was that I didn't want to overload you with a bunch of feature requests. In this case, though, it seems like supporting tac-in-term is generally pretty useful?
Enrico Tassi (Mar 08 2022 at 18:14):This feature is important for mlock, so I'm OK with it (we hit the limitation about if-t-else also in math comp)
Gordon Stewart (Sep 15 2022 at 15:11):Hey, Enrico. Do you know if any progress has been made on reifying if-then-else and/or deep matches.
We're trying to use coq-elpi in a somewhat pervasive way (to normalize how we specify C++ functions) and have again run into these corner cases in some places.
Gordon Stewart (Sep 15 2022 at 15:57):if-then-else is the bigger blocker for us (we're using a slightly out-of-date coq-elpi but it seems still nYI in the most recent version).
I wonder whether coq-elpi quotation could just desugar if-then-else to match?
Enrico Tassi (Sep 15 2022 at 16:16):The status is that terms passed to commands are now by default elaborated by Coq, so you can use anything (eg mlock should now work for you, full syntax, tac in terms, eval ..).
I guess you talk about quotations inside elpi code, that are still incomplete. Yes, if then else should be desugared to a match, I guess I never wrote the code in coq_elpi_glob_quotation. Unfortunately it is impossible to reuse the code that does so in Coq because it is mixed with type checking, and a quotation is just a fragment, it can't be typed as is.
Gordon Stewart (Sep 15 2022 at 16:20):Oh, interesting. I think we're still using coq-elpi 1.14 (we're waiting to upgrade until we also upgrade to coq 8.16).
Perhaps the behavior is different from 1.14 to the current version of coq-elpi?
Enrico Tassi (Sep 15 2022 at 16:20):If you need that some engineering work is needed in order to refactor coq code, and splut match compilation from typing
Gordon Stewart (Sep 15 2022 at 16:21):Our issue is primarily in terms passed to elpi commands, not term quotation inside elpi code.
Gordon Stewart (Sep 15 2022 at 16:21):So it sounds like the support you added will fix our use case?
Enrico Tassi (Sep 15 2022 at 16:22):Absolutely, see the changelog for 1.15.0
Gordon Stewart (Sep 15 2022 at 16:22):Great, thanks so much for the quick response!
Enrico Tassi (Sep 15 2022 at 16:24):There is also some support for universe polymorphism, thanks to @Enzo Crance . Feedback is welcome since it is a large, still experimental chage. It should not break existing code.
Enrico Tassi (Sep 15 2022 at 16:25):locker is the only code which takes advantage of it, for now.
Gordon Stewart (Sep 15 2022 at 16:29):that's awesome. i should certainly take a closer look at the changelog :-)
Last updated: Oct 13 2024 at 01:02 UTC