The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Tue, Apr 25, 2006 at 10:48:47AM +0200, Pierre Casteran wrote:
> Philippe Andouard wrote:
> 
> >Bonjour,
> >
> >J'aimerais pouvoir simuler le fonctionnement d'un octet. J'ai vu que
> >la librairie standard de Coq proposait des vecteurs de bits au travers
> >du module Bvector.
> >
> >Mon problème est le suivant, je voudrais convertir un entier en base
> >dix en sa représentation en base deux et le stocker dans un vecteur de
> >bits. Par exemple si on considère l'entier 15 je voudrais pouvoir
> >stoker [0 0 0 0 1 1 1 1] dans mon vecteur.
> >J'arrive à déclarer des Bvector mais je n'arrive pas à stocker quoi
> >que ce soit dedans.
> >
> >Quelqu'un saurait-il comment stocker des valeurs dans des vecteurs?
> > 
> >
> The constructor Vcons can be used to store values in vectors.
> 
...
> 
> Pierre
> 

* NArith:
---------

It just happens that I've been busy these days improving Coq library
NArith. This not-so-well-known part of the standard library proposes a
type N = N0 | Npos of positive, i.e. a type for natural numbers coded
in a binary way. In particular, you may find interesting the new file
theories/NArith/Ndigits.v, that contains some operations over bits of
an N number (for instance a bitwise xor). After seeing your mail, I've
placed at the end of this file some conversions functions between N
and Bvector: N2Bv and Bv2N. There is also a N2Bv_gen that forces the
production of a bit vector with a precise size.

All this is currently only available for Coq SVN, that you can
download or browse at: http://gforge.inria.fr/scm/?group_id=269 ;
With it, you can now write for instance: 

Require Import Bvector BinNat Ndigits.
Implicit Arguments Vcons.
Eval compute in (N2Bv 15).

(*   = Vcons true (Vcons true (Vcons true (Vcons true (Vnil bool))))
     : Bvector (Nsize 15)
*)

Moreover, conversion functions between N and nat are now also
available, in file Nnat, so it should be fairly easy now to access the
binary digits of any form of natural numbers.

* Intmap: 
--------

A somewhat related question: is anyone on this list aware of any
development that uses the library IntMap, apart from the ones already
in the user's contribs (Rocq/GRAPHS, Rocq/TreeAutomata, Dyade/BDDS,
Cachan/SMC) ? These recent additions to the library NArith are mostly
bits and parts coming from IntMap, since the type of addresses in
IntMap is ad, which is isomorphic to N. Overall, NArith+Intmap
contains now at least as much as before, but lots of names have
changed. Moreover, Intmap now uses the same option type as the rest of
Coq. I've adapted the four user's contribs to this revised Intmap,
please contact me if you have code that needs to be adapted as well,
since I've a script that can do a good deal of the job. More
generally, I would be glad to hear from anybody that uses or plans to
use finite sets or maps, in order to see if the new FSet/Fmap
framework fits her/his needs (see directory theories/FSets/ in the SVN
repository of Coq).

Best regards, 

Pierre Letouzey