Module Mlsem_common.Env

Typing environment: binds each variable in scope to a type scheme.

type t
val empty : t
val is_empty : t -> bool

Whether the environment has no binding at all.

val singleton : Variable.t -> Mlsem_types.TyScheme.t -> t
val construct : (Variable.t * Mlsem_types.TyScheme.t) list -> t

Binds a variable that is not already bound; use replace otherwise.

  • raises Invalid_argument

    if the variable is already bound.

val replace : Variable.t -> Mlsem_types.TyScheme.t -> t -> t

Binds a variable, overriding any previous binding.

val domain : t -> Variable.t list
val bindings : t -> (Variable.t * Mlsem_types.TyScheme.t) list
val mem : Variable.t -> t -> bool
  • raises Not_found

    if the variable is not bound.

val find_opt : Variable.t -> t -> Mlsem_types.TyScheme.t option
val rm : Variable.t -> t -> t
val rms : Variable.t list -> t -> t
val restrict : Variable.t list -> t -> t
val filter : (Variable.t -> Mlsem_types.TyScheme.t -> bool) -> t -> t
val tvars : t -> Mlsem_types.MVarSet.t

An over-approximation of the type variables occurring in the environment: it is maintained incrementally and not recomputed when a binding is combined with another. Sound wherever it is used to build a set of monomorphic variables, but not a reliable "occurs" test.

val substitute : Mlsem_types.Subst.t -> t -> t
val equiv : t -> t -> bool
val leq : t -> t -> bool

leq env1 env2 holds when env1 is at least as precise as env2: it binds at least the same variables, at smaller types.

val show : t -> string
val pp : Stdlib.Format.formatter -> t -> unit
val pp_filtered : string list -> Stdlib.Format.formatter -> t -> unit

Like pp, restricted to the variables whose display name is listed.