[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants
Peter Lammich
lammich at in.tum.de
Wed Sep 22 13:16:14 CEST 2021
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>
More information about the isabelle-dev
mailing list