Module Shared_ast.TypingSource

Typing for the default calculus. Because of the error terms, we perform type inference using the classical W algorithm with union-find unification.

Sourcemodule Env : sig ... end
Sourceval expr : Shared_ast__.Definitions.decl_ctx -> ?env:'e Env.t -> ?typ:Shared_ast__.Definitions.naked_typ Catala_utils.Marked.pos -> ((('a, 'm Shared_ast__.Definitions.mark) Shared_ast__.Definitions.naked_gexpr, 'm Shared_ast__.Definitions.mark) Catala_utils.Marked.t as 'e) -> (('a, Shared_ast__.Definitions.typed Shared_ast__.Definitions.mark) Shared_ast__.Definitions.naked_gexpr Bindlib.box, Shared_ast__.Definitions.typed Shared_ast__.Definitions.mark) Catala_utils.Marked.t

Infers and marks the types for the given expression. If typ is provided, it is assumed to be the outer type and used for inference top-down.

If the input expression already has type annotations, the full inference is still done, but with unification with the existing annotations at every step. This can be used for double-checking after AST transformations and filling the gaps (TAny) if any. Use Expr.untype first if this is not what you want.

Sourceval check_expr : Shared_ast__.Definitions.decl_ctx -> ?env:'e Env.t -> ?typ:Shared_ast__.Definitions.naked_typ Catala_utils.Marked.pos -> ((('a, 'm Shared_ast__.Definitions.mark) Shared_ast__.Definitions.naked_gexpr, 'm Shared_ast__.Definitions.mark) Catala_utils.Marked.t as 'e) -> (('a, Shared_ast__.Definitions.untyped Shared_ast__.Definitions.mark) Shared_ast__.Definitions.naked_gexpr Bindlib.box, Shared_ast__.Definitions.untyped Shared_ast__.Definitions.mark) Catala_utils.Marked.t

Same as expr, but doesn't annotate the returned expression. Equivalent to Typing.expr |> Expr.untype, but more efficient. This can be useful for type-checking and disambiguation (some AST nodes are updated with missing information, e.g. any TAny appearing in the AST is replaced)

Sourceval program : (('a, 'm Shared_ast__.Definitions.mark) Shared_ast__.Definitions.naked_gexpr, 'm Shared_ast__.Definitions.mark) Catala_utils.Marked.t Shared_ast__.Definitions.program -> (('a, Shared_ast__.Definitions.typed Shared_ast__.Definitions.mark) Shared_ast__.Definitions.naked_gexpr, Shared_ast__.Definitions.typed Shared_ast__.Definitions.mark) Catala_utils.Marked.t Shared_ast__.Definitions.program

Typing on whole programs (as defined in Shared_ast.program, i.e. for the later dcalc/lcalc stages.

Any existing type annotations are checked for unification. Use Program.untype to remove them beforehand if this is not the desired behaviour.