Automating tutorial contents recap

.github/workflows/mdbook.yml

@@ -43,6 +43,8 @@ jobs:
         uses: actions/configure-pages@v5
       - name: Build with mdBook
         run: mdbook build
+      - name: Typecheck Catala examples
+        run: make -C examples typecheck
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v3
         with:

.gitignore

@@ -1 +1,2 @@
 book
+_build

examples/Makefile

@@ -0,0 +1,8 @@
+
+SRC = $(wildcard *.catala_en)
+
+%.typecheck: %
+	catala typecheck -I src $^
+.PHONY: %.typecheck
+
+typecheck: $(addsuffix .typecheck,$(SRC))

examples/tutorial_end_2_1.catala_en

@@ -0,0 +1,48 @@
+```catala
+declaration structure Individual:
+  data income content money
+  data number_of_children content integer
+
+declaration scope IncomeTaxComputation:
+  input individual content Individual
+  internal tax_rate content decimal
+  output income_tax content money
+```
+
+## Article 1
+
+ The income tax for an individual is defined as a fixed percentage of the
+ individual's income over a year.
+
+```catala
+scope IncomeTaxComputation:
+  definition income_tax equals
+    individual.income * tax_rate
+```
+
+## Article 2
+
+The fixed percentage mentioned at article 1 is equal to 20 %.
+
+```catala
+scope IncomeTaxComputation:
+  label article_2
+  definition tax_rate equals 20%
+```
+
+## Test
+
+```catala
+declaration scope Test:
+  output computation content IncomeTaxComputation
+
+scope Test:
+  definition computation equals
+    output of IncomeTaxComputation with {
+      -- individual:
+        Individual {
+          -- income: $20,000
+          -- number_of_children: 0
+        }
+    }
+```

examples/tutorial_end_2_2.catala_en

@@ -0,0 +1,120 @@
+```catala
+declaration structure Individual:
+  data income content money
+  data number_of_children content integer
+
+declaration scope IncomeTaxComputation:
+  input current_date content date
+  input individual content Individual
+  input overseas_territories content boolean
+  internal tax_rate content decimal
+  output income_tax content money
+```
+
+## Article 1
+
+ The income tax for an individual is defined as a fixed percentage of the
+ individual's income over a year.
+
+```catala
+scope IncomeTaxComputation:
+  definition income_tax equals
+    individual.income * tax_rate
+```
+
+## Article 2 (old version before 2000)
+
+The fixed percentage mentioned at article 1 is equal to 20 %.
+
+```catala
+scope IncomeTaxComputation:
+  label article_2
+  definition tax_rate under condition
+    current_date < |2000-01-01|
+  consequence equals 20%
+```
+
+## Article 2 (new version after 2000)
+
+The fixed percentage mentioned at article 1 is equal to 21 % %.
+
+```catala
+scope IncomeTaxComputation:
+  # Simply use the same label "article_2" as the previous definition to group
+  # them together
+  label article_2
+  definition tax_rate under condition
+    current_date >= |2000-01-01|
+  consequence equals 21%
+```
+
+## Article 3
+
+If the individual is in charge of 2 or more children, then the fixed
+percentage mentioned at article 1 is equal to 15 %.
+
+```catala
+scope IncomeTaxComputation:
+  label article_3 exception article_2
+  definition tax_rate under condition
+    individual.number_of_children >= 2
+  consequence equals 15%
+```
+
+## Article 4
+
+Individuals earning less than $10,000 are exempted of the income tax mentioned
+at article 1.
+
+```catala
+scope IncomeTaxComputation:
+  label article_4 exception article_3
+  definition tax_rate under condition
+    individual.income <= $10,000
+  consequence equals 0%
+```
+
+## Article 5
+
+Individuals earning more than $100,000 are subjects to a tax rate of
+30%, regardless of their number of children.
+
+```catala
+scope IncomeTaxComputation:
+  label article_5 exception article_3
+  definition tax_rate under condition
+    individual.income > $100,000
+  consequence equals 30%
+```
+
+## Article 6
+
+In the overseas territories, the tax rate for individuals earning
+more than $100,000 specified at article 5 is reduced to 25 %.
+
+```catala
+scope IncomeTaxComputation:
+  label article_6 exception article_5
+  definition tax_rate under condition
+    individual.income > $100,000 and overseas_territories
+  consequence equals 25%
+```
+
+## Test
+
+```catala
+declaration scope Test:
+  output computation content IncomeTaxComputation
+
+scope Test:
+  definition computation equals
+    output of IncomeTaxComputation with {
+      -- individual:
+        Individual {
+          -- income: $20,000
+          -- number_of_children: 0
+        }
+      -- overseas_territories: false
+      -- current_date: |1999-01-01|
+    }
+```

src/2-1-basic-blocks.md

@@ -429,3 +429,13 @@ like `structure` and `enumeration`, representing the types of `scope`
 variables, and `definition` of formulas for these variables, you should now be able to
 code in Catala the equivalent of single-function programs that perform common
 arithmetic operations and define local variables.
+
+
+~~~~~~admonish info collapsible=true title="Recap of the current section"
+For reference, here is the final version of the Catala code consolidated at
+the end of this section of the tutorial.
+
+~~~
+{{#include ../examples/tutorial_end_2_1.catala_en}}
+~~~
+~~~~~~

src/2-2-conditionals-exceptions.md

@@ -12,53 +12,7 @@ and will reuse the same running example, but all the Catala code necessary
 to execute the example is included below for reference.
 
 ~~~
-```catala
-declaration structure Individual:
-  data income content money
-  data number_of_children content integer
-
-declaration scope IncomeTaxComputation:
-   input individual content Individual
-   internal tax_rate content decimal
-   output income_tax content money
-```
-
-## Article 1
-
-The income tax for an individual is defined as a fixed percentage of the
-individual's income over a year.
-
-```catala
-scope IncomeTaxComputation:
-  definition income_tax equals
-    individual.income * tax_rate
-```
-
-## Article 2
-
-The fixed percentage mentioned at article 1 is equal to 20 %.
-
-```catala
-scope IncomeTaxComputation:
-  definition tax_rate equals 20 %
-```
-
-## Test
-
-```catala
-declaration scope Test:
-  output computation content IncomeTaxComputation
-
-scope Test:
-  definition computation equals
-    output of IncomeTaxComputation with {
-      -- individual:
-        Individual {
-          -- income: $20,000
-          -- number_of_children: 0
-        }
-    }
-```
+{{#include ../examples/tutorial_end_2_1.catala_en}}
 ~~~
 ~~~~~~
 
@@ -507,7 +461,7 @@ is an exception to the label `article_2`, it suffices to give the same label
 `article_2` to the two conditional definitions of the two versions of `article_2`:
 
 ~~~admonish note title="Grouping mutually exclusive conditional definitions"
-#### Article 2 (new version before 2000)
+#### Article 2 (old version before 2000)
 
 The fixed percentage mentioned at article 1 is equal to 20 %.
 
@@ -544,3 +498,12 @@ multiple conditions apply, one can prioritize the conditional definitions using
 the `exception` and `label` keywords to form exception trees able to capture the
 complex logic behind the legal texts while conserving the same structure as
 them.
+
+~~~~~~admonish info collapsible=true title="Recap of the current section"
+For reference, here is the final version of the Catala code consolidated at
+the end of this section of the tutorial.
+
+~~~
+{{#include ../examples/tutorial_end_2_2.catala_en}}
+~~~
+~~~~~~