Previous  Up  Next

Module TypeCore

module TypeCore: sig .. end
This module defines the syntax of types, as manipulated by the type-checker.

This module defines the syntax of types, as manipulated by the type-checker.

The definition of types


module Field: module type of Variable  with type name = SurfaceSyntax.Field.name

Auxiliary definitions


type name =
| User of Module.name * Variable.name
| Auto of Variable.name
The type of user-generated or auto-generated names.
type location = Lexing.position * Lexing.position
Our locations are made up of ranges.
type quantifier =
| Forall
| Exists
A quantifier is universal or existential.
type type_binding = name * Kind.kind * location
A type binding defines a type variable bound in a type.
type flavor = SurfaceSyntax.binding_flavor =
| UserIntroduced
| AutoIntroduced
A type binding can be either user-provided, through a universal quantification for instance, or auto-generated, by the desugaring pass for instance.
type db_index = int
In the surface syntax, variables are named. Here, variables are represented as de Bruijn indices. We keep a variable name at each binding site as a pretty-printing hint.
type var
We adopt a locally nameless style; therefore, variables can be opened. This is the type of open variales; it's abstract, because we provide a set of wrappers and want to prevent mistakes in client code.

The type of types


type data_field_def = Field.name * typ
A field in a data type
type typ =
| TyUnknown
| TyDynamic
| TyBound of db_index
| TyOpen of var
| TyQ of quantifier * type_binding * flavor * typ
| TyApp of typ * typ list
| TyTuple of typ list
| TyConcrete of branch
| TySingleton of typ
| TyArrow of typ * typ
| TyBar of typ * typ
| TyAnchoredPermission of typ * typ
| TyEmpty
| TyStar of typ * typ
| TyAnd of mode_constraint * typ
The type of types.
type mode_constraint = Mode.mode * typ 
type branch = {
   branch_flavor : DataTypeFlavor.flavor;
   branch_datacon : resolved_datacon;
   branch_fields : data_field_def list;
   branch_adopts : typ;
} 
type resolved_datacon = typ * Datacon.name

Type definitions


type variance = SurfaceSyntax.variance =
| Invariant
| Covariant
| Contravariant
| Bivariant
Our data constructors have the standard variance.
type type_def =
| Concrete of typ list
| Abstract
| Abbrev of typ 
type data_type = {
   data_name : Variable.name;
   data_location : location;
   data_definition : type_def;
   data_variance : variance list;
   data_fact : Fact.fact;
   data_kind : Kind.kind;
} 
type data_type_group = {
   group_recursive : SurfaceSyntax.rec_flag;
   group_items : data_type list;
}

Various useful modules


module DataconMap: MzMap.S  with type key = Module.name * Datacon.name
module VarMap: MzMap.S  with type key = var
This module provides a clean way to map a variable to any given piece of data. 
module IVarMap: Fix.IMPERATIVE_MAPS  with type key = var
This is an imperative version of VarMap, in the form expected by Fix.

Program-wide environment


