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:

The following tasks are optional:

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