package catala

  1. Overview
  2. Docs
package catala
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

module Env : sig ... end
val 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.

val 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)

val 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.