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

[Makarius]

*** ML ***

* ML antiquotations for type constructors and term constants:

    \<^Type>‹c›
    \<^Type>‹c T …›       ― ‹same with type arguments›
    \<^Type>_fn‹c T …›    ― ‹fn abstraction, failure via exception TYPE›
    \<^Const>‹c›
    \<^Const>‹c T …›      ― ‹same with type arguments›
    \<^Const>‹c for t …›  ― ‹same with term arguments›
    \<^Const_>‹c …›       ― ‹same for patterns: case, let, fn›
    \<^Const>_fn‹c T …›   ― ‹fn abstraction, failure via exception TERM›

Examples in HOL:

  val natT = \<^Type>‹nat›;
  fun mk_funT (A, B) = \<^Type>‹fun A B›;
  val dest_funT = fn \<^Type>‹fun A B› => (A, B);
  fun mk_conj (A, B) = \<^Const>‹conj for A B›;
  val dest_conj = fn \<^Const_>‹conj for A B› => (A, B);
  fun mk_eq T (t, u) = \<^Const>‹HOL.eq T for t u›;
  val dest_eq = fn \<^Const_>‹HOL.eq T for t u› => (T, (t, u));


This refers to Isabelle/4974c3697fee.

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.


Another motivation: the Const antiquotations already use "typargs", e.g. just
one type T for overloaded "plus", instead of "T => T => T". When all
Isabelle/ML have been upgraded to use that form, we may have a chance to trim
down the redundant type information in datatype term for Const (within a few
years).

This has the potential to speed-up term/type
instantiation/matching/unification considerably: profiles always show a lot of
activity on types, rather than actual term structure.


	Makarius