Fix a Catala program bug thanks to Proof mode!

compiler/shared_ast/print.ml

@@ -375,7 +375,7 @@ let rec expr_aux :
     | e -> e
   in
   let e = skip_log e in
-  let paren ~rhs expr fmt e1 =
+  let paren ~rhs ?(colors = colors) expr fmt e1 =
     if Precedence.needs_parens ~rhs ~context:e (skip_log e1) then (
       Format.pp_open_hvbox fmt 1;
       Cli.format_with_style [List.hd colors] fmt "(";
@@ -384,7 +384,8 @@ let rec expr_aux :
       Cli.format_with_style [List.hd colors] fmt ")")
     else expr colors fmt e1
   in
-  let lhs ex = paren ~rhs:false ex in
+  let default_punct color fmt s = Cli.format_with_style [color] fmt s in
+  let lhs ?(colors = colors) ex = paren ~colors ~rhs:false ex in
   let rhs ex = paren ~rhs:true ex in
   match Marked.unmark e with
   | EVar v -> var fmt v
@@ -455,15 +456,36 @@ let rec expr_aux :
   | EOp { op; _ } -> operator fmt op
   | EDefault { excepts; just; cons } ->
     if List.length excepts = 0 then
-      Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a%a@]" punctuation "⟨" expr just
-        punctuation "⊢" expr cons punctuation "⟩"
+      Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a%a@]"
+        (default_punct (List.hd colors))
+        "⟨"
+        (exprc (List.tl colors))
+        just
+        (default_punct (List.hd colors))
+        "⊢"
+        (exprc (List.tl colors))
+        cons
+        (default_punct (List.hd colors))
+        "⟩"
     else
       Format.fprintf fmt
-        "@[<hv 0>@[<hov 2>%a %a@]@ @[<hov 2>%a %a@ %a %a@] %a@]" punctuation "⟨"
+        "@[<hv 0>@[<hov 2>%a %a@]@ @[<hov 2>%a %a@ %a %a@] %a@]"
+        (default_punct (List.hd colors))
+        "⟨"
         (Format.pp_print_list
-           ~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ",")
-           (lhs exprc))
-        excepts punctuation "|" expr just punctuation "⊢" expr cons punctuation
+           ~pp_sep:(fun fmt () ->
+             Format.fprintf fmt "%a@ " (default_punct (List.hd colors)) ",")
+           (lhs ~colors:(List.tl colors) exprc))
+        excepts
+        (default_punct (List.hd colors))
+        "|"
+        (exprc (List.tl colors))
+        just
+        (default_punct (List.hd colors))
+        "⊢"
+        (exprc (List.tl colors))
+        cons
+        (default_punct (List.hd colors))
         "⟩"
   | EEmptyError -> lit_style fmt "∅"
   | EErrorOnEmpty e' ->

examples/aides_logement/code_construction_legislatif.catala_fr

@@ -702,7 +702,7 @@ des conventions régies par le chapitre III du titre V du livre III ;
 
 ```catala
 champ d'application ÉligibilitéAidePersonnaliséeLogement:
-  étiquette l831_1_alinea_5
+  étiquette logement_foyer
   règle condition_logement_bailleur sous condition
     selon ménage.logement.mode_occupation sous forme
       -- RésidentLogementFoyer de location:
@@ -1382,7 +1382,7 @@ champ d'application ÉligibilitéAidePersonnaliséeLogement sous condition
   -- LaRéunion: vrai
   -- Mayotte: vrai
   -- n'importe quel: faux):
-  exception l831_1_alinea_5
+  étiquette logement_foyer
   règle condition_logement_bailleur sous condition
     selon ménage.logement.mode_occupation sous forme
       -- RésidentLogementFoyer de location:

examples/aides_logement/code_construction_reglementaire.catala_fr

@@ -3565,7 +3565,7 @@ déclaration énumération TypeLogementFoyer:
 # "ÉligibilitéAidePersonnaliséeLogement" qui assurera que les logements-foyer
 # "Autre" soient bien exclus de l'éligibilité à l'APL.
 champ d'application ÉligibilitéAidePersonnaliséeLogement:
-  exception l831_1_alinea_5
+  exception logement_foyer
   règle condition_logement_bailleur sous condition
     selon ménage.logement.mode_occupation sous forme
       -- RésidentLogementFoyer de logement_foyer:
@@ -3624,6 +3624,7 @@ remplacée par la convention prévue au III de l'article R. 353-159 .
 
 ```catala
 champ d'application ÉligibilitéAidePersonnaliséeLogement:
+  étiquette logement_foyer
   règle condition_logement_bailleur sous condition
     selon ménage.logement.mode_occupation sous forme
       -- RésidentLogementFoyer de logement_foyer:
@@ -5693,7 +5694,7 @@ champ d'application ÉligibilitéAidePersonnaliséeLogement sous condition
   -- LaRéunion: vrai
   -- Mayotte: vrai
   -- n'importe quel: faux:
-   exception l831_1_alinea_5
+   exception logement_foyer
    règle condition_logement_bailleur sous condition
     selon ménage.logement.mode_occupation sous forme
       -- RésidentLogementFoyer de logement_foyer:

examples/aides_logement/tests/tests_eligibilite_apl.catala_fr

@@ -153,103 +153,11 @@ champ d'application Exemple2 :
   }
   définition éligibilité.bénéficie_aide_personnalisée_logement égal à faux
 
-
-
-# déclaration champ d'application Exemple2 :
-#   éligibilité champ d'application ÉligibilitéAidesPersonnelleLogement
-#   résultat éligible contenu booléen
-
-# champ d'application Exemple2 :
-# définition éligible égal à éligibilité.éligibilité
-# assertion non éligible
-#  définition éligibilité.date_ouverture_droits égal à |2020-03-10|
-#  définition éligibilité.ménage égal à Ménage {
-#   -- prestations_reçues: []
-#   -- situation_familiale: Concubins
-#   -- personnes_à_charge: []
-#   -- logement: Logement {
-#     -- résidence_principale : vrai
-#     -- est_ehpad_ou_maison_autonomie_l313_12_asf : faux
-#     -- mode_occupation : Locataire contenu (Location {
-#       -- bailleur: Bailleur {
-#         -- type_bailleur: BailleurPrivé
-#         -- respecte_convention_titre_V: vrai
-#         -- respecte_convention_titre_II: vrai
-#         -- construit_amélioré_conditions_l831_1_4: faux
-#         -- acquisition_aides_état_prêt_titre_II_ou_livre_III: faux
-#       }
-#     })
-#     -- propriétaire : ParentOuAutre.Autre
-#     -- loué_ou_sous_loué_à_des_tiers : LouéOuSousLouéÀDesTiers.Non
-#     -- usufruit : ParentOuAutre.Autre
-#     -- logement_decent_l89_462 : vrai
-#     -- surface_m_carrés : 25
-#   }
-#   -- nombre_autres_occupants_logement: 0
-#   -- condition_rattaché_foyer_fiscal_parent_ifi: vrai
-#  }
-#  définition éligibilité.demandeur égal à Demandeur {
-#    -- age_demandeur : 22
-#    -- date_naissance : |2000-01-03|
-#    -- nationalité : Française
-#    -- patrimoine : Patrimoine {
-#      # D'après le R822_3_3, la periode est annuelle.
-#      -- produisant_revenu_période_r822_3_3_r822_4: 7800€
-#      -- ne_produisant_pas_revenu_période_r822_3_3_r822_4: 0€
-#      }
-#    }
-
-# déclaration champ d'application Exemple3 :
-#   éligibilité champ d'application ÉligibilitéAidesPersonnelleLogement
-#   résultat éligible contenu booléen
-
-# champ d'application Exemple3 :
-# définition éligible égal à éligibilité.éligibilité
-# assertion éligible
-#  définition éligibilité.date_ouverture_droits égal à |2020-03-10|
-#  définition éligibilité.ménage égal à Ménage {
-#   -- prestations_reçues: []
-#   -- situation_familiale: Concubins
-#   -- personnes_à_charge: []
-#   -- logement: Logement {
-#     -- résidence_principale : vrai
-#     -- est_ehpad_ou_maison_autonomie_l313_12_asf : faux
-#     -- mode_occupation : Locataire contenu (Location {
-#       -- bailleur: Bailleur {
-#         -- type_bailleur: BailleurPrivé
-#         -- respecte_convention_titre_V: vrai
-#         -- respecte_convention_titre_II: vrai
-#         -- construit_amélioré_conditions_l831_1_4: faux
-#         -- acquisition_aides_état_prêt_titre_II_ou_livre_III: faux
-#       }
-#     })
-#     -- propriétaire : ParentOuAutre.Autre
-#     -- loué_ou_sous_loué_à_des_tiers : LouéOuSousLouéÀDesTiers.Non
-#     -- usufruit : ParentOuAutre.Autre
-#     -- logement_decent_l89_462 : vrai
-#     -- surface_m_carrés : 25
-#   }
-#   -- nombre_autres_occupants_logement: 0
-#   -- condition_rattaché_foyer_fiscal_parent_ifi: faux
-#  }
-#  définition éligibilité.demandeur égal à Demandeur {
-#    -- age_demandeur : 22
-#    -- date_naissance : |2000-01-03|
-#    -- nationalité : Française
-#    -- patrimoine : Patrimoine {
-#      # D'après le R822_3_3, la periode est annuelle.
-#      -- produisant_revenu_période_r822_3_3_r822_4: 7800€
-#      -- ne_produisant_pas_revenu_période_r822_3_3_r822_4: 0€
-#      }
-#  }
-```
-
-```catala
-déclaration champ d'application Exemple4 :
+déclaration champ d'application Exemple3 :
   éligibilité champ d'application ÉligibilitéAllocationLogement
   résultat éligible contenu TypeÉligibilitéAllocationLogement
 
-champ d'application Exemple4 :
+champ d'application Exemple3 :
   définition éligible égal à éligibilité.éligibilité
   assertion éligible = TypeÉligibilitéAllocationLogement.AllocationLogementFamiliale
   définition éligibilité.date_courante égal à |2023-04-01|
@@ -310,12 +218,40 @@ $ catala Interpret -s Exemple1 --disable_warnings
 [RESULT] éligible = true
 ```
 
-```catala-test-inline
-$ catala Typecheck
-[RESULT] Typechecking successful!
-```
 ```catala-test-inline
 $ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions
 [RESULT] Computation successful! Results:
 [RESULT] éligible = ESome true
 ```
+
+
+```catala-test-inline
+$ catala Interpret -s Exemple2 --disable_warnings
+[RESULT] Computation successful! Results:
+[RESULT] éligible = AllocationLogementFamiliale ()
+```
+
+```catala-test-inline
+$ catala Interpret_Lcalc -s Exemple2 --avoid_exceptions
+[RESULT] Computation successful! Results:
+[RESULT] éligible = ESome AllocationLogementFamiliale ()
+```
+
+
+```catala-test-inline
+$ catala Interpret -s Exemple3 --disable_warnings
+[RESULT] Computation successful! Results:
+[RESULT] éligible = AllocationLogementFamiliale ()
+```
+
+```catala-test-inline
+$ catala Interpret_Lcalc -s Exemple3 --avoid_exceptions
+[RESULT] Computation successful! Results:
+[RESULT] éligible = ESome AllocationLogementFamiliale ()
+```
+
+```catala-test-inline
+$ catala Typecheck
+[RESULT] Typechecking successful!
+```
+