links

The Links Programming Language
IN THIS PACKAGE
Module Links_core . Types

Core types

type 'a stringmap = 'a Utility.StringMap.t
type 'a field_env = 'a stringmap
module TypeVarSet : sig ... end
val tag_expectation_mismatch : exn
type 'a point = 'a Unionfind.point
module Abstype : sig ... end
module Vars : sig ... end
module Policy : sig ... end
val process : Abstype.t
val list : Abstype.t
val event : Abstype.t
val dom_node : Abstype.t
val access_point : Abstype.t
val socket : Abstype.t
val spawn_location : Abstype.t
val transaction_time_data : Abstype.t
val valid_time_data : Abstype.t
type rec_id =
| MuBoundId of int
| NominalId of string
val show_rec_id : rec_id -> Ppx_deriving_runtime.string
module type RECIDMAP = Utility.Map with type key = rec_id
module type RECIDSET = Utility.Set with type elt = rec_id
type tygroup = {
id : int;
type_map : (CommonTypes.Quantifier.t list * typ) Utility.StringMap.t;
linearity_map : bool Utility.StringMap.t;
}
and rec_appl = {
r_name : string;
r_dual : bool;
r_unique_name : string;
r_quantifiers : CommonTypes.Kind.t list;
r_args : type_arg list;
r_unwind : type_arg list -> bool -> typ;
r_linear : unit -> bool option;
}
and tid = int
and typ =
| Not_typed
| Var of tid * CommonTypes.Kind.t * CommonTypes.Freedom.t
| Recursive of tid * CommonTypes.Kind.t * typ
| Alias of (string * CommonTypes.Kind.t list * type_arg list * bool) * typ
| Application of Abstype.t * type_arg list
| RecursiveApplication of rec_appl
| Meta of typ point
| Primitive of CommonTypes.Primitive.t
| Function of typ * row * typ
| Lolli of typ * row * typ
| Record of row
| Variant of row
| Table of CommonTypes.Temporality.t * typ * typ * typ
| Lens of Lens.Type.t
| ForAll of CommonTypes.Quantifier.t list * typ
| Effect of row
| Row of field_spec_map * row_var * bool
| Closed
| Absent
| Present of typ
| Input of typ * session_type
| Output of typ * session_type
| Select of row
| Choice of row
| Dual of typ
| End
and t = typ
and session_type = typ
and datatype = typ
and field_spec = typ
and field_spec_map = field_spec Utility.StringMap.t
and meta_type_var = typ point
and meta_row_var = row point
and meta_presence_var = typ point
and row = typ
and row' = field_spec_map * row_var * bool
and row_var = meta_row_var
val is_type_body : typ -> bool
val is_row_body : row -> bool
val is_field_spec_body : field_spec -> bool
module type Constraint = sig ... end

A constraint that a subkind imposes on types.

module Base : Constraint
module Unl : Constraint
module Mono : Constraint
val get_restriction_constraint : CommonTypes.Restriction.t -> (module Constraint) option

Get a Constraint for a specific subkind Restriction.t.

