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