The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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