The Mini inference engine

The source code of this package compiles a program called mini, a type inference engine for the Mini language.

A basic usage of mini is to provide a source file as input. Let's foo.ml be this file:

let id x = x

# mini foo.ml

returns

val id: forall a. a -> a

The documentation of the module MiniAst explains the concrete syntax of the Mini language. The "tests" directory contains examples of valid Mini programs.

General modules for type inference

UnionFind	This module implements a simple and efficient union/find algorithm.
BasicSetEquations	This module provides a solver for equations involving set constants, variables, and disjoint sums (i.e.
CoreAlgebra	This module implements a core algebra of first order terms.
MultiEquation	This module implements a data structure for multi-equations.
Constraint	This module manages a data structure for constraint in a multi-equation framework.
Unifier	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`).
Solver	This module provides a constraint solver based on unification under a mixed prefix.
Print	This module provides a simple pretty-printer for the terms maintained by a unifier.

Modules related to the Mini programming language

MiniSyntacticAnalysis	This module provides a parser for program and a parser for constraint.
MiniAst	The abstract syntax of MiniML programs.
MiniAlgebra	This module provides the type algebra for the Mini language.
MiniTypingExceptions	This modules declares the exceptions raised by the type inference engine.
MiniInfer	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.
MiniSolver	This module provides a constraint solver based on unification under a mixed prefix.
AstPositions	This module provides shortcuts for AST position handling.
MiniPrettyPrinter	This modules instanciates `PrettyPrinter` for the Mini language.

Miscellaneous

Misc	This module contains miscellaneous utilities.
Processing	A simple task manager.
Errors	`handle f` runs `f` and exits with exit status 0.
Positions	Extension of standard library's positions.
PrettyPrinter	This module provides a common formatting interface to pretty-print in LaTeX, raw text or module Format mode.
InfiniteArray	This module implements infinite arrays.
Mark	This module implements a very simple notion of ``mark''.
IntRank	This module describes an ordered type `t` equipped with a distinguished constant `none`.

How to compile the source code ?

Decompress the distributed package. In the newly created folder, do:

# ./configure

This should check if you have the necessary tools to compile mini. Then, you just have to launch the compilation using:

# make

To generate this documentation, type the following command:

# make doc

Do not hesitate to contact us if the compilation process fails.

Options

By default, mini processes the following tasks:

parse-program, parse the input file as a Mini program
generate-constraint, generate the typing constraint of this program
solve-constraint, solve this constraint
print-env, print the types of the toplevel definitions

The following tasks are optional:

print-program, pretty-print the parsed program
parse-constraint, parse the input file as a typing constraint not as a Mini program
print-constraint, print the typing constraint

The options of mini enable the use of these optional tasks:

usage: ./mini [options] filename
  --start taskname             Task to begin with
  --end taskname               Task to end with
  --trace-all                  Trace
  --do taskname                Do a task
  --trace-solve-constraint     Trace solve-constraint
  --trace-print-program        Trace print-program
  --trace-generate-constraint  Trace generate-constraint
  --trace-print-constraint     Trace print-constraint
  --trace-parse-program        Trace parse-program
  --trace-print-env            Trace print-env
  --trace-parse-constraint     Trace parse-constraint
  -help                        Display this list of options
  --help                       Display this list of options