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

[Makarius]

On 22/09/2021 13:16, Peter Lammich wrote:

> Just as a remark, and maybe "feature request" of what I would like to see, I'm
> using the following antiquotations for several years now. They are in the AFP. 
> https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mpat_Antiquot.html
> https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mk_Term_Antiquot.html
> 
> There is an antiquotation @{mpat} that generates a ML matching pattern from a
> term, and one @{mk_term} that constructs a term. 
> mk_term also tries hard to infer types from the arguments (examples below). 
> 
> These are definitely not include-in-distribution quality yet, as they use a
> hack of identifying term-variables (?x) with ML variables. However, I use them
> a lot, and would like to 
> ultimately see robust and clean means to efficiently match against and
> constructs complex terms from ML level in a readable way.

This looks like enormous complexity, with remaining open questions and
problems. It is like an attempt to implement my postulates from many years
ago, to connect inner syntax somehow to ML.

My current move deviates from that, returning to a more basic and more robust
scheme. Recall these explanations:

> On Wed, 2021-09-22 at 12:50 +0200, Makarius wrote:
>>
>> The question of how to represent outlines for type and term expressions
>> adequately and robustly in Isabelle/ML has remained open for a long time.
>> After 2007/2008, I always thought that we should use more concrete syntax
>> (namely inner syntax).
>>
>> After rethinking it thoroughly, the outcome is now as above. The key idea is
>> to nest ML source inside antiquotations: this has become possible in recent
>> antiquotations \<^try>‹expr› and \<^can>‹expr›.
>>
>> The result looks a bit like enhanced S-expressions from the old LISP days:
>> this fits perfectly well into the idea of antiquotations and nesting of
>> sublanguages via cartouches --- instead of lots of silly parentheses.


So my counter feature request: Can you upgrade your applications to the new ML
antiquotations, and remove your attempt?

Looking briefly at actual uses of @{mpat} in AFP, most of them look very basic.

Here is an example at the upper end in complexity, translated into the new
Type/Const/Const_ scheme:

ML ‹
(*
  fun constraints_of_goal i st =
    case Logic.concl_of_goal (Thm.prop_of st) i of
      @{mpat "Trueprop ((_,?a)∈_)"} => constraints_of_term a
    | _ => raise THM ("constraints_of_goal",i,[st])
*)

  val constraints_of_term: term -> (term * term) list = undefined;

  fun constraints_of_goal i st =
    case Logic.concl_of_goal (Thm.prop_of st) i of
      \<^Const_>‹Trueprop for ‹\<^Const_>‹Set.member _ for ‹\<^Const_>‹Pair _
_ for _ a›› _››› =>
        constraints_of_term a
    | _ => raise THM ("constraints_of_goal",i,[st])
›

Most other uses will be even easier to rephrase.


	Makarius