Index of modules

Provides wrappers for some bash fancy printing, mainly boxes and colors.

Dealing with binders.

This module provide a convenient way to print a typing derivation into a (supposedly) human-readable form.

This file provides a representation of typing derivations, built by Permissions.

This module sets up a lexer and a parser to create an AST.

Handling the names exported by interfaces and implementations.

Our not-so-pretty printer for expressions.

This module defines substitution functions and binding functions on expressions as well as data type groups.

This module defines the syntax of expressions.

Conjunction of hypotheses.

This module analyzes data type declarations to synthesize facts about data types.

This is a stripped down version of GSet that describes both Patricia and CompressedBitSet.

A simple Hashconsing facility.

This is an imperative version of VarMap, in the form expected by Fix.

This functor creates a fresh abstract type of names.

This module implements infinite arrays.

Treatment of interfaces.

as_arrow k transforms the kind k to an n-ary arrow kind.

This module implements a well-kindedness check for the types of the surface language.

This module implements lazy lists.

The lexer for Mezzo.

This module provides error reporting functions for Mezzo.

This module implements the merge operation.

This is the entry point of the program.

The four modes.

Maps over modes.

Find the dependencies of a module.

A bunch of useful functions for lists.

Various missing functions from the Map module.

Various string utilities.

No "J" prefix for this module since OCaml's standard library does not have an Option module.

This is an implementation of Patricia trees, following Chris Okasaki's paper at the 1998 ML Workshop in Baltimore.

This module provides permission manipulation functions.

This module implements a persistent store: in other words, it is a purely functional implementation of references, with an explicit store.

A persistent version of the classic union-find algorithm.

This function converts an internal name to a possibly-qualified name in the surface syntax.

Translating the surface syntax down into the core language syntax.

This is the top of the pyramid: the module that actually performs type-checking.

This module defines the syntax of types, as manipulated by the type-checker.

Everything you ever dreamed of for reporting errors.

Our not-so-pretty printer for types.

This module provides a variety of functions for dealing with types, mostly built on top of DeBruijn and TypeCore.

This module provides a clean way to map a variable to any given piece of data.

This module is entirely devoted to computing the variance of type parameters in data types.