Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: ML antiquotations for type construct...


view this post on Zulip Email Gateway (Sep 22 2021 at 10:50):

From: Makarius <makarius@sketis.net>
* ML *

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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 22 2021 at 11:16):

From: Peter Lammich <lammich@in.tum.de>
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

view this post on Zulip Email Gateway (Sep 22 2021 at 11:59):

From: Makarius <makarius@sketis.net>
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


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 22 2021 at 12:15):

From: Peter Lammich <lammich@in.tum.de>

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])

Unfortunately, the translation sacrifices quite some readability. In my
latest developments (not yet in AFP), I'd use @{mprop "(_,?a)∈_"} for
the above pattern, which is even more concise.

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'.

view this post on Zulip Email Gateway (Sep 22 2021 at 15:50):

From: Makarius <makarius@sketis.net>
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


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 29 2021 at 09:43):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Excellent!

The abstraction form syntax is not so trivial to grasp, maybe one
example coulde be added to the NEWS, e. g.

val dest_add_nat = \<^Const_fn>‹Groups.plus \<^Type>‹nat› for a b =>
‹(a, b)››

Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Sep 29 2021 at 09:58):

From: Makarius <makarius@sketis.net>
In Isabelle/b9331caf92c3, I have updated the above examples using
Type_fn/Const_fn (they were from an earlier stage, before these extra
antiquotations).

Also note that in Isabelle/e585e5a906ba, I have tune the syntax to allow the
\<^Type>‹nat› in your example stand on its own, without an extra cartouche
around it.

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 29 2021 at 10:20):

From: Makarius <makarius@sketis.net>
Update for Isabelle/e585e5a906ba:

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

Thus it is a bit more concise and to the point: no extra nesting of cartouches.

Are there any remaining uses of your alternative antiquotations that are not
covered properly by the new official scheme?

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Oct 02 2021 at 08:51):

From: Norbert Schirmer <nschirmer@apple.com>
In AutoCorres there are also alternative antiquotations for matching and building terms, similar to the ones presented by Peter:
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy>

Also I see great potential for providing similar antiquotations also for cterms, offering the possibility to ‘match’ sub-cterms and build cterms from certified sub-cterms. In contrast to terms also the matching part will result in a matching function, as cterms are an abstract data type.

In my experience recertifying cterms in proof tools like simprocs or tactics can easily become a performance hot-spot when terms become large.

As taking apart and recombining cterms manually with functions like Thm.dest_comb / Thm.apply is quite verbose and hard to maintain it rarely is used in practise. Instead terms are decomposed by ML-matching, recombined and recertified. In the presence of your new antiquotations this idiom is likely to become even more attractive and commonplace.

Having antiquotations for cterms can be a powerful show-case for the potential of antiquotations, bringing together readability / conciseness as well as scalability.

Regards,
Norbert

view this post on Zulip Email Gateway (Oct 13 2021 at 21:05):

From: Makarius <makarius@sketis.net>
On 02/10/2021 10:51, Norbert Schirmer wrote:

In AutoCorres there are also alternative antiquotations for matching and
building terms, similar to the ones presented by Peter:
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy > https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy

I have looked through this a bit, with the same questions in mind: What are
the remaining uses of these @{mk_term} and @{term_pat} antiquotations? Would
these antiquotations be introduced today, as replacement or improvement over
the new \<^Type> and \<^Const> forms?

My impressions so far:

* @{term_pat} is potentially more relevant, but hardly used in that code
base at all. Most applications are actually tests, to demonstrate what it is
supposed to be. It could be very easily eliminated and simplified, using the
new antiquotations from Isabelle2021-1.

* @{mk_term} has more actual applications, but about 30% very basic that
could be done with the same amount of text with \<^Type> and \<^Const>; 30%
involve relatively complex terms like this:

@{mk_term "ran (RangeMap.lookup_range_tree ?tree)" (tree)} tree_const
|> Thm.cterm_of ctxt

It might be actually better to produce a closed @{cterm} with lambdas inside,
and use cterm application in ML --- it would avoid rechecking the whole cterm.

Moreover, the antiquotation itself contains hidden Term.fastype_of: another
relatively costly operation (for complex terms).

The whole point of the new \<^Const> antiquotation is to cultivate a view of
Consts.typargs almost everywhere, with very little recomputation of types for
subterms (no more Term.fastype_of).

This technique also has the potential to simplify the ML source complexity, at
least in the most common cases. Sometimes there are tough situations seen in
the wild, where ML operates in rather non-standard ways on terms, like working
morally ill-typed constants.

