Typing (catala.Shared

module Env : sig ... end

In the following functions, the ~leave_unresolved labeled parameter controls the behavior of the typer in the case where polymorphic expressions are still found after typing: if set to true, it allows them (giving them TAny and losing typing information), if set to false, it aborts.

val expr : 
  leave_unresolved:bool ->
  Shared_ast__Definitions.decl_ctx ->
  ?env:'e Env.t ->
  ?typ:Shared_ast__Definitions.naked_typ Catala_utils.Mark.pos ->
  ( ( 'a, 'a, 'm ) Shared_ast__Definitions.base_gexpr,
    'm Shared_ast__Definitions.mark )
    Catala_utils.Mark.ed as 'e ->
  ( ( 'a, 'a, Shared_ast__Definitions.typed )
      Shared_ast__Definitions.base_gexpr
      Bindlib.box,
    Shared_ast__Definitions.typed Shared_ast__Definitions.mark )
    Catala_utils.Mark.ed

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 : 
  leave_unresolved:bool ->
  Shared_ast__Definitions.decl_ctx ->
  ?env:'e Env.t ->
  ?typ:Shared_ast__Definitions.naked_typ Catala_utils.Mark.pos ->
  ( ( 'a, 'a, 'm ) Shared_ast__Definitions.base_gexpr,
    'm Shared_ast__Definitions.mark )
    Catala_utils.Mark.ed as 'e ->
  ( ( 'a, 'a, Shared_ast__Definitions.untyped )
      Shared_ast__Definitions.base_gexpr
      Bindlib.box,
    Shared_ast__Definitions.untyped Shared_ast__Definitions.mark )
    Catala_utils.Mark.ed

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 : 
  leave_unresolved:bool ->
  ( ( 'a, 'a, 'm ) Shared_ast__Definitions.base_gexpr,
    'm Shared_ast__Definitions.mark )
    Catala_utils.Mark.ed
    Shared_ast__Definitions.program ->
  ( ( 'a, 'a, Shared_ast__Definitions.typed )
      Shared_ast__Definitions.base_gexpr,
    Shared_ast__Definitions.typed Shared_ast__Definitions.mark )
    Catala_utils.Mark.ed
    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.