Index of values

x <? t is a conjunction constraint.

t1 =?= t2 is an equality constraint

c1 ^ c2 is a conjunction constraint.

abs env return the type abs.

Set the active mode.

add env k v associates v to k in env.

Add a data constructor into the environment.

Merge a environment fragment with an environment.

Add a type constructor into the environment.

Add a set of type variables into the environment, associating a name to each.

app t ts built the term corresponding to the (...((t t0) t1)... tn).

are_equivalent v1 v2 tests if v1 and v2 are in the same multi-equation.

result_type env t returns the argument types of the type t if t is an arrow type.

arity (t1 -> ... -> tn) returns n.

arrow env x1 x2 builds the internal representation of the type x1 -> x2.

arrow env t1 t2 return the type t1 -> t2.

as_fun env provides a view of env as function from names to variable.

as_kind env provides a view of env as kind environment.

as_symbol s maps the string s to a symbol if s is a valid symbol name.

associativity s returns the associativity of s.

If l is a list of pairs of a key and a datum, and if p is a predicate on keys, then assocp p l returns the datum associated with the first key that satisfies p in l.

change p d updates the descriptor of p to d.

characters p1 p2 returns the character interval between p1 and p2 assuming they are located in the same line.

check pos env typ kind verifies that typ can be given the kind kind.

chop p t introduces t into p by registering a variable into p for each node of its tree maintaining its structure using links between these variables.

chopi rank term chops a term.

column p returns the number of characters from the beginning of the line of the Lexing.position p.

compare x y is a total ordering.

compare x y is a total ordering.

concat env env' merges the mapping of env and env' preferring the mapping of env if there is a clash.

conj cs builds a conjunction between a list of constraints.

cpos lexbuf returns the current position of the lexer.

cposition c returns the position related to c.

A debugging flag.

diff returns the difference of two sets.

empty is the empty set.

empty denotes the constant empty set.

empty is the environment with no binding at all.

The empty environment.

environment_as_list env converts env into a list.

environment_as_list env converts env into a list.

equal tells whether two sets are equal.

equivalent point1 point2 tells whether point1 and point2 belong to the same equivalence class.

ex qs c returns the constraint exists qs.c.

exists f creates a fresh variable x and returns the constraint exists x.(f x).

exists3 f is a shortcut for exists (fun x -> exists (fun y -> exists (fun z -> f x y z))).

exists_list l f associates a fresh variable with every element in the list l, yielding an association list m, and returns the constraint exists m.(f m).

exists_set names f associates a fresh variable with every name in the set names, yielding a map m of names to variables, and returns the constraint exists m.(f m).

explicit_or_implicit p e tests if a definition is annotated or not and normalizes it such that type constraint can be found at the top of the term.

explode t converts an arbitrary depth tree into a 1-depth one using variables.

export i provides access to the inverse of the global mapping, that is, associates a unique identifier with every label.

extract_type examines an expression and looks for a sufficiently explicit type annotation.

filter env pred returns the set of values that verify pred.

find point returns the descriptor associated with point's equivalence class.

fl qs c returns the constraint forall qs.c.

fold f term accu folds f over term's parameters, using accu as initial value.

fold2 f term term' accu folds f over term's parameters, using accu as initial value.

fold f init env iterates over the mappings of env conveying an accumulator whose value is init initially.

fold_type_info folds over the environment focusing on type's information.

forall_list l f associates a fresh variable with every element in the list l, yielding an association list m, and returns the constraint forall m.(f m).

fresh desc creates a fresh point and returns it.

fresh() generates a fresh mark, that is, a mark that is guaranteed to be distinct from all existing marks.

fresh_datacon_scheme env dname vs retrieves the type scheme of dname in env and alpha convert it using vs as a set of names to use preferentially when printing.

fresh_flexible_vars pos env vs returns a list of fresh flexible variables whose visible names are vs and an environment fragment.

fresh_kind returns a fresh kind for a type.

fresh_flexible_vars pos env vs returns a list of fresh rigid variables whose visible names are vs and an environment fragment.

fresh_flexible_vars pos env returns a list of fresh rigid variables without visible names and an environment fragment.

generate_constraint p generates a closed constraint that describes the typing of p.

get a i returns the element contained at offset i in the array a.

import s associates a unique label with the identifier s, possibly extending the global mapping if s was never encountered so far.

infer env typ infers a kind for typ.

infer_program p generates a constraint context that describes program p.

infix s tests if s is infix.

inhabitants p returns the type variables of a pool.

init () returns a fresh pool.

init_builtin_env variable_maker uses variable_maker to built a typing environment that maps type constructor names to their arities and their type variables.

init_env () returns a constraint context that defines the builtins of the source language.

instance p v returns a valid instance of v.

inter returns the intersection of two sets.

intern env ty converts ty into its internal representation.

intern_kind env kind internalizes a kind in the user-syntax.

internal_let_env env fqs rqs internalizes the flexible variables fqs and the rigid variables rqs into env.

intern_scheme env x fqs ty returns the internal representation of the type scheme forall fqs.ty and the binding of x to it.

introduce p v registers v into p and updates its rank accordingly.

is_empty tells whether a set is empty.

is_flexible v returns true if v is a flexible variable.

is_regular_datacon_scheme env vs ty checks that forall vs.ty is a valid scheme for a data constructor that is to say following the shape: K :: forall a1 ..

is_rigid v returns true if v is a constant or rigid variable.

is_structured v tests if v is related to a term.

iter f term applies f successively to every parameter of the term term.

iter f env iterates over the mappings of env.

iter is similar to List.iter, but does not require f to return a result of type unit.

iteri f t computes f i x on every element x at position i in t.

join p1 p2 returns a position that starts where p1 starts and stops where p2 stops.

Returns the last element of a list.

column p returns the line number of to the Lexing.position p.

lookup env k returns the value associated to k or raises Not_found.

lookup_datacon env k gives access to the typing information related to the data constructor k in env.

Looks for a type constructor given its name.

make x creates an infinite array, where every slot contains x.

Returns a pair of function import and export to assign a unique integer to a given value.

map f term returns a term whose head symbol is that of term and whose parameters are the images of term's parameters through f.

map f env applies a function f on each mapping of env building a list f (k, v).

monoscheme header turns header into a monomorphic type scheme.

arrow env ts returns the type t0 -> ... -> tn.

n_rowcons l ts r returns the row type (l0: t0; ...; ln: tn; r).

new_pool p introduces a new pool with a rank equals to the one of p + 1.

none is the special value used to identify the universal quantifiers of a type scheme in an environment frame.

none is a distinguished mark, created via an initial call to fresh().

number p returns the rank of a p.

outermost is the rank assigned to variables that are existentially bound at the outermost level.

Parse a constraint given as a string.

Parse a program given as string.

pos_or_undef po is the identity function except if po = None, in that case, it returns undefined_position.

pre env t returns the type pre t.

print s provides a textual representation of the set s.

print t returns a string representation of the disjoint sum t.

print_binding b pretty-prints b according to the active printing mode.

print_env printer env use the printer of variable in order to display env.

print_expression e pretty-prints e according to the active printing mode.

print_binding p pretty-prints p according to the active printing mode.

Prints a list of elements, with one occurrence of the separator between every two consecutive elements.

print_type paren t pretty-prints t according to the active printing mode.

print context x returns a printable representation of the object x.

Pretty printer for formula.

priority s returns the priority of s.

record_constructor env return the type constructor {.}.

redundant maps all members of an equivalence class, but one, to true.

register p v adds v into the pool p without modifying the rank of v.

remove_init_context returns the context part that concerns the initial environment.

reset() clears print's memoization table.

result_type env t returns the result type of the type t if t is an arrow type.

rowcons l t r returns the row type (l: t; r).

same mark1 mark2 tells whether mark1 and mark2 are the same mark, that is, were created by the same call to fresh.

scheme rqs names f associates a fresh variable with every name in the set names, yielding a map m of names to variables, and returns the type scheme forall rqs m [f m] m, where the variables in rqs are rigid and the variables in m are flexible.

scheme' rqs rnames fnames f associates a fresh variable with every name in the set fnames and rnames, yielding a map m of names to variables, and returns the type scheme forall (rqs @ rm) fm [f m] m, where the variables in rqs and rm are rigid and the variables in fm are flexible.

set a i x sets the element contained at offset i in the array a to x.

set_error_channel c defines the channel into which we print the error messages.

solve tracer c solves c by doing in-place modifications resulting in a environment.

solve tracer c solves c by doing in-place modifications resulting in a environment.

star is the kind of ml values.

string_of_characters (c1,c2) returns the standard (Emacs-like) representation of the character interval (c1,c2).

string_of_cpos p returns a string representation of the lexer's current position.

string_of_lex_pos p returns a string representation for the lexing position p.

string_of_pos p returns the standard (Emacs-like) representation of the position p.

sum s t adds s to the sum denoted by t.

svariable () is equivalent to variable Set.empty.

tuple env ts returns t0 * ... * tn.

tycon t xs builds the internal representation of the type t xs.

Accessor to the kind of a type.

Accessor the unification variable of a type.

type_of_primitive p returns the type of a source language primitive.

This value is used when an object does not from a particular input location.

uniform t returns the row type that maps any label to t.

unify pos register v1 v2 equates the variables v1 and v2.

unify t t' solves the equality between two disjoint sums by determining the unification variable if necessary.

union returns the union of two sets, which may safely be assumed disjoint.

union point1 point2 merges the equivalence classes associated with point1 and point2 (which must be distinct) into a single class whose descriptor is that originally associated with point2.

variable() returns a new variable.

variable s returns a fresh unification variable whose denotation cannot intersect s.

variable_list xs allocates a fresh variable for every element in the list xs, and returns both a list of these variables and an association list that maps elements to variables, viewed as types.

variable_list_from_strings f xs allocates a fresh variable for every string in the list xs, and returns both a list of these variables and an association list that maps elements to variables, viewed as types.

variable_name v returns the name of v if it exists.

variable_set xs allocates a fresh variable for every element in the set xs, and returns both a list of these variables and a map of elements to variables.

variable_structure v returns the structure of v if it exists.

variables_of_typ ty returns the type variables of ty.