Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle Cookbook example

Email Gateway (Aug 18 2022 at 16:04):

From: Steve W <s.wong.731@gmail.com>
Hi all,

I'm reading the Isabelle Cookbook and trying some of the examples provided.
There's something I don't quite understand: I'm looking at the June 8, 2010
version and on page 22, there's an example on implementing a custom
antiquotation:

"let
val parser = Args.context

fun term_pat (ctxt, str) =
...

end"

Then there's an example on calling this antiquotation:

@{term_pat "Suc (?x::nat)"}

Since term_pat takes two arguments ctxt and str, how come the antiquotation
@{term_pat "Suc (?x::nat)"} only has one argument?

Thanks for the help.

Steve

Email Gateway (Aug 18 2022 at 16:05):

From: Makarius <makarius@sketis.net>
The context is implicit here. The ML compilation takes place in a certain
Isar text, and the formal context (at compile time) is derived from that
position.

Makarius

Email Gateway (Aug 18 2022 at 16:05):

From: Steve W <s.wong.731@gmail.com>
On Mon, Sep 13, 2010 at 7:32 PM, Makarius <makarius@sketis.net> wrote:

On Mon, 13 Sep 2010, Steve W wrote:

there's an example on implementing a custom antiquotation:

"let
val parser = Args.context

fun term_pat (ctxt, str) =
...

end"

Then there's an example on calling this antiquotation:

@{term_pat "Suc (?x::nat)"}

Since term_pat takes two arguments ctxt and str, how come the
antiquotation
@{term_pat "Suc (?x::nat)"} only has one argument?

The context is implicit here. The ML compilation takes place in a certain
Isar text, and the formal context (at compile time) is derived from that
position.

I see. Even if the context is implicit, does the position of the argument
'str' not matter? 'str' is the second argument of term_pat, but "Suc
(?x::nat)" is in the first position in @{term_pat "Suc (?x::nat)"}.

Thanks

Makarius

Email Gateway (Aug 18 2022 at 16:05):

From: Makarius <makarius@sketis.net>
I do not really understand the question. The parser for the antiquotation
is defined like this:

val parser = Args.context -- Scan.lift Args.name_source

This means it produces a pair (ctxt, str) in exactly that way. The
context for Args.context is provided by the infrastructure -- these
parsers are context-sensitive.

Makarius

Email Gateway (Aug 18 2022 at 16:07):

From: Steve W <s.wong.731@gmail.com>
On Tue, Sep 14, 2010 at 1:17 PM, Makarius <makarius@sketis.net> wrote:

On Mon, 13 Sep 2010, Steve W wrote:

"let

val parser = Args.context

fun term_pat (ctxt, str) =
...

end"

Then there's an example on calling this antiquotation:

@{term_pat "Suc (?x::nat)"}

Since term_pat takes two arguments ctxt and str, how come the
antiquotation
@{term_pat "Suc (?x::nat)"} only has one argument?

The context is implicit here. The ML compilation takes place in a
certain
Isar text, and the formal context (at compile time) is derived from that
position.

I see. Even if the context is implicit, does the position of the
argument 'str' not matter? 'str' is the second argument of term_pat, but
"Suc (?x::nat)" is in the first position in @{term_pat "Suc (?x::nat)"}.

I do not really understand the question. The parser for the antiquotation
is defined like this:

val parser = Args.context -- Scan.lift Args.name_source

This means it produces a pair (ctxt, str) in exactly that way. The context
for Args.context is provided by the infrastructure -- these parsers are
context-sensitive.

I see. Could you tell me where '--' and the '>>' infix operators are
implemented?

Thanks
Steve

Makarius

Email Gateway (Aug 18 2022 at 16:07):

From: Makarius <makarius@sketis.net>
Most of this is in src/Pure/General/scan.ML -- the only non-conventional
extension of well-established ideas of combinator parsing is support for
potentially infinite input.

Many textbooks on functional programming explain the general idea, e.g.
Larry's ML book. In the end only some notational details differ, i.e. the
names of the usual cominators, such as "--" for pairing and ">>" for
mapping of results.

Makarius

Email Gateway (Aug 18 2022 at 16:07):

From: Christian Urban <urbanc@in.tum.de>
Makarius writes:

On Wed, 15 Sep 2010, Steve W wrote:

Could you tell me where '--' and the '>>' infix operators are
implemented?

Most of this is in src/Pure/General/scan.ML -- the only non-conventional
extension of well-established ideas of combinator parsing is support for
potentially infinite input.

Many textbooks on functional programming explain the general idea, e.g.
Larry's ML book. In the end only some notational details differ, i.e. the
names of the usual cominators, such as "--" for pairing and ">>" for
mapping of results.

Hi Steve,

These combinators are also explained with examples in the
parsing chapter of the Isabelle programming tutorial.

Hope this helps,
Christian

Last updated: Apr 26 2024 at 08:19 UTC