package catala
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8f891209d18b6540df9c34b2d1a6a783
sha512=737770b87a057674bceefe77e8526720732552f51f424afcebcb6a628267eab522c4fd993caca1ae8ed7ace65a4a87e485af10c1676e51ca5939509a1b841ac2
doc/catala.shared_ast/Shared_ast/Typing/index.html
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.
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.edInfers 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:
EDStructAccessnodes are translated intoEStructAccesswith the suitable structure and field idents (this only concernsdesugaredexpressions). - resolution of operator types, which are stored (monomorphised) back in the
EAppOpnodes - resolution of function application input types on the
EAppnodes, when that was originally empty ([]): this documents the arity of the function application, taking de-tuplification into account. TAnyappearing 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 ;~leave_unresolved:falsechecks that it didn't cause problems)
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.edSame 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.programTyping 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.