Stream: Coq users

Topic: TacArg in ltac


view this post on Zulip liao zhang (May 18 2020 at 11:23):

I am confused with tacarg in Ltac. In the documentation I found,
In tacarg, there is an overlap between qualid as a direct tactic argument and qualid as a particular case of term. I think for split, qualid is a direct tactic argument. Could you give some help about in which case the qualid can be a term for tacarg?

view this post on Zulip Pierre-Marie Pédrot (May 18 2020 at 11:26):

I am not sure I understand what you mean, but Coq terms definitely contain qualified identifiers. Furthermore the split tactic doesn't take arguments, so I don't know what you refer to.

view this post on Zulip Kenji Maillard (May 18 2020 at 11:27):

In the doc, split can only take a binding list...

view this post on Zulip Pierre-Marie Pédrot (May 18 2020 at 11:27):

It's technically split with ..., so I don't think it qualifies as split.

view this post on Zulip liao zhang (May 18 2020 at 11:32):

When I use serapi to execute (Parse () "split."). The result is
(ObjList ((CoqAst ((((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 0) (ep 6))) (VernacExpr () (VernacExtend (VernacSolve 0) ((GenArg raw (OptArg (ExtraArg ltac_selector)) ()) (GenArg raw (OptArg (ExtraArg ltac_info)) ()) (GenArg raw (ExtraArg tactic) (TacArg ((((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 0) (ep 5))) (TacCall ((((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 0) (ep 5))) (((v (Ser_Qualid (DirPath ()) (Id split))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 0) (ep 5))))) ()))))))
It seems that split is recognized as a qualid in Coq. I am confused with will TacArgonly treat qualid as reference to some tactic? Because qualid can also point to many other things like a Constant in Coq.

view this post on Zulip Pierre-Marie Pédrot (May 18 2020 at 11:44):

Ah, this is a SerAPI question then. I have no idea what it does to the AST answer. If it is a mere s-expr reification, then split should just be a string that refers to the ML code defining it in terms of TACTIC EXTEND.

view this post on Zulip Pierre-Marie Pédrot (May 18 2020 at 11:46):

If I am not mistaken, you're confused by the fact that Coq uses qualids for a lot of stuff.

view this post on Zulip Pierre-Marie Pédrot (May 18 2020 at 11:46):

This is true, but it's just that depending on the context a qualid can refer to a lot of different kind of objects.

view this post on Zulip Pierre-Marie Pédrot (May 18 2020 at 11:46):

But the same happens in, say, OCaml.

view this post on Zulip Pierre-Marie Pédrot (May 18 2020 at 11:47):

when you write Foo.bar in OCaml, then depending on the context it'll be a term, a type or a projection for instance

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 11:47):

This is indeed just an automatically derived serialization of the tactic AST @Pierre-Marie Pédrot

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 12:28):

removing noise:

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 12:28):


view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 12:28):

(VernacExpr ()
 (VernacExtend (VernacSolve 0)
  ((GenArg raw (OptArg (ExtraArg ltac_selector)) ())
   (GenArg raw (OptArg (ExtraArg ltac_info)) ())
   (GenArg raw (ExtraArg tactic
    (TacArg (TacCall (Qualid (DirPath ()) (Id split))))))))

Last updated: Jan 28 2023 at 05:02 UTC