Merge pull request #268 from AltGr/combined-exns

Compiler: support cumulative exceptions

.git-blame-ignore-revs

@@ -1,6 +1,8 @@
 # Reformatting commits to be skipped when running 'git blame'
 # Use `git config --global blame.ignoreRevsFile .git-blame-ignore-revs` to use it
 # Add new reformatting commits at the top
+f9fc1a8e8b0b2dcbf5361f95ca778df63ac4e247
+
 f17875f90e07688f683e5ea6e880c57ded640a81
 74c56291530569c6a1ad1ddc5d97dd10dedc37b3
 fa3693d813c89f2cade851e275cd0000b642fdf6

.gitignore

@@ -1,5 +1,6 @@
 _build/
 _opam/
+dune-workspace*
 result
 *.install
 *.spellok
@@ -10,4 +11,4 @@ legifrance_oauth*
 .vscode/
 .ninja_*
 
-build.ninja
+build.ninja

Makefile

@@ -78,7 +78,7 @@ compiler/surface/parser.messages: compiler/surface/tokens.mly compiler/surface/p
 parser-messages: compiler/surface/parser.messages
 
 format:
-	dune build @fmt --auto-promote >/dev/null || true
+	dune build @fmt --auto-promote 2>/dev/null || true
 
 ##########################################
 # Syntax highlighting rules
@@ -272,7 +272,7 @@ test_examples: .FORCE
 	$(CLERK) test examples
 
 test_clerk: .FORCE
-	cd $(BUILD_SYSTEM_DIR) && dune test
+	dune test $(BUILD_SYSTEM_DIR)
 
 #> tests					: Run interpreter tests
 tests: test_suite test_examples test_clerk

build_system/clerk_driver.ml

@@ -147,7 +147,7 @@ type expected_output_descr = {
   scope : string option;
 }
 
-let catala_suffix_regex = Re.Pcre.regexp "\\.catala_(\\w){2}"
+let catala_suffix_regex = Re.Pcre.regexp "\\.catala_(\\w){2}$"
 
 let filename_to_expected_output_descr (output_dir : string) (filename : string)
     : expected_output_descr option =

build_system/ninja_utils.ml

@@ -18,17 +18,14 @@ module Expr = struct
   type t = Lit of string | Var of string | Seq of t list
 
   let rec format fmt = function
-    | Lit s -> Format.fprintf fmt "%s" s
+    | Lit s -> Format.pp_print_string fmt s
     | Var s -> Format.fprintf fmt "$%s" s
     | Seq ls -> format_list fmt ls
 
-  and format_list fmt = function
-    | hd :: tl ->
-      Format.fprintf fmt "%a%a" format hd
-        (fun fmt tl ->
-          tl |> List.iter (fun s -> Format.fprintf fmt " %a" format s))
-        tl
-    | [] -> ()
+  and format_list fmt ls =
+    Format.pp_print_list
+      ~pp_sep:(fun fmt () -> Format.pp_print_char fmt ' ')
+      format fmt ls
 end
 
 module Rule = struct

compiler/desugared/ast.ml

@@ -155,6 +155,116 @@ type expr =
   | EArray of expr Pos.marked list
   | ErrorOnEmpty of expr Pos.marked
 
+module Expr = struct
+  type t = expr
+
+  (** Syntactic comparison, up to locations and alpha-renaming *)
+  let rec compare e1 e2 =
+    let rec list_compare cmp l1 l2 =
+      (* List.compare is available from OCaml 4.12 on *)
+      match l1, l2 with
+      | [], [] -> 0
+      | [], _ :: _ -> -1
+      | _ :: _, [] -> 1
+      | a1 :: l1, a2 :: l2 ->
+        let c = cmp a1 a2 in
+        if c <> 0 then c else list_compare cmp l1 l2
+    in
+    match e1, e2 with
+    | ELocation _, ELocation _ -> 0
+    | EVar (v1, _), EVar (v2, _) -> Bindlib.compare_vars v1 v2
+    | EStruct (name1, field_map1), EStruct (name2, field_map2) -> (
+      match Scopelang.Ast.StructName.compare name1 name2 with
+      | 0 ->
+        Scopelang.Ast.StructFieldMap.compare
+          (Pos.compare_marked compare)
+          field_map1 field_map2
+      | n -> n)
+    | ( EStructAccess ((e1, _), field_name1, struct_name1),
+        EStructAccess ((e2, _), field_name2, struct_name2) ) -> (
+      match compare e1 e2 with
+      | 0 -> (
+        match Scopelang.Ast.StructFieldName.compare field_name1 field_name2 with
+        | 0 -> Scopelang.Ast.StructName.compare struct_name1 struct_name2
+        | n -> n)
+      | n -> n)
+    | EEnumInj ((e1, _), cstr1, name1), EEnumInj ((e2, _), cstr2, name2) -> (
+      match compare e1 e2 with
+      | 0 -> (
+        match Scopelang.Ast.EnumName.compare name1 name2 with
+        | 0 -> Scopelang.Ast.EnumConstructor.compare cstr1 cstr2
+        | n -> n)
+      | n -> n)
+    | EMatch ((e1, _), name1, emap1), EMatch ((e2, _), name2, emap2) -> (
+      match compare e1 e2 with
+      | 0 -> (
+        match Scopelang.Ast.EnumName.compare name1 name2 with
+        | 0 ->
+          Scopelang.Ast.EnumConstructorMap.compare
+            (Pos.compare_marked compare)
+            emap1 emap2
+        | n -> n)
+      | n -> n)
+    | ELit l1, ELit l2 -> Stdlib.compare l1 l2
+    | EAbs ((binder1, _), typs1), EAbs ((binder2, _), typs2) -> (
+      match
+        list_compare (Pos.compare_marked Scopelang.Ast.Typ.compare) typs1 typs2
+      with
+      | 0 ->
+        let _, (e1, _), (e2, _) = Bindlib.unmbind2 binder1 binder2 in
+        compare e1 e2
+      | n -> n)
+    | EApp ((f1, _), args1), EApp ((f2, _), args2) -> (
+      match compare f1 f2 with
+      | 0 -> list_compare (fun (x1, _) (x2, _) -> compare x1 x2) args1 args2
+      | n -> n)
+    | EOp op1, EOp op2 -> Stdlib.compare op1 op2
+    | ( EDefault (exs1, (just1, _), (cons1, _)),
+        EDefault (exs2, (just2, _), (cons2, _)) ) -> (
+      match compare just1 just2 with
+      | 0 -> (
+        match compare cons1 cons2 with
+        | 0 -> list_compare (Pos.compare_marked compare) exs1 exs2
+        | n -> n)
+      | n -> n)
+    | ( EIfThenElse ((i1, _), (t1, _), (e1, _)),
+        EIfThenElse ((i2, _), (t2, _), (e2, _)) ) -> (
+      match compare i1 i2 with
+      | 0 -> ( match compare t1 t2 with 0 -> compare e1 e2 | n -> n)
+      | n -> n)
+    | EArray a1, EArray a2 ->
+      list_compare (fun (e1, _) (e2, _) -> compare e1 e2) a1 a2
+    | ErrorOnEmpty (e1, _), ErrorOnEmpty (e2, _) -> compare e1 e2
+    | ELocation _, _ -> -1
+    | _, ELocation _ -> 1
+    | EVar _, _ -> -1
+    | _, EVar _ -> 1
+    | EStruct _, _ -> -1
+    | _, EStruct _ -> 1
+    | EStructAccess _, _ -> -1
+    | _, EStructAccess _ -> 1
+    | EEnumInj _, _ -> -1
+    | _, EEnumInj _ -> 1
+    | EMatch _, _ -> -1
+    | _, EMatch _ -> 1
+    | ELit _, _ -> -1
+    | _, ELit _ -> 1
+    | EAbs _, _ -> -1
+    | _, EAbs _ -> 1
+    | EApp _, _ -> -1
+    | _, EApp _ -> 1
+    | EOp _, _ -> -1
+    | _, EOp _ -> 1
+    | EDefault _, _ -> -1
+    | _, EDefault _ -> 1
+    | EIfThenElse _, _ -> -1
+    | _, EIfThenElse _ -> 1
+    | EArray _, _ -> -1
+    | _, EArray _ -> 1
+end
+
+module ExprMap = Map.Make (Expr)
+
 module Var = struct
   type t = expr Bindlib.var
 
@@ -176,6 +286,41 @@ type rule = {
   rule_exception_to_rules : RuleSet.t Pos.marked;
 }
 
+module Rule = struct
+  type t = rule
+
+  (** Structural equality (otherwise, you should just compare the [rule_id]
+      fields) *)
+  let compare r1 r2 =
+    match r1.rule_parameter, r2.rule_parameter with
+    | None, None -> (
+      let j1, _ = Bindlib.unbox r1.rule_just in
+      let j2, _ = Bindlib.unbox r2.rule_just in
+      match Expr.compare j1 j2 with
+      | 0 ->
+        let c1, _ = Bindlib.unbox r1.rule_cons in
+        let c2, _ = Bindlib.unbox r2.rule_cons in
+        Expr.compare c1 c2
+      | n -> n)
+    | Some (v1, (t1, _)), Some (v2, (t2, _)) -> (
+      match Scopelang.Ast.Typ.compare t1 t2 with
+      | 0 -> (
+        let open Bindlib in
+        let b1 = unbox (bind_var v1 r1.rule_just) in
+        let b2 = unbox (bind_var v2 r2.rule_just) in
+        let _, (j1, _), (j2, _) = unbind2 b1 b2 in
+        match Expr.compare j1 j2 with
+        | 0 ->
+          let b1 = unbox (bind_var v1 r1.rule_cons) in
+          let b2 = unbox (bind_var v2 r2.rule_cons) in
+          let _, (c1, _), (c2, _) = unbind2 b1 b2 in
+          Expr.compare c1 c2
+        | n -> n)
+      | n -> n)
+    | None, Some _ -> -1
+    | Some _, None -> 1
+end
+
 let empty_rule
     (pos : Pos.t)
     (have_parameter : Scopelang.Ast.typ Pos.marked option) : rule =

compiler/desugared/ast.mli

@@ -91,6 +91,8 @@ type expr =
   | EArray of expr Pos.marked list
   | ErrorOnEmpty of expr Pos.marked
 
+module ExprMap : Map.S with type key = expr
+
 (** {2 Variable helpers} *)
 
 module Var : sig
@@ -137,6 +139,8 @@ type rule = {
   rule_exception_to_rules : RuleSet.t Pos.marked;
 }
 
+module Rule : Set.OrderedType with type t = rule
+
 val empty_rule : Pos.t -> Scopelang.Ast.typ Pos.marked option -> rule
 val always_false_rule : Pos.t -> Scopelang.Ast.typ Pos.marked option -> rule
 

compiler/desugared/desugared_to_scope.ml

@@ -129,8 +129,8 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
   | EDefault (excepts, just, cons) ->
     Bindlib.box_apply3
       (fun new_excepts new_just new_cons ->
-        ( Scopelang.Ast.EDefault (new_excepts, new_just, new_cons),
-          Pos.get_position e ))
+        Scopelang.Ast.make_default ~pos:(Pos.get_position e) new_excepts
+          new_just new_cons)
       (Bindlib.box_list (List.map (translate_expr ctx) excepts))
       (translate_expr ctx just) (translate_expr ctx cons)
   | EIfThenElse (e1, e2, e3) ->
@@ -181,7 +181,7 @@ let def_map_to_tree (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) :
     let base_case_as_rule_list =
       List.map
         (fun r -> Ast.RuleMap.find r def)
-        (List.of_seq (Ast.RuleSet.to_seq base_cases))
+        (Ast.RuleSet.elements base_cases)
     in
     match exceptions with
     | [] -> Leaf base_case_as_rule_list
@@ -261,21 +261,17 @@ let rec rule_tree_to_expr
   let default_containing_base_cases =
     Bindlib.box_apply2
       (fun base_just_list base_cons_list ->
-        ( Scopelang.Ast.EDefault
-            ( List.map2
-                (fun base_just base_cons ->
-                  ( Scopelang.Ast.EDefault
-                      ( [],
-                        (* Here we insert the logging command that records when
-                           a decision is taken for the value of a variable. *)
-                        tag_with_log_entry base_just
-                          Dcalc.Ast.PosRecordIfTrueBool [],
-                        base_cons ),
-                    Pos.get_position base_just ))
-                base_just_list base_cons_list,
-              (Scopelang.Ast.ELit (Dcalc.Ast.LBool false), def_pos),
-              (Scopelang.Ast.ELit Dcalc.Ast.LEmptyError, def_pos) ),
-          def_pos ))
+        Scopelang.Ast.make_default
+          (List.map2
+             (fun base_just base_cons ->
+               Scopelang.Ast.make_default ~pos:def_pos []
+                 (* Here we insert the logging command that records when a
+                    decision is taken for the value of a variable. *)
+                 (tag_with_log_entry base_just Dcalc.Ast.PosRecordIfTrueBool [])
+                 base_cons)
+             base_just_list base_cons_list)
+          (Scopelang.Ast.ELit (Dcalc.Ast.LBool false), def_pos)
+          (Scopelang.Ast.ELit Dcalc.Ast.LEmptyError, def_pos))
       (Bindlib.box_list (translate_and_unbox_list base_just_list))
       (Bindlib.box_list (translate_and_unbox_list base_cons_list))
   in
@@ -288,11 +284,9 @@ let rec rule_tree_to_expr
   let default =
     Bindlib.box_apply2
       (fun exceptions default_containing_base_cases ->
-        ( Scopelang.Ast.EDefault
-            ( exceptions,
-              (Scopelang.Ast.ELit (Dcalc.Ast.LBool true), def_pos),
-              default_containing_base_cases ),
-          def_pos ))
+        Scopelang.Ast.make_default exceptions
+          (Scopelang.Ast.ELit (Dcalc.Ast.LBool true), def_pos)
+          default_containing_base_cases)
       exceptions default_containing_base_cases
   in
   match is_func, (List.hd base_rules).Ast.rule_parameter with

compiler/scopelang/ast.ml

@@ -78,6 +78,30 @@ type typ =
   | TArray of typ
   | TAny
 
+module Typ = struct
+  type t = typ
+
+  let rec compare ty1 ty2 =
+    match ty1, ty2 with
+    | TLit l1, TLit l2 -> Stdlib.compare l1 l2
+    | TStruct n1, TStruct n2 -> StructName.compare n1 n2
+    | TEnum en1, TEnum en2 -> EnumName.compare en1 en2
+    | TArrow ((a1, _), (b1, _)), TArrow ((a2, _), (b2, _)) -> (
+      match compare a1 a2 with 0 -> compare b1 b2 | n -> n)
+    | TArray t1, TArray t2 -> compare t1 t2
+    | TAny, TAny -> 0
+    | TLit _, _ -> -1
+    | _, TLit _ -> 1
+    | TStruct _, _ -> -1
+    | _, TStruct _ -> 1
+    | TEnum _, _ -> -1
+    | _, TEnum _ -> 1
+    | TArrow _, _ -> -1
+    | _, TArrow _ -> 1
+    | TArray _, _ -> -1
+    | _, TArray _ -> 1
+end
+
 type expr =
   | ELocation of location
   | EVar of expr Bindlib.var Pos.marked
@@ -96,6 +120,111 @@ type expr =
   | EArray of expr Pos.marked list
   | ErrorOnEmpty of expr Pos.marked
 
+module Expr = struct
+  type t = expr
+
+  let rec compare e1 e2 =
+    let rec list_compare cmp l1 l2 =
+      (* List.compare is available from OCaml 4.12 on *)
+      match l1, l2 with
+      | [], [] -> 0
+      | [], _ :: _ -> -1
+      | _ :: _, [] -> 1
+      | a1 :: l1, a2 :: l2 ->
+        let c = cmp a1 a2 in
+        if c <> 0 then c else list_compare cmp l1 l2
+    in
+    match e1, e2 with
+    | ELocation _, ELocation _ -> 0
+    | EVar (v1, _), EVar (v2, _) -> Bindlib.compare_vars v1 v2
+    | EStruct (name1, field_map1), EStruct (name2, field_map2) -> (
+      match StructName.compare name1 name2 with
+      | 0 ->
+        StructFieldMap.compare
+          (Pos.compare_marked compare)
+          field_map1 field_map2
+      | n -> n)
+    | ( EStructAccess ((e1, _), field_name1, struct_name1),
+        EStructAccess ((e2, _), field_name2, struct_name2) ) -> (
+      match compare e1 e2 with
+      | 0 -> (
+        match StructFieldName.compare field_name1 field_name2 with
+        | 0 -> StructName.compare struct_name1 struct_name2
+        | n -> n)
+      | n -> n)
+    | EEnumInj ((e1, _), cstr1, name1), EEnumInj ((e2, _), cstr2, name2) -> (
+      match compare e1 e2 with
+      | 0 -> (
+        match EnumName.compare name1 name2 with
+        | 0 -> EnumConstructor.compare cstr1 cstr2
+        | n -> n)
+      | n -> n)
+    | EMatch ((e1, _), name1, emap1), EMatch ((e2, _), name2, emap2) -> (
+      match compare e1 e2 with
+      | 0 -> (
+        match EnumName.compare name1 name2 with
+        | 0 ->
+          EnumConstructorMap.compare (Pos.compare_marked compare) emap1 emap2
+        | n -> n)
+      | n -> n)
+    | ELit l1, ELit l2 -> Stdlib.compare l1 l2
+    | EAbs ((binder1, _), typs1), EAbs ((binder2, _), typs2) -> (
+      match list_compare (Pos.compare_marked Typ.compare) typs1 typs2 with
+      | 0 ->
+        let _, (e1, _), (e2, _) = Bindlib.unmbind2 binder1 binder2 in
+        compare e1 e2
+      | n -> n)
+    | EApp ((f1, _), args1), EApp ((f2, _), args2) -> (
+      match compare f1 f2 with
+      | 0 -> list_compare (fun (x1, _) (x2, _) -> compare x1 x2) args1 args2
+      | n -> n)
+    | EOp op1, EOp op2 -> Stdlib.compare op1 op2
+    | ( EDefault (exs1, (just1, _), (cons1, _)),
+        EDefault (exs2, (just2, _), (cons2, _)) ) -> (
+      match compare just1 just2 with
+      | 0 -> (
+        match compare cons1 cons2 with
+        | 0 -> list_compare (Pos.compare_marked compare) exs1 exs2
+        | n -> n)
+      | n -> n)
+    | ( EIfThenElse ((i1, _), (t1, _), (e1, _)),
+        EIfThenElse ((i2, _), (t2, _), (e2, _)) ) -> (
+      match compare i1 i2 with
+      | 0 -> ( match compare t1 t2 with 0 -> compare e1 e2 | n -> n)
+      | n -> n)
+    | EArray a1, EArray a2 ->
+      list_compare (fun (e1, _) (e2, _) -> compare e1 e2) a1 a2
+    | ErrorOnEmpty (e1, _), ErrorOnEmpty (e2, _) -> compare e1 e2
+    | ELocation _, _ -> -1
+    | _, ELocation _ -> 1
+    | EVar _, _ -> -1
+    | _, EVar _ -> 1
+    | EStruct _, _ -> -1
+    | _, EStruct _ -> 1
+    | EStructAccess _, _ -> -1
+    | _, EStructAccess _ -> 1
+    | EEnumInj _, _ -> -1
+    | _, EEnumInj _ -> 1
+    | EMatch _, _ -> -1
+    | _, EMatch _ -> 1
+    | ELit _, _ -> -1
+    | _, ELit _ -> 1
+    | EAbs _, _ -> -1
+    | _, EAbs _ -> 1
+    | EApp _, _ -> -1
+    | _, EApp _ -> 1
+    | EOp _, _ -> -1
+    | _, EOp _ -> 1
+    | EDefault _, _ -> -1
+    | _, EDefault _ -> 1
+    | EIfThenElse _, _ -> -1
+    | _, EIfThenElse _ -> 1
+    | EArray _, _ -> -1
+    | _, EArray _ -> 1
+end
+
+module ExprMap = Map.Make (Expr)
+
 let rec locations_used (e : expr Pos.marked) : LocationSet.t =
   match Pos.unmark e with
   | ELocation l -> LocationSet.singleton (l, Pos.get_position e)
@@ -199,4 +328,19 @@ let make_let_in
        (Pos.get_position (Bindlib.unbox e2)))
     (Bindlib.box_list [e1])
 
+let make_default ?(pos = Pos.no_pos) exceptions just cons =
+  let rec bool_value = function
+    | ELit (Dcalc.Ast.LBool b), _ -> Some b
+    | EApp ((EOp (Unop (Log _)), _), [e]), _ -> bool_value e
+    | _ -> None
+  in
+  match exceptions, bool_value just, cons with
+  | [], Some true, cons -> cons
+  | exceptions, Some true, (EDefault ([], just, cons), pos) ->
+    EDefault (exceptions, just, cons), pos
+  | [except], Some false, _ -> except
+  | exceptions, _, cons ->
+    let pos = if pos <> Pos.no_pos then pos else Pos.get_position just in
+    EDefault (exceptions, just, cons), pos
+
 module VarMap = Map.Make (Var)

compiler/scopelang/ast.mli

@@ -66,6 +66,8 @@ type typ =
   | TArray of typ
   | TAny
 
+module Typ : Set.OrderedType with type t = typ
+
 (** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib}
     library, based on higher-order abstract syntax*)
 type expr =
@@ -86,6 +88,9 @@ type expr =
   | EArray of expr Pos.marked list
   | ErrorOnEmpty of expr Pos.marked
 
+module Expr : Set.OrderedType with type t = expr
+module ExprMap : Map.S with type key = expr
+
 val locations_used : expr Pos.marked -> LocationSet.t
 
 (** This type characterizes the three levels of visibility for a given scope
@@ -164,3 +169,22 @@ val make_let_in :
   expr Pos.marked Bindlib.box ->
   expr Pos.marked Bindlib.box ->
   expr Pos.marked Bindlib.box
+
+val make_default :
+  ?pos:Pos.t ->
+  expr Pos.marked list ->
+  expr Pos.marked ->
+  expr Pos.marked ->
+  expr Pos.marked
+(** [make_default ?pos exceptions just cons] builds a term semantically
+    equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor)
+    while avoiding redundant nested constructions. The position is extracted
+    from [just] by default.
+
+    Note that, due to the simplifications taking place, the result might not be
+    of the form [EDefault]:
+
+    - [<true :- x>] is rewritten as [x]
+    - [<ex | true :- def>], when [def] is a default term [<j :- c>] without
+      exceptions, is collapsed into [<ex | def>]
+    - [<ex | false :- _>], when [ex] is a single exception, is rewritten as [ex] *)

compiler/scopelang/scope_to_dcalc.ml

@@ -115,6 +115,45 @@ let tag_with_log_entry
         Pos.get_position e ))
     e
 
+(* In a list of exceptions, it is normally an error if more than a single one
+   apply at the same time. This relaxes this constraint slightly, allowing a
+   conflict if all the triggered conflicting exception yield syntactically equal
+   results (and as long as none of these exceptions have exceptions themselves)
+
+   NOTE: the choice of the exception that will be triggered and show in the
+   trace is arbitrary (but deterministic). *)
+let collapse_similar_outcomes (excepts : Ast.expr Pos.marked list) :
+    Ast.expr Pos.marked list =
+  let cons_map =
+    List.fold_left
+      (fun map -> function
+        | (Ast.EDefault ([], _, (cons, _)), _) as e ->
+          Ast.ExprMap.update cons
+            (fun prev -> Some (e :: Option.value ~default:[] prev))
+            map
+        | _ -> map)
+      Ast.ExprMap.empty excepts
+  in
+  let _, excepts =
+    List.fold_right
+      (fun e (cons_map, excepts) ->
+        match e with
+        | Ast.EDefault ([], _, (cons, _)), _ ->
+          let collapsed_exc =
+            List.fold_left
+              (fun acc -> function
+                | Ast.EDefault ([], just, cons), pos ->
+                  [Ast.EDefault (acc, just, cons), pos]
+                | _ -> assert false)
+              []
+              (Ast.ExprMap.find cons cons_map)
+          in
+          Ast.ExprMap.add cons [] cons_map, collapsed_exc @ excepts
+        | e -> cons_map, e :: excepts)
+      excepts (cons_map, [])
+  in
+  excepts
+
 let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
     Dcalc.Ast.expr Pos.marked Bindlib.box =
   Bindlib.box_apply
@@ -287,6 +326,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
           Dcalc.Ast.EAbs ((b, pos_binder), List.map (translate_typ ctx) typ))
         binder
     | EDefault (excepts, just, cons) ->
+      let excepts = collapse_similar_outcomes excepts in
       Bindlib.box_apply3
         (fun e j c -> Dcalc.Ast.EDefault (e, j, c))
         (Bindlib.box_list (List.map (translate_expr ctx) excepts))

compiler/utils/pos.ml

