Module Mlsem_system.Ast

The functional core language.

The full language of Mlsem_lang.Ast is compiled down to this small lambda-calculus, which is what Checker and Reconstruction work on.

Terms are expected to be alpha-converted (every binder introduces a distinct Mlsem_common.Variable.t) and to carry pairwise distinct Eid.ts.

type pcustom = {
  1. pname : string;
  2. pdom : Mlsem_types.Ty.t -> Mlsem_types.Ty.t;
  3. proj : Mlsem_types.Ty.t -> Mlsem_types.Ty.t;
  4. pgen : bool;
}

A user-defined projection. proj computes the type of the result from the type of the argument and must be monotonic; pdom t is the largest argument type whose projection is below t; pgen says whether the projection is generalizable, i.e. free of effects (cf. Checker.generalize).

type ccustom = {
  1. cname : string;
  2. cdom : Mlsem_types.Ty.t -> Mlsem_types.Ty.t list list;
  3. cons : Mlsem_types.Ty.t list -> Mlsem_types.Ty.t;
  4. cgen : bool;
}

A user-defined constructor. cons computes the type of the result from the types of the arguments and must be monotonic; cdom t returns the alternative argument-type tuples whose construction is below t, each of which must have the constructor's arity; cgen as in pcustom.

type ocustom = {
  1. oname : string;
  2. ofun : Mlsem_common.Env.t -> Mlsem_types.TyScheme.t;
  3. ogen : bool;
}

A user-defined operation, typed by the arrow scheme ofun returns. ogen as in pcustom.

type check =
  1. | Check
  2. | CheckStatic
  3. | NoCheck
    (*

    How much of a cast or coercion is verified statically: Check requires both bounds of the gradual type to be respected, CheckStatic only the lower one (the rest being deferred to a runtime check), and NoCheck nothing.

    *)
type projection =
  1. | Pi of int * int
  2. | PiField of string
  3. | PiFieldOpt of string
  4. | Hd
  5. | Tl
  6. | PiTag of Mlsem_types.Tag.t
  7. | PCustom of pcustom
type constructor =
  1. | Tuple of int
  2. | Cons
  3. | Rec of string list * bool
  4. | Tag of Mlsem_types.Tag.t
  5. | Enum of Mlsem_types.Enum.t
  6. | Join of int
  7. | Meet of int
  8. | Ternary of Mlsem_types.Ty.t
  9. | Voidify of Mlsem_types.Ty.t
  10. | Normalize
  11. | CCustom of ccustom
type operation =
  1. | RecUpd of string
  2. | RecDel of string
  3. | Ignore of Mlsem_types.Ty.t
  4. | OCustom of ocustom
type alt_settings = {
  1. aname : string;
  2. amask : Mlsem_common.Env.t -> bool list;
  3. aerror : Mlsem_common.Env.t -> string;
}

Settings of an Alt expression. amask env selects the branches that may be typed under env: it must return exactly one boolean per branch of the Alt, in the same order. aerror env builds the error message reported when no branch could be typed.

type param_annot = Mlsem_types.GTy.t option
type e =
  1. | Value of Mlsem_types.GTy.t
  2. | Var of Mlsem_common.Variable.t
  3. | Constructor of constructor * t list
  4. | Lambda of param_annot * Mlsem_common.Variable.t * t
  5. | LambdaRec of (param_annot * Mlsem_common.Variable.t * t) list
  6. | Ite of t * Mlsem_types.GTy.t * t * t
  7. | App of t * t
  8. | Operation of operation * t
  9. | Projection of projection * t
  10. | Let of Mlsem_types.Ty.t list * Mlsem_common.Variable.t * t * t
    (*

    The type list is a suggested decomposition of the bound variable: the body is typed once per cell and the results are joined, which is what lets a single definition be used at several types in a same scope. An empty list disables partitioning; note that only a partitioned Let propagates the divergence of its definition (an empty definition type makes every cell vanish).

    *)
  11. | TypeCast of t * Mlsem_types.GTy.t * check
  12. | TypeCoerce of t * Mlsem_types.GTy.t * check
  13. | Alt of alt_settings * t list
