Module Checker.Type

the module holding the definition of semantic types, and various operations on them

module L = Location
type typ =
| T_Int
| T_Tuple of typ list
| T_IBorrow of Location.abstract_loc * typ
| T_MBorrow of Location.abstract_loc * typ * typ
| T_Function of typ list * typ

the abstract syntax of semantic types. Note that:

  • borrow types are always annotated with a plain L.abstract_loc without any path

  • mutable borrow types are of the form MBorrow(aloc, typ_read, typ_write), where typ_read is the type for reading from the mutable borrow, and typ_write is the type for writing to the mutable borrow. It should always be the case that:

    • typ_write is a subtype of typ_read
    • typ_read and typ_write have the same shape (differ only in abstract lactions)
type function_typ = {
params : typ list;
ret : typ;
constrs : Location.ConstrSet.t;
}

the type of top-level functions

val read_path : L.path -> typ -> Syntax.permission * typ * typ

read_path path typ select the path part of the type typ, returning a triple (permission, typ_read, typ_write) where:

  • permission is the permission allowed to access path in typ
  • typ_read is the type for reading from path in typ
  • typ_write is the type for writing to path in typ
val write_path : L.path -> typ -> typ -> typ
val get_borrows : only_toplevel:bool -> typ -> (L.path * Syntax.mutability * L.abstract_loc) Stdlib.Seq.t

get_borrows ~only_toplevel typ collect and return all borrows in typ. Every triple (path, mt, aloc) in the result indicates path at typ is a borrow type (IBorrow if mt = Imm or MBorrow if mt = Mut), with annotated abstract location aloc.

If only_toplevel is true, then only borrows types that are not behind another borrow type is returned.

val subtyp : L.ConstrSet.t -> typ -> typ -> L.ConstrSet.t

subtyp cset sub sup makes sub a sub type of sup by adding constraints to cset, and returns the new constraint set. If sub and sup don't have the same shape, TypeMismatch is raised.

val fresh_subtyp : L.ConstrSet.t -> typ -> typ * L.ConstrSet.t

fresh_subtyp cset typ creates a type typ' that is a sub type of typ. To make typ' a sub type of typ, some new constraints are added to cset and the new constraint set is returned together with typ'

val fresh_suptyp : L.ConstrSet.t -> typ -> typ * L.ConstrSet.t

fresh_suptyp cset typ creates a type typ' that is a super type of typ. To make typ' a super type of typ, some new constraints are added to cset and the new constraint set is returned together with typ'

val smallest_common_suptyp : L.ConstrSet.t -> typ list -> typ * L.ConstrSet.t

smallest_common_suptyp cset typs creates a type typ' that is a super type of every type in typs. Necessary new constraints are added to cset and returned together with typ'

val greatest_common_subtyp : L.ConstrSet.t -> typ list -> typ * L.ConstrSet.t

greatest_common_subtyp cset typs creates a type typ' that is a sub type of every type in typs. Necessary new constraints are added to cset and returned together with typ'

val instantiate_function : L.ConstrSet.t -> function_typ -> typ * L.ConstrSet.t

instantiate_function ctx func_typ instantiates top-level function type func_typ by substituting every abstract location in func_typ with new fresh abstract locations

val from_syntactic_typ : Syntax.typ -> typ

generate a fresh semantic type from a syntactic type