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

Operators

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.

Branches.

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 -> TypeCore.Field.name 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.

Inspecting

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 : TypeCore.name -> 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.

Instantiation

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 -> Datacon.name -> TypeCore.typ list -> TypeCore.typ

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

Miscellaneous

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

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.