Module Mlsem_system.Annot

Typing derivations, in the two forms the reconstruction works with.

A derivation mirrors the shape of the expression it types and supplies, at each node, the choices the typing rules cannot make on their own: which instance of a polymorphic variable to take, which type to give a lambda's parameter, which branches of a typecase to explore, and so on.

Annot is a complete derivation, the input of Mlsem_system.Checker. IAnnot is an intermediate one, in which some choices are still undecided; it embeds completed sub-derivations through its A constructor, so the reconstruction gradually rewrites I nodes into A ones.

module Annot : sig ... end

A complete derivation.

module Rid : sig ... end

Identifies the node a result type comes from, so that two results are only compared when they constrain the same node.

module IAnnot : sig ... end

An intermediate derivation, still containing undecided choices.

module LazyIAnnot : sig ... end

A derivation whose construction is deferred.

module Domain : sig ... end

The part of an expression's typing already covered by the branches of an intersection, used to avoid exploring a branch that would add nothing.