Mlsem_system.CheckerType checker for the functional core language.
The checker is purely a verifier: it takes an expression together with a complete Annot.t — the derivation reconstructed by Mlsem_system.Reconstruction — and computes the type it proves, raising Untypeable if the annotation is not a valid derivation. It never searches for an annotation itself.
val is_type_test_unsat :
tau:Mlsem_types.GTy.t ->
Mlsem_types.GTy.t ->
Mlsem_types.Ty.tis_type_test_unsat ~tau ty returns a type that is empty if and only if a branch tau of a typecase on an expression of type ty is unreachable
exception Untypeable of errorRaised when the annotation is not a valid derivation for the expression. In normal operation the reconstruction only produces valid annotations, so this escaping from typeof indicates an internal inconsistency rather than a user type error — user errors are reported by the reconstruction.
val typeof : Mlsem_common.Env.t -> Annot.Annot.t -> Ast.t -> Mlsem_types.GTy.ttypeof env a e returns the type that a proves for e under env.
The annotation must structurally match the expression, i.e. have the same shape at every node. The result is memoised in the annotation, and the cache is not keyed by env: a given annotation node must therefore only ever be typed under one environment. The reconstruction maintains this by only ever applying to an annotation substitutions that are disjoint from the environment's variables.
val generalize :
e:Ast.t ->
Mlsem_common.Env.t ->
Mlsem_types.GTy.t ->
Mlsem_types.TyScheme.tgeneralize ~e env ty quantifies the variables of ty that do not occur in env, then simplifies the result with TyScheme.bot_instance. Under the value restriction (see Config.value_restriction) nothing is quantified unless e is a generalizable expression, i.e. one whose evaluation cannot have an effect.
val typeof_def :
Mlsem_common.Env.t ->
Annot.Annot.t ->
Ast.t ->
Mlsem_types.TyScheme.ttypeof followed by generalize.