From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <maranget@yquem.inria.fr>
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: by yquem.inria.fr (Postfix, from userid 18041)
	id 4777ABBAF; Thu, 20 Jul 2006 10:38:28 +0200 (CEST)
Date: Thu, 20 Jul 2006 10:38:28 +0200
To: Jim Miller <gordon.j.miller@gmail.com>
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Pattern matching question
Message-ID: <20060720083828.GA16258@yquem.inria.fr>
References: <beed19130607191148k4d94b706mf1f7ce222b1d7fba@mail.gmail.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <beed19130607191148k4d94b706mf1f7ce222b1d7fba@mail.gmail.com>
User-Agent: Mutt/1.5.9i
From: maranget@yquem.inria.fr (Luc Maranget)
X-Spam: no; 0.00; maranget:01 maranget:01 ocaml:01 ocaml:01 specifies:01 parsing:01 luc:01 luc:01 caml-list:01 int:01 defining:02 caml:02 match:02 match:02 types:02 
X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=-2.8 required=5.0 tests=ALL_TRUSTED 
	autolearn=disabled version=3.0.3

> 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