The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

  I'll not really encourage you to do such low-level work on tactic
abstract syntax trees as shown below since these abstract syntax trees
will disappear in the next version of Coq (and are already removed
from the anon cvs repository). What will remain only is the
possibility to define a concrete syntax for already existing tactics
(i.e command "Grammar tactic simple_tactic := ...").

  Then, what I suggest is that you (try to) write first your tactic in
Ltac then, give to it a concrete syntax using this "Grammar tactic
simple_tactic := ...". E.g.

  Tactic Definition GeneralizeHypClear id := Generalize id; Clear id.
  Grammar tactic simple_tactic :=
    gen [ "Generalize" "{" constr:ident($id) "}" ]
    -> [ GeneralizeHypClear $id ].

> I would like to write my own tactical with a variable number of arguments.
> Like Intros: we can use Intros, but also Intros a b.

  Currently (in cvs Coq), there is no way to define a syntax for
tactics with a variable number of arguments, except writing grammar
rules at the ocaml/camlp4 level [plans exist for supporting
intropatterns grammar entry at the Coq level though].

  Regards.

  Hugo
  
Jasper Stein wrote
> Bas Spitters wrote:
> Dear Coq users,
> 
> I would like to write my own tactical with a variable number of arguments.
> Like Intros: we can use Intros, but also Intros a b.
> 
> How would I do this?
> 
> A related question.
> I would like to make a tactical existing of several words.
> Like Unfold: Unfold x in H.
> 
> How would I do this?
> 
> Thanks in advance,
> 
> Bas Spitters
> 
> Hi Bas,
> 
> I don't know if this is possible using Coq's own tactic language L_tac 
> as described in the Reference Manual, but you can try and tap into Coq's 
> parser. Using commands like "Print Grammar tactic tactic" one can try to 
> figure out the way Coq handles other commands with variable numbers of 
> arguments. This may take a bit of work to get some proper understanding, 
> but the results can be rewarding,; in fact, I'd be very surprised if one 
> cannot program exactly those tactics you speak of. New tactic grammar is 
> then entered by "Grammar ..." commands, just as one defines new input 
> grammar for terms. But instead of "Grammar constr constr0" and the like, 
> one now uses e.g. "Grammar tactic simple_tactic" (which is incidentally 
> the grammar parsing the "basic" tactics like Auto, Auto with ..., 
> Rewrite, Apply, etc.) The top-level tactic parser is "tactic tactic", 
> which invokes other more low-level parsers.
> 
> I don't know if they're still on-line, but the Coq v.6.3 reference 
> manuals had some more info on this; otherwise, just ask :-)
>  
> Oh, and I forget, one also needs to analyse the resulting Abstract 
> Syntax Tree (ast) that gets passed to the Coq core. For this I use the 
> following thingy:
> 
> Grammar vernac vernac :=
>   test ["Test" vernac:vernac($a)] -> case [$a] of (JASPER) -> 
> [verygood.] esac.
> 
> This "Test" vernacular command always fails (because nothing results in 
> the ast (JASPER), but the error message one gets is informative enough 
> to play around with and analyse, so that one may eventually write one's 
> own tactics. (One can also use it to view the passed asts for vernacular 
> commands.) Notice one has to somehow enter two (instead of the regular 
> one) full stops when one uses Test.
> 
> E.g. "Coq < Test Apply Lemma with arg1 arg2..
> Toplevel input, characters 0-32
>  > Test Apply Lemma with arg1 arg2..
>  > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> Error: during interpretation of grammar rule test,
>   Grammar case failure. The ast
>   (SOLVE 1
>      (TACTIC
>         (Apply (COMMAND (QUALID Lemma))
>            (BINDINGS (BINDING (COMMAND (QUALID arg1)))
>               (BINDING (COMMAND (QUALID arg2)))))))
>   does not match any of the patterns : (JASPER )
>   with constraints :
>    $a = (SOLVE 1
>            (TACTIC
>               (Apply (COMMAND (QUALID Lemma))
>                  (BINDINGS (BINDING (COMMAND (QUALID arg1)))
>                     (BINDING (COMMAND (QUALID arg2)))))))
> 
> I used this technique myself for writing a tactic "Use" that behaves 
> (grammatically speaking) exactly like Apply (i.e. one can say both "Use 
> lemma1" and "Use lemma2 with arg1 arg2 arg3"), but if the given lemma 
> doesn't apply to the subgoal, it tries one or two other lemma's first, 
> then applies the given argument, and does "Auto with algebra" on all 
> resulting subgoals.
> 
> I suggest playing around with this system for an afternoon or so to find 
> out the exact details.
> 
> Cheers,
> 
> Jasper
> -- 
> +++ Out of Cheese error +++ MELON MELON MELON +++ Redo from Start +++