Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange interaction between ambiguous syntax a...

Email Gateway (Aug 22 2022 at 10:00):

From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Hi,

I'm experiencing an unexpected behvior with function definitions that
use both ambiguous syntax and dummy patterns. This happens with
Isabelle 2015 and Isabelle 2014, so it's not a regression. I tried to
find similar reports, but had a hard time coming up with search
terms; apologies if this is a known limitation.

For example, using the following two artificial data declarations,

datatype o1 = O1 unit unit (infixr "?" 70)
datatype o2 = O2 unit unit (infixr "?" 70)

the following function declaration is accepted with an ambiguity
warning,

fun ok :: "o1 ⇒ unit option ⇒ o2" where
"ok (a ? b) (Some c) = () ? ()"

but after replacing the unused 'c' variable by a dummy pattern, an
error is produced.

fun fail1 :: "o1 ⇒ unit option ⇒ unit" where
"fail1 (a ? b) (Some _) = ()"

After manually resolving the ambiguity, the function definition is
accepted:

fun ok1 :: "o1 ⇒ unit option ⇒ unit" where
"ok1 (O1 a b) (Some _) = ()"

So for some reason, a dummy pattern behaves differently from a fresh
variable. What's going on?

Cheers,

Bertram
AmbiguousSyntaxBug.thy

Email Gateway (Aug 22 2022 at 10:13):

From: Makarius <makarius@sketis.net>
On Thu, 28 May 2015, Bertram Felgenhauer wrote:

I'm experiencing an unexpected behvior with function definitions that
use both ambiguous syntax and dummy patterns.

Treatment of ambiguous syntax is inherently fragile -- in internal jargon
it is called "*brute-force disambiguation". Many unexpected things have
happened in the past, and are in fact expected from the approach of it.

For example, using the following two artificial data declarations,

datatype o1 = O1 unit unit (infixr "?" 70)
datatype o2 = O2 unit unit (infixr "?" 70)

the following function declaration is accepted with an ambiguity
warning,

fun ok :: "o1 ⇒ unit option ⇒ o2" where
"ok (a ? b) (Some c) = () ? ()"

but after replacing the unused 'c' variable by a dummy pattern, an
error is produced.

fun fail1 :: "o1 ⇒ unit option ⇒ unit" where
"fail1 (a ? b) (Some _) = ()"
|
| Illegal dummy pattern(s) in term

This particular case is relatively easy to allow, and should be possible
in the next Isabelle release.

Makarius

Email Gateway (Aug 22 2022 at 10:27):

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

I guess dummy parameters are treated differently during type inference.

Maybe this is just an accidental behaviour, but I do not know the details.

Generally, over the last years there has been the tendency to avoid
ambiguous syntax altogether, e.g. using ad-hoc overloading etc.
Isabelle symbols give you access to plenty of unicode glyphs which can
offer alternatives.

Cheers,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC