Refinement (mlsem-system.Mlsem

module Refinements : sig ... end

Refinements collected over a whole expression: those attached to a program point, plus anonymous ones that only contribute to partitioning.

val typeof_def : Mlsem_common.Env.t -> Ast.t -> Mlsem_types.TyScheme.t

typeof_def env e returns an approximation of the type of the definition e under the environment env. This approximation is TyScheme.any for non-trivial cases, but it can be more precise for simple constructs (e.g. variables, casts, projections) or in the presence of user type annotations (coercions).

val refine : 
  Mlsem_common.Env.t ->
  Ast.t ->
  Mlsem_types.Ty.t ->
  Mlsem_common.REnv.t

refine env e t returns what must hold of the variables in scope for e to have type t: a necessary condition, obtained as a fixpoint over the negation of the sufficient conditions for e to not have type t. It is always sound to under-refine, and the analysis does so whenever it cannot invert a construct, so the result may be the empty (trivially true) environment.

val refinements : 
  ?extra_checks:(Mlsem_common.Eid.t * Mlsem_types.Ty.t) list ->
  ?refine_on_typecases:bool ->
  ?refine_on_casts:bool ->
  Mlsem_common.Env.t ->
  Ast.t ->
  Refinements.t

Collects the refinements of a whole expression by calling refine at each test. extra_checks adds "expression eid has type t" hypotheses to refine on, refine_on_typecases (default true) refines the branches of each typecase, and refine_on_casts (default false) also refines on type casts.

module Partitioner : sig ... end

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.