Pattern matching question

Pattern matching question

[Jim Miller]

[-- Attachment #1: Type: text/plain, Size: 1311 bytes --]

I'm trying to use an OCaml program to form an umambiguous protocol
specification.  I've convinced myself that by proper definition of my types,
and avoiding using the _ in matches, I can get OCaml to help me verify that
I have a complete specification.  I'm doing this by defining a function that
specifies the behavior of one of the protocol partners when it receives a
message.  Here is an example of what I have.

let requestOp = REQUEST_KEY | SUCCESS;;

let message = None | Register of requestOp * int;;

let receive idList msg =
  match message with
     None -> None

|    Register( REQUEST_KEY, id ) -> begin
         match idList with
             [] -> Register(SUCCESS, id)
         |   l when (List.mem id l) -> Register(Success, (next_available_id
l))
         |  _ -> Register(Success, id)
;;

The problem is with the final pattern in the inner match expression.  I'm
really trying to avoid using _ in patterns so that I'm forced to specify an
action for each possible case (hence the reason I'm trying to use OCaml
here).    It appears that since I'm using a guard here that OCaml can't, at
compile time, determine whether or not I'm being exhaustive.

Is there a way to accomplish the same thing as above without using guards so
that OCaml will be able to determine that my match is exhaustive?

[-- Attachment #2: Type: text/html, Size: 1706 bytes --]

Re: [Caml-list] Pattern matching question

[Seth J. Fogarty]

On 7/19/06, Jim Miller <gordon.j.miller@gmail.com> wrote:
> I'm trying to use an OCaml program to form an umambiguous protocol
> specification.  I've convinced myself that by proper definition of my types,
> and avoiding using the _ in matches, I can get OCaml to help me verify that
> I have a complete specification.  I'm doing this by defining a function that
> specifies the behavior of one of the protocol partners when it receives a
> message.  Here is an example of what I have.
>
>  let requestOp = REQUEST_KEY | SUCCESS;;
>
>  let message = None | Register of requestOp * int;;
>
>  let receive idList msg =
>    match message with
>       None -> None
>
>  |    Register( REQUEST_KEY, id ) -> begin
>           match idList with
>               [] -> Register(SUCCESS, id)
>           |   l when (List.mem id l) -> Register(Success, (next_available_id
> l))
>           |  _ -> Register(Success, id)
>  ;;


Try something like

match idList with
     [] -> Register(SUCCESS, id)
   | l -> if List.mem id l then Register(foo) else Register(bar)

And replace the guard with an if statement.

-- 
Seth Fogarty             sfogarty@[gmail.com|rice.edu|livejournal]
Neep-neep at large    AIM: Sorrath
"I know there are people in this world who do not love their fellow
human beings - and I hate people like that" --Tom Lehrer.

Re: [Caml-list] Pattern matching question

[Jim Miller]

[-- Attachment #1: Type: text/plain, Size: 1403 bytes --]

On 7/19/06, Jonathan Roewen <jonathan.roewen@gmail.com> wrote:
>
> > let receive idList msg =
> >   match message with
> >      None -> None
> >
> > |    Register( REQUEST_KEY, id ) -> begin
> >          match idList with
> >              [] -> Register(SUCCESS, id)
> >          |   l when (List.mem id l) -> Register(Success,
> (next_available_id
> > l))
> >          |  _ -> Register(Success, id)
> > ;;
>
> For the inner match, why you even both with it is beyond me. All you
> are doing is wrapping List.mem in an unnecessary test.
>
> It should be:
> | Register(REQUEST_KEY,id) ->
>    if List.mem id idList then
>       Register(Success, next_available_id l)
>    else
>       Register(Success, id)
>
> Perhaps the fact that your example makes no sense (it's not a complete
> definition, nor is Success defined anywhere, nor does Register even
> accept the constructor Success) doesn't help here.



The main purpose is not to actually construct a program but to construct a
specification of a communications protocol in a syntax that I can give to a
non-coder and have them read but also have some validation that I'm checking
all possible cases.

You are correct in your statement that the match isn't necessary but that's
assuming that I care about the program.  The match is much more explicit to
a non-coder (at least that's the feedback I've gotten) of the case that
we''re trying to test.

[-- Attachment #2: Type: text/html, Size: 2174 bytes --]

Re: [Caml-list] Pattern matching question

[Luc Maranget]

> I'm trying to use an OCaml program to form an umambiguous protocol
> specification.  I've convinced myself that by proper definition of my types,
> and avoiding using the _ in matches, I can get OCaml to help me verify that
> I have a complete specification.  I'm doing this by defining a function that
> specifies the behavior of one of the protocol partners when it receives a
> message.  Here is an example of what I have.
> 
> let requestOp = REQUEST_KEY | SUCCESS;;
> 
> let message = None | Register of requestOp * int;;
> 
> let receive idList msg =
>  match message with
>     None -> None
> 
> |    Register( REQUEST_KEY, id ) -> begin
>         match idList with
>             [] -> Register(SUCCESS, id)
>         |   l when (List.mem id l) -> Register(Success, (next_available_id
> l))
>         |  _ -> Register(Success, id)
> ;;
> 

To avoid | _ -> ... matching clauses, have a look at the -w E warning.
<http://caml.inria.fr/pub/docs/manual-ocaml/manual022.html>
Section 8.2 'Options'


I cannot get your exact point, besides the above code does not even go through
parsing (missing end), let -> type etc.

In fact what you want to achieve is still unclear.
As regards your message and requestOp types there should be no problem,

Something like

match msg with
| None -> ...
| Register (REQUEST_KEY, id) -> ...
| Register (SUCCESS, id) -> ...

Is easily shown to be exhaustive.

As regards your list example, perhaps you'd like better
match idList with
| [] -> Register(SUCCESS, id)
| _::_ ->
  if List.mem id idList then  Register(SUCCESS, next_available idList)
  else Register(SUCCESS, id)

or even

match idList with
| [] -> Register(SUCCESS, id)
| _::_ when List.mem id idList -> Register(SUCCESS, next_available idList)
| _::_ -> Register(SUCCESS, id)

Both are easily shown to be exhaustive, but frankly, this brings you
no more guarantee than the much more direct code

if List.mem  id idList then
   Register(SUCCESS, next_available_id idList))
else
   Register (SUCESS, id)

-- 
Luc Maranget