Index of values

This is Lazy.force.

Asserts that this type is actually a TyOpen.

Asserts that this type is actually a TySingleton (TyOpen ...).

Use this operator to chain the premises of a rule in a monadic style.

bind for the option monad.

Simple composition that discards derivations.

Perform an operation on the env part of a state without giving any justification for it.

The standard implication connector, with the right associativity.

The pipe operator.

either operator for the option monad

add env var t adds t to the list of permissions for p, performing all the necessary legwork.

add_perm env t adds a type t with kind PERM to env, returning the new environment.

A utility function for extending a fact with the statement ``without any hypotheses, this type is exclusive''.

Perform variance computations on a set of data types, and return an environment where variances have been updated.

analyze_data_types env vars assumes that vars forms a group of mutually recursive algebraic data type definitions.

This is a way of proving a judgement by using a rule without premises, i.e.

arity k is the arity of k, viewed as an arrow kind.

as_arrow k transforms the kind k to an n-ary arrow kind.

assume env c produces a new environment where the mode constraint c is assumed (i.e., it is added to the environment as a new hypothesis).

Make all your pretty-printers work with buffers, use them with %a and use this to get a Printf.eprintf

Make all your pretty-printers work with buffers, use them with %a and use this to get a Printf.fprintf

Maps None to None and Some x to f x.

This function processes a data_type_group, and opens the corresponding binders in the toplevel_items that follow.

Bind a set of term variables (let-bindings).

Bind a flexible type variable.

bind_rigid_in_type env binding ty opens the binding binding, whose scope is the type ty, by replacing the bound variable with a new flexible variable.

Bind a set of multiple bindings (and keyword).

Bind a rigid type variable.

bind_rigid_in_type env binding ty opens the binding binding, whose scope is the type ty, by replacing the bound variable with a rigid variable.

Bind a set of type variables (Λ-bindings).

In case you need to ignore some stuff.

The least fact is defined as constant Mode.bottom.

The least element of the lattice.

Make a title.

Make all your pretty-printers work with buffers, use them with %a and use this to get a Printf.printf

Make all your pretty-printers work with buffers and use this to get a Printf.sprintf

Because this is a tricky operation, the check function needs access to both the internal representation of the type-checked file (this is a TypeCore.env), the external representation of the interface (this is a SurfaceSyntax.interface), and the list of exported variables from the implementation, along with their canonical names and kinds (Driver knows how to figure that out).

Assert something, otherwise display an error message and fail

check_declaration_group env declarations items type-checks a set of top-level declarations; in order to do that, it will end up opening certain binders, which is why it takes a list of items which will be correctly transformed so as to refer to the variables that have been opened.

Checking for duplicates in a list.

clean env sub_env t tries to clean up t, found in sub_env, so that it makes sense in env, and throws UnboundPoint otherwise

collect t syntactically separates t into a structural part and a permission part, i.e.

They have been chosen arbitrarily out of the 256-color set available.

Same as List.combine but for triples instead of pairs.

complete fact completes an incomplete fact (i.e., a mode map whose domain does not contain all modes) so as to obtain a valid fact.

compose fact facts composes a fact of arity n -- i.e.

Conjunction of hypotheses.

A mode m can be viewed as a fact: every mode m' that is equal to or above m is mapped to true, the empty conjunction, and every mode m' that does not satisfy this is mapped to false.

A CPS version of List.map.

Report some debugging information.

A utility function for removing the possibility that ``this type is exclusive''.

domain a is a fresh copy of an initial segment of the array a whose length is extent a.

Tie the knot.

Get the env option part of a result.

duplicable is implication ModeDuplicable.

The () (unit) expression.

The empty environment.

Enable debugging information.

Equality.

equal env t1 t2 tells whether t1 and t2 can be determined to be equal in environment env; it raises UnboundPoint is any of these two types doesn't make sense in env.

Equality.

Equality of lists, up to equality of elements.

Report a fatal error.

Remove any ELocated node in front of an expression.

extent a is the length of an initial segment of the array a that is sufficiently large to contain all set operations ever performed.

When you're sure you have Some

If a derivation fails...

Turns [Some a; None; ...] into [a; ...]

same as Map.find but returns a 'a option

General fold operation.

Fold over all opened types definitions.

Same as fold_left2 except that the function takes the current index in the list

Same as fold_left2 but with three lists.

Same as fold_left except that the function takes the current index in the list

Same as fold_right except that the function takes the current index in the list.

Fold over all opened terms, providing the corresponding var and permissions.

This is only for display purposes.

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

Get the definition, if any.

get_exports env mname lists the names exported by module mname in env.

Get a fact

Get the list of permissions that are floating in this environment.

Get the kind of any given variable.

Get the locations

Get the names associated to a variable.

Get the permissions of a term variable.

has_mode mode env ty tells whether the predicate mode ty is satisfied, using the information stored in env about the ambient type definitions and mode assumptions.

...

Map a function and then discard the result.

implication h m constructs a fact of the form h => m.