val dual_row : row -> row
val dual_type : datatype -> datatype
type alias_type = CommonTypes.Quantifier.t list * typ
val show_alias_type : alias_type -> Ppx_deriving_runtime.string
type tycon_spec = [
| `Alias of alias_type
| `Abstract of Abstype.t
| `Mutual of CommonTypes.Quantifier.t list * tygroup ref
]
type environment = datatype Env.String.t
type tycon_environment = tycon_spec Env.String.t
type typing_environment = {
var_env : environment;
rec_vars : Utility.StringSet.t;
tycon_env : tycon_environment;
effect_row : row;
desugared : bool;
}
val empty_typing_environment : typing_environment
val concrete_type : datatype -> datatype
val concrete_field_spec : field_spec -> field_spec
val normalise_datatype : datatype -> datatype
val normalise_row : row -> row
val normalise_typing_environment : typing_environment -> typing_environment
val for_all : (CommonTypes.Quantifier.t list * datatype) -> datatype
val unit_type : datatype

useful types

val string_type : datatype
val keys_type : datatype
val char_type : datatype
val bool_type : datatype
val int_type : datatype
val float_type : datatype
val datetime_type : datatype
val database_type : datatype
val xml_type : datatype
val empty_type : datatype
val wild_present : CommonTypes.Label.t * datatype
val hear_present : datatype -> CommonTypes.Label.t * datatype
val is_builtin_effect : string -> bool
val free_type_vars : datatype -> TypeVarSet.t

get type variables

val free_flexible_type_vars : datatype -> TypeVarSet.t
val free_row_type_vars : row -> TypeVarSet.t
val free_tyarg_vars : type_arg -> TypeVarSet.t
val free_bound_type_vars : typ -> Vars.vars_list
val free_bound_row_type_vars : row -> Vars.vars_list
val free_bound_type_arg_type_vars : type_arg -> Vars.vars_list
val type_arg_of_quantifier : CommonTypes.Quantifier.t -> type_arg
val quantifier_of_type_arg : type_arg -> CommonTypes.Quantifier.t
val quantifiers_of_type_args : type_arg list -> CommonTypes.Quantifier.t list
val primary_kind_of_type_arg : type_arg -> CommonTypes.PrimaryKind.t
val type_variable_counter : int ref

Fresh type variables

val fresh_raw_variable : unit -> int
val make_type_variable : int -> CommonTypes.Subkind.t -> datatype

type variable construction

val make_rigid_type_variable : int -> CommonTypes.Subkind.t -> datatype
val make_row_variable : int -> CommonTypes.Subkind.t -> row_var
val make_rigid_row_variable : int -> CommonTypes.Subkind.t -> row_var
val make_rigid_presence_variable : int -> CommonTypes.Subkind.t -> field_spec
val make_rigid_variable : int -> CommonTypes.Kind.t -> datatype
val fresh_type_variable : CommonTypes.Subkind.t -> datatype

fresh type variable generation

val fresh_rigid_type_variable : CommonTypes.Subkind.t -> datatype
val fresh_row_variable : CommonTypes.Subkind.t -> row_var
val fresh_rigid_row_variable : CommonTypes.Subkind.t -> row_var
val fresh_session_variable : CommonTypes.Linearity.t -> datatype
val fresh_presence_variable : CommonTypes.Subkind.t -> field_spec
val fresh_rigid_presence_variable : CommonTypes.Subkind.t -> field_spec

fresh quantifiers

val fresh_row_quantifier : CommonTypes.Subkind.t -> CommonTypes.Quantifier.t * row
val fresh_presence_quantifier : CommonTypes.Subkind.t -> CommonTypes.Quantifier.t * field_spec
val make_empty_closed_row : unit -> row

empty row constructors

val make_empty_open_row : CommonTypes.Subkind.t -> row
val make_singleton_closed_row : (string * field_spec) -> row

singleton row constructors

val make_singleton_open_row : (string * field_spec) -> CommonTypes.Subkind.t -> row
val is_closed_row : row -> bool

row predicates

val is_absent_from_row : string -> row -> bool
val is_tuple : ?allow_onetuples:bool -> row -> bool
val get_row_var : row -> int option

row_var retrieval

val make_closed_row : datatype field_env -> row

building rows

val row_with : (string * field_spec) -> row -> row
val extend_row : datatype field_env -> row -> row
val extend_row_safe : datatype field_env -> row -> row option
val open_row : CommonTypes.Subkind.t -> row -> row
val close_row : row -> row
val closed_wild_row : row
val remove_field : ?idempotent:bool -> CommonTypes.Label.t -> row -> row
val concrete_type' : datatype -> datatype

removing top-level meta typevars and aliases; imported from typeUtils.ml

val extract_row : datatype -> row

deconstructing rows

val extract_row_parts : datatype -> row'
val empty_field_env : field_spec_map

constants

val closed_row_var : row_var
val field_env_union : (field_spec_map * field_spec_map) -> field_spec_map
val is_canonical_row_var : row_var -> bool
val is_rigid_row : row -> bool
val is_rigid_row_with_var : int -> row -> bool
val is_flattened_row : row -> bool
val is_empty_row : row -> bool
val flatten_row : row -> row

Convert a row to the form (field_env, row_var) where row_var is of the form: `Closed | `Flexible var | `Rigid var | `Recursive

val unwrap_row : row -> row * row_var option

As flatten_row except if the flattened row_var is of the form:

`Recursive (var, rec_row)

then it is unwrapped. This ensures that all the fields are exposed in field_env.

Also returns the outermost `Recursive that was unwrapped if it exists, or None otherwise.

val unwrap_list_type : typ -> typ
val extract_tuple : row -> datatype list
val make_tuple_type : datatype list -> datatype

type constructors

val make_list_type : datatype -> datatype
val make_process_type : row -> datatype
val make_record_type : datatype field_env -> datatype
val make_variant_type : datatype field_env -> datatype
val make_tablehandle_alias : (datatype * datatype * datatype) -> datatype
val make_endbang_type : datatype
val make_transaction_time_data_type : datatype -> datatype
val make_valid_time_data_type : datatype -> datatype
val is_sub_type : (datatype * datatype) -> bool

subtyping

val is_sub_row : (row * row) -> bool
val extend_typing_environment : typing_environment -> typing_environment -> typing_environment
val print_types_pretty : bool Settings.setting

pretty printing

val string_of_datatype : ?policy:( unit -> Policy.t ) -> ?refresh_tyvar_names:bool -> datatype -> string
val string_of_row : ?policy:( unit -> Policy.t ) -> ?refresh_tyvar_names:bool -> row -> string
val string_of_presence : ?policy:( unit -> Policy.t ) -> ?refresh_tyvar_names:bool -> field_spec -> string
val string_of_type_arg : ?policy:( unit -> Policy.t ) -> ?refresh_tyvar_names:bool -> type_arg -> string
val string_of_row_var : ?policy:( unit -> Policy.t ) -> ?refresh_tyvar_names:bool -> row_var -> string
val string_of_tycon_spec : ?policy:( unit -> Policy.t ) -> ?refresh_tyvar_names:bool -> tycon_spec -> string
val string_of_environment : environment -> string
val string_of_typing_environment : typing_environment -> string
val build_tyvar_names : refresh_tyvar_names:bool -> ( 'a -> Vars.vars_list ) -> 'a list -> unit

generating type variable names

val add_tyvar_names : ( 'a -> Vars.vars_list ) -> 'a list -> unit
val make_pure_function_type : datatype list -> datatype -> datatype
val make_function_type : ?linear:bool -> datatype list -> row -> datatype -> datatype
val make_thunk_type : row -> datatype -> datatype
val pp : Format.formatter -> t -> unit
val pp_datatype : Format.formatter -> t -> unit
val pp_meta_type_var : Format.formatter -> meta_type_var -> unit
val pp_row : Format.formatter -> row -> unit
val pp_row' : Format.formatter -> row' -> unit
val pp_type_arg : Format.formatter -> type_arg -> unit
val pp_tycon_spec : Format.formatter -> tycon_spec -> unit
val recursive_applications : datatype -> string list
module type TYPE_VISITOR = sig ... end
class virtual type_predicate : object ... end