In the process of switching some money types to decimal [skip ci]

compiler/verification/z3backend.real.ml

@@ -576,6 +576,12 @@ let rec translate_op
     | IntToRat ->
       failwith
         "[Z3 encoding] application of unary operator IntToRat not supported"
+    | MoneyToRat ->
+      failwith
+        "[Z3 encoding] application of unary operator MoneyToRat not supported"
+    | RatToMoney ->
+      failwith
+        "[Z3 encoding] application of unary operator RatToMoney not supported"
     | GetDay ->
       failwith
         "[Z3 encoding] application of unary operator GetDay not supported"

examples/aides_logement/arrete_2019-09-27.catala_fr

@@ -2831,28 +2831,36 @@ de charges locatives minimale « E0 », mentionnés à l'article D. 832-26 du m
 ```catala
 champ d'application CalculÉquivalenceLoyerMinimale:
   définition tranches_revenus_d832_26 égal à [
-    TrancheRevenu { -- haut: Revenu contenu 1948,10€  -- bas: 0€ -- taux: 4%};
     TrancheRevenu {
-      -- haut: Revenu contenu 2678,71€
+      -- haut: LimiteTranche.Revenu contenu 1948,10€
+      -- bas: 0€
+      -- taux: 4%
+    };
+    TrancheRevenu {
+      -- haut: LimiteTranche.Revenu contenu 2678,71€
       -- bas: 1948,10€
       -- taux: 10,40%
     };
     TrancheRevenu {
-      -- haut: Revenu contenu 3896,18€
+      -- haut: LimiteTranche.Revenu contenu 3896,18€
       -- bas: 2678,71€
       -- taux: 21,60%
     };
     TrancheRevenu {
-      -- haut: Revenu contenu 5 357,44€
+      -- haut: LimiteTranche.Revenu contenu 5 357,44€
       -- bas: 3896,18€
       -- taux: 26,40%
     };
     TrancheRevenu {
-      -- haut: Revenu contenu 6 331,29€
+      -- haut: LimiteTranche.Revenu contenu 6 331,29€
       -- bas: 5 357,44€
       -- taux: 32%
     };
-    TrancheRevenu { -- haut: Infini  -- bas: 6 331,29€ -- taux: 48%}
+    TrancheRevenu {
+      -- haut: LimiteTranche.Infini
+      -- bas: 6 331,29€
+      -- taux: 48%
+    }
   ]
 
   # Cette exception ne figure pas dans le texte de l'arrête mais cette absence
@@ -2863,23 +2871,31 @@ champ d'application CalculÉquivalenceLoyerMinimale:
   exception définition tranches_revenus_d832_26 sous condition
     condition_2_du_832_25
   conséquence égal à [
-    TrancheRevenu { -- haut: Revenu contenu 1423,03€  -- bas: 0€ -- taux: 0%};
     TrancheRevenu {
-      -- haut: Revenu contenu 2047,61€
+      -- haut: LimiteTranche.Revenu contenu 1423,03€
+      -- bas: 0€
+      -- taux: 0%
+    };
+    TrancheRevenu {
+      -- haut: LimiteTranche.Revenu contenu 2047,61€
       -- bas: 1423,03€
       -- taux: 2,40%
     };
     TrancheRevenu {
-      -- haut: Revenu contenu 2629,85€
+      -- haut: LimiteTranche.Revenu contenu 2629,85€
       -- bas: 2047,61€
       -- taux: 20,80%
     };
     TrancheRevenu {
-      -- haut: Revenu contenu 4095,05€
+      -- haut: LimiteTranche.Revenu contenu 4095,05€
       -- bas: 2629,85€
       -- taux: 23,20%
     };
-    TrancheRevenu { -- haut: Infini  -- bas: 4095,05€ -- taux: 32,80%}
+    TrancheRevenu {
+      -- haut: LimiteTranche.Infini
+      -- bas: 4095,05€
+      -- taux: 32,80%
+    }
   ]
 ```
 

examples/aides_logement/code_construction_reglementaire.catala_fr

