[isabelle-dev] Ambiguous grammar

[Brian Huffman]

Hello,

I recently found an ambiguity in Isabelle/HOL's grammar:

term "if p then x else y :: 'a"

*** Ambiguous input, 2 terms are type correct:
*** (if p then x else (y::'a::type))
*** ((if p then x else y)::'a::type)
*** Failed to parse term
*** At command "term".

Here is the declaration of "If" from HOL.thy:
consts
  If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)

And here are the relevant entries from "Show me ... inner syntax":
  logic = "if" logic[0] "then" any[0] "else" any[0] => "\<^const>HOL.If" (10)
  logic = logic[4] "::" type[0] => "_constrain" (3)

Note that the "else" argument has no more symbols after it, yet it has
a lower precedence (0) than the entire if-then-else production (10).
(It is OK for the right-hand argument of "_constrain" to have low
precedence, because the syntactic category "type" is completely
separate from "logic", whereas "any" includes "logic".)

I propose that we change the syntax declaration for "HOL.If" to this:
consts
  If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" [0,0,10] 10)

Are there any objections?

Looking through the output of "Show me ... inner syntax", I also find
a few other similar situations:

  logic = "UN" pttrn[0] ":" logic[10] "." logic[0] => "_UNION" (10)
  logic = "UN" any[0] "<" any[0] "." logic[0] => "_UNION_less" (10)
  logic = "UN" any[0] "<=" any[0] "." logic[0] => "_UNION_le" (10)
  logic = "INT" pttrn[0] ":" logic[10] "." logic[0] => "_INTER" (10)
  logic = "INT" any[0] "<" any[0] "." logic[0] => "_INTER_less" (10)
  logic = "INT" any[0] "<=" any[0] "." logic[0] => "_INTER_le" (10)
  (and the xsymbol versions of the same)

  logic = "INF" pttrn[0] ":" logic[10] "." any[0] => "_INF" (10)
  logic = "let" HOL.letbinds[0] "in" any[0] => "_Let" (10)

So the following terms are ambiguous as well:
term "UN x<y. f x :: 'a set"
term "let x = y in f x :: 'a"

I propose to modify the following declarations from HOL.thy and
SetInterval.thy in the same way as "If":

syntax
  "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/
in (_))" 10)

syntax
  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" 10)

Here are some syntax declarations from Complete_Lattice.thy:

syntax
  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./
_)" [0, 10] 10)
  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT
_:_./ _)" [0, 10] 10)
(similarly for UNION)

The second one looks like it is a typo: three slots, but only two
numbers. I'm a bit surprised that this doesn't produce an error
message. Obviously it should be "[0, 0, 10]".

- Brian