import_flex_instanciations env sub_env brings into env all the flexible variable instanciations that happened in sub_env without modifying the rest of env.

Import a given module into scope.

Find the index of the first element in a list that satisfies a predicate.

init filename must be called before using the lexer.

instantiate env var t tries to instantiate the flexible variable var with t.

inter m1 m2 keeps the values from m1

internal_print fact is a textual representation of the fact fact.

A specialized version of has_mode.

A specialized version of has_mode.

Is this variable a flexible type variable or not?

This tells whether a result is successful or not.

Is the current environment inconsistent?

Recognition of maximal facts is not performed.

A test for the top element of the lattice.

Inspecting

The name speaks for itself

Same as List.iteri but with two lists.

Same as List.iter but with three lists.

The lattice join (i.e., least upper bound).

Only keep the duplicable portions of the environment.

Get a list of all keys in a map.

Get the last element of a list.

The lattice ordering.

Compare two variances and tell if the second one subsumes the first one.

The lattice ordering.

lift i t lifts type t by i

Refresh the location of an environment.

Get the current location in the environment.

make n f creates [f 1; ...; f n].

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

General map operation.

map f opt maps None to None and Some a to Some (f a)

Same as map2 but pass an extra parameter that represents the index

map_none n opt maps None to n and Some m to m.

Map and discard some elements at the same time.

Mark the environment as being inconsistent.

Mark all type variables reachable from a type, including via the ambient permissions.

Find the biggest element in a list

The lattice meet.

The lattice meet (i.e., greatest lower bound).

When the control-flow diverges, one needs to merge the environments, that is, compute a set of permissions that subsumes the two environments.

Merge two variables while keeping the information about the left one.

minus m1 m2 returns m1 minus all the elements that are also in m2, that is, m1 \ (m1 ∩ m2)

Get the current module name.

Make sure we're dealing with the real representation of a variable.

Analogous to error, but does not raise any exception; instead, just produces and returns the error message as a string.

Here is how to not prove a judgement.

If you're iterating over a series of premises, it is sometimes convenient to say that one of them requires no special operations because of a certain rule...

Just like List.nth except it returns an Option type.

p displays the position that is passed as an argument.

The () (unit) pattern.

A fact for a parameter p is a conjunction of implications of the form m p => m, where m ranges over every mode.

point_by_name env ?mname x finds name x as exported by module mname (default: module_name env) in env.

The most intuitive way of writing down the premises for a judgement: you just list all the results that have to be successful for this judgement to be true, and premises takes care of chaining them left-to-right.

print param head fact is a textual representation of the fact fact.

Printing.

Once an exception is catched, it can be printed with Log.error and %a...

print_error displays a lexer error.

print_kind converts a kind to a textual representation.

print_position displays the lexer's current position.

print_signature prints out (in order, and in a fancy manner) the types that have been found in the file.

process doesn't catch exceptions.

This is the final operator that finishes a derivation.

This function raises an exception that will be later on catched in Driver.

Perform an operation with the debug level raised by an amount.

Same as fold_left, but start folding on the head of the list instead of giving an initial element.

replace s1 s2 s replaces all occurrences of s1 with s2 in s.

Reset the cursor to the top-left corner of the screen

Reset the permissions of a term variable.

Equality function on resolved data constructors.

run runs the specified function and prints any error that may pop up.

Are these two variables the same? This is a low-level operation and you probably want to use equal instead.

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

Set a definition.

Set a fact

Set the list of permissions that are floating in this environment.

Set the current module name.

Set the permissions of a term variable.

Perform an operation with the debug output disabled.

split s c will split string s on character c

Same as List.split but for triples instead of pairs.

sub env var t tries to extract t from the available permissions for var and returns, if successful, the resulting environment.

sub_type env t1 t2 tries to perform t1 - t2.

substring s i j will return all characters from string s comprised between indices i (included) and j (excluded).

If f may convert an 'a into a 'b, then take f l returns the first convertible element in the list, along with the remaining elements in the list.

The terminal's height.

to_list translates the map to a list.

token is the main entry point of the lexer.

The greatest element of the lattice.

tpsubst env t1 var t2 subtitutes t1 for var in t2.

translate_data_type_group bind env group translates a data type group.

translate_implementation translates a compilation unit.

translate_interface translates an interface.

translate_type translates a type.

This is the most frequent way of trying to prove a judgement.

This is another way of proving a judgement, namely by trying several instances of the same rule on different items.

tsubst t1 i t2 substitues t1 for index i in t2

Same thing with a data type group.

Same thing with a data type branch.

The terminal's width.

unify env p1 p2 merges two vars, and takes care of dealing with how the permissions should be merged.

union m1 m2 keeps the values from m1

Since unit option and bool are isomorphic, this function implements the morphism from unit option to bool.

Update a definition.

Get the variance of the i-th parameter of a data type.

A warning is a message that always appears, even when debug is disabled.

This function will emit a warning or potentially raise an error, depending on the runtime flags.

xor m1 m2 is (m1 ∪ m2) \ (m1 ∩ m2)