Module Mlsem_lang.Config

Properties of the source language that the translation to the functional core must respect.

These are global mutable settings, read at each use rather than captured, so changing one affects every subsequent translation. The evaluation orders below are what Optimize relies on to decide, for each sub-expression, which assignments to a mutable variable may already have happened. Declaring an order the source language does not actually have makes the dataflow optimization unsound; UnknownOrder is always a safe default.

type 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.