[isabelle] signature of ml_antiquotation.ML: inline, valu... · Mirror: Isabelle Users Mailing List

I fail to understand the signature provided by
Pure/ML/ml_antiquotation.ML (see below).
Can someone explain the meaning of declaration, inline, value, and
special_form? Moreover, what is the meaning of embedded (e.g.
inline vs inline_embedded)?

val value_decl: string -> string -> Proof.context ->
(Proof.context -> string * string) * Proof.context
val declaration: binding -> 'a context_parser ->
(Token.src -> 'a -> Proof.context -> (Proof.context -> string * string)
* Proof.context) ->
theory -> theory
val declaration_embedded: binding -> 'a context_parser ->
(Token.src -> 'a -> Proof.context -> (Proof.context -> string * string)
* Proof.context) ->
theory -> theory
val inline: binding -> string context_parser -> theory -> theory
val inline_embedded: binding -> string context_parser -> theory -> theory
val value: binding -> string context_parser -> theory -> theory
val value_embedded: binding -> string context_parser -> theory -> theory
val special_form: binding -> string -> theory -> theory

Email Gateway (Oct 12 2021 at 15:49):

From: Makarius <makarius@sketis.net>
On 11/10/2021 12:13, Kevin Kappelmann wrote:

Isabelle sources are written for the human reader, but one needs to read them
properly:

0. Overview: read the signatures as entries in "table of contents" of a
module (not as "specifications").

1. Look inside: the definitions in the body tell how things are constructed
from more basic things. Usually there are extra headlines and other clues in
the source text.

2. Look outside: do a hypersearch in Isabelle/jEdit as "induction over the
sources" to see how certain items are being used. This implicitly defines
intended semantics for them, and provides examples.

I don't see this in the published Isabelle2021, which is the implicit context
of this mailing list. If you have a different version, you need to say which one.

The terminology "embedded" refers to Isabelle embedded languages, normally via
cartouches. The idea is also from LISP, but the syntax from myself after
staying > 3 years in France.

Email Gateway (Oct 12 2021 at 16:51):

Thanks for the hints. I am very well aware of what you call an
"induction over the sources" and do it all the time. In this particular
case, however, I got lost because there are no extra headlines and
chasing down the definitions for the flag "embedded" left me puzzled (I
stopped at update_reports in antiquote.ML). I'd find a note about
the meaning of the flag embedded helpful.

Email Gateway (Oct 12 2021 at 17:30):

From: Makarius <makarius@sketis.net>
There is another meta story behind it that is not explained anywhere, but very
implicit in the history of the past 10 years.

The traditional antiquotation syntax @{name args} stems from the early times
of Isabelle/Isar > 20 years ago.

usually with fancy symbol rendering for the control symbol, e.g. \<^verbatim>
for string literals in Isabelle/ML (or verbatim text in LaTeX documents).

The "embedded" antiquotations prefer this syntax, with formal markup to update
sources via "isabelle update_cartouches". Thus there is a chance to
discontinue the old antiquotation syntax eventually. (But that will require to
change syntax e.g. for @{thms} or @{lemma}).

There will be more such "embedded" forms in other sublanguages of Isabelle
without the old antiquote syntax. E.g. in inner syntax (types and terms).

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] signature of ml_antiquotation.ML: inline, valu...

Email Gateway (Oct 11 2021 at 10:14):

Email Gateway (Oct 12 2021 at 15:49):

Email Gateway (Oct 12 2021 at 16:51):

Email Gateway (Oct 12 2021 at 17:30):