ee569657e1
we want our pointers to "const" (in the C sense, i.e. read-only) values in
general; but structures need to be initialised field by field. We handle the
absence of `const` in this case (the pointer target will be made `const` upon
function return).
When we compile with `-O`, though, intermediate variables are removed, and we
have branchings with one side getting an already allocated (`const`) structure,
while the other one will need to init through allocation of individual fields.
In the current state of this patch, we define the structure as non-const and
malloc it when this happens, like in the basic definition case. It works, but in
the branch of the already allocated structure, the malloc is discarded (wasted),
and there is a legitimate warning because we strip the `const` flag from the
source pointer.
I see only two solutions:
- remove all consts (beh, they are very good for understanding what's going on,
and I'm sure that without them we'll fall into more traps later)
- in the branch(es) needing malloc, allocate and initialise to a temporary
non-const structure, then affect it to the return pointer ("sealing" it as
const after initialisation). This basically what happens without `-O` because
we have more intermediate variables... But we want to target that specifically
at cases that need malloc.
A variant of the 2nd option could be to define initialiser functions for all
structs, but we loose in readability since the arguments would be unlabelled.
The cleaner way to do it would probably be at the scalc level, depending on the
`--no-struct-literals` flag.
|
||
|---|---|---|
| .github/workflows | ||
| .nix | ||
| build_system | ||
| compiler | ||
| doc | ||
| runtimes | ||
| syntax_highlighting | ||
| tests | ||
| .git-blame-ignore-revs | ||
| .gitattributes | ||
| .gitignore | ||
| .ocamlformat | ||
| build_release.sh | ||
| catala.opam | ||
| catala.opam.locked | ||
| CITATION.cff | ||
| CONTRIBUTING.md | ||
| Dockerfile | ||
| dune | ||
| dune-project | ||
| flake.lock | ||
| flake.nix | ||
| INSTALL.md | ||
| LICENSE.txt | ||
| Makefile | ||
| README.md | ||
Catala
Explore the docs »
View Tutorial
•
Report Bug
•
Contribute
•
Join Zulip Chat
Catala is a domain-specific language for deriving faithful-by-construction algorithms from legislative texts. To learn quickly about the language and its features, you can jump right to the official Catala tutorial. You can join the Catala community on Zulip!
Table of Contents
Concepts
Catala is a programming language adapted for socio-fiscal legislative literate programming. By annotating each line of the legislative text with its meaning in terms of code, one can derive an implementation of complex socio-fiscal mechanisms that enjoys a high level of assurance regarding the code-law faithfulness.
Concretely, you have to first gather all the laws, executive orders, previous cases, etc. that contain information about the socio-fiscal mechanism that you want to implement. Then, you can proceed to annotate the text article by article, in your favorite text editor :
Once your code is complete and tested, you can use the Catala compiler to produce a lawyer-readable PDF version of your implementation. The Catala language has been specially designed in collaboration with law professionals to ensure that the code can be reviewed and certified correct by the domain experts, which are in this case lawyers and not programmers.
The Catala language is special because its logical structure mimics the logical structure of the law. Indeed, the core concept of "definition-under-conditions" that builds on default logic has been formalized by Professor Sarah Lawsky in her article A Logic for Statutes. The Catala language is the only programming language to our knowledge that embeds default logic as a first-class feature, which is why it is the only language perfectly adapted to literate legislative programming.
Getting started
To get started, the best place is the tutorial of the language. A French version is also available but might be out of sync with the latest language features.
Note: bleeding-edge version
If you are interested in the latest development version, pre-built artifacts including binaries and API documentation can be found at https://catalalang.github.io/catala
Building and installation
Catala is available as an opam package! If opam is installed on your machine, simply execute:
opam install catala
To get the cutting-edge, latest version of Catala, you can also do
opam pin add catala --dev-repo
However, if you wish to get the latest developments of the compiler, you probably want to compile it from the sources of this repository or use nix. For that, see the dedicated readme.
Usage
Catala
Use catala --help if you have installed it to get more information about the
command line options available. The man page is also available
online. To get the development version
of the help, run make help_catala after make build. The catala binary
corresponds to the Catala compiler.
The top-level Makefile contains a lot of useful targets to run. To display
them, use
make help
Plugin backends
While the compiler has some builtin backends for Catala (Python, Ocaml, etc.), it is also possible to add a custom backend to the Catala compiler without having to modify its source code. This plugin solution relies on dynamic linking: see the dedicated README.
Clerk
Use clerk --help if you have installed it to get more information about the
command line options available. To get the development version of the help, run
make help_clerk after make build. The clerk binary corresponds to the
Catala build system, responsible for testing among other things.
To get more information about Clerk, see the dedicated readme
Catleg
Catleg is a command line utility providing useful integration with LégiFrance, the official repository of French legal documentation. See the decidated repository for more information.
Documentation
Syntax cheat sheet
A complete and handy reference of the Catala syntax can be found in the cheat sheet (for French and English versions of the syntax).
Formal semantics
To audit the formal proof of the partial certification of the Catala compiler, see the dedicated readme.
Compiler documentation
The documentation is accessible online, both for the latest release and bleeding-edge version.
It is otherwise generated from the compiler source code using
dune and odoc. Run
make doc
to generate the documentation, then open the doc/odoc.html file in any browser.
Examples
To explore the different programs written in Catala, see the dedicated readme.
API
To know how to use the code generated by the Catala compiler in your favorite programming language, head to the readme of the French law library. The corresponding pre-built examples are also available.
Contributing
To know how you can contribute to the project, see the dedicated readme.
Test suite
To know how to run or improve the Catala reference test suite, see the dedicated readme.
License
The compiler and all the code contained in this repository is released under the Apache license (version 2) unless another license is explicited for a sub-directory.
Limitations and disclaimer
Catala is a research project from Inria, the French National Research Institute for Computer Science. The compiler is yet unstable and lacks some of its features.
Pierre Catala
The language is named after Pierre Catala, a professor of law who pionneered the French legaltech by creating a computer database of law cases, Juris-Data. The research group that he led in the late 1960s, the Centre d’études et de traitement de l’information juridique (CETIJ), has also influenced the creation by state conselor Lucien Mehl of the Centre de recherches et développement en informatique juridique (CENIJ), which eventually transformed into the entity managing the LegiFrance website, acting as the public service of legislative documentation.