Module Refinement.Partitioner

Turns collected refinements into type decompositions for let-bound variables. A decomposition splits a variable's type into cases that are typed separately, so that each branch of a later test sees a precise type.

type t
val from_refinements : Refinements.t -> t
val filter_compatible : t -> Mlsem_common.Variable.t -> Mlsem_types.Ty.t -> t

Keeps the refinements that are compatible with v having type t, i.e. those to be considered inside the corresponding case.

val decomposition_for : t -> Mlsem_common.Variable.t -> Mlsem_types.Ty.t list -> Mlsem_types.Ty.t list

decomposition_for t v suggs refines the suggested decomposition suggs of v by splitting each of its cells along the refinements recorded for v. Returns the empty list — meaning "do not partition v" — exactly when suggs is empty.