From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 842627EE25 for ; Tue, 12 Nov 2013 15:00:58 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of caml-list.lebotlan@antichef.net) identity=pra; client-ip=195.83.9.36; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="caml-list.lebotlan@antichef.net"; x-sender="caml-list.lebotlan@antichef.net"; x-conformance=sidf_compatible Received-SPF: Fail (mail2-smtp-roc.national.inria.fr: domain of caml-list.lebotlan@antichef.net does not designate 195.83.9.36 as permitted sender) identity=mailfrom; client-ip=195.83.9.36; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="caml-list.lebotlan@antichef.net"; x-sender="caml-list.lebotlan@antichef.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@frontsmtp2.insa-toulouse.fr) identity=helo; client-ip=195.83.9.36; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="caml-list.lebotlan@antichef.net"; x-sender="postmaster@frontsmtp2.insa-toulouse.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: An8CAEszglLDUwkknGdsb2JhbABZgz/BFRYOAQEBAQEIFAk8glMRQD0WGAMCAQIBWAgBAYgBCZxwoTSPfIQbA5k+lAI X-IPAS-Result: An8CAEszglLDUwkknGdsb2JhbABZgz/BFRYOAQEBAQEIFAk8glMRQD0WGAMCAQIBWAgBAYgBCZxwoTSPfIQbA5k+lAI X-IronPort-AV: E=Sophos;i="4.93,685,1378850400"; d="scan'208";a="42335090" Received: from frontsmtp2.insa-toulouse.fr ([195.83.9.36]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 12 Nov 2013 15:00:58 +0100 Received: from insatlse.insa-toulouse.fr ([195.83.9.34] ident=Debian-exim) by frontsmtp2.insa-toulouse.fr with esmtp (Exim 4.69) (envelope-from ) id 1VgEWX-0008GB-Pt; Tue, 12 Nov 2013 15:00:57 +0100 Received: from nomade-personnel53.insa-toulouse.fr ([10.31.30.53]) by insatlse.insa-toulouse.fr with smtp (Exim 4.50) id 1VgEWX-0003nW-Ld; Tue, 12 Nov 2013 15:00:57 +0100 Message-ID: <52823499.9090901@antichef.net> Date: Tue, 12 Nov 2013 15:00:57 +0100 From: Didier Le Botlan User-Agent: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.1.0 MIME-Version: 1.0 To: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Subject: [Caml-list] [ANN] exenum.0.6: exhaustive enumerations for datatypes Hi list, Let me introduce exenum, the "exhaustive enumeration"(1) library. You all probably wonder what "the" 42,000th lambda-term is. It happens to be (((fun x -> v) (v v)) ((x x) v)) (2) As for "the" 10^400th lambda-term, it is ((((((fun x -> (v v)) ((fun v -> y) (fun x -> x))) ((fun v -> (x x))[...and 20 more lines...] (1) where "exhaustive" means that every value (of the given datatype) is eventually enumerated. (2) where variables are restricted to "x", "y", "u", "v". In short : - exenum makes it easy to build enumerations for any datatype. - Very handy to carry out intensive unit testing (Students' motto : "If you know your code is unsound, test it anyway, it might work by accident"). - exenum is inspired by FEAT for Haskell. - Impress coq's users with statements such as: "I have successfully checked my code up to index 17 !" - Quick overview and API on the homepage: http://exenum.forge.ocamlcore.org/ - Install with: opam install exenum * * * As a side dish, let me mention the oasis- and ocamlbuild-based packaging I used for this library. For quite a while, I had been looking for a neat way to pack an ocaml library, that is: - Only one main module is "exported" to users (or, say, just a couple of modules). - The library may define several internal modules, but they should remain hidden (that is, as hidden as possible). In particular, they should not pollute the global module namespace. I was not able to find satisfactory examples on the net (most likely, though, I have not searched enough). Finally, I wrote an _oasis file as follows (excerpt): ## Exported library Library "exenum" Path: src/ Modules: ExEnum BuildDepends: exenum.internals Install: true ## This library packs internal modules, so that they may not conflict with anything else. Library "exenum_internals" Path: src/ Modules: Convenience InternalModules: Exen, ExtArray, Parts, Shuffle FindlibParent: exenum FindlibName: internals Pack: true Thus, the internal modules are all packed in an ocaml module "Exenum_Internals" (the -pack option of ocamlc). Only the main module "ExEnum" and "Exenum_internals" are visible at top-level. See details at the bottom of: http://exenum.forge.ocamlcore.org/ -- D. Le Botlan