Module Mlsem_common.REnv

Refinement environment: a conjunction of constraints "variable v has type t", used to narrow a typing environment at a given program point.

Unlike Env, an REnv is partial: a variable it does not bind is unconstrained, i.e. implicitly bound to any (see REnv.find'). So the empty environment is the trivially true constraint, and an environment binding some variable to empty is unsatisfiable. This convention explains the approximations below.

include Env.Env with type ty := Mlsem_types.Ty.t
type t
val empty : t
val is_empty : t -> bool

Whether the environment has no binding at all.

val singleton : Variable.t -> Mlsem_types.Ty.t -> t
val construct : (Variable.t * Mlsem_types.Ty.t) list -> t
val add : Variable.t -> Mlsem_types.Ty.t -> t -> 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.Ty.t -> t -> t

Binds a variable, overriding any previous binding.

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

    if the variable is not bound.

val find_opt : Variable.t -> t -> Mlsem_types.Ty.t option
val rm : Variable.t -> t -> t
val rms : Variable.t list -> t -> t
val restrict : Variable.t list -> t -> t
val map : (Mlsem_types.Ty.t -> Mlsem_types.Ty.t) -> t -> t
val filter : (Variable.t -> Mlsem_types.Ty.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.

val find' : Variable.t -> t -> Mlsem_types.Ty.t

Like find, returning any instead of raising Not_found for an unbound variable. This is the reading that matches the partiality of an REnv.

val cap : t -> t -> t

Conjunction of two refinements.

val conj : t list -> t
val neg : t -> t list

Negation, as a disjunction: negating a conjunction of constraints yields one alternative per constraint. The empty environment (true) negates to the empty list (false).

val cup_approx : t -> t -> t

Over-approximation of the disjunction of two refinements: a variable constrained in only one of them becomes unconstrained, since nothing can be assumed about it in the other branch.

val disj_approx : t list -> t
  • raises Invalid_argument

    on the empty list, which has no representation.

val neg_approx : t -> t option

neg followed by disj_approx; None represents the unsatisfiable refinement, which disj_approx cannot express.

val refine_env : Env.t -> t -> Env.t

refine_env env renv intersects the type of each variable of env with its constraint in renv. Variables of renv that are not in env are ignored: refining never extends the scope.

  • raises Invalid_argument

    if a refined variable has a scheme quantifying a variable that occurs in the constraint.