[isabelle-dev] Ambiguous grammar
Brian Huffman
brianh at cs.pdx.edu
Mon Apr 26 17:16:06 CEST 2010
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
More information about the isabelle-dev
mailing list