Index of modules

This module provides shortcuts for AST position handling.

This module provides a solver for equations involving set constants, variables, and disjoint sums (i.e.

This module manages a data structure for constraint in a multi-equation framework.

The constraint over equality between terms.

This module implements a core algebra of first order terms.

Environment who maps keys whose type is 'a to values of type 'b.

handle f runs f and exits with exit status 0.

This module implements infinite arrays.

This module describes an ordered type t equipped with a distinguished constant none.

This module implements a very simple notion of ``mark''.

This module provides the type algebra for the Mini language.

The abstract syntax of MiniML programs.

This module implements a pretty printer for the constraint of the Mini language.

This module expresses the problem of type inference for MiniML programs to the problem of constraint solving by a transformation of program into typing constraints.

This module provides a simple inference engine for the kinds of the Mini type system.

This modules instanciates PrettyPrinter for the Mini language.

This module provides a constraint solver based on unification under a mixed prefix.

This module provides a parser for program and a parser for constraint.

This module transforms types from the user's syntax to the internal representation of the inference engine.

TypingEnvironment implements two mappings used during the constraint generation.

This modules declares the exceptions raised by the type inference engine.

This module contains miscellaneous utilities.

This module implements a data structure for multi-equations.

This module handles parsing errors.

Extension of standard library's positions.

This module provides a common formatting interface to pretty-print in LaTeX, raw text or module Format mode.

This module provides a simple pretty-printer for the terms maintained by a unifier.

A simple task manager.

The universe of row labels.

This module provides a constraint solver based on unification under a mixed prefix.

Maps over strings.

Sets of strings.

This module implements unification of (ranked) multi-equations over a row algebra, that is, an algebra obtained by extending a free algebra A with rows (see module CoreAlgebra).

This module implements a simple and efficient union/find algorithm.