coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Question about tacargs
- Date: Mon, 4 Apr 2016 10:52:07 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f54.google.com
- Ironport-phdr: 9a23:2ePYRRBW1V5K9lcPLDn4UyQJP3N1i/DPJgcQr6AfoPdwSP74rsbcNUDSrc9gkEXOFd2CrakU26yN7Ou/CSQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTnkbvtsMKDKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1kbVGwKkhNOSyzI7Q/3WIu55in9sOt+1S2XMOX5SLk1XXKp6KI9G0ygszsOKzNsqDKfscd3lq8O+B8=
On 04/04/2016 09:29 AM, scott constable wrote:
Jonathan,
Thanks for the quick response. I have two follow-up questions:
1. Based on your description, it seems as though arguments to Ltac sometimes
are call-by-value (i.e. the first exactor') and at other times are
call-by-name (i.e. the second exactor'). Is this statement correct?
My understanding is that it is not quite correct. I think Ltac is always call-by-value, but that what happens during arg evaluation depends on the contents of the arg. Most tactic expressions are evaluated to tactics. A tactic expression that "is" a match variant is special in that during the evaluation-of-tactic-expression-to-tactic, it executes. This, for example, means that one can simulate call-by-value for any tactic using a trivial match tactic:
Ltac callByValue tac := match goal with _ => tac end.
2. If the answer to (1) was "Yes," then is there a general rule to determine
whether an argument will be evaluated by call-by-value or call-by-name?
Perhaps, if in my best Bostonian accent, I say, "Bewaa-ah the Ides of Maahch!" ;)
About a month ago, Gabriel Scherer mentioned this interesting article:
Another complementary document is
An Operational Foundation for the Tactic Language of Coq
Wojciech Jedynak, Małgorzata Biernacka, Dariusz Biernacki
2013
http://www.ii.uni.wroc.pl/~mabi/papers/PPDP13.pdf
It describes the dynamic semantics of a small fragment of Ltac, focusing in
particular on the subtle backtracking semantics of pattern-matching.
-- Jonathan
- [Coq-Club] Question about tacargs, scott constable, 04/03/2016
- Re: [Coq-Club] Question about tacargs, Jonathan Leivent, 04/03/2016
- Re: [Coq-Club] Question about tacargs, scott constable, 04/04/2016
- Re: [Coq-Club] Question about tacargs, Jonathan Leivent, 04/04/2016
- Re: [Coq-Club] Question about tacargs, scott constable, 04/04/2016
- Re: [Coq-Club] Question about tacargs, Jonathan Leivent, 04/03/2016
Archive powered by MHonArc 2.6.18.