Module Types

module Types: sig .. end
This module provides a variety of functions for dealing with types, mostly built on top of DeBruijn and TypeCore.

Convenient combinators.

Dealing with triples.

val fst3 : 'a * 'b * 'c -> 'a
val snd3 : 'a * 'b * 'c -> 'b
val thd3 : 'a * 'b * 'c -> 'c


val (!!) : TypeCore.typ -> TypeCore.var
Asserts that this type is actually a TyOpen.
val (!!=) : TypeCore.typ -> TypeCore.var
Asserts that this type is actually a TySingleton (TyOpen ...).
val ( !* ) : 'a Lazy.t -> 'a
This is Lazy.force.
val (>>=) : 'a option -> ('a -> 'b option) -> 'b option
bind for the option monad.
val (|||) : 'a option -> 'a option -> 'a option
either operator for the option monad
val (^=>) : bool -> bool -> bool
The standard implication connector, with the right associativity.
val (|>) : 'a -> ('a -> 'b) -> 'b
The pipe operator.

Normalizing types.

These functions, when combined with TypeCore.modulo_flex, allow one to manipulate a "canonical" representation of a type, where permissions have been stripped out and unfoldings have been performed. One will still want to use Permissions.open_all_rigid_in, though.
val expand_if_one_branch : TypeCore.env -> TypeCore.typ -> TypeCore.typ
expand_if_one_branch env t expands t when t is either a type abbreviation, or a data type with one branch.
val collect : TypeCore.typ -> TypeCore.typ * TypeCore.typ list
collect t syntactically separates t into a structural part and a permission part, i.e. it extracts all the permissions hidden inside t and returns them as a separate list.


Data types have branches. A branch has a _parent_ data type. branch is the type that represents an actual branch under a TyConcrete; a branch in a data type definition can be any type, most functions return a typ.
val branches_for_branch : TypeCore.env -> TypeCore.branch -> TypeCore.typ list
Given a branch, get all the other branches of the parent type.
val branches_for_datacon : TypeCore.env -> TypeCore.resolved_datacon -> TypeCore.typ list
Given a resolved_datacon, get all the other branches of the parent type.
val branch_for_datacon : TypeCore.env -> TypeCore.resolved_datacon -> TypeCore.typ
Given a resolved_datacon, get the corresponding branch.
val fields_for_datacon : TypeCore.env -> TypeCore.resolved_datacon -> list
Given a resolved_datacon, get all its fields.
val flavor_for_datacon : TypeCore.env -> TypeCore.resolved_datacon -> DataTypeFlavor.flavor
Given a resolved_datacon, get its flavor.

Manipulating types.

Building types.

We provide a set of wrappers to easily build types. These often perform extra checks.
val ty_unit : TypeCore.typ
Shortcut for the empty tuple TyTuple [].
val ty_tuple : TypeCore.typ list -> TypeCore.typ
A tuple.
val (@->) : TypeCore.typ -> TypeCore.typ -> TypeCore.typ
An arrow. The operator has the right associativity.
val ty_bar : TypeCore.typ -> TypeCore.typ -> TypeCore.typ
ty_bar t1 t2 is TyBar (t1, t2) is t2 is not TyEmpty, t1 otherwise.
val ty_app : TypeCore.typ -> TypeCore.typ list -> TypeCore.typ
ty_app t ts is TyApp (t, ts) if List.length ts > 0, t otherwise.
val ty_equals : TypeCore.var -> TypeCore.typ
Shortcut for TySingleton (TyOpen _).
val ty_open : TypeCore.var -> TypeCore.typ
A open variable.


We provide a set of wrappers to inspect types.
val is_tyapp : TypeCore.typ -> (TypeCore.var * TypeCore.typ list) option
Works with either TyOpen or TyApp.
val is_star : TypeCore.env -> TypeCore.typ -> bool
Calls modulo_flex and expand_if_one_branch before determining whether it's a TyStar or not.
val is_concrete : TypeCore.typ -> bool
Is this a concrete type?
val assert_concrete : TypeCore.typ -> TypeCore.branch
If you know this is a concrete type, extract the branch.
val is_tyopen : TypeCore.typ -> bool
Is this an open variable?
val is_abbrev : TypeCore.env -> TypeCore.var -> bool
Determines whether a variable corresponds to a type abbreviation definition.
val is_term : TypeCore.env -> TypeCore.var -> bool
Has this variable kind term?
val is_perm : TypeCore.env -> TypeCore.var -> bool
Has this variable kind perm?
val is_type : TypeCore.env -> TypeCore.var -> bool
Has this variable kind type?
val is_user : -> bool
Is this name user-provided?

Folding and flattening

val flatten_star : TypeCore.env -> TypeCore.typ -> TypeCore.typ list
Transform a TyStar into a flat list of permissions. This function performs quite a bit of work to make sure there are no nested permissions: it calls modulo_flex and expand_if_one_branch and extract all permissions nested in t when it encounters x @ t.
val fold_star : TypeCore.typ list -> TypeCore.typ
This function has a special case to make sure it doesn't introduce useless TyEmptys.
val fold_forall : (TypeCore.type_binding * TypeCore.flavor) list ->
TypeCore.typ -> TypeCore.typ
Fold a type under a series of universal bindings.
val fold_exists : (TypeCore.type_binding * TypeCore.flavor) list ->
TypeCore.typ -> TypeCore.typ
Fold a type under a series of existential bindings.

Type traversals

val mark_reachable : TypeCore.env -> TypeCore.typ -> TypeCore.env
Mark all type variables reachable from a type, including via the ambient permissions.

Binding and instantiating

Binding types

val bind_datacon_parameters : TypeCore.env ->
Kind.kind ->
TypeCore.typ list -> TypeCore.env * TypeCore.var list * TypeCore.typ list
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.


val instantiate_type : TypeCore.typ -> TypeCore.typ list -> TypeCore.typ
instantiate_type t ts substitutes the givens types t0, ..., tn for TyBound 0, ... TyBound n in t.
val find_and_instantiate_branch : TypeCore.env ->
TypeCore.var -> -> TypeCore.typ list -> TypeCore.typ
Find the branch and substitute the data type's parameters in it.


Various getters

val get_location : TypeCore.env -> TypeCore.var -> TypeCore.location
val get_adopts_clause : TypeCore.env -> TypeCore.var -> TypeCore.typ
val get_arity : TypeCore.env -> TypeCore.var -> int
val get_kind_for_type : TypeCore.env -> TypeCore.typ -> Kind.kind
val variance : TypeCore.env -> TypeCore.var -> int -> TypeCore.variance
Get the variance of the i-th parameter of a data type.
val fresh_auto_name : string ->
val make_datacon_letters : TypeCore.env -> Kind.kind -> bool -> TypeCore.env * TypeCore.var list
module TypePrinter: sig .. end
Our not-so-pretty printer for types.