[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants

[Norbert Schirmer]

> On 13. Oct 2021, at 23:05, Makarius <makarius at sketis.net> wrote:
> 
> 
> My impressions so far:
> 
>  * @{term_pat} is potentially more relevant, but hardly used in that code
> base at all. Most applications are actually tests, to demonstrate what it is
> supposed to be. It could be very easily eliminated and simplified, using the
> new antiquotations from Isabelle2021-1.
> 
>  * @{mk_term} has more actual applications, but about 30% very basic that
> could be done with the same amount of text with \<^Type> and \<^Const>; 30%
> involve relatively complex terms like this:
> 
>  @{mk_term "ran (RangeMap.lookup_range_tree ?tree)" (tree)} tree_const
>  |> Thm.cterm_of ctxt
> 
> It might be actually better to produce a closed @{cterm} with lambdas inside,
> and use cterm application in ML --- it would avoid rechecking the whole cterm.
> 
> Moreover, the antiquotation itself contains hidden Term.fastype_of: another
> relatively costly operation (for complex terms).
> 

Meanwhile there are many more applications of the two antiquotations.
We plan to release these extensions of the AutoCorres code-base following Isabelle2021-1.


> 
> The whole point of the new \<^Const> antiquotation is to cultivate a view of
> Consts.typargs almost everywhere, with very little recomputation of types for
> subterms (no more Term.fastype_of).
> 
You are right with the cost of Term.fastype_of. But many use-cases of
@{mk_term} are situations where the term size is under control of the actual code. 
There is no additional user-space input coming in. E.g. think of something like the
@{command record} where you have to generate lots of lemmas about 
field lookup / update etc. There something like @{mk_term} leads to very readable and compact code
to generate the terms for the propositions.


> 
> 
>> Having antiquotations for cterms can be a powerful show-case for the potential
>> of antiquotations, bringing together readability / conciseness as well as
>> scalability.
> 
> This sounds like marketing-speak.

What I like about the application here is that the antiquation in a sense stretches the type-system of ML. 
What results in a sequence of combinator applications becomes an atomic entity.

> Note that too much complexity in ML antiquotations can degrade the robustness
> and maintainability of ML tools. For example, too much concrete syntax will
> lead to surprises after inevitable changes of abbreviations, translations etc.
> over the years / decades.
> 
> With \<^Type> / \<^Const> everything is clear and well-defined.
> 
That is certainly true. The more syntax is involved the more can go wrong. But in my experience with these antiquotation so far this
falls in the category of “benign” issues. Meaning that you will hit the problem quite early. In the best case
already at compile time. Or if that does not work the problem manifests upon every and thus already the first actual usage of the antiquotation.
In those situations the benefits of a readable and concise term overweight.

  Norbert