Module Mlsem_app.Config

include module type of struct include Mlsem_system.Config end
val value_restriction : bool Stdlib.ref

Whether generalization is restricted to expressions whose evaluation cannot have an effect (cf. Checker.generalize). Disabling it makes inference more permissive but unsound in the presence of mutable state.

val infer_overload : bool Stdlib.ref

Whether the reconstruction should try to infer intersection (overloaded) types for functions, by exploring the branches of a typecase separately even when the scrutinee's type does not decide between them. Disabling it makes inference cheaper and the inferred types simpler.

val reexplore_failed_domains : bool Stdlib.ref

Whether a branch of an intersection whose exploration failed should be explored again in the other branches' domains. Disabling it makes reconstruction cheaper at the cost of precision.

val normalization_fun : (Mlsem_types.Ty.t -> Mlsem_types.Ty.t) Stdlib.ref

Normalization applied to a type before its emptiness is tested. It must return a type that is empty if and only if the argument is "empty enough" to be considered uninhabited — which is where assumptions about abstract types are injected (cf. Heuristics.normalize_empty_abstracts). Use Fun.id for no normalization.

val subst_normalization_fun : (Mlsem_system.Heuristics.tally_context -> Mlsem_types.Subst.t list -> Mlsem_types.Subst.t list) Stdlib.ref

Normalization applied to the set of solutions of a tallying instance. It may split, reorder or drop solutions, but every returned substitution must be a solution of the instance: the reconstruction relies on them being sound, not on them being complete (cf. Heuristics.normalize_abstract_factors). Use fun _ x -> x for no normalization.

include module type of struct include Mlsem_lang.Config end
type eval_order = Mlsem_lang.Config.eval_order =
  1. | LeftToRight
    (*

    Evaluates arguments left-to-right.

    *)
  2. | RightToLeft
    (*

    Evaluates arguments right-to-left.

    *)
  3. | UnknownOrder
    (*

    Default. Evaluation order is unknown (and/or optional). Once started, evaluation cannot be aborted (e.g. Ternary, Join, Meet).

    *)
  4. | Abortable
    (*

    Evaluation order is unknown (and/or optional). Evaluation can be aborted (e.g. Voidify, Try).

    *)
val void_ty : Mlsem_types.Ty.t Stdlib.ref

Type given to expressions evaluated only for their effects (statements, loops, assignments).

val app_eval_order : eval_order Stdlib.ref

Order in which a function and its argument are evaluated.

val tuple_eval_order : eval_order Stdlib.ref
val record_eval_order : eval_order Stdlib.ref
val cons_eval_order : eval_order Stdlib.ref
val ccustom_eval_order : (string, eval_order) Stdlib.Hashtbl.t

Evaluation order of the arguments of a user-defined constructor, by name. Constructors absent from the table default to UnknownOrder.

type narrowing =
  1. | NoNarrowing
  2. | DirectNarrowing
  3. | PartitionNarrowing
  4. | BothNarrowing
val type_narrowing : narrowing Stdlib.ref
val allow_implicit_downcast : bool Stdlib.ref
val save_all : unit -> unit
val restore_all : unit -> unit