Contribution: Containers

Containers: a typeclass-based library of finite sets/maps

Authors

Description

This is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. See tests files for usage. A new vernacular command is provided by Generate.v and the plugin to automatically generate ordered types for user-defined inductive types.

Keywords

data structures, type classes

README

Containers: a typeclass-based library of finite sets/maps
=========================================================
Copyright 2010 Stéphane Lescuyer <stephane.lescuyer@inria.fr>

Features
========

A reimplementation of the FSets/FMaps library from the standard
library, using typeclasses. See tests files for usage.
A new vernacular command is provided by Generate.v and the plugin
to automatically generate ordered types for user-defined inductive
types.

Files
=====

The archive has 4 subdirectories:
src/ contains the code of the plugin and commands

theories/ contains all the vernacular files of the library
  and Generate.v, used to load the [Generate] plugin in Coq

tests/ just demonstrates usage of the basic data structures

docs/ contains an in-depth description of the Generate
  OrderedType vernacular, and a guide to start using this
  library

Installation
============

First, you should have coqc, ocamlc and make in your path.
Then simply do:

# make -j

To consecutively build the plugin and the supporting theories.
Optionally you can launch the tests and benchmarks with

# make test

You can then either install the plugin with

# sudo make install

or leave it in its current directory and to be able to import it
from anywhere in Coq, simply add the following to ~/.coqrc:

Add Rec LoadPath "path_to_containers/theories" as Containers.
Add ML Path "path_to_containers/src".

Available files