[cwn] Attn: Development Editor, Latest Caml Weekly News
Alan Schmitt
alan.schmitt at polytechnique.org
Tue Feb 19 00:31:27 PST 2008
Hello,
Here is the latest Caml Weekly News, for the week of February 12 to
19, 2008.
1) Sydney (Australia) Functional Programming Group
2) New release of moca
3) GLCaml version 20080215 available
========================================================================
1) Sydney (Australia) Functional Programming Group
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/74a593636ce833e0/57665f9bfaf8de8e#57665f9bfaf8de8e
>
------------------------------------------------------------------------
** Erik de Castro Lopo announced:
I'd like to announce the FP-SYD, the Sydney (Australia) Functional
Programming group. The intro page is here:
<http://groups.google.com/group/fp-syd>
To subscribe to the mailing list (mainly for meeting organisation,
meeting announcements, and Sydney job offers) either go to the URL
above of send mail to:
fp-syd-subscribe at googlegroups dot com
========================================================================
2) New release of moca
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/2367110884582c64/931dab1123c26e16#931dab1123c26e16
>
------------------------------------------------------------------------
** Pierre Weis and Frédéric Blanqui announced:
Relational types in Caml
We are pleased to announce the 0.5.0 version of Moca, a general
construction
functions generator for relational types in Objective Caml.
In short:
=========
Moca allows the high-level definition and automatic management of
complex invariants for data types; Moca also supports the automatic
generation
of maximally shared values, independantly or in conjunction with the
declared invariants.
Moca's home page is <http://moca.inria.fr/>
Moca's source files can be found at
<ftp://ftp.inria.fr/INRIA/caml-light/bazar-ocaml/moca-0.5.0.tgz>
Moca is developped by Pierre Weis and Frédéric Blanqui, Richard
Bonichon and
Laura Lowenthal (see the file AUTHORS in the main directory of the
distribution).
In long:
========
A relational type is a concrete type that declares invariants or
relations
that are verified by its constructors. For each relational type
definition,
Moca compiles a set of Caml construction functions that implements the
declared relations.
Moca supports two kinds of relations:
- algebraic relations (such as associativity or commutativity of a
binary
constructor),
- general rewrite rules that map some pattern of constructors and
variables to
some arbitrary user's defined expression.
Algebraic relations are primitive, so that Moca ensures the
correctness of
their treatment. By contrast, the general rewrite rules are under the
programmer's responsability, so that the desired properties must be
verified
by a programmer's proof before compilation (including for completeness,
termination, and confluence of the resulting term rewriting system).
What's new in this release ?
============================
* Lot of work on the documentation: a research paper has been
published to
described the framework at ESOP'07, talks about relational types and
the
internal of the compiler are included in the distribution.
* An automatic test generation facility has been developped to test the
specifications written in Moca.
* Arbitrary Caml code can be written in the .mlm files (any sequence
of Caml
signature items are allowed as extra algebraic properties of
generators). This ``external'' code is included as is in the resulting
module.
* Commutativity relation gets an extra argument which gives the order
used to
sort the combs (or lists in case of a vary-adic generator).
* Source code of the compiler has been documented.
* No more shell scripts: the compiler is entirely written in Caml.
* User's defined rules have been generalized from pattern -> pattern
to pattern -> expr.
An example
==========
The Moca compiler (named mocac) takes as input a file with
extension .mlm
that contains the definition of a relational type (a type with
``private''
constructors, each constructor possibly decorated with a set of
invariants or
algebraic relations).
For instance, consider peano.mlm, that defines the type peano with a
binary
constructor Plus that is associative, treats the nullary constructor
Zero as
its neutral element, and such that the rewrite rule Plus (Succ n, p) -
> Succ
(Plus (n, p)) should be used whenever an instance of its left hand side
appears in a peano value:
type peano = private
| Zero
| Succ of peano
| Plus of peano * peano
begin
associative
neutral (Zero)
rule Plus (Succ n, p) -> Succ (Plus (n, p))
end;;
From this relational type definition, mocac will generate a regular
Objective
Caml data type implementation, as a usual two files module.
From peano.mlm, mocac produces the following peano.mli interface file:
type peano = private
| Zero
| Succ of peano
| Plus of peano * peano
val plus : peano * peano -> peano
val zero : peano
val succ : peano -> peano
mocac also writes the following peano.ml file that implements this
interface:
type peano =
| Zero
| Succ of peano
| Plus of peano * peano
let rec plus z =
match z with
| Succ n, p -> succ (plus (n, p))
| Zero, y -> y
| x, Zero -> x
| Plus (x, y), z -> plus (x, plus (y, z))
| x, y -> insert_in_plus x y
and insert_in_plus x u =
match x, u with
| _ -> Plus (x, u)
and zero = Zero
and succ x1 = Succ x1
To prove these construction functions to be correct, you would prove
that
- no Plus (Zero, x) nor Plus (x, Zero) can be a value in type peano,
- for any x, y, z in peano. plus (plus (x, y), z) = plus (x, plus
(y, z))
- etc
Hopefully, this is useless if mocac is correct: the construction
functions
respect all the declared invariants and relations.
To prove these construction functions to be incorrect, you would have to
- find an example that violates the relations.
Hopefully, this is not possible (or please, report it!)
And, if you needed maximum sharing for peano values, you just have to
compile
peano.mlm with the "--sharing" option of the mocac compiler:
$ mocac --sharing peano.mlm
would do the trick !
Conclusion:
===========
Moca is still evolving and a lot of proofs has still to be done about
the
compiler and its algorithms.
Anyhow, we think Moca to be already usable and worth to give it a try.
Don't hesitate to send your constructive remarks and contributions !
========================================================================
3) GLCaml version 20080215 available
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/c93b5de9198722a1/e74999ae061a4afe#e74999ae061a4afe
>
------------------------------------------------------------------------
** Elliott Oti announced:
GLCaml version 20080215 is now available at <http://glcaml.sourceforge.net
>
GLCaml is a collection of three modules:
1. Glcaml, which offers dynamic bindings to OpenGL 1.1 through 2.1
plus all
ARB and vendor specific extensions.
2. SDLCaml, which offers bindings to SDL (<http://libsdl.org>), a
graphics
library
3. Win, which allows OpenGL calls to be used from an Ocaml Graphics
window
without requiring other libraries such as SDL or GTK.
This version of GLCaml has major API changes with respect to the
previous
versions. The following changes have been made:
1. Bigarrays are no longer necessary for using OpenGL functions.
Standard
Ocaml types (ints, floats, bools and strings, and corresponding
arrays) are
now used.
2. Enumerated constants (glenums) have been replaced by ints. As a
result,
there are no more GL_ALL_CAPS constants; these have been replaced by
gl_no_caps ints
3. An exception is now always thrown if an OpenGL call is not
available. This
is because silent fails can leave mutable parameters in an undefined
state.
Extra examples have been added that make use of the Win module,
including an
example demonstrating the use of OpenGL shaders.
========================================================================
Using folding to read the cwn in vim 6+
------------------------------------------------------------------------
Here is a quick trick to help you read this CWN if you are viewing it
using
vim (version 6 or greater).
:set foldmethod=expr
:set foldexpr=getline(v:lnum)=~'^=\\{78}$'?'<1':1
zM
If you know of a better way, please let me know.
========================================================================
Old cwn
------------------------------------------------------------------------
If you happen to miss a CWN, you can send me a message
(alan.schmitt at polytechnique.org) and I'll mail it to you, or go take a
look at
the archive (<http://alan.petitepomme.net/cwn/>) or the RSS feed of the
archives (<http://alan.petitepomme.net/cwn/cwn.rss>). If you also wish
to receive it every week by mail, you may subscribe online at
<http://lists.idyll.org/listinfo/caml-news-weekly/> .
========================================================================
--
Alan Schmitt <http://alan.petitepomme.net/>
The hacker: someone who figured things out and made something cool
happen.
.O.
..O
OOO
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.idyll.org/pipermail/caml-news-weekly/attachments/20080219/6cf206d7/attachment.htm
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 186 bytes
Desc: This is a digitally signed message part
Url : http://lists.idyll.org/pipermail/caml-news-weekly/attachments/20080219/6cf206d7/attachment-0001.pgp
More information about the caml-news-weekly
mailing list