package catala
Install
Dune Dependency
Authors
Maintainers
Sources
md5=5abd76e8c51a47670645e91b21b57fc5
sha512=9c6fbe50c0b5a60566e877eeddadca0a339e2ce35deb5c1beceb03bc40eb6af2d519313e71859d88645b53fad591d4fa5288c633b185c9d765603da0f5b7dd7b
doc/catala.shared_ast/Shared_ast/Typing/index.html
Module Shared_ast.Typing
Source
Typing for the default calculus. Because of the error terms, we perform type inference using the classical W algorithm with union-find unification.
val expr :
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.
Note that typing also transparently performs the following changes to the AST nodes, outside of typing annotations:
- disambiguation of constructors:
EDStructAccess
nodes are translated intoEStructAccess
with the suitable structure and field idents (this only concernsdesugared
expressions). - disambiguation of structure names in
EDStructAmend
nodes (desugared
as well) - resolution of tuple size (when equal to 0) on
ETupleAccess
nodes - resolution of operator types, which are stored (monomorphised) back in the
EAppOp
nodes - resolution of function application input types on the
EApp
nodes, when that was originally empty ([]
): this documents the arity of the function application, taking de-tuplification into account. TAny
appearing within nodes are refined to more precise types, e.g. on `EAbs` nodes (but be careful with this, it may only work for specific structures of generated code ; having~fail_on_any:true
set in the environment (this is the default) checks that it didn't cause problems)
val check_expr :
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 :
?fail_on_any:bool ->
?assume_op_types: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.