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.

Various useful modules


module DataconMap: MzMap.S  with type key = Module.name * Datacon.name
module Field: module type of Variable  with type name = SurfaceSyntax.Field.name

The definition of types



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 type_binding = name * Kind.kind * location
A type binding defines a type variable bound in a type.
type flavor = SurfaceSyntax.binding_flavor =
| CanInstantiate
| CannotInstantiate
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 =
| FieldValue of (Field.name * typ)
| FieldPermission of typ
A field in a data type
type typ =
| TyUnknown
| TyDynamic
| TyBound of db_index
| TyOpen of var
| TyForall of (type_binding * flavor) * typ
| TyExists of type_binding * typ
| TyApp of typ * typ list
| TyTuple of typ list
| TyConcreteUnfolded of resolved_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 resolved_datacon = typ * Datacon.name
Since data constructors are now properly scoped, they are resolved, that is, they are either attached to a point, or a De Bruijn index, which will later resolve to a point when we open the corresponding type definition. That way, we can easily jump from a data constructor to the corresponding type definition.
type mode_constraint = Mode.mode * typ

Type definitions


type ('flavor, 'datacon) data_type_def_branch = {
   branch_flavor :'flavor; (*DataTypeFlavor.flavor or unit*)
   branch_datacon :'datacon; (*Datacon.name or resolved_datacon*)
   branch_fields :data_field_def list; (*The type of the adoptees; initially it's bottom and then it gets instantiated to something less precise.*)
   branch_adopts :typ;
} 
type resolved_branch = (unit, resolved_datacon) data_type_def_branch 
type unresolved_branch = (DataTypeFlavor.flavor, Datacon.name) data_type_def_branch 
type data_type_def = unresolved_branch list 
type variance = SurfaceSyntax.variance =
| Invariant
| Covariant
| Contravariant
| Bivariant
Our data constructors have the standard variance.
type type_def = data_type_def option * variance list 
type data_type_group = (Variable.name * location * type_def * Fact.fact *
        Kind.kind)
       list

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 set_module_name : env -> Module.name -> env
Set the current module name.
val is_inconsistent : env -> bool
Is the current environment inconsistent?
val mark_inconsistent : env -> env
Mark the environment as being inconsistent.

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 instantiate_flexible : env -> var -> typ -> env option
instantiate 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.
val modulo_flex_v : env -> var -> 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 these two functions; then, whenever they encounter a TyOpen, they need not worry about it having a structure (because it won't).
val modulo_flex : env -> typ -> typ
val import_flex_instanciations : 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.

Low-level operations


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.

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 update_definition : env ->
       var -> (type_def -> type_def) -> env
Update a definition. This asserts that there used to be a definition before.
val set_definition : env -> var -> type_def -> env
Set a definition. This asserts that there was no definition before.

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.

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.

Exports


val get_exports : env ->
       Module.name -> (Variable.name * Kind.kind * var) list
get_exports env mname lists the names exported by module mname in env. mname can be either the current module name, or some other module name.
val point_by_name : env -> ?mname:Module.name -> Variable.name -> var
point_by_name env ?mname x finds name x as exported by module mname (default: module_name env) in env.

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

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