Stream: Coq devs & plugin devs

Topic: Documentation for ".mlg" file syntax


view this post on Zulip Rodolphe Lepigre (Apr 13 2023 at 12:37):

Is there any decent documentation for the ".mlg" file format? After a quick search, I only found a migration guide from camlp5, which is not really helpful at all. In particular, I'm trying to figure out how I can extend the Ltac syntax in some non-trivial way.

Right now I'm looking for how to:

view this post on Zulip Gaëtan Gilbert (Apr 13 2023 at 12:42):

I guess there's https://github.com/coq/coq/blob/master/dev/doc/parsing.md

view this post on Zulip Rodolphe Lepigre (Apr 13 2023 at 13:58):

Thanks, that look helpful indeed.

view this post on Zulip Rodolphe Lepigre (Apr 13 2023 at 15:22):

That helped, but I'm still very confused as to whether there are "hidden" scopes. For instance, with the following .mlg file, the commented code produces an error saying preident does not exist (in an ARGUMENT EXTEND), while it exists in a TACTIC EXTEND.

DECLARE PLUGIN "my_package.my_plugin"

{

open Ltac_plugin
open Stdarg
open Pltac
open Pcoq

}

TACTIC EXTEND test_tactics
| [ "test" ne_preident_list(l) ] -> { assert false }
END

(* Error: Unbound value preident
ARGUMENT EXTEND test_modifier
| [ "with" ne_preident_list(l) ] -> { assert false }
END
*)

Any clue as to how things work would be appreciated.

view this post on Zulip Gaëtan Gilbert (Apr 13 2023 at 15:41):

I guess it comes from pcoq.prim
no idea how people are supposed to figure it out though :(

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 15:45):

you can look at the generated ml file to have an idea of what the preprocessor does. It's kind of trivial.

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 15:46):

this kind of discrepancy is due to the fact that we abuse the names to describe different objects

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 15:46):

this relies on a naming convention

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 15:47):

here there is probably a problem between a grammar entry called preident and a generic argument called wit_preident, one of those is in scope but not the other

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 15:48):

given the open statements above, I'd lean towards the grammar being in scope and the genarg not

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 15:49):

try open Stdarg somewhere

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 15:51):

Ah, yes, this is the other way around and @Gaëtan Gilbert is right. You need to open Pcoq.Prim instead.

view this post on Zulip Rodolphe Lepigre (Apr 13 2023 at 15:56):

I see, thanks for the clarification! I did spend a bit of time looking at the generated code, I guess I'll have to do that some more! :laughter_tears:

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 09:46):

I'm starting to loose my mind with parsing... Here is a minimal example of what I am trying to achieve:

DECLARE PLUGIN "my_package.my_plugin"

{

open Ltac_plugin

open Stdarg
open Pcoq.Prim
open Pcoq.Constr
open Pltac
open Hints

type cgc = Ltac_pretype.closed_glob_constr

type 'a modifier =
  | Using of 'a

let my_tactic : cgc modifier list -> unit Proofview.tactic = fun _ ->
  Tacticals.tclIDTAC

(*
let wit_my_modifier :
    (Constrexpr.constr_expr modifier,
     Genintern.glob_constr_and_expr modifier,
     Ltac_pretype.closed_glob_constr modifier) Genarg.genarg_type =
  let wit = Genarg.make0 "my_modifier" in
  Geninterp.register_val0 wit None; wit
*)

}

ARGUMENT EXTEND using_uconstr
TYPED AS uconstr
| [ "using" uconstr(lem) ] -> { lem }
END

ARGUMENT EXTEND modifier
(*TYPED AS my_modifier*)
| [ "using" uconstr(lem) ] -> { Using(lem) }
END

TACTIC EXTEND my_tactic
| [ "xxx" "using" uconstr(lem) ] -> { my_tactic [Using(lem)] }
| [ "yyy" using_uconstr(lem)   ] -> { my_tactic [Using(lem)] }
(*| [ "zzz" modifier(m)          ] -> { my_tactic [m]          }*)
END

Basically, I want the zzz version because I want to be able to add "modifiers" in a modular way. So what I think I understand after looking at a bunch of examples for the Coq repo and trying many combinations is the following:

