Module Mlsem_system

module Analyzer : sig ... end
module Annot : sig ... end

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

module Ast : sig ... end

The functional core language.

module Checker : sig ... end

Type checker for the functional core language.

module Config : sig ... end

Tuning knobs of the type system.

module Heuristics : sig ... end

Default implementations for the normalization hooks of Mlsem_system.Config. Both encode the same assumption about abstract types: an abstract type with an empty parameter is uninhabited (there is no value of type ref(empty), say). This is not a neutral simplification — it is only sound for abstract types whose parameters are genuinely inhabited-by-construction.

module Reconstruction : sig ... end

Reconstruction of typing derivations.

module Refinement : sig ... end

Occurrence typing: computing what a test tells us about the variables in scope.