From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA30689 for caml-redistribution; Tue, 11 May 1999 10:39:33 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA10511 for ; Mon, 10 May 1999 18:12:08 +0200 (MET DST) Received: from pss-imc-01.microsoft.com (pss-imc-01.microsoft.com [131.107.3.100]) by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id SAA24842 for ; Mon, 10 May 1999 18:12:06 +0200 (MET DST) Received: from mail1.microsoft.com (INET-IMC-01 [157.54.9.125]) by pss-imc-01.microsoft.com with SMTP (Microsoft Exchange Internet Mail Service Version 5.5.2591.0) id KSD9WG55; Mon, 10 May 1999 09:12:06 -0700 Received: by INET-IMC-01 with Internet Mail Service (5.5.2524.0) id ; Mon, 10 May 1999 09:12:03 -0700 Message-ID: <39ADCF833E74D111A2D700805F1951EF0F00BB6B@RED-MSG-06> From: Don Syme To: Manuel Fahndrich , "'caml-list@inria.fr'" Subject: RE: stream pattern [< pat=exp >] and extensions to ordinary patte rn m atching Date: Mon, 10 May 1999 09:12:01 -0700 X-Mailer: Internet Mail Service (5.5.2524.0) Sender: weis An abstract pattern matching language would also be quite useful when implementing theorem provers and other applications that involve a lot of term manipulations. You would like to keep your terms abstract for obvious software engineering reasons. Cheers, Don -----Original Message----- From: Manuel Fahndrich [mailto:maf@microsoft.com] Sent: 07 May 1999 23:28 To: 'caml-list@inria.fr' Subject: stream pattern [< pat=exp >] and extensions to ordinary pattern m atching Hi, I just discovered the stream parser pattern [< pat = exp >] and I was wondering why this kind of pattern is not allowed in regular patterns? It is a very useful construct. For example: Suppose I have some type ast for abstract syntax type ast = Constant of constant | Binary of oper * ast * ast | ... where the type "constant" is not a datatype. There is however a function refine : constant -> con where type con = String of string | Int of int | ... In order to use pattern matching to detect a string constant, I have to use the following two auxiliary functions (which can be defined with what is given): isString : constant -> bool getString : constant -> string Then I can write: match a with Constant c when isString c -> ... getString c ... However, this is really not what I want, since I essentially test twice if c is a string (i.e. getString needs an error case), and furthermore, my operation 'refine' from above may be expensive. Now, in a paper ICFP'97 "Statically Checkable Pattern Abstraction", me and a colleague have explored more expressive patterns in the context of ML. It seems to me that the stream patterns in OCAML would allow me to do what we described in this paper, except for the fact that they can only appear in stream parsers. Suppose I could write pat = exp in the regular pattern language, with the semantics that the value being matched is first passed to the function exp, and the result is matched against pat: Then I can write the above code as follows: I write a different auxilary function to test whether a constant is a string that returns the string in case it is one. let isString2 c = match refine c with String s -> Some s | _ -> None Then my match becomes: match a with Constant (Some s = isString2) -> .... s .... | ... which is exactly what I want. I believe that with such an extension to OCAML, the pattern language we explored in the ICFP paper could be expressed completely (and more). In our paper, we used syntax that swaps the arguments and returns to pattern abstractions, so we could write the above as match a with Constant (isString2(s)) -> ... s ... Note that in this case the success/failure of the pattern is implicit, whereas in the above case I used an option to encode it. Any pattern abstraction could be encoded in this form, where the pattern bindings become the argument to Some. ... Just a random thought, but it would be neat. -Manuel Fahndrich