Re: [isabelle] Strange interaction between ambiguous syntax and dummy patterns
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and