Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Prefix syntax for Bit-Not (NOT and ~~)

Email Gateway (Aug 22 2022 at 20:55):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,

I stumbled over a syntax issue with Bit-Not.

("NOT _" [70] 71)
("~~ _" [70] 71)

This non-regular syntax leads to ambiguities:

term ‹NOT (2 * a)› \<comment>‹Prints as NOT 2 * a›
term ‹(NOT 2) * a› \<comment>‹Prints as NOT 2 * a›
term ‹NOT 2 * a› \<comment>‹Does not parse›

Since NOT is a regular prefix operation, it would be much better to
avoid any tinkering with priorities:

("NOT")
("~~")

The change would require some precedence clarification in the
distribution and AFP, but to me it seems worth the effort.

Cheers,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 20:55):

From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
I’ll probably regret saying this, but I agree, better to clarify this, even if it will be annoying to fix the fallout.

Cheers,
Gerwin

Email Gateway (Aug 22 2022 at 20:55):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gerwin,

I’ll probably regret saying this, but I agree, better to clarify this, even if it will be annoying to fix the fallout.

the problem mainly manifests if NOT is applied to regular prefix operations:

NOT f x ~> NOT (f x)
~~ f x ~> ~~ (f x)

The examples I found so far are all for unary f. Hence there is a good
chance that most required changes can be done using sth like

find -type f -exec perl -i -pe 's/(NOT|~~)\s+([^(]+)\s+([^(]+)/$1 ($2 $3)/g' {} +

(not tested).

Anyway I tend to keep this issue »on hold« for a few more days in case
there is further feedback.

Cheers,
Florian

Cheers,
Gerwin

On 9 Nov 2019, at 21:04, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> wrote:

Dear all,

I stumbled over a syntax issue with Bit-Not.

("NOT _" [70] 71)
("~~ _" [70] 71)

This non-regular syntax leads to ambiguities:

term ‹NOT (2 * a)› \<comment>‹Prints as NOT 2 * a›
term ‹(NOT 2) * a› \<comment>‹Prints as NOT 2 * a›
term ‹NOT 2 * a› \<comment>‹Does not parse›

Since NOT is a regular prefix operation, it would be much better to
avoid any tinkering with priorities:

("NOT")
("~~")

The change would require some precedence clarification in the
distribution and AFP, but to me it seems worth the effort.

Cheers,
Florian

signature.asc

Email Gateway (Aug 22 2022 at 21:01):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now rev. a7d1fb0c9e16.

Florian
signature.asc

Last updated: Apr 18 2024 at 04:17 UTC