@@ -4094,28 +4094,34 @@ champ d'application CalculÉquivalenceLoyerMinimale:
   définition tranches_revenus_d832_26_multipliées égal à
     application pour tranche dans tranches_revenus_d832_26 de
       TrancheRevenu {
-        -- haut: (selon tranche.haut sous forme
-          -- Infini: Infini
-          -- Revenu de tranche_haut:
-            Revenu contenu (tranche_haut *€ n_nombre_parts_d832_25))
-        -- bas: tranche.bas *€ n_nombre_parts_d832_25
-        -- taux: tranche.taux
+        -- haut: (selon tranche.TrancheRevenu.haut sous forme
+          -- LimiteTranche.Infini: LimiteTrancheDécimal.Infini
+          -- LimiteTranche.Revenu de tranche_haut:
+            LimiteTrancheDécimal.Revenu contenu
+              ((argent_vers_décimal de tranche_haut) *. n_nombre_parts_d832_25))
+        -- bas: tranche.TrancheRevenu.bas *€ n_nombre_parts_d832_25
+        -- taux: tranche.TrancheRevenu.taux
       }
 
   définition montant égal à
     (((somme argent pour tranche dans tranches_revenus_d832_26_multipliées de
-      (si ressources_ménage_arrondies <=€ tranche.bas
+      (si
+        argent_vers_décimal de ressources_ménage_arrondies <=.
+          tranche.TrancheRevenuDécimal.bas
       alors 0€
       sinon
-        (selon tranche.haut sous forme
-        -- Revenu de tranche_haut:
+        (selon tranche.TrancheRevenuDécimal.haut sous forme
+        -- LimiteTrancheDécimal.Revenu de tranche_haut:
           (si ressources_ménage_arrondies >=€ tranche_haut
           alors
-            (tranche_haut -€ tranche.bas) *€ tranche.taux
+            (tranche_haut -€ tranche.TrancheRevenuDécimal.bas) *€
+              tranche.TrancheRevenuDécimal.taux
           sinon
-            ((ressources_ménage_arrondies -€ tranche.bas) *€ tranche.taux))
-        -- Infini:
-          (ressources_ménage_arrondies -€ tranche.bas) *€ tranche.taux)
+            ((ressources_ménage_arrondies -€ tranche.TrancheRevenuDécimal.bas) *€
+              tranche.TrancheRevenuDécimal.taux))
+        -- LimiteTrancheDécimal.Infini:
+          (ressources_ménage_arrondies -€ tranche.TrancheRevenuDécimal.bas) *€
+            tranche.TrancheRevenuDécimal.taux)
       ))) +€
     montant_forfaitaire_d832_26 *€ n_nombre_parts_d832_25) *€ (1,0 /. 12,0)
 ```
@@ -4132,18 +4138,21 @@ champ d'application CalculÉquivalenceLoyerMinimale:
     condition_2_du_832_25
   conséquence égal à
     (((somme argent pour tranche dans tranches_revenus_d832_26_multipliées de
-      (si ressources_ménage_arrondies <=€ tranche.bas
+      (si ressources_ménage_arrondies <=€ tranche.TrancheRevenu.bas
       alors 0€
       sinon
-        (selon tranche.haut sous forme
-        -- Revenu de tranche_haut:
+        (selon tranche.TrancheRevenu.haut sous forme
+        -- LimiteTranche.Revenu de tranche_haut:
           (si ressources_ménage_arrondies >=€ tranche_haut
           alors
-            (tranche_haut -€ tranche.bas) *€ tranche.taux
+            (tranche_haut -€ tranche.TrancheRevenu.bas) *€
+              tranche.TrancheRevenu.taux
           sinon
-            ((ressources_ménage_arrondies -€ tranche.bas) *€ tranche.taux))
-        -- Infini:
-          (ressources_ménage_arrondies -€ tranche.bas) *€ tranche.taux)
+            ((ressources_ménage_arrondies -€ tranche.TrancheRevenu.bas) *€
+              tranche.TrancheRevenu.taux))
+        -- LimiteTranche.Infini:
+          (ressources_ménage_arrondies -€ tranche.TrancheRevenu.bas) *€
+            tranche.TrancheRevenu.taux)
       ))) +€
     montant_forfaitaire_d832_26) *€ (1,0 /. 12,0)
 ```

examples/aides_logement/prologue.catala_fr

@@ -107,6 +107,15 @@ déclaration structure TrancheRevenu:
   donnée bas contenu argent
   donnée taux contenu décimal
 
+déclaration énumération LimiteTrancheDécimal:
+  -- Revenu contenu décimal
+  -- Infini
+
+déclaration structure TrancheRevenuDécimal:
+  donnée haut contenu LimiteTranche
+  donnée bas contenu décimal
+  donnée taux contenu décimal
+
 déclaration structure LogementFoyer:
   donnée type contenu TypeLogementFoyer
   donnée date_conventionnement contenu date
@@ -605,7 +614,8 @@ déclaration champ d'application CalculÉquivalenceLoyerMinimale:
   entrée n_nombre_parts_d832_25 contenu décimal
 
   interne tranches_revenus_d832_26 contenu collection TrancheRevenu
-  interne tranches_revenus_d832_26_multipliées contenu collection TrancheRevenu
+  interne tranches_revenus_d832_26_multipliées contenu
+    collection TrancheRevenuDécimal
   interne montant_forfaitaire_d832_26 contenu argent
 
   sortie montant contenu argent