val map : (t -> t) -> t -> t

Bottom-up: f is applied to a node after its children have been rewritten, and is not re-applied to the node it returns.

val map' : (t -> t option) -> t -> t

Top-down with early stop: f is applied to a node first, and when it returns Some e' the node is replaced by e' without descending into it. Returning None recurses into the children.

val iter : (t -> unit) -> t -> unit

Bottom-up traversal, as map.

val iter' : (t -> bool) -> t -> unit

Top-down traversal, as map': descends into a node only if f returns true on it.

val fv : t -> Mlsem_common.VarSet.t

Free variables, computed as "used minus bound" over the whole term. This is only correct because terms are alpha-converted, so a variable bound in one sub-term cannot occur free in another.

val vars : t -> Mlsem_common.VarSet.t

All variables, used or bound.

val apply_subst : Mlsem_types.Subst.t -> t -> t

Substitutes type variables in the type annotations of the term. The types embedded in Ternary, Voidify, Ignore and in the pcustom / ccustom / ocustom closures are not traversed: they are required to be free of type variables.

val refresh : t -> t

Refreshes all Eid.t, preserving localization data. Useful when duplicating an expression.

val pp_raw : Stdlib.Format.formatter -> t -> unit

Prints the term as a data structure, annotations included; pp prints it as source-like syntax.

val pp : Stdlib.Format.formatter -> t -> unit

Prints the term as a data structure, annotations included; pp prints it as source-like syntax.

val pp_e : Stdlib.Format.formatter -> e -> unit
val pp_check : Stdlib.Format.formatter -> check -> unit
val pp_projection : Stdlib.Format.formatter -> projection -> unit
val pp_constructor : Stdlib.Format.formatter -> constructor -> unit
val pp_operation : Stdlib.Format.formatter -> operation -> unit
val pp_alt_settings : Stdlib.Format.formatter -> alt_settings -> unit
val pp_param_annot : Stdlib.Format.formatter -> param_annot -> unit
val pp_pcustom : Stdlib.Format.formatter -> pcustom -> unit
val pp_ccustom : Stdlib.Format.formatter -> ccustom -> unit

Typing of the primitives

val domain_of_proj : projection -> Mlsem_types.Ty.t -> Mlsem_types.Ty.t

domain_of_proj p t is the largest argument type whose projection by p is below t. In particular domain_of_proj p Ty.any is the domain of p.

The type of the projection of an argument of the given type. Monotonic; only meaningful on a type within the projection's domain.

val domains_of_construct : constructor -> Mlsem_types.Ty.t -> Mlsem_types.Ty.t list list

domains_of_construct c t returns the alternative argument-type tuples whose construction by c is below t; the empty list means c cannot produce a value in t. Each tuple has the arity of c.

val construct : constructor -> Mlsem_types.Ty.t list -> Mlsem_types.Ty.t

The type of the construction of arguments of the given types. Monotonic.

  • raises Invalid_argument

    if the number of arguments does not match c.

The arrow scheme an operation is typed with; an operation is applied like a function whose type is fixed rather than inferred.

Coercions

val coerce : ?coercion_id:Mlsem_common.Eid.t -> ?duplicate_arrows:bool -> check -> Mlsem_types.GTy.t -> t -> t

coerce c ty e wraps e in a TypeCoerce to ty, pushing the coercion inwards as far as the shape of e allows: coercing a lambda to an arrow type coerces its body and annotates its parameter, coercing a constructor coerces its arguments, and so on. This is what lets a user signature guide the reconstruction inside a definition instead of only constraining its result. The outer coercion is always kept as well, under coercion_id if given and under a refreshed id otherwise; sub-terms whose shape does not match the target type are simply left alone. If duplicate_arrows is set to true, Lambda expressions may be duplicated when necessary to allow pushing coercions inside (for intersections of arrows).

val push_coercions : ?duplicate_arrows:bool -> t -> t

Applies coerce to every TypeCoerce already present in the term.