On 4 Apr 2012, at 11:48, David Matthews wrote:
On 03/04/2012 16:20, Rob Arthan wrote:
On 30 Mar 2012, at 12:52, David Matthews wrote:
Looking carefully at the syntax, though, "op" is not allowed in a datatype specification although in all other respects the syntax of a binding and a specification are the same. I've added an error message if "op" is used in a specification.
I didn't look at the syntax of modules. You are quite right. In fact, as far as I can see, op is not allowed anywhere in a signature.
I've now reduced the error message to a warning since it seems Isabelle has "op" in signatures.
Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply with the standard syntax, even though I was completely unaware that "op" wasn't allowed in signatures.
I hadn't actually realised that "op" was allowed on exception bindings and I've now fixed that. I think a sensible approach is to produce a warning in the cases where a symbol could be used as an infix; in an expression, a fun binding or in a pattern (val binding) and to ignore it in other cases.
I think it is wise to give the warning in those cases, because other compilers are not as liberal as Poly/ML, so I read the warning as a warning about a potential portability problem (and always act on it).
Do any other compilers complain about missing "op" in those cases?
Yes, SML/NJ and MLton don't allow an infix vid without an "op" as an expression or a pattern.
Phil's point was that SML/NJ was complaining about the presence of "op" rather than its absence.
It is only a warning. I think Phil's point was that, as things stood, you couldn't write a datatype declaration with an infix constructor that would not give a warning on one of the two compilers: as was, Poly/ML warned when you didn't use "op" before an infix constructor in a datatype, while SML/NJ warned when you did.
I tried an "op" in a datatype in a signature in MLton and it didn't say anything although it's not correct.
Likewise SML/NJ appears to extend the standard syntax by allowing "op" in datatypes in signature (but giving a warning saying that they are unnecessary).
Out of interest, are you still planning to allow things like "(+)"?
Do you mean something like val p = map (+) rather than val p = map (op +) ? I wasn't planning to since I don't think it's legal ML. Did you mean somewhere else?
No, that is what I meant: Poly/ML 5.4.1 doesn't share your view that it is illegal:
Poly/ML 5.4.1 Release
(+);
Warning-(+) has infix status but was not preceded by op. val it = fn: int * int -> int
map (+);
Warning-(+) has infix status but was not preceded by op. val it = fn: (int * int) list -> int list
This is why I said the warning is useful as it flags a potential portability problem: other compilers won't compile the above.
Regards,
Rob.