type env
This is the environment that we use throughout Mezzo.
val empty_env : env
The empty environment.
val locate : env -> location -> env
Refresh the location of an environment.
val location : env -> location
Get the current location in the environment.
val module_name : env -> Module.name
Get the current module name.
val enter_module : env -> Module.name -> env
Enter another toplevel unit (implementation, interface).
val is_inconsistent : env -> bool
Is the current environment inconsistent?
val mark_inconsistent : env -> env
Mark the environment as being inconsistent.
val modify_kenv : env ->
       (var KindCheck.env ->
        (var KindCheck.env -> (env -> 'a) -> 'a) -> 'a) ->
       'a
An environment contains a kind-checking environment that contains mapping for all the current module's _dependencies_.
val kenv : env -> var KindCheck.env

Flexible variables



A client of this module, in order to properly deal with flexible variables, must use the wrappers below.
val is_flexible : env -> var -> bool
Is this variable a flexible type variable or not?
val is_rigid : env -> var -> bool
val modulo_flex : env -> typ -> typ
Make sure we're dealing with the real representation of a variable. Any function wishing to examine either a type or a variable should call this function; then, whenever they encounter a TyOpen, they need not worry about it having a structure (because it won't). modulo_flex env ty raises UnboundPoint if it finds a flexible variable that does not exist in env. This behavior is exploited by advanced users...

Low-level operations


val import_flex_instanciations_raw : env -> env -> env
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. This is a low-level operation, and you're better off using Permissions.import_flex_instanciations.
val instantiate_flexible_raw : env -> var -> typ -> env option
instantiate_raw env var t tries to instantiate the flexible variable var with t. However, because of various reasons (e.g. levels) this instantiation may or may not be possible directly. There are extra steps needed (e.g. reanchoring) to properly perform this operation, so please use Permissions.instantiate_flexible instead.
val same : env -> var -> var -> bool
Are these two variables the same? This is a low-level operation and you probably want to use equal instead.
val merge_left : env -> var -> var -> env option
Merge two variables while keeping the information about the left one. You must make sure that both variables have been run through modulo_flex_v first. This is a low-level operation and you probably want to use Permissions.unify instead.
val get_floating_permissions : env -> typ list
Get the list of permissions that are floating in this environment.
val set_floating_permissions : env -> typ list -> env
Set the list of permissions that are floating in this environment.

Playing with variables


val get_names : env -> var -> name list
Get the names associated to a variable.
val get_name : env -> var -> name
val get_kind : env -> var -> Kind.kind
Get the kind of any given variable.
val get_fact : env -> var -> Fact.fact
Get a fact
val get_locations : env -> var -> location list
Get the locations
val get_definition : env -> var -> type_def option
Get the definition, if any.
val get_variance : env -> var -> variance list
Get the variance, asserting that this variable is that of a type definition.

Low-level variable manipulation functions.


val add_location : env -> var -> location -> env

Low-level permissions manipulation functions.



If you're considering playing with the list of permissions available for a given variable, you should consider using Permissions.add and Permissions.sub instead of these low-level, potentially dangerous functions.
val get_permissions : env -> var -> typ list
Get the permissions of a term variable.
val set_permissions : env -> var -> typ list -> env
Set the permissions of a term variable.
val reset_permissions : env -> var -> env
Reset the permissions of a term variable.

Low-level setters



These functions should only be used during the very first few stages of type-checking.
val set_fact : env -> var -> Fact.fact -> env
Set a fact
val set_definition : env ->
       var -> type_def -> variance list -> env
Set a definition. This asserts that there was no definition before.
val update_definition : env ->
       var -> (type_def -> type_def) -> env
Update a definition. This asserts that there used to be a definition before.
val update_variance : env ->
       var ->
       (variance list -> variance list) -> env
Update variance.

Fun with sub-environments


exception UnboundPoint
val clean : env -> env -> typ -> typ
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
val equal : env -> typ -> typ -> bool
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.
val resolved_datacons_equal : env ->
       resolved_datacon -> resolved_datacon -> bool
Equality function on resolved data constructors.

Data type definitions



The branches in data type definitions are now represented as types. If the branch contains permissions, there will be a TyBar. There may be other type constructors above the TyConcrete. Thus, we provide a set of wrappers to peek at / modify the branch found below other type constructors.
val construct_branch : type_binding list ->
       branch -> typ list -> typ
Need to translate a branch definition b with nested permissions ps into a type? Use construct_branch b ps.
val find_branch : typ -> branch
Need to see the branch hidden beneath a type? Use this helper. This will _not_ open quantifiers.
val touch_branch : typ -> (branch -> branch) -> typ
Need to modify the branch hidden beneath a type? Use this helper. This will _not_ open quantifiers.

Binding


val bind_rigid : env -> type_binding -> env * var
Bind a rigid type variable.
val bind_flexible : env -> type_binding -> env * var
Bind a flexible type variable.
val bind_flexible_before : env ->
       type_binding -> var -> env * var
Bind a flexible type variables before another one.

Iterating on the bindings



We provide a set of fold/map operations on variables defined in the environment. Existential variables are not folded over, as they only serve as placeholders; only rigid variables are considered when performing the various fold operations.

Of course, we only fold over variables that have been opened in the current environment.

val fold_definitions : env ->
       ('acc -> var -> type_def -> 'acc) -> 'acc -> 'acc
Fold over all opened type definitions.
val fold_terms : env ->
       ('acc -> var -> typ list -> 'acc) -> 'acc -> 'acc
Fold over all opened terms, providing the corresponding var and permissions.
val fold : env -> ('acc -> var -> 'acc) -> 'acc -> 'acc
General fold operation.
val map : env -> (var -> 'a) -> 'a list
General map operation.

Marks


val is_marked : env -> var -> bool
val mark : env -> var -> env
val refresh_mark : env -> env

Visitors for the internal syntax of types



A generic visitor.
class virtual [['env, 'result]] visitor : object .. end

A map specialization of the visitor.
class ['env] map : object .. end

An iter specialization of the visitor.
class ['env] iter : object .. end

Misc.


val ty_bottom : typ
The bottom type.
val is_non_bottom : typ -> typ option