[isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.

[Makarius]

On Wed, 8 Oct 2014, Makarius wrote:

> *** ML ***
>
> * Basic combinators map, fold, fold_map, split_list are available as
> parameterized antiquotations, e.g. @{map 4} for lists of quadruples.

There was an off-list proposal by René Thiemann to define the following 
antiquotation:

   @{map_tuple n} = fn f => fn (x1, .., xn) => (f x1, ..., f xn)

See also AFP/ae1e2e9d56d3.


That actually generalizes the existing pairself combinator, which goes as 
far back as Isabelle86 (at least).  See its unify.ML:

   (*handy functional for tpairs*)
   fun pairself f (x,y) = (f x, f y);

Later we found this handy in many more situations, and it has become part 
of the standard canon long ago.


Maybe we can unify the old and new sprouts further.  What is the canonical 
name for this combinator, potentially with some additional generalization?

How about this?

   ap2 f (x, y) = (f x, f y)
   @{ap n} f (x1, ..., xn) = (f x1, ..., f xn)

Maybe even this as well?

   @{ap n(k)} f (x1, ..., xn) = (x1, ..., f xk, ..., xn)

That might be occasionally useful to map field 1, or 2, or 3 of a triple:
@{ap 3(1)}, @{ap 3(2)}, @{ap 3(3)}.  The existing combinators apfst, apsnd 
fit into the same scheme.

Of course, the Isabelle/Pure bootstrap environment would retain the 
important apfst, apsnd, ap2 (renamed from pairself).


> Isabelle/ML has antiquotations as some kind of macro language.  It can 
> do certain things better than the C preprocessor, although one always 
> needs to be careful to stay within reason.

@{ap n} still seems to be within reason, but @{ap n(k)} might be already 
unreasonable.


Is there a better name for that combinator?

Note that "app" is already defined in the SML97 basis: alias for List.app. 
Also note that "ap1" would be just an instance of "I", and is rarely used 
as such anyway.


 	Makarius

----------------------------------------------------------------------------
                               http://stop-ttip.org
----------------------------------------------------------------------------