Added beginning of tutorial

This commit is contained in:
Denis Merigoux 2020-05-17 18:51:00 +02:00
parent dbe7845235
commit 1ade06a8f9
6 changed files with 138 additions and 15 deletions

View File

@ -78,17 +78,21 @@ atom: atom_fr atom_en
EXAMPLES_DIR=examples
ALLOCATIONS_FAMILIALES_DIR=$(EXAMPLES_DIR)/allocations_familiales
ENGLISH_DUMMY_DIR=$(EXAMPLES_DIR)/dummy_english
TUTORIAL_DIR=$(EXAMPLES_DIR)/tutorial
allocations_familiales: pygments build
$(MAKE) -C $(ALLOCATIONS_FAMILIALES_DIR) allocations_familiales.pdf
allocations_familiales_expired: pygments build
$(MAKE) -C $(ALLOCATIONS_FAMILIALES_DIR) allocations_familiales.expired
$(MAKE) -C $(ALLOCATIONS_FAMILIALES_DIR) $@.pdf
$(MAKE) -C $(ALLOCATIONS_FAMILIALES_DIR) $@.html
english: pygments build
$(MAKE) -C $(ENGLISH_DUMMY_DIR) english.pdf
$(MAKE) -C $(ENGLISH_DUMMY_DIR) $@.pdf
$(MAKE) -C $(ENGLISH_DUMMY_DIR) $@.html
all_examples: allocations_familiales english
tutorial_en: pygments build
$(MAKE) -C $(TUTORIAL_DIR) $@.pdf
$(MAKE) -C $(TUTORIAL_DIR) $@.html
all_examples: allocations_familiales english tutorial_en
##########################################
# Website assets
@ -102,14 +106,14 @@ GENERATE_MAN_PAGE_ARGS=\
| tac | sed "1,18d" | tac
catala.html: src/catala/cli.ml
dune exec src/catala.exe -- $(GENERATE_MAN_PAGE_ARGS) > $@
dune exec src/catala.exe -- --help=groff | man2html | sed -e '1,8d' \
| tac | sed "1,20d" | tac > $@
legifrance_catala.html: src/legifrance_catala/main.ml
dune exec src/legifrance_catala.exe -- $(GENERATE_MAN_PAGE_ARGS) > $@
dune exec src/legifrance_catala.exe -- --help=groff | man2html | sed -e '1,8d' \
| tac | sed "1,18d" | tac > $@ > $@
website-assets: build pygments grammar.html catala.html legifrance_catala.html
$(MAKE) -C examples/allocations_familiales allocations_familiales.html
$(MAKE) -C examples/dummy_english english.html
website-assets: all_examples grammar.html catala.html legifrance_catala.html
##########################################
# Misceallenous

13
examples/tutorial/.gitignore vendored Normal file
View File

@ -0,0 +1,13 @@
*.aux
*.dvi
*.fdb_latexmk
*.fls
*.log
*.out
*.fls
tutorial_en.tex
tutorial_en.pdf
_minted*
*.toc
*.pyg
*.d

View File

@ -0,0 +1,4 @@
CATALA_LANG=en
SRC=tutorial_en.catala
include ../Makefile.common

View File