Also I see great potential for providing similar antiquotations also for
cterms, offering the possibility to ‘match’ sub-cterms and build cterms from
certified sub-cterms. In contrast to terms also the matching part will result
in a matching function, as cterms are an abstract data type.

In my experience recertifying cterms in proof tools like simprocs or tactics
can easily become a performance hot-spot when terms become large.

That is a separate concern, independent of the question of concrete term
syntax vs. abstract ML syntax.

We do waste a lot in frequent ctyp_of/cterm_of operations, but doing it
differently is quite a lot of work.

Also note that the cterm destructors are not for free either. In particular,
Thm.dest_abs needs to replace a de-Bruijn Bound by a fresh Free. Over the
years I have fine-tuned this a lot, with measurable impact; the latest update
is here:
https://isabelle.sketis.net/repos/isabelle/annotate/21a20b990724/src/Pure/term.ML#l966

(Staring at this again, I immediately see further potential for improvement,
like an explicit Name.context as argument, taken from the implicit
Proof.context of the application.)

As taking apart and recombining cterms manually with functions like
Thm.dest_comb / Thm.apply is quite verbose and hard to maintain it rarely is
used in practise. Instead terms are decomposed by ML-matching, recombined and
recertified. In the presence of your new antiquotations this idiom is likely
to become even more attractive and commonplace.

The state-of-the art is to decompose the Thm.term_of view of cterms and
re-certify. The cost for that is well-known, but could be trimmed down a bit
by treating the types within terms more carefully (or by reducing them via
Consts.typargs as hinted above).

Having antiquotations for cterms can be a powerful show-case for the potential
of antiquotations, bringing together readability / conciseness as well as
scalability.

This sounds like marketing-speak.

Note that too much complexity in ML antiquotations can degrade the robustness
and maintainability of ML tools. For example, too much concrete syntax will
lead to surprises after inevitable changes of abbreviations, translations etc.
over the years / decades.

With \<^Type> / \<^Const> everything is clear and well-defined.

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Oct 14 2021 at 07:07):

From: Norbert Schirmer <nschirmer@apple.com>

On 13. Oct 2021, at 23:05, Makarius <makarius@sketis.net> wrote:

My impressions so far:

@{mk_term "ran (RangeMap.lookup_range_tree ?tree)" (tree)} tree_const
|> Thm.cterm_of ctxt

It might be actually better to produce a closed @{cterm} with lambdas inside,
and use cterm application in ML --- it would avoid rechecking the whole cterm.

Moreover, the antiquotation itself contains hidden Term.fastype_of: another
relatively costly operation (for complex terms).

Meanwhile there are many more applications of the two antiquotations.
We plan to release these extensions of the AutoCorres code-base following Isabelle2021-1.

The whole point of the new \<^Const> antiquotation is to cultivate a view of
Consts.typargs almost everywhere, with very little recomputation of types for
subterms (no more Term.fastype_of).

You are right with the cost of Term.fastype_of. But many use-cases of
@{mk_term} are situations where the term size is under control of the actual code.
There is no additional user-space input coming in. E.g. think of something like the
@{command record} where you have to generate lots of lemmas about
field lookup / update etc. There something like @{mk_term} leads to very readable and compact code
to generate the terms for the propositions.

Having antiquotations for cterms can be a powerful show-case for the potential
of antiquotations, bringing together readability / conciseness as well as
scalability.

This sounds like marketing-speak.

What I like about the application here is that the antiquation in a sense stretches the type-system of ML.
What results in a sequence of combinator applications becomes an atomic entity.

Note that too much complexity in ML antiquotations can degrade the robustness
and maintainability of ML tools. For example, too much concrete syntax will
lead to surprises after inevitable changes of abbreviations, translations etc.
over the years / decades.

With \<^Type> / \<^Const> everything is clear and well-defined.

That is certainly true. The more syntax is involved the more can go wrong. But in my experience with these antiquotation so far this
falls in the category of “benign” issues. Meaning that you will hit the problem quite early. In the best case
already at compile time. Or if that does not work the problem manifests upon every and thus already the first actual usage of the antiquotation.
In those situations the benefits of a readable and concise term overweight.

Norbert


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Oct 14 2021 at 07:49):

From: Peter Lammich <lammich@in.tum.de>
Hi all.

The whole point of the new \<^Const> antiquotation is to cultivate
a view of
Consts.typargs almost everywhere, with very little recomputation of
types for
subterms (no more Term.fastype_of).

