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.

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

An arrow.

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.

If you know this is a concrete type, extract the branch.

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.

bind_data_group_datacons env group extends the environment with bindings for the data constructors of the data group.

Used by the type-checker to process local type declarations.

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

bind_datacon_parameters env k ts takes the kind of the parent data type k, its branches ts, and introduces open variables that stand for the data type's parameters in all the branches.

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

Bind a flexible type variable.

Bind a flexible type variables before another one.

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.

Record exported types and data constructors in an implementation.

Record exported values in an implementation.

Record exported types and data constructors from an interface.

Record exported values from an interface.

bind_nonlocal env (x, kind, v) binds the unqualified variable x to the non-local name v, whose kind is kind.

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).

bindings_data_group_types group returns a list of bindings for the types of the data group.

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

Given a resolved_datacon, get the corresponding branch.

Given a branch, get all the other branches of the parent type.

Given a resolved_datacon, get all the other branches of the parent type.

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

bv p returns the names bound by the pattern p, in left-to-right order.

The second operation related to interfaces consists in checking that an implementation satisfies a given interface.

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.

check_implementation env i checks that the implementation file i is well-formed, i.e.

check_implementation env i checks that the interface file i is well-formed, i.e.

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.

Ordering.

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.

Need to translate a branch definition b with nested permissions ps into a type? Use construct_branch b ps.

A CPS version of List.map.

Report some debugging information.

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

dissolve env m has the effect of introducing a new binding of x for every existing binding of m::x.

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

Drop the derivation information and just get an env option.

duplicable is implication ModeDuplicable.

The () (unit) expression.

An empty environment.

The empty environment.

Enable debugging information.

Enter another toplevel unit (implementation, interface).

enter_module env m resets env so that it is ready to translate another unit (interface or implementation) named m.

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.

equal tests the equality of two kinds.

Equality of lists, up to equality of elements.

Report a fatal error.

Remove any ELocated node in front of an expression.

Checking for duplicates in a list.

expand_if_one_branch env t expands t when t is either a type abbreviation, or a data type with one branch.

extend env bindings iterates over the list bindings, from left to right, and for each binding of the form (x, kind, loc), it extends the environment by binding the unqualified variable x to a new local name whose kind is kind.

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...

Given a resolved_datacon, get all its fields.

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

Find the branch and substitute the data type's parameters in it.

Need to see the branch hidden beneath a type? Use this helper.

find_kind env x returns the kind of the possibly-qualified variable x.

find_nonlocal_variable env x looks up the unqualified variable x in the environment env.

same as Map.find but returns a 'a option

find_qualified_var env mname x finds name x as exported by module mname.

find_unqualified_var env x finds the name x as exported by the current module.

find_variable env x looks up the possibly-qualified variable x in the environment env.

Transform a TyStar into a flat list of permissions.

Given a resolved_datacon, get its flavor.

General fold operation.

Fold over all opened type definitions.

Fold a type under a series of existential bindings.

Fold a type under a series of universal bindings.

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.

This function has a special case to make sure it doesn't introduce useless TyEmptys.

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 returns the list of names that are exported by 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.

Get the variance, asserting that this variable is that of a type definition.

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.

This error is detected during the translation towards the internal syntax.

The safe version of the function found in TypeCore.

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.

The first operation related to interfaces consists in importing a given interface into an environment.

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

infer_reset env ty returns the kind of the type ty.

init filename must be called before using the lexer.

The safe version of the function found in TypeCore.

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

instantiate_type t ts substitutes the givens types t0, ..., tn for TyBound 0, ... TyBound n in t.

inter m1 m2 keeps the values from m1

internal_print fact is a textual representation of the fact fact.

interpret is a driver for the interpreter.

Determines whether a variable corresponds to a type abbreviation definition.

Is this a concrete type?

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.

Has this variable kind perm?

Calls modulo_flex and expand_if_one_branch before determining whether it's a TyStar or not.

Has this variable kind term?

Works with either TyOpen or TyApp.

Is this an open variable?

Has this variable kind type?

Is this name user-provided?

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.

locate env loc updates env with the location loc.

Get the current location in the environment.

location env is the current location in the source code.

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

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

General map operation.

A sharing-preserving version of List.map.

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.

Composition of List.map and filter_some.

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

This function may raise an exception that will be later on catched in Driver, or emit a warning, or do nothing, depending on whether the error has been tweaked with the warn/error string.

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)

An environment contains a kind-checking environment that contains mapping for all the current module's _dependencies_.

Get the current module name.

module_name env is the name of the current module.

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.

names ty returns a list of the names introduced by the type ty, via TyNameIntro forms.

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.

Get the env option part of a result.

p displays the position that is passed as an argument.

The () (unit) pattern.

This is a slightly different combinator, that allows you to try several rules to prove the same judgement.

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

Set up the module to take into account the warn / error / silent settings specified on the command-line.

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.

print and print_kind convert a kind to a textual representation.

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

print_error displays a lexer error.

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.

Use this to transform the branch from a type_def into something that's suitable for manipulation as a type.

resolve_datacon env dref looks up the possibly-qualified data constructor dref.datacon_unresolved in the environment env.

Equality function on resolved data constructors.

This function converts a type expressed in the internal syntax back to the surface syntax.

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 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.

split_map f xs is equivalent to List.split (List.map f xs).

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).

This function converts an internal name to a possibly-qualified name in the surface syntax.

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.

Need to modify the branch hidden beneath a type? Use this helper.

translate_data_type_group extend env group translates a data type group.

translate_implementation translates a compilation unit.

translate_interface translates an interface.

translate_type_reset 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 branch.

Same thing with a data type group.

The terminal's width.

ty_app t ts is TyApp (t, ts) if List.length ts > 0, t otherwise.

ty_bar t1 t2 is TyBar (t1, t2) is t2 is not TyEmpty, t1 otherwise.

The bottom type.

Shortcut for TySingleton (TyOpen _).

A open variable.

A tuple.

Shortcut for the empty tuple TyTuple [].

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.

Update variance.

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.

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