Stream: Mirror: Isabelle Users Mailing List

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


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

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Dear 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)?

Best wishes,

Kevin

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

view this post on Zulip Email Gateway (Oct 12 2021 at 15:49):

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

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

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.

val special_form: binding -> string -> theory -> theory

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 "special form" is standard in LISP.

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.

Makarius

view this post on Zulip Email Gateway (Oct 12 2021 at 16:51):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Hi Makarius,

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.

Thanks and best wishes,

Kevin.

view this post on Zulip 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.

Approx. 7 years ago, this was refined for control-cartouches:

@{NAME CARTOUCHE}

becomes

\<^NAME>CARTOUCHE

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

Makarius


Last updated: Dec 05 2021 at 22:18 UTC