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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml