Add lint and fix bugs related

compiler/desugared/linting.ml

@@ -44,6 +44,62 @@ let detect_empty_definitions (p : program) : unit =
         scope.scope_defs)
     p.program_scopes
 
+(* To detect rules that have the same justification and conclusion, we create a
+   set data structure with an appropriate comparison function *)
+module RuleExpressionsMap = Map.Make (struct
+  type t = rule
+
+  let compare x y =
+    let xj, xj_mark = x.rule_just in
+    let yj, yj_mark = y.rule_just in
+    let just =
+      Bindlib.unbox
+        (Bindlib.box_apply2
+           (fun xj yj -> Expr.compare (xj, xj_mark) (yj, yj_mark))
+           xj yj)
+    in
+    if just = 0 then
+      let xc, xc_mark = x.rule_cons in
+      let yc, yc_mark = y.rule_cons in
+      Bindlib.unbox
+        (Bindlib.box_apply2
+           (fun xc yc -> Expr.compare (xc, xc_mark) (yc, yc_mark))
+           xc yc)
+    else just
+end)
+
+let detect_identical_rules (p : program) : unit =
+  ScopeName.Map.iter
+    (fun _ scope ->
+      ScopeDefMap.iter
+        (fun _ scope_def ->
+          let rules_seen =
+            RuleName.Map.fold
+              (fun _ rule rules_seen ->
+                RuleExpressionsMap.update rule
+                  (fun l ->
+                    let x =
+                      ( None,
+                        Pos.overwrite_law_info
+                          (snd (RuleName.get_info rule.rule_id))
+                          (Pos.get_law_info (Expr.pos rule.rule_just)) )
+                    in
+                    match l with None -> Some [x] | Some l -> Some (x :: l))
+                  rules_seen)
+              scope_def.scope_def_rules RuleExpressionsMap.empty
+          in
+          RuleExpressionsMap.iter
+            (fun _ pos ->
+              if List.length pos > 1 then
+                Errors.format_multispanned_warning pos
+                  "These %s have identical justifications and consequences; is \
+                   it a mistake?"
+                  (if scope_def.scope_def_is_condition then "rules"
+                  else "definitions"))
+            rules_seen)
+        scope.scope_defs)
+    p.program_scopes
+
 let detect_unused_scope_vars (p : program) : unit =
   let used_scope_vars =
     Ast.fold_exprs
@@ -200,4 +256,5 @@ let lint_program (p : program) : unit =
   detect_empty_definitions p;
   detect_unused_scope_vars p;
   detect_unused_struct_fields p;
-  detect_unused_enum_constructors p
+  detect_unused_enum_constructors p;
+  detect_identical_rules p

examples/aides_logement/archives.catala_fr

@@ -3600,7 +3600,7 @@ Couple sans enfant                  2,99%
 
 ```catala
 champ d'application CalculAidePersonnaliséeLogementLocatif
-  sous condition date_courante >= |2020-10-01| et date_courante < |2021-10-01|:
+  sous condition date_courante >= |2020-01-01| et date_courante < |2020-10-01|:
   exception base définition taux_composition_familiale sous condition
     (selon résidence sous forme
     -- Guadeloupe: vrai

examples/allocations_familiales/prologue.catala_fr

@@ -142,6 +142,7 @@ déclaration champ d'application AllocationsFamiliales:
   interne âge_minimum_alinéa_1_l521_3 contenu durée
     dépend de enfant contenu Enfant
   interne nombre_enfants_alinéa_2_l521_3 contenu entier
+  interne nombre_enfants_alinéa_2_l521_1 contenu entier
   interne est_enfant_le_plus_âgé contenu booléen
     dépend de enfant contenu Enfant
   interne plafond_I_d521_3 contenu argent

examples/allocations_familiales/securite_sociale_D.catala_fr

@@ -291,7 +291,7 @@ l'article L. 521-1 est fixé à trois.
 
 ```catala
 champ d'application AllocationsFamiliales :
-  définition nombre_enfants_alinéa_2_l521_3 égal à 3
+  définition nombre_enfants_alinéa_2_l521_1 égal à 3
 ```
 
 ####### Article D521-3|LEGIARTI000030678079

examples/allocations_familiales/securite_sociale_L.catala_fr

@@ -116,7 +116,7 @@ champ d'application AllocationsFamiliales :
 
   règle droit_ouvert_forfaitaire de enfant sous condition
     # nombre_enfants_alinéa_2_l521_3 sera défini dans l'article R521-3
-    (nombre de enfants_à_charge >= nombre_enfants_alinéa_2_l521_3) et
+    (nombre de enfants_à_charge >= nombre_enfants_alinéa_2_l521_1) et
     # Puisqu'un enfant ne garde un âge donné que pour une période d'un an,
     # cette condition assure que l'allocation ne peut être distribuée que pour
     # un an.

tests/test_exception/good/double_definition.catala_en

@@ -12,8 +12,22 @@ scope Foo:
 
 ```catala-test-inline
 $ catala Scopelang -s Foo
+[WARNING] These definitions have identical justifications and consequences; is it a mistake?
+
+┌─⯈ tests/test_exception/good/double_definition.catala_en:9.2-14:
+└─┐
+9 │   definition x equals 1
+  │   ‾‾‾‾‾‾‾‾‾‾‾‾
+  └─ Foo
+
+┌─⯈ tests/test_exception/good/double_definition.catala_en:8.2-14:
+└─┐
+8 │   definition x equals 1
+  │   ‾‾‾‾‾‾‾‾‾‾‾‾
+  └─ Foo
 let scope Foo (x: integer|internal|output) =
-  let x : integer = ⟨⟨true ⊢ 1⟩, ⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩
+  let x : integer =
+    ⟨ ⟨true ⊢ 1⟩, ⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩
 ```
 
 In Scopelang we have what looks like conflicting exceptions. But after
@@ -24,9 +38,24 @@ Dcalc translation below.
 
 ```catala-test-inline
 $ catala Dcalc -s Foo
+[WARNING] These definitions have identical justifications and consequences; is it a mistake?
+
+┌─⯈ tests/test_exception/good/double_definition.catala_en:9.2-14:
+└─┐
+9 │   definition x equals 1
+  │   ‾‾‾‾‾‾‾‾‾‾‾‾
+  └─ Foo
+
+┌─⯈ tests/test_exception/good/double_definition.catala_en:8.2-14:
+└─┐
+8 │   definition x equals 1
+  │   ‾‾‾‾‾‾‾‾‾‾‾‾
+  └─ Foo
 let Foo =
   λ (Foo_in: Foo_in {}) →
-    let x : integer = error_empty
-      ⟨⟨⟨true ⊢ 1⟩ | true ⊢ 1⟩ | false ⊢ ∅ ⟩ in
-    Foo { "x"= x }
+    let x : integer =
+      error_empty
+        ⟨ ⟨ ⟨true ⊢ 1⟩ | true ⊢ 1 ⟩ | false ⊢ ∅ ⟩
+    in
+    {Foo "x" = x}
 ```