You are right with the cost of Term.fastype_of. But many use-cases of
@{mk_term} are situations where the term size is under control of the
actual code.
There is no additional user-space input coming in. E.g. think of
something like the
@{command record} where you have to generate lots of lemmas about
field lookup / update etc. There something like @{mk_term} leads to
very readable and compact code
to generate the terms for the propositions.

I'm also, in many cases, in favour of clear and readable code over
efficient and less readable. (That's the reason why we use functional
programming for Isabelle, in first place!)

Having antiquotations for cterms can be a powerful show-case for
the potential
of antiquotations, bringing together readability / conciseness as
well as
scalability.

This sounds like marketing-speak.

What I like about the application here is that the antiquation in a
sense stretches the type-system of ML.
What results in a sequence of combinator applications becomes an
atomic entity.

Note that too much complexity in ML antiquotations can degrade the
robustness
and maintainability of ML tools. For example, too much concrete
syntax will
lead to surprises after inevitable changes of abbreviations,
translations etc.
over the years / decades.

With \<^Type> / \<^Const> everything is clear and well-defined.

That is certainly true. The more syntax is involved the more can go
wrong. But in my experience with these antiquotation so far this
falls in the category of “benign” issues. Meaning that you will hit
the problem quite early. In the best case
already at compile time. Or if that does not work the problem
manifests upon every and thus already the first actual usage of the
antiquotation.
In those situations the benefits of a readable and concise term
overweight.

I agree here.

Me, personally, am not yet convinced to switch from the very consise
and high-level mk_term / mpat to the still more verbose and low-level
Type/Const. Obviously, I would like to improve these high-level
concepts, but not at the cost of readability or conciseness, which is
exactly what makes them so appealing.

Peter

Norbert


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Oct 14 2021 at 08:06):

From: Makarius <makarius@sketis.net>
The new \<^Type> / \<^Const> antiquotations are designed to be both
efficient in the runtime, and efficient in the source text (readable,
maintainable).

As usual, it is just a matter to get used to a new way of thinking,
which is actually closer to the old way of direct use of datatype
constructors.

Moreover, the treatment of type arguments is much more concise: the term
(patterns) are rather awkward in that respect: both in the text and at
runtime (fastype_of).

This thread was mainly meant to figure out shortcomings that can be
improved further: this often becomes apparent in concrete use, e.g.
while converting an application to the new format.

(Doing that here and there, I did already see another are of reform,
namely "instantiate" forms for thm, cterm, maybe even term.)

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Oct 14 2021 at 08:22):

From: Peter Lammich <lammich@in.tum.de>
On Thu, 2021-10-14 at 10:06 +0200, Makarius wrote:

On 14.10.21 09:49, Peter Lammich wrote:

I'm also, in many cases, in favour of clear and readable code over
efficient and less readable. (That's the reason why we use
functional
programming for Isabelle, in first place!)

The new \<^Type> / \<^Const> antiquotations are designed to be both
efficient in the runtime, and efficient in the source text (readable,
maintainable).

but they are clearly less concise than mk_term/pat, at least for some
applications.

The usage of mk_term/pat, and the fact that it has been invented at
least twice independently, indicates that there is some sweet spot
here, which, at least for some use cases, allows a very concise
notation.

This still has some problems in other cases (e.g., treatment of types).
However, this should not be a reason for abandoning this promising
find, but to try to understand it further: in what cases is use of
mk_term/pat adequate, and in what cases do we have to fall back to the
more low-level but robust/general Type/Const. Can we even have both:
the benefit of concise treatment of type arguments AND the benefit of
concise, high-level notation?

view this post on Zulip Email Gateway (Oct 14 2021 at 13:15):

From: Makarius <makarius@sketis.net>
All these attempts are rather fragile and incomplete. Over a long time, I used
to tell the story myself, that we should use inner syntax for term patterns
and it never quite worked out.

There are various dimensions in the problem that should not be collapsed:

* Patterns should be considered separately from expressions (but: the new
\<^Type>/\<^Const> antiquotations are so elementary and close to ML that they
can do both).

* Expressions can be easily used with concrete syntax, e.g. a version of
@{term} / @{cterm} / @{thm} combined with instantiation (Thm.instantiate): I
have started to think about that some weeks ago, and might manage to do
something for the release. This will supersede earlier attempts like @{mk_term}.

* Genuine cterms are probably better treated like the core logic does, e.g.
with Thm.match / Thm.first_order_match. Instead of raw decomposition of cterms
(with awkward invention of frees for bounds), regular matching can treat
binders directly.

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 04 2024 at 10:08 UTC