The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

I'm trying to write a tactic in Coq that traverses the subterms of a term and 
adds identity functions around some terms to annotate them. As an example, 
say I had an identity function called 'a'. To annotate this term (where f is 
some function):

f x1 x2 x3...

we wrap each parameter with a call to 'a' like this:

f (a x1) (a x2) (a x3) ...

This is easy to do using Ltac except when dealing with functions with 
different numbers of parameters. The reason is that the Ltac pattern ?f ?x 
will only match with function that have one parameter. This means I need a 
new match clause to handle functions with different numbers of parameters. 
Here is an example Ltac implementation that will work for up to 3 parameters:

Let a := (fun (A:Type) (x:A) => x).

Ltac example x :=
match x with
| ?f ?x ?y ?z => (constr:(f (a x) (a y) (a z)))
| ?f ?x ?y    => (constr:(f (a x) (a y)))
| ?f ?x       => (constr:(f (a x)))
| ?x          => (constr:((a x)))
end.

This approach isn't very elegant. What I really want to be able to do is, 
say, 
when I had the term "plus 1 2", ?f ?x would match as ?f = plus 1 and ?x = 2 
(the curried form). I could then deal with all possible cases with one match 
clause and some recursion.

I could code this at the OCaml level as I can take advantage of the array 
used 
to represent parameters for App constructs but I'd rather use Ltac as Ltac 
gives a higher-level way of dealing with terms. Perhaps I could modify Ltac 
to provide a match construct which allows matching against the curried form? 
Would this be hard to do?

Any suggestions would be much appreciated.

Regards,

Sean