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

[Makarius]

On 22/09/2021 14:15, Peter Lammich wrote:
> 
> Btw, the upper end of complexity for term creation @{mk_term} is
> something like:
> 
> @{mk_term "Refine_Basic.bind$(RETURN$(COPY$?p))$?t'"}
> 
> which looks like a lot of effort to write down in plain ML, or with
> basic Const antiquotations. In particular, note that all types in the
> term need to be inferred from the types of ?p and ?t'.

Here is the direct correspondence to the new antiquotations:

theory Scratch
  imports Refine_Imperative_HOL.Sepref_Rules Refine_Imperative_HOL.Sepref_Monadify
begin

ML ‹
  fn p => fn t' =>
    @{mk_term "Refine_Basic.bind$(RETURN$(COPY$?p))$?t'"}›

ML ‹
  fn A => fn B => fn p => fn t' =>
    \<^Const>‹Refine_Basic.bind A B for
      ‹\<^Const>‹RETURN A for ‹\<^Const>‹COPY A for p›››› t'›
›

end


Of course, this needs to be viewed in Isabelle/jEdit, to make the \<^Const>
symbol look nice.

Note that the explicit data-flow concerning the type parameters (for Type and
Const likewise) is intentional: it is the key information without extra
redundancy; it is provided statically from the program structure, instead of
doing Term.fastype_of again at run-time (like your mk_term antiquotation).
That operation is actually called "fastype_of", because re-checking the type
of a term is very slow, but here a few extra checks are omitted compared to
full Term.type_of (this works under the assumption that the term is well-typed).

If we do manage to brush-up our thinking and working with types and terms, we
could get a somewhat smoother system within a few years. See also the thread
on locale performance opened by Norber Schirmer
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-September/msg00034.html


	Makarius