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?
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.
In the doc, split
can only take a binding list...
It's technically split with ...
, so I don't think it qualifies as split
.
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 TacArg
only treat qualid as reference to some tactic? Because qualid
can also point to many other things like a Constant
in Coq.
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.
If I am not mistaken, you're confused by the fact that Coq uses qualids for a lot of stuff.
This is true, but it's just that depending on the context a qualid can refer to a lot of different kind of objects.
But the same happens in, say, OCaml.
when you write Foo.bar in OCaml, then depending on the context it'll be a term, a type or a projection for instance
This is indeed just an automatically derived serialization of the tactic AST @Pierre-Marie Pédrot
removing noise:
(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: Oct 13 2024 at 01:02 UTC