package catala
Install
Dune Dependency
Authors
Maintainers
Sources
md5=1408a1cce45c7d5990b981e83e7589c2
sha512=eb3b923aa1f743378b4a05e30f50be5d180dc862a716270d747a90e469017f42fa5fc41352f02fbbf59cd2560f91c4f1b32cf38d80085b105d9387b0aed2039d
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.
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.tInfers 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.tSame 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.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.