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

[Peter Lammich]

Hi,
nice that term handling from ML gets some attention now.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.
--  Peter
Examples to generate matching patterns from terms:
  fun dest_pair_singleton @{mpat "{(?a,_)}"} = (a)
    | dest_pair_singleton t = raise TERM ("dest_pair_singleton",[t])

  fun dest_nat_pair_singleton @{mpat (typs) "{(?a::nat,?b::nat)}"} =
(a,b)
    | dest_nat_pair_singleton t = raise TERM
("dest_nat_pair_singleton",[t])

  fun dest_pair_singleton_T @{mpat (typs) "{(?a::_ ⇒
?'v_Ta,?b::?'v_Tb)}"} = 
    ((a,Ta),(b,Tb))
    | dest_pair_singleton_T t = raise TERM
("dest_pair_singleton_T",[t])

  fun dest_pair_lambda @{mpat "{(λa _ _. ?Ta, λb. ?Tb)}"} =
(a,a_T,b,b_T,Ta,Tb)
    | dest_pair_lambda t = raise TERM ("dest_pair_lambda",[t])


  fun foo @{mpat "[?a,?b AS⇩s mpaq_Bound ?i,?c AS⇩p [?n]]"} = 
    (a,b,i,c,n)
  | foo t = raise TERM ("foo",[t])

Examples to generate term templates:  fun mk_2elem_list a b = @{mk_term
"[?a,?b]"}
  fun mk_compr s P = @{mk_term "{ x∈?s. ?P x}"}

  val test1 = mk_2elem_list @{term "1::nat"} @{term "2::nat"} |>
Thm.cterm_of @{context}
  val test2 = mk_compr @{term "{1,2,3::nat}"} @{term "(<) (2::nat)"} |>
Thm.cterm_of @{context}

  val test3 = let 
    val x = Bound 0 
    val env = [@{typ nat}]
  in 
    @{mk_term env: "?x+?x"}
  end


On Wed, 2021-09-22 at 12:50 +0200, Makarius wrote:
> *** 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210922/6d53221e/attachment-0001.htm>