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.
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? Phil's point was that SML/NJ was complaining about the presence of "op" rather than its absence. I tried an "op" in a datatype in a signature in MLton and it didn't say anything although it's not correct.
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?
Regards, David