@ -0,0 +1,99 @@
@@The Catala language tutorial@@
Welcome to this tutorial, whose objective is to guide you through the features of the Catala language and trach you how to annotate a legislative text using the language. This document is addressed primarily to developers or people that have a programming background. It will use terms and jargon that might be unintelligible for lawyers in general.
@@Literate programming@@+
To begin writing a Catala program, you must start from the text of the legislative source that will justify the code that you will write. Concretely, that means copy-pasting the text of the law into a Catala source file and formatting it according so that Catala can understand it.
You can write any kind of plain text in Catala, and it will be printed as is in PDF or HTML output. Keep in mind however that one line in the source file corresponds to a paragraph in the output. Catala allows you to declare section or subsection headers as it is done here, but the fundamental division unit is the article. Let's analyse a fictional example that defines an income tax.
@Article 1@
The income tax for an individual is defined as a fixed percentage of the individual's income over a year.
/*
# This is a placeholder comment, the code for that article should go here
*/
We will now proceed to encode the algorithmic content of this article using the Catala language. To do that, we will intertwine short snippets of code between the sentences of the legislative text. Each snippet of code should be as short as possible and as close as possible to the actual sentence that justifies the code.
@@Defining a fictional income tax@@+
The content of article 1 uses a lot of implicit context : there exists an individual with an income, as well as an income tax that the individual has to pay each year. Even if this implicit context is not verbatim in the law, we have to explicit it for programming purposes. Concretely, we need a "metadata" section that defines the shape and types of the data used inside the law.
Let's start our metadata section by declaring the type information for the individual and the income tax computation:
@@Begin metadata@@
/*
declaration structure Individual:
data income content amount
declaration structure Article1:
data fixed_percentage content decimal
data income_tax content amount
*/
@@End metadata@@
Each of this declaration is a structure, containing one or more data fields. Structures are useful to group together data that goes together. Usually, you get one structure per concrete object on which the law applies (like the individual), but also one structure for each article that defines quantities (like the article 1). It is up to you to decide how to group the data together, but you should aim to optimize code readability.
Sometimes, the law gives an enumeration of different situations. These enumerations are modeled in Catala using an enumeration type, like:
@@Begin metadata@@
/*
declaration enumeration TaxCredit:
-- NoTaxCredit
-- ChildrenTaxCredit content integer # the integer corresponds
# to the number of children
*/
@@End metadata@@
We've defined and typed the data that the program will manipulate. Now we have to define the logical context in which these data will evolve. This is done in Catala using "scopes". Scopes also have to be declared in metadata, so here we go:
@@Begin metadata@@
/*
declaration scope IncomeTaxComputation:
context individual content Individual
context article1 content Article1
*/
@@End metadata@@
This scope declaration says that whenever we're in the scope "IncomeTaxComputation", then we have access to two elements in context, namely the individual's data and the data defined by article 1. We will be able to refer to the lowercase variables in our code, either to use them or to define them or one of their part.
We now have everything to annotate the contents of article 1, which is copied over below.
@Article 1@
The income tax for an individual is defined as a fixed percentage of the individual's income over a year.
/*
scope IncomeTaxComputation:
definition article1.income_tax equals
invidual.income * article1.fixed_percentage
*/
In the code, we are defining inside our scope the amount of the income tax according to the formula described in the article. When defining formulaes, you have access to all the usual arithmetic operators. But what is the value of that fixed percentage? Often, precise values are defined elsewhere in the legislative source. Here, let's suppose we have:
@Article 2@
The fixed percentage mentionned at article 1 is equal to 20 %.
/*
scope IncomeTaxComputation:
definition article1.fixed_percentage equals 20 %
*/
You can see here that Catala allows definitions to be scattered throughout the annotation of the legislative text, so that each
definition is as close as possible to its location in the text.
@@Conditional definitions@@
So far so good, but now the legislative text introduces some trickyness. Let us suppose the third article says:
@Article 3@ If the individual is in charge of 2 or more children, then the fixed percentage mentionned at article 1 is equal to 15 %.
/*
# How to redefine article1.fixed_percentage?
*/
This article actually gives another definition for the fixed percentage, which was already defined in article 2. However, article 3 defines the percentage conditionnally to the individual having more than 2 children. Catala allows you precisely to redefine a variable under a condition:
/*
scope IncomeTaxComputation:
definition article1.fixed_percentage under condition
individual.number_of_children >= 2
consequence equals 20 %
*/
When the Catala program will execute, the right definition will be dynamically chosen by looking at which condition is true. A correctly drafted legislative source should always ensure that at most one condition is true at all times. However, if it is not the case, Catala will let you define a precedence on the conditions, which has to be justified by the law.

View File

@ -11,6 +11,7 @@ make website-assets
scp examples/allocations_familiales/allocations_familiales.html $1/
scp examples/dummy_english/english.html $1/
scp examples/tutorial/tutorial.html $1/
scp grammar.html $1/
scp catala.html $1/
scp legifrance_catala.html $1/

View File

@ -135,19 +135,21 @@ let program_item_to_latex (i : A.program_item) (language : C.language_option) :
/*%s*/\n\
\\end{minted}"
(pre_latexify (Filename.basename (Pos.get_file (Pos.get_position c))))
(Pos.get_start_line (Pos.get_position c) + 1)
(Pos.get_start_line (Pos.get_position c))
(match language with C.Fr -> "catala_fr" | C.En -> "catala_en")
(math_syms_replace (Pos.unmark c))
| A.MetadataBlock (_, c) ->
let metadata_title = match language with C.Fr -> "Métadonnées" | C.En -> "Metadata" in
P.sprintf
"\\begin{tcolorbox}[colframe=OliveGreen, breakable, \
title=\\textcolor{black}{\\texttt{Métadonnées}},title after \
break=\\textcolor{black}{\\texttt{Métadonnées}},before skip=1em, after skip=1em]\n\
title=\\textcolor{black}{\\texttt{%s}},title after \
break=\\textcolor{black}{\\texttt{%s}},before skip=1em, after skip=1em]\n\
\\begin{minted}[numbersep=9mm, firstnumber=%d, label={\\hspace*{\\fill}\\texttt{%s}}]{%s}\n\
/*%s*/\n\
\\end{minted}\n\
\\end{tcolorbox}"
(Pos.get_start_line (Pos.get_position c) + 1)
metadata_title metadata_title
(Pos.get_start_line (Pos.get_position c))
(pre_latexify (Filename.basename (Pos.get_file (Pos.get_position c))))
(match language with C.Fr -> "catala_fr" | C.En -> "catala_en")
(math_syms_replace (Pos.unmark c))