@@ -222,6 +222,12 @@ let get_position ((_, x) : 'a marked) : t = x
 let map_under_mark (f : 'a -> 'b) ((x, y) : 'a marked) : 'b marked = f x, y
 let same_pos_as (x : 'a) ((_, y) : 'b marked) : 'a marked = x, y
 
+let compare_marked
+    (cmp : 'a -> 'a -> int)
+    ((x, _) : 'a marked)
+    ((y, _) : 'a marked) : int =
+  cmp x y
+
 let unmark_option (x : 'a marked option) : 'a option =
   match x with Some x -> Some (unmark x) | None -> None
 

compiler/utils/pos.mli

@@ -68,6 +68,9 @@ val map_under_mark : ('a -> 'b) -> 'a marked -> 'b marked
 val same_pos_as : 'a -> 'b marked -> 'a marked
 val unmark_option : 'a marked option -> 'a option
 
+val compare_marked : ('a -> 'a -> int) -> 'a marked -> 'a marked -> int
+(** Compares two marked values {b ignoring positions} *)
+
 (** Visitors *)
 
 class ['self] marked_map :

dune

@@ -1 +1,21 @@
-(dirs compiler plugins french_law build_system syntax_highlighting)
+(dirs compiler french_law build_system)
+
+(data_only_dirs tests examples syntax_highlighting)
+
+(alias
+ (name exec)
+ (deps compiler/catala.exe build_system/clerk.exe))
+
+(rule
+ (alias runtest)
+ (deps
+  (source_tree tests))
+ (action
+  (run clerk --exe %{bin:catala} test tests)))
+
+(rule
+ (alias runtest)
+ (deps
+  (source_tree examples))
+ (action
+  (run clerk --exe %{bin:catala} test examples)))

examples/tutorial_en/tutorial_en.catala_en

@@ -526,6 +526,44 @@ patterns. Sometimes, you want to declare an exception to a group of
 piecewise definitions. To do that, simply use the same label for all
 the piecewise definitions.
 
+### Cumulative exceptions
+
+As we have seen, two exceptions applying at the same time to a given rule are in
+conflict, and trigger an error. It happens, though, that these exceptions yield
+the same end result: for convenience, Catala tolerates this case and returns the
+common result, as long as there is a strict syntactic equality.
+
+#### Article 6 bis
+
+Individuals with 7 children or more are exempted of the income tax mentioned
+at article 1.
+
+```catala
+scope NewIncomeTaxComputationFixed:
+  exception article_5
+  definition income_tax under condition
+    individual.number_of_children >= 7
+  consequence equals $0
+```
+
+The same problem as above would be triggered for families with an income below
+`$10,000` and 7 children or more. But here Catala can detect that it won't
+matter since the result in both cases is an exemption.
+
+```catala
+declaration scope Test4:
+  tax_computation scope NewIncomeTaxComputationFixed
+  output income_tax content money
+
+scope Test4:
+  definition tax_computation.individual equals Individual {
+    -- income: $7,000
+    -- number_of_children: 7
+  }
+  definition income_tax equals tax_computation.income_tax
+  assertion income_tax = $0
+```
+
 ## Context scope variables
 
 With its "input","output" and "internal" variables, Catala's scope are close

tests/test_bool/good/output/test_bool.catala_en.Dcalc

@@ -6,13 +6,10 @@ let TestBool_13 :
     let foo_15 : unit → bool = TestBool_in_14."foo_in" in
     let bar_16 : unit → integer = TestBool_in_14."bar_in" in
     let bar_17 : integer = error_empty
-      ⟨bar_16 () | true ⊢
-        ⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
-          ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
+      ⟨bar_16 () | true ⊢ ⟨1 | false ⊢ ∅ ⟩⟩ in
     let foo_18 : bool = error_empty
       ⟨foo_15 () | true ⊢
-        ⟨⟨true ⊢ ⟨⟨bar_17 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
-          ⟨true ⊢ ⟨⟨bar_17 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
-          true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
+        ⟨⟨bar_17 < 0 ⊢ false⟩, ⟨bar_17 >= 0 ⊢ true⟩ | false ⊢
+          ∅ ⟩⟩ in
     TestBool_out {"foo_out"= foo_18; "bar_out"= bar_17} in
 TestBool_13

tests/test_bool/good/output/test_bool.catala_en.Scopelang

@@ -1,8 +1,4 @@
 let scope TestBool (foo: bool|context|output) (bar: integer|context|output) =
-  let bar : integer = reentrant or by default
-    ⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
-      ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩;
+  let bar : integer = reentrant or by default ⟨1 | false ⊢ ∅ ⟩;
   let foo : bool = reentrant or by default
-    ⟨⟨true ⊢ ⟨⟨bar < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
-      ⟨true ⊢ ⟨⟨bar >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
-      true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩
+    ⟨⟨bar < 0 ⊢ false⟩, ⟨bar >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩

tests/test_exception/good/output/two_exceptions_same_outcome.catala_en.A.Interpret

@@ -0,0 +1,2 @@
+[RESULT] Computation successful! Results:
+[RESULT] x = 0

tests/test_exception/good/two_exceptions_same_outcome.catala_en

@@ -0,0 +1,21 @@
+## Test
+
+```catala
+declaration scope A:
+  output x content integer
+  internal y content integer
+  internal z content integer
+
+scope A:
+  label base
+  definition x equals -1
+
+  definition y equals 0
+  definition z equals 0
+
+  exception base
+  definition x under condition y = 0 consequence equals 0
+
+  exception base
+  definition x under condition z = 0 consequence equals 0
+```

tests/test_io/good/output/all_io.catala_en.A.Dcalc

@@ -5,19 +5,11 @@ let A =
     let d_33 : integer = A_in_31."d_in" in
     let e_34 : unit → integer = A_in_31."e_in" in
     let f_35 : unit → integer = A_in_31."f_in" in
-    let a_36 : integer = error_empty
-      ⟨⟨true ⊢ ⟨⟨true ⊢ 0⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
-        ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
-    let b_37 : integer = error_empty
-      ⟨⟨true ⊢ ⟨⟨true ⊢ a_36 + 1⟩ | false ⊢ ∅ ⟩⟩ | true
-        ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
+    let a_36 : integer = error_empty ⟨0 | false ⊢ ∅ ⟩ in
+    let b_37 : integer = error_empty ⟨a_36 + 1 | false ⊢ ∅ ⟩ in
     let e_38 : integer = error_empty
-      ⟨e_34 () | true ⊢
-        ⟨⟨true ⊢
-             ⟨⟨true ⊢ b_37 + c_32 + d_33 + 1⟩ | false ⊢ ∅ ⟩⟩
-          | true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
+      ⟨e_34 () | true ⊢ ⟨b_37 + c_32 + d_33 + 1 | false ⊢ ∅ ⟩⟩
+      in
     let f_39 : integer = error_empty
-      ⟨f_35 () | true ⊢
-        ⟨⟨true ⊢ ⟨⟨true ⊢ e_38 + 1⟩ | false ⊢ ∅ ⟩⟩ |
-          true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
+      ⟨f_35 () | true ⊢ ⟨e_38 + 1 | false ⊢ ∅ ⟩⟩ in
     A_out {"b_out"= b_37; "d_out"= d_33; "f_out"= f_39}

tests/test_io/good/output/condition_only_input.catala_en.B.Dcalc

@@ -1,7 +1,6 @@
 let B =
   λ (B_in_31: B_in{}) →
-    let a.x_32 : bool = error_empty
-      ⟨true ⊢ ⟨⟨true ⊢ false⟩ | false ⊢ ∅ ⟩⟩ in
+    let a.x_32 : bool = error_empty false in
     let result_33 : A_out{"y_out": integer} = A_24 (A_in {"x_in"= a.x_32}) in
     let a.y_34 : integer = result_33."y_out" in
     let __35 : unit = assert (error_empty a.y_34 = 1) in

tests/test_io/good/output/subscope.catala_en.B.Dcalc

@@ -1,9 +1,7 @@
 let B =
   λ (B_in_40: B_in{}) →
     let a.a_41 : unit → integer = λ (__42: unit) → ∅  in
-    let a.b_43 : integer = error_empty
-      ⟨⟨true ⊢ ⟨⟨true ⊢ 2⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
-        ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
+    let a.b_43 : integer = error_empty ⟨2 | false ⊢ ∅ ⟩ in
     let result_44 : A_out{"c_out": integer} =
       A_32 (A_in {"a_in"= a.a_41; "b_in"= a.b_43}) in
     let a.c_45 : integer = result_44."c_out" in

tests/test_proof/bad/enums_unit-overlap.catala_en

@@ -13,8 +13,8 @@ scope A:
   definition x equals Case1 content 2
   definition y under condition match x with pattern
     -- Case1 of i : true
-    -- Case2 : true consequence equals 2
+    -- Case2 : true consequence equals 3
   definition y under condition match x with pattern
     -- Case1 of i : false
-    -- Case2 : true consequence equals 2
+    -- Case2 : true consequence equals 4
 ```

tests/test_scope/bad/bad_sub_sub_scope.catala_en

@@ -1,31 +0,0 @@
-## Article
-
-```catala
-declaration scope A:
-  context output x content integer
-  context output u content boolean
-
-declaration scope B:
-  a1 scope A
-  a2 scope A
-  context output y content integer
-
-declaration scope C:
-  a scope A
-  b scope B
-  context output z content integer
-
-scope A:
- definition x equals 0
- definition u equals true
-
-scope B:
-  definition a2.x under condition a1.u consequence equals 1
-  definition y under condition a2.x = 1 consequence equals 1
-  definition y under condition a2.x + 1 = 2 consequence equals 1
-
-scope C:
-  definition a.x equals 2
-  definition b.y equals 3
-  definition z equals 2
-```

tests/test_scope/bad/output/bad_sub_sub_scope.catala_en.B.Interpret

@@ -1,15 +0,0 @@
-[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
-
-This consequence has a valid justification:
-  --> tests/test_scope/bad/bad_sub_sub_scope.catala_en
-   | 
-25 |   definition y under condition a2.x + 1 = 2 consequence equals 1
-   |                                                                ^
-   + Article
-
-This consequence has a valid justification:
-  --> tests/test_scope/bad/bad_sub_sub_scope.catala_en
-   | 
-24 |   definition y under condition a2.x = 1 consequence equals 1
-   |                                                            ^
-   + Article

tests/test_scope/good/output/sub_sub_scope.catala_en.B.Interpret

@@ -0,0 +1,2 @@
+[RESULT] Computation successful! Results:
+[RESULT] y = 1