[isabelle-dev] Ambiguous grammar

[Tobias Nipkow]

I think you are right. At least it would mean that the priorities are
brought in line with those of the quantifiers (eg ALL), where the body
has the same priority has the whole construct.

Tobias

Brian Huffman wrote:
> 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
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev