Module Mlsem_common.GREnv

Same as REnv, but holding gradual types.

include Env.Env with type ty := Mlsem_types.GTy.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.GTy.t -> t
val construct : (Variable.t * Mlsem_types.GTy.t) list -> t
val add : Variable.t -> Mlsem_types.GTy.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.GTy.t -> t -> t

Binds a variable, overriding any previous binding.

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

    if the variable is not bound.

val find_opt : Variable.t -> t -> Mlsem_types.GTy.t option
val map : (Mlsem_types.GTy.t -> Mlsem_types.GTy.t) -> t -> t
val rm : Variable.t -> t -> t

Removes a binding. The result is not necessarily a weaker environment, as the set of type variables captured tvars may decrease.

val filter : (Variable.t -> Mlsem_types.GTy.t -> bool) -> t -> t

Filters bindings. The result is not necessarily a weaker environment, as the set of type variables captured tvars may decrease.

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.GTy.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 : unsat:t -> t -> t

neg followed by disj_approx; ~unsat represents the unsatisfiable refinement, whose representation may depend on the variables in scope.

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.