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

[Makarius]

On 02/10/2021 10:51, Norbert Schirmer wrote:
> 
> In AutoCorres there are also alternative antiquotations for matching and
> building terms, similar to the ones presented by Peter:
> https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy
> https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy
> https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy > https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy

I have looked through this a bit, with the same questions in mind: What are
the remaining uses of these @{mk_term} and @{term_pat} antiquotations? Would
these antiquotations be introduced today, as replacement or improvement over
the new \<^Type> and \<^Const> forms?

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).


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).

This technique also has the potential to simplify the ML source complexity, at
least in the most common cases. Sometimes there are tough situations seen in
the wild, where ML operates in rather non-standard ways on terms, like working
morally ill-typed constants.


> Also I see great potential for providing similar antiquotations also for
> cterms, offering the possibility to ‘match’ sub-cterms and build cterms from
> certified sub-cterms. In contrast to terms also the matching part will result
> in a matching function, as cterms are an abstract data type.
> 
> In my experience recertifying cterms in proof tools like simprocs or tactics
> can easily become a performance hot-spot when terms become large.

That is a separate concern, independent of the question of concrete term
syntax vs. abstract ML syntax.

We do waste a lot in frequent ctyp_of/cterm_of operations, but doing it
differently is quite a lot of work.

Also note that the cterm destructors are not for free either. In particular,
Thm.dest_abs needs to replace a de-Bruijn Bound by a fresh Free. Over the
years I have fine-tuned this a lot, with measurable impact; the latest update
is here:
https://isabelle.sketis.net/repos/isabelle/annotate/21a20b990724/src/Pure/term.ML#l966

(Staring at this again, I immediately see further potential for improvement,
like an explicit Name.context as argument, taken from the implicit
Proof.context of the application.)


> As taking apart and recombining cterms manually with functions like
> Thm.dest_comb / Thm.apply is quite verbose and hard to maintain it rarely is
> used in practise. Instead terms are decomposed by ML-matching, recombined and
> recertified. In the presence of your new antiquotations this idiom is likely
> to become even more attractive and commonplace. 

The state-of-the art is to decompose the Thm.term_of view of cterms and
re-certify. The cost for that is well-known, but could be trimmed down a bit
by treating the types within terms more carefully (or by reducing them via
Consts.typargs as hinted above).


> 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.

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.


	Makarius