Removing the three commented-out blocks of code, I get a version that type-checks, but then fails at runtime with Error: Anomaly "intern function not found: my_modifier.. This makes sense, because I never explained that the 'a modifier can account for the three levels of interpretations by injecting a different version of uconstr. However, I have no idea how I'm supposed to do that.

view this post on Zulip Gaëtan Gilbert (Apr 17 2023 at 10:09):

you need to register the wit in genintern.register_intern0 and geninterp.register_interp0
you may also want to register with genintern.register_subst0 to support being used in Ltac definitions from module types, functors, included and aliases modules

view this post on Zulip Gaëtan Gilbert (Apr 17 2023 at 10:10):

cf

./plugins/ltac/tacintern.ml:800:  Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c));
./plugins/ltac/tacinterp.ml:2159:  register_interp0 wit_uconstr (fun ist c -> Ftactic.enter begin fun gl ->
./plugins/ltac/tacsubst.ml:294:  Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 12:17):

Great, that's exactly what I was looking for! Thank you!

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 13:33):

Thanks to your pointer, I was able to make my code work, with one exception: variables from the environment cannot be used in a "modifier" (I get Error: The variable x was not found in the current environment.). Is there anything special that I need to do to allow such variables? It seems to me that I'm threading through the ist variable correctly, but is that the only thing I need to pay attention to?

view this post on Zulip Gaëtan Gilbert (Apr 17 2023 at 13:35):

please show your code

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 13:41):

This is what I have for the "wit" part.

type 'a usable_lemma = bool * 'a

type 'a br_modifier =
  | Using of 'a usable_lemma list

let map_modifier : ('a -> 'b) -> 'a br_modifier -> 'b br_modifier = fun f m ->
  let map (must_use, lemma) = (must_use, f lemma) in
  match m with
  | Using(ls) -> Using(List.map map ls)

type full_modifier = Ltac_pretype.closed_glob_constr br_modifier

let wit_br_modifier :
    (Constrexpr.constr_expr br_modifier,
     Genintern.glob_constr_and_expr br_modifier,
     Ltac_pretype.closed_glob_constr br_modifier) Genarg.genarg_type =
  let wit = Genarg.make0 "br_modifier_grammar" in
  let intern ist m =
    (ist, map_modifier (Ltac_plugin.Tacintern.intern_constr ist) m)
  in
  Genintern.register_intern0 wit intern;
  let interp ist m =
    Ftactic.enter @@ fun gl ->
    let env = Proofview.Goal.env gl in
    let p = Tacmach.project gl in
    let m = map_modifier (Ltac_plugin.Tacinterp.interp_uconstr ist env p) m in
    Ftactic.return Geninterp.(Val.inject (val_tag (Genarg.Topwit(wit))) m)
  in
  Geninterp.register_interp0 wit interp;
  let subst subst m =
    map_modifier (Ltac_plugin.Tacsubst.subst_glob_constr_and_expr subst) m
  in
  Genintern.register_subst0 wit subst;
  Geninterp.register_val0 wit None; wit

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 13:49):

(Note that this code is for a slightly more general version of the plugin than what I showed before, but the only difference is the list I think.)

view this post on Zulip Gaëtan Gilbert (Apr 17 2023 at 13:49):

then it's used with

| [ "zzz" modifier(m)          ] -> { my_tactic [m]          }

and my_tactic is fun _ => idtac?
what about the .v?

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 13:53):

I basically do:

Declare ML Module "...".

Lemma lemma : forall x y z : nat, True.
Proof. auto. Qed.

Goal forall x y z : nat, True.
Proof.
  intros.
  zzz (lemma x y z). (* <- This fails saying x is not in scope *)

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 14:00):

OK, I'm super puzzled: I minimized the code to show you something self-contained, and now it works. Must be something silly going on with my more complicated version... I'll investigate on my side, and ask again if I can't find the problem.

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 14:45):

@Gaëtan Gilbert in then end I realized I was just being silly: the error I was getting was not from parsing, but from the implementation of the tactic, in which I was picking the wrong environment... So I don't have any parsing problem left. :wink:


Last updated: May 20 2024 at 22:01 UTC