package catala

  1. Overview
  2. Docs
Compiler and library for the literate programming language for tax code specification

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (9)

Authors

  1. V
    Vincent Botbol
  2. N
    Nicolas Chataing
  3. A
    Alain Delaët-Tixeuil
  4. L
    Louis Gesbert
  5. A
    Aymeric Fromherz
  6. D
    Denis Merigoux
  7. R
    Raphaël Monat
  8. R
    Romain Primet
  9. E
    Emile Rolley

Maintainers

  1. C
    contact@catala-lang.org

Sources

1.0.0-alpha.tar.gz
md5=2615968670ac21b1d00386a9b04b3843
sha512=eff292fdd75012f26ce7b17020f5a8374eef37cd4dd6ba60338dfbe89fbcad3443d1b409e44c182b740da9f58dff7e76dcb8ddefe47f9b2b160666d1c6930143

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.

Sourcemodule Env : sig ... end
Sourceval 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 (TForAll) 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 into EStructAccess with the suitable structure and field idents (this only concerns desugared 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.
  • TForAll 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)
Sourceval 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 TForAll appearing in the AST is replaced)

Sourceval program : ?assume_op_types:bool -> ?internal_check: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.

If internal_check is set to true, typing errors will be marked as internal, and the faulty program will be printed if '--debug' is set.