A | |
| algebraic_datatype [MiniTypingEnvironment] |
An algebraic datatype is characterized by a list of data constructors.
|
| arterm [CoreAlgebra] |
Terms whose parameters are either leaves of type
'a, or terms.
|
| associativity [MiniAlgebra] |
Associativity of a symbol.
|
B | |
| binding [MiniAst] |
A
binding is
a set of value definition (MiniAst.value_definition):
MiniAst.type_definition).
|
| builtin_dataconstructor [MiniAlgebra] |
The type of predefined data constructors.
|
C | |
| clause [MiniAst] |
Pattern matching clause.
|
| context [MiniInfer] |
Constraint contexts.
|
| crterm [Constraint] |
The types in contraints are implemented using the internal data structure
defined in
CoreAlgebra.
|
| crterm [MultiEquation] |
The type of term of arbitrary depth.
|
D | |
| data_constructor [MiniTypingEnvironment] |
A data constructor's type is denoted by an ML scheme.
|
| descriptor [MultiEquation] |
A descriptor contains several pieces of information, the most
important of which is the structure of the multi-equation, or,
in other words, its unique non-variable member, if there is one.
|
| dname [MiniAst] |
Data constructors.
|
E | |
| env [MiniKindInferencer] |
The kind inference engine uses an environment implemented by
two functions (get, add).
|
| environment [MiniSolver] |
The solver environment.
|
| environment [MiniTypingEnvironment] |
The type of the typing environement.
|
| environment [MiniAlgebra] |
A type constructor is a type variable with higher-order kind.
|
| environment [Solver] |
The solver environment.
|
| expression [MiniAst] |
An
expression in Mini.
|
F | |
| formatter_output [PrettyPrinter] | |
| formula [MiniConstraintPrinter] | |
| formula [ConstraintPrettyPrinter] |
The constraint over equality between terms.
|
K | |
| kind [MiniAst] | |
L | |
| lname [MiniAst] |
Record labels.
|
| lname [CoreAlgebra] | lname is the type of label.
|
M | |
| mode [PrettyPrinter] | |
N | |
| name [MiniAst] |
Program identifiers.
|
O | |
| options [Processing] | |
| output [PrettyPrinter] | |
P | |
| pattern [MiniAst] | |
| point [UnionFind] |
The abstraction defined by this module is a set of points,
partitioned into equivalence classes.
|
| pool [MultiEquation] | pool is an abstract type denoting a set of type variables related
to a variable binding location.
|
| position [Positions] |
Abstract for position in the lexing stream.
|
| primitive [MiniAst] |
Constant.
|
| process [Processing] | |
| process_data [Processing] | |
| process_datas [Processing] | |
| process_type [Processing] | |
| process_types [Processing] | |
| program [MiniAst] |
A
program in the Mini language is a sequence of toplevel bindings.
|
R | |
| record_binding [MiniAst] | |
| recursive_value_definition_kind [MiniTypes] | recursive_value_definition_kind tests if a recursive definition
is annotated or not.
|
S | |
| scheme [Constraint] |
A type scheme is a pair of a constraint
c and a header h,
wrapped within two sets of universal quantifiers rqs and
fqs.
|
| sname [Constraint] | sname is the type of the names that are used to refer to type
schemes inside constraints.
|
| solving_step [MiniSolver] |
A
solving_step describes a elementary step of the solver.
|
| solving_step [Solver] |
A
solving_step describes a elementary step of the solver.
|
| structure [MultiEquation] |
A multi-equation can be related to a term.
|
| symbol [MiniAlgebra] |
Head symbols.
|
T | |
| t [MiniKindInferencer] |
Internal kind representation.
|
| t [CoreAlgebra.RowLabel] |
A row label is an object of type
t, that is, an integer.
|
| t [IntRank] | |
| t [BasicSetEquations.SetType] |
The type of sets.
|
| t [Mark] |
The type of marks.
|
| t [Env] | |
| t [InfiniteArray] | |
| task [Processing] | |
| task_name [Processing] | |
| tconstraint [MiniSolver] |
The constraint to solve.
|
| tconstraint [Solver] |
The constraint to solve.
|
| tconstraint [Constraint] |
Here is an abbreviation for the type constraint structure instantiated using
our internal variable and term representations.
|
| term [CoreAlgebra] |
Terms whose parameters are of type
'a.
|
| term [BasicSetEquations.Make] |
A
term denotes a disjoint sum of sets with unification
variables inside.
|
| tname [MiniAst] |
Type variable names.
|
| tname [MultiEquation] | tname is the type of type identifiers.
|
| tscheme [Constraint] |
Here is an abbreviation for the type scheme structure instantiated using
out internal variable and term representations.
|
| typ [MiniAst] | |
| type_constraint [Constraint] | type_constraint defines a syntax for the constraints between
types.
|
| type_declaration [MiniAst] | |
| type_definition [MiniAst] |
Type definitions.
|
| type_info [MiniTypingEnvironment] |
A type is characterized by a kind, a variable and an optional set of
algebraic data constructors.
|
V | |
| value_definition [MiniAst] |
A value definition consists of a list of explicit universal
quantifiers, a pattern, and an expression.
|
| variable [Constraint] |
The variables that appear in contraints are the same as the multi-equation
ones.
|
| variable [MultiEquation] |
The structure of the terms manipulated by a unifier is fixed and
made visible to the outside, because it must be accessible to
the constraint solver, which is built on top of a unifier.
|
| variable_kind [MultiEquation] |
There are two kinds of variable.
|