DOCSEARCHbyAlgolia
Submit Docs

Catala Documentation

repository·master·Indexed 25 days ago

https://github.com/catalalang/catala

Catala is a domain-specific language (DSL) for socio-fiscal legislative literate programming, designed to bridge the gap between legislative text and executable code. It allows for the annotation of laws to derive algorithms and verify their faithfulness to legal logic. The ecosystem includes a compiler with customizable backends, a build system called Clerk, a Python runtime (catala-runtime 1.2.1), a ReScript wrapper, and a VSCode extension with LSP support.

Tokens
5.3K
Snippets
11
Records
35
Agent score
82%

What's inside Catala

  1. What is Catala and how does it work?

    master

    Catala is a domain-specific language designed for socio-fiscal legislative literate programming. It allows developers to annotate legislative texts (laws, executive orders, etc.) with their computational meaning.

    Core Workflow:

    1. Annotate: Gather legislative texts and annotate them article by article in a text editor.
    2. Compile: Use the Catala compiler to derive algorithms from the annotated text.
    3. Verify: The compiler can produce a lawyer-readable PDF version of the implementation, allowing domain experts (lawyers) to certify the code's faithfulness to the law.

    Key Concept: Default Logic Catala embeds 'definition-under-conditions' (based on default logic) as a first-class feature. This allows the language's logical structure to mimic the logical structure of legal statutes.

  2. Structure of the Catala F* formalization

    master

    The F* proof of correctness for the translation from the default calculus to the target lambda calculus is organized into several modules:

    • Catala.DefaultCalculus.fst: Semantics of the default calculus, type safety theorems, and proofs.
    • Catala.LambdaCalculus.fst: Semantics of the lambda calculus, type safety theorems, and proofs.
    • Catala.Translation.Helpers.fst: Helpers related to the lambda calculus used in the translation correctness proof.
    • Catala.Translation.fst: Definition of the translation and its proof of correctness (including the final wrap-up theorem).

    Additionally, *.hints files are technical helpers used to speed up proof replay by providing a prioritized list of lemmas to the SMT solver.

  3. Create customized backends using Catala compiler plugins

    master

    You can extend the Catala compiler by creating customized backends via dynamic linking without modifying the compiler's source code. This allows you to tailor the generated target code to match specific naming conventions, module structures, or coding styles required by your application.

    For detailed implementation instructions, refer to the online documentation.

  4. How Clerk performs tests

    master

    When performing tests, Clerk follows a two-step process:

    1. It generates a build.ninja file containing the necessary rules and build statements based on the provided input path(s).
    2. It executes the command ninja test to run the test suite.

    The internal management of the Ninja structure is handled by the Ninja_utils module.

  5. Define data structures and types in Catala

    master

    Catala uses structure to define product types (records) and enumeration to define sum types (alternatives). Data fields within these structures are introduced with the data keyword and annotated with a type using content.

    Base Data Types

    • integer: Base integer type.
    • amount: Represents money.
    • text: Represents strings.
    • decimal: Fixed- or floating-point numbers.
    • date: Represents dates.
    • boolean: Boolean values.

    Complex Types

    • collection: Annotates data that is a collection of other data.
    • optional: A shorthand for an Absent/Present enumeration.
    • condition: A special type of data representing logical or juridical conditions (defaults to false).
    declaration structure Foo:
  fieldA content integer
  fieldB content boolean

declaration enumeration Foo:
  -- ChoiceA
  -- ChoiceB content Bar

data bar content boolean
data children content collection Child
data husband optional

structure ArticleFoo:
  condition eligible_for_credit

  6. Format Catala code with catala-format

    master
    Code formatting is provided by the catala-format tool, which is based on a tree-sitter grammar. If catala-format is installed alongside the LSP server, code formatting becomes directly available within VSCode.

  10. Style conventions for the Catala standard library

    master

    When contributing to or using the Catala standard library, follow these naming and documentation conventions to ensure consistency across English and French modules.

    Function Naming

    • Predicates: Functions returning a boolean must be named as predicates using prefixes like is_.../est_... or are_.../sont_... (for multiple arguments).
    • Documentation wording: Use "Checks if" or "Teste si" instead of "Returns true if".

    Documentation (Docstring) Structure

    Docstrings starting with ## must follow a specific format. Descriptions should use the third person (e.g., "Computes" instead of "Compute").

    English Format:

    ## Main message describing what is the goal of the function. New sentence with
## additional information.
## **Example(s):** Unique example here or
## - First example
## - Second example
## **Aborts:** List of input conditions for which the function crashes.

    French Format:

    ## Message principal décrivant le but de la fonction. Nouvelle
## phrase avec des informations additionnelles.
## **Exemple(s):** Exemple unique ici ou
## - Premier exemple
## - Deuxième exemple
## **Échoue:** Liste de conditions sur les entrées telles que la fonction
## crashe.

    Argument Naming

    • Base types: One-letter initials are acceptable for arguments of a "base type".
    • Multiple base types: If multiple arguments of the same base type have similar roles (e.g., in comparisons), use numbered identifiers like d1, d2 instead of x, y.
    • General rule: Name arguments based on their type when unambiguous, or based on their role otherwise.
    • Localization: Argument names must be localized when translating a module.