Builder (mlsem-types.Mlsem_types.GTy.Builder)

val dyn : unit -> Ty.t

dyn () returns a fresh instance of the dyn type for the builder. Each occurrence of dyn in a type should use a fresh instance.

val refresh : Ty.t -> Ty.t

refresh ty refreshes the instances of dyn in ty. This function should be called when combining multiple occurrences of a gradual type that is in the process of being built.

val non_gradual : Ty.t -> bool

non_gradual ty returns true if and only if ty is not gradual, i.e. it has no instance of dyn.

val is_valid : Ty.t -> bool

is_valid ty returns true if and only if ty is a valid gradual type, i.e. it has no invariant instance of dyn.

val build : Ty.t -> t

build ty builds the gradual type corresponding to ty. Raises Invalid_argument if a dyn occurs in an invariant position.

val all_dyn_vars : unit -> TVarSet.t

all_dyn_vars () returns the current set of all dyn vars.

val pp : Stdlib.Format.formatter -> Ty.t -> unit

val pp' : Mlsem_types__.Tvar.Subst.t -> Stdlib.Format.formatter -> Ty.t -> unit