Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about tacargs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about tacargs


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page