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