With Pierre Boutillier, we have been working on a new Coq tactic lately, called
invert. From my point of view, it started as a quest to build a replacement to the
inversion is a pain to use, as it generates sub-goals with many (dependent) equalities that must be substituted, which force the use of
subst, which in turns also has its quirks, making the mantra
inversion H; clear H; subst quite fragile. Furthermore,
inversion has efficiency problems, being quite slow and generating big proof terms. From Pierre's point of view, this work was a good way to implement a better
destruct tactic, based on what he did during an internship (report in French (PDF)).
In a previous post I described two extensions to CompCert's memory model that I implemented during my visit at Gallium. Another thing I have been working on is non-determinism and sequence points in C. As some of you will know, the evaluation order of expressions is not specified by the C standard. This allows a compiler to pick its preferred evaluation strategy. To allow a compiler also to delay side-effects, and to interleave evaluation, the allowed non-determinism is slightly restricted.
Let me start this post by briefly introducing myself: I am a PhD student at the Radboud University Nijmegen, the Netherlands, working on developing a formal semantics for the C11 standard in Coq. Between January and March, I have been a guest at Gallium (many thanks to Xavier Leroy for inviting me!). During this stay I have been able to do some CompCert hacking, and to get more experience with CompCert and its semantics.
For my 25th birthday, my (awesome) friends offered me a new gadget, a Nexus 7 tablet. Of course, my first impulse was to install Debian on it. That seemed a little bit excessive; I tried to be reasonable, and decided to first try to run OCaml programs on the tablet.
I successfully managed to set up Unison on the tablet, and used it to synchronize documents between the tablet and my home computer. At the end of this blog post, hopefully you'll be able to do the same!
OCAMLRUNPARAM="b" returns a disappointingly
unhelpful backtrace, because the program you're trying to debug
has a non-trivial usage of exceptions that destroys the
backtrace information you were expecting. Here is a new library
that should solve this problem, by allowing you to reliably
register backtraces. Read more for the source, and the juicy
internal details: weak tables, semi-manual garbage collection
logic, and an optional change to the OCaml runtime to
improve the library performances.
Batteries contributors recently started a new discussion on the Enum module, whose purpose is to provide an good intermediate representation for conversion between data-structures, but whose implementation is perceived as too complicated and not well-understood enough. Going back to fundamentals (forgetting about half the features of Enum), what is the ultimate intermediate traversal interface?
There are two obvious choices in an effectful setting: a generator, that is a "next-element" function of type
('a -> unit) that generates the next element each time it is called, or an exception to signal end of input; or an iterator, a fold-function of type
('a -> unit) -> unit, that iterates a consumer function through all elements of the list.
Both are suitable as an abstract representation of any sequence (the second is precisely the basis for Simon Cruanes' Sequence library), and their are at opposite ends of the control spectrum: generators give control to the consumer of the sequence (she decides when to call the generator function), while iterators give control to the producer of the sequence (she decides when to call the iterated function). It's easy to transform a structure into a iter (
to_iter), or to build a structure from a next (
of_next), because you have the control. But as a library writer, you should also write the without-control conversions (
to_next), despite them being slower and harder to implement, so that your users can live the easy in-control life!
Finally, continuation capture is a well-known technique to invert control, letting you write code in "direct style", as if you were in control, when you're not. In this post, I will demonstrate how you can start from a conversion function that has control and, by systematic source-to-source transformations of conversion to continuation-passing-style (CPS) and defunctionalization, obtain a conversion function that works without the control.
The n-ary cartesian product (on lists) returns the cartesian product of a list of list, rather than just two lists:
product [; [2;3]; [4;5]] is
[[1;2;4]; [1;2;5]; [1;3;4]; [1;3;5]]. The result is the empty list as soon of one of the input lists is empty. But what is the product of the empty list of lists?
I first answered this question with mathematical considerations that, while working on set theory, will fell familiar to anyone having worked with dependent types. But there is a direct, much simpler answer in the code.
During the second part of my internship this summer, I worked on a test implementation for a new data structure in OCaml : Hash Array Mapped Tries (HAMT). I did not have the time to finish it, but I now have a usable and quite complete version, still to be more documented but already available at http://gitorious.org/ocaml-hamt.
On this article, I will quickly explain the principles and the use cases of this structure, and I will expose a few details of my implementation in OCaml.