Module Mlsem_types.TVOp

val all_vars : kind -> Mlsem_types__.Tvar.MVarSet.t

Every type and row variable of that kind created since the program started (cf. Var.all_vars). all_vars KNoInfer is the set of rigid variables passed as monomorphic to tally.

val vars : Ty.t -> Mlsem_types__.Tvar.MVarSet.t

All the variables of a type. This is a syntactic notion inherited from sstt: a variable that does not affect the denotation of the type may or may not be reported, depending on the simplifications already applied to it.

val vars' : Ty.t list -> Mlsem_types__.Tvar.MVarSet.t
val top_vars : Ty.t -> Mlsem_types__.Tvar.MVarSet.t

Only the variables occurring at top level, i.e. not under a type constructor.

val strict_vars : Ty.t -> Mlsem_types__.Tvar.MVarSet.t

Only the variables occurring strictly under a type constructor.

val vars_of_kind : kind -> Ty.t -> Mlsem_types__.Tvar.MVarSet.t

Polarity

`Pos (resp. `Neg) means the type is monotonic (resp. anti-monotonic) in the variable, `Both that it is neither, and `None that the variable does not affect the denotation at all — which can happen because vars is syntactic, so a reported variable may be vacuous.

val polarity1 : TVar.t -> Ty.t -> [ `Both | `Neg | `Pos | `None ]
val polarity2 : RVar.t -> Ty.t -> [ `Both | `Neg | `Pos | `None ]
val polarity1' : TVar.t -> Ty.t list -> [ `Both | `Neg | `Pos | `None ]
val polarity2' : RVar.t -> Ty.t list -> [ `Both | `Neg | `Pos | `None ]

The primed variants below combine the polarities over a list of types, as if the variable occurred in each of them. Variables of polarity `None are omitted from the results.

val vars_with_polarity1 : Ty.t -> (TVar.t * [ `Both | `Neg | `Pos ]) list
val vars_with_polarity2 : Ty.t -> (RVar.t * [ `Both | `Neg | `Pos ]) list
val vars_with_polarity1' : Ty.t list -> (TVar.t * [ `Both | `Neg | `Pos ]) list
val vars_with_polarity2' : Ty.t list -> (RVar.t * [ `Both | `Neg | `Pos ]) list
val is_ground_typ : Ty.t -> bool
val refresh : ?preserve_names:bool -> kind:kind -> Mlsem_types__.Tvar.MVarSet.t -> Mlsem_types__.Tvar.Subst.t

A substitution renaming each given variable to a fresh one of the given kind. With ~preserve_names:true the fresh variables keep the display name of the originals, which makes them indistinguishable when printed with TVar.pp.

val shorten_names : ?kind:kind -> Mlsem_types__.Tvar.MVarSet.t -> Mlsem_types__.Tvar.Subst.t

A substitution renaming the given variables to fresh ones named a, b, … — for display only.

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

Prints with variables renamed by shorten_names.

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

Prints with variables renamed so that distinct variables print differently, even when they share a display name.

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

Prints the type after applying the given substitution.

val clean : pos1:Ty.t -> neg1:Ty.t -> pos2:Mlsem_types__.Tvar.Row.t -> neg2:Mlsem_types__.Tvar.Row.t -> Mlsem_types__.Tvar.MVarSet.t -> Ty.t -> Ty.t

clean p n mono t substitutes in t all variables not in mono and only occurring positively by p, and all variables not in mono and only occurring negatively by n

val clean_subst : pos1:Ty.t -> neg1:Ty.t -> pos2:Mlsem_types__.Tvar.Row.t -> neg2:Mlsem_types__.Tvar.Row.t -> Mlsem_types__.Tvar.MVarSet.t -> Ty.t -> Mlsem_types__.Tvar.Subst.t
val clean' : pos1:Ty.t -> neg1:Ty.t -> pos2:Mlsem_types__.Tvar.Row.t -> neg2:Mlsem_types__.Tvar.Row.t -> Mlsem_types__.Tvar.MVarSet.t -> Ty.t list -> Ty.t list
val clean_subst' : pos1:Ty.t -> neg1:Ty.t -> pos2:Mlsem_types__.Tvar.Row.t -> neg2:Mlsem_types__.Tvar.Row.t -> Mlsem_types__.Tvar.MVarSet.t -> Ty.t list -> Mlsem_types__.Tvar.Subst.t
val bot_instance : Mlsem_types__.Tvar.MVarSet.t -> Ty.t -> Ty.t

The smallest instance of the type, obtained by cleaning the variables outside mono with empty positively and any negatively.

val top_instance : Mlsem_types__.Tvar.MVarSet.t -> Ty.t -> Ty.t

Dual of bot_instance: the largest instance.

val tally : ?record:bool -> Mlsem_types__.Tvar.MVarSet.t -> (Ty.t * Ty.t) list -> Mlsem_types__.Tvar.Subst.t list

tally mono cs returns substitutions — of the variables not in mono — that make every constraint (s,t) of cs satisfy s ≤ t. The empty list means the constraints are unsatisfiable. Set ~record:false to keep the instance out of Recording's log; this matters for calls made while comparing candidate solutions, which are not part of the derivation being built.

val tally_const_rows : ?record:bool -> Mlsem_types__.Tvar.MVarSet.t -> (Ty.t * Ty.t) list -> Mlsem_types__.Tvar.Subst.t list

Like tally, but row variables are not instantiated with rows that introduce new fields.

val decompose : Mlsem_types__.Tvar.MVarSet.t -> Mlsem_types__.Tvar.Subst.t -> Mlsem_types__.Tvar.Subst.t -> Mlsem_types__.Tvar.Subst.t list

decompose mono s1 s2 returns the substitutions s such that applying s after s2 is at least as precise as s1; the empty list when s1 is not an instance of s2. Used to compare candidate solutions.

val factorize : (TVarSet.t * TVarSet.t) -> Ty.t -> Ty.t * Ty.t

factorize (pvs,nvs) t splits t into a part that can be factorized by pvs and nvs, and a remainder: it returns (t1,t2) such that t is equivalent to (/\pvs /\ ~\/nvs /\ t1) \/ t2. The factorized part gathers the DNF lines of t in which every variable of pvs occurs positively and every variable of nvs occurs negatively, with those occurrences removed.