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:
ARGUMENT EXTEND
is about (Can it be used to define custom syntactic categories? Probably not.).I guess there's https://github.com/coq/coq/blob/master/dev/doc/parsing.md
Thanks, that look helpful indeed.
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.
I guess it comes from pcoq.prim
no idea how people are supposed to figure it out though :(
you can look at the generated ml file to have an idea of what the preprocessor does. It's kind of trivial.
this kind of discrepancy is due to the fact that we abuse the names to describe different objects
this relies on a naming convention
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
given the open statements above, I'd lean towards the grammar being in scope and the genarg not
try open Stdarg
somewhere
Ah, yes, this is the other way around and @Gaëtan Gilbert is right. You need to open Pcoq.Prim
instead.
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:
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:
uconstr
grammar is interpreted via the Genarg
module, which gives three levels of interpretation ("raw", "glob" and "top"). As part of a TACTIC EXTEND
block, you automatically get the "top" version, which explains why the xxx
case in my example works as I expect.ARGUMENT EXTEND
block the default is different, and the interpretation seems to be fixed to "raw". You can circumvent that by adding a type annotations, which is what I managed to do to make the yyy
example work.zzz
version, I need to somehow need to make the parser understand how to inject the three levels of interpretation in the type. There seems to only built-in support for lists, options and pairs, so I need to implement my own.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.
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
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);
Great, that's exactly what I was looking for! Thank you!
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?
please show your code
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
(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.)
then it's used with
| [ "zzz" modifier(m) ] -> { my_tactic [m] }
and my_tactic is fun _ => idtac
?
what about the .v?
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 *)
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.
@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: Oct 13 2024 at 01:02 UTC