Merge branch 'master' into refactor-clerk-w-ninja

2024-09-19 16:28:12 +03:00 · 2022-02-25 12:31:16 +01:00 · 2022-02-25 12:31:16 +01:00 · 3a6450b42f
commit 3a6450b42f
parent 4a83360220 c4a7fe36c1
54 changed files with 9691 additions and 7524 deletions
--- a/.gitattributes
+++ b/.gitattributes
@ -1,6 +1,4 @@
-*.catala* linguist-language=Markdown
 *.ml linguist-language=OCaml
-*.fst linguist-language=Fstar
 *.mld linguist-documentation
 *.md linguist-documentation
 *.hints linguist-generated
--- a/.nix/cmdliner.nix
+++ b/.nix/cmdliner.nix
@ -1,38 +0,0 @@
-{ lib, stdenv, fetchurl, ocaml, findlib, ocamlbuild, topkg, result }:
-
-let
-  pname = "cmdliner";
-in
-
-assert lib.versionAtLeast ocaml.version "4.01.0";
-
-let param =
-  {
-    version = "1.1.0";
-    hash = "sha256-irWd4HTlJSYuz3HMgi1de2GVL2qus0QjeCe1WdsSs8Q=";
-  }
-; in
-
-stdenv.mkDerivation rec {
-  name = "ocaml${ocaml.version}-${pname}-${version}";
-  inherit (param) version;
-
-  src = fetchurl {
-    url = "https://erratique.ch/software/${pname}/releases/${pname}-${version}.tbz";
-    inherit (param) hash;
-  };
-
-  nativeBuildInputs = [ ocaml ocamlbuild findlib ];
-  buildInputs = [ topkg ];
-  propagatedBuildInputs = [ result ];
-
-  inherit (topkg) buildPhase installPhase;
-
-  meta = with lib; {
-    homepage = "https://erratique.ch/software/cmdliner";
-    description = "An OCaml module for the declarative definition of command line interfaces";
-    license = licenses.bsd3;
-    platforms = ocaml.meta.platforms or [];
-    maintainers = [ ];
-  };
-}
--- a/.nix/no-web.patch
+++ b/.nix/no-web.patch
@ -14,7 +14,7 @@ index 31d5289..0000000
 -           (language : Js.js_string Js.t) (trace : bool) =
 -         driver
 -           (Contents (Js.to_string contents))
-           false false false "Interpret"
+-           false false false false "Interpret"
 -           (Some (Js.to_string language))
 -           None trace false false
 -           (Some (Js.to_string scope))
--- a/build_system/clerk.ml
+++ b/build_system/clerk.ml
@ -99,8 +99,8 @@ let info =
      `P "Please file bug reports at https://github.com/CatalaLang/catala/issues";
    ]
  in
-  let exits = Cmd.Exit.defaults @ [ Cmd.Exit.info ~doc:"on error." 1 ] in
-  Cmd.info "clerk" ~version ~doc ~exits ~man
+  let exits = Term.default_exits @ [ Term.exit_info ~doc:"on error." 1 ] in
+  Term.info "clerk" ~version ~doc ~exits ~man

 (**{1 Testing}*)

@ -630,5 +630,7 @@ let driver (files_or_folders : string list) (command : string) (catala_exe : str
      1

 let _ =
-  let return_code = Cmdliner.Cmd.eval' (Cmdliner.Cmd.v info (clerk_t driver)) in
-  exit return_code
+  let return_code = Cmdliner.Term.eval (clerk_t driver, info) in
+  match return_code with
+  | `Ok 0 -> Cmdliner.Term.exit (`Ok 0)
+  | _ -> Cmdliner.Term.exit (`Error `Term)
--- a/catala.opam
+++ b/catala.opam
@ -21,7 +21,7 @@ depends: [
  "menhirLib" {>= "20200211"}
  "unionFind" {>= "20200320"}
  "bindlib" {>= "5.0.1"}
-  "cmdliner" {>= "1.1.0"}
+  "cmdliner" {= "1.0.4"}
  "re" {>= "1.9.0"}
  "zarith" {>= "1.12"}
  "zarith_stubs_js" {>= "v0.14.1"}
--- a/compiler/catala_web_interpreter.ml
+++ b/compiler/catala_web_interpreter.ml
@ -8,7 +8,7 @@ let _ =
           (language : Js.js_string Js.t) (trace : bool) =
         driver
           (Contents (Js.to_string contents))
-           false false false "Interpret"
+           false false false false "Interpret"
           (Some (Js.to_string language))
           None trace false false
           (Some (Js.to_string scope))
--- a/compiler/dcalc/ast.ml
+++ b/compiler/dcalc/ast.ml
@ -93,7 +93,7 @@ type log_entry = VarDef of typ | BeginCall | EndCall | PosRecordIfTrueBool
 type unop =
  | Not
  | Minus of op_kind
-  | Log of log_entry * (Utils.Uid.MarkedString.info list[@opaque])
+  | Log of log_entry * Utils.Uid.MarkedString.info list
  | Length
  | IntToRat
  | GetDay
@ -103,7 +103,7 @@ type unop =
 type operator = Ternop of ternop | Binop of binop | Unop of unop

 type expr =
-  | EVar of (expr Bindlib.var[@opaque]) Pos.marked
+  | EVar of expr Bindlib.var Pos.marked
  | ETuple of expr Pos.marked list * struct_name option
  | ETupleAccess of expr Pos.marked * int * struct_name option * typ Pos.marked list
  | EInj of expr Pos.marked * int * enum_name * typ Pos.marked list
@ -143,8 +143,8 @@ type scope_let = {

 type scope_body = {
  scope_body_lets : scope_let list;
-  scope_body_result : expr Pos.marked Bindlib.box;
-  scope_body_arg : expr Bindlib.var;
+  scope_body_result : expr Pos.marked Bindlib.box;  (** {x1 = x1; x2 = x2; x3 = x3; ... } *)
+  scope_body_arg : expr Bindlib.var;  (** x: input_struct *)
  scope_body_input_struct : StructName.t;
  scope_body_output_struct : StructName.t;
 }
@ -164,6 +164,28 @@ end

 module VarMap = Map.Make (Var)

+let union : unit VarMap.t -> unit VarMap.t -> unit VarMap.t = VarMap.union (fun _ _ _ -> Some ())
+
+let rec free_vars_set (e : expr Pos.marked) : unit VarMap.t =
+  match Pos.unmark e with
+  | EVar (v, _) -> VarMap.singleton v ()
+  | ETuple (es, _) | EArray es -> es |> List.map free_vars_set |> List.fold_left union VarMap.empty
+  | ETupleAccess (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 | EInj (e1, _, _, _) ->
+      free_vars_set e1
+  | EApp (e1, es) | EMatch (e1, es, _) ->
+      e1 :: es |> List.map free_vars_set |> List.fold_left union VarMap.empty
+  | EDefault (es, ejust, econs) ->
+      ejust :: econs :: es |> List.map free_vars_set |> List.fold_left union VarMap.empty
+  | EOp _ | ELit _ -> VarMap.empty
+  | EIfThenElse (e1, e2, e3) ->
+      [ e1; e2; e3 ] |> List.map free_vars_set |> List.fold_left union VarMap.empty
+  | EAbs ((binder, _), _) ->
+      let vs, body = Bindlib.unmbind binder in
+      Array.fold_right VarMap.remove vs (free_vars_set body)
+
+let free_vars_list (e : expr Pos.marked) : Var.t list =
+  free_vars_set e |> VarMap.bindings |> List.map fst
+
 type vars = expr Bindlib.mvar

 let make_var ((x, pos) : Var.t Pos.marked) : expr Pos.marked Bindlib.box =
--- a/compiler/dcalc/ast.mli
+++ b/compiler/dcalc/ast.mli
@ -119,7 +119,7 @@ type expr =
      (** The [MarkedString.info] is the former enum case name *)
  | EArray of expr Pos.marked list
  | ELit of lit
-  | EAbs of (expr, expr Pos.marked) Bindlib.mbinder Pos.marked * typ Pos.marked list
+  | EAbs of ((expr, expr Pos.marked) Bindlib.mbinder[@opaque]) Pos.marked * typ Pos.marked list
  | EApp of expr Pos.marked * expr Pos.marked list
  | EAssert of expr Pos.marked
  | EOp of operator
@ -183,6 +183,10 @@ end

 module VarMap : Map.S with type key = Var.t

+val free_vars_set : expr Pos.marked -> unit VarMap.t
+
+val free_vars_list : expr Pos.marked -> Var.t list
+
 type vars = expr Bindlib.mvar

 val make_var : Var.t Pos.marked -> expr Pos.marked Bindlib.box
--- a/compiler/dcalc/binded_representation.ml
+++ b/compiler/dcalc/binded_representation.ml
@ -0,0 +1,132 @@
+(* This file is part of the Catala compiler, a specification language for tax and social benefits
+   computation rules. Copyright (C) 2020-2022 Inria, contributor: Alain Delaët-Tixeuil
+   <alain.delaet--tixeuil@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
+   in compliance with the License. You may obtain a copy of the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software distributed under the License
+   is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
+   or implied. See the License for the specific language governing permissions and limitations under
+   the License. *)
+
+open Utils
+module D = Ast
+
+type scope_lets =
+  | Result of D.expr Pos.marked
+  | ScopeLet of {
+      scope_let_kind : D.scope_let_kind;
+      scope_let_typ : D.typ Pos.marked;
+      scope_let_expr : D.expr Pos.marked;
+      scope_let_next : (D.expr, scope_lets) Bindlib.binder;
+      scope_let_pos : Pos.t;
+    }
+
+type scope_body = {
+  scope_body_input_struct : D.StructName.t;
+  scope_body_output_struct : D.StructName.t;
+  scope_body_result : (D.expr, scope_lets) Bindlib.binder;
+}
+
+type scopes =
+  | Nil
+  | ScopeDef of {
+      scope_name : D.ScopeName.t;
+      scope_body : scope_body;
+      scope_next : (D.expr, scopes) Bindlib.binder;
+    }
+
+let union : unit D.VarMap.t -> unit D.VarMap.t -> unit D.VarMap.t =
+  D.VarMap.union (fun _ _ _ -> Some ())
+
+let rec free_vars_set_scope_lets (scope_lets : scope_lets) : unit D.VarMap.t =
+  match scope_lets with
+  | Result e -> D.free_vars_set e
+  | ScopeLet { scope_let_expr = e; scope_let_next = next; _ } ->
+      let v, body = Bindlib.unbind next in
+      union (D.free_vars_set e) (D.VarMap.remove v (free_vars_set_scope_lets body))
+
+let free_vars_set_scope_body (scope_body : scope_body) : unit D.VarMap.t =
+  let { scope_body_result = binder; _ } = scope_body in
+  let v, body = Bindlib.unbind binder in
+  D.VarMap.remove v (free_vars_set_scope_lets body)
+
+let rec free_vars_set_scopes (scopes : scopes) : unit D.VarMap.t =
+  match scopes with
+  | Nil -> D.VarMap.empty
+  | ScopeDef { scope_body = body; scope_next = next; _ } ->
+      let v, next = Bindlib.unbind next in
+
+      union (D.VarMap.remove v (free_vars_set_scopes next)) (free_vars_set_scope_body body)
+
+let free_vars_list_scope_lets (scope_lets : scope_lets) : D.Var.t list =
+  free_vars_set_scope_lets scope_lets |> D.VarMap.bindings |> List.map fst
+
+let free_vars_list_scope_body (scope_body : scope_body) : D.Var.t list =
+  free_vars_set_scope_body scope_body |> D.VarMap.bindings |> List.map fst
+
+let free_vars_list_scopes (scopes : scopes) : D.Var.t list =
+  free_vars_set_scopes scopes |> D.VarMap.bindings |> List.map fst
+
+(** Actual transformation for scopes. *)
+let bind_scope_lets (acc : scope_lets Bindlib.box) (scope_let : D.scope_let) :
+    scope_lets Bindlib.box =
+  let pos = snd scope_let.D.scope_let_var in
+
+  (* Cli.debug_print @@ Format.asprintf "binding let %a. Variable occurs = %b" Print.format_var (fst
+     scope_let.D.scope_let_var) (Bindlib.occur (fst scope_let.D.scope_let_var) acc); *)
+  let binder = Bindlib.bind_var (fst scope_let.D.scope_let_var) acc in
+  Bindlib.box_apply2
+    (fun expr binder ->
+      (* Cli.debug_print @@ Format.asprintf "free variables in expression: %a" (Format.pp_print_list
+         Print.format_var) (D.free_vars_list expr); *)
+      ScopeLet
+        {
+          scope_let_kind = scope_let.D.scope_let_kind;
+          scope_let_typ = scope_let.D.scope_let_typ;
+          scope_let_expr = expr;
+          scope_let_next = binder;
+          scope_let_pos = pos;
+        })
+    scope_let.D.scope_let_expr binder
+
+let bind_scope_body (body : D.scope_body) : scope_body Bindlib.box =
+  (* it is a fold_right and not a fold_left. *)
+  let body_result =
+    ListLabels.fold_right body.D.scope_body_lets
+      ~init:(Bindlib.box_apply (fun e -> Result e) body.D.scope_body_result)
+      ~f:(Fun.flip bind_scope_lets)
+  in
+
+  (* Cli.debug_print @@ Format.asprintf "binding arg %a" Print.format_var body.D.scope_body_arg; *)
+  let scope_body_result = Bindlib.bind_var body.D.scope_body_arg body_result in
+
+  (* Cli.debug_print @@ Format.asprintf "isfinal term is closed: %b" (Bindlib.is_closed
+     scope_body_result); *)
+  Bindlib.box_apply
+    (fun scope_body_result ->
+      (* Cli.debug_print @@ Format.asprintf "rank of the final term: %i" (Bindlib.binder_rank
+         scope_body_result); *)
+      {
+        scope_body_output_struct = body.D.scope_body_output_struct;
+        scope_body_input_struct = body.D.scope_body_input_struct;
+        scope_body_result;
+      })
+    scope_body_result
+
+let bind_scope
+    ((scope_name, scope_var, scope_body) : D.ScopeName.t * D.expr Bindlib.var * D.scope_body)
+    (acc : scopes Bindlib.box) : scopes Bindlib.box =
+  Bindlib.box_apply2
+    (fun scope_body scope_next -> ScopeDef { scope_name; scope_body; scope_next })
+    (bind_scope_body scope_body) (Bindlib.bind_var scope_var acc)
+
+let bind_scopes (scopes : (D.ScopeName.t * D.expr Bindlib.var * D.scope_body) list) :
+    scopes Bindlib.box =
+  let result = ListLabels.fold_right scopes ~init:(Bindlib.box Nil) ~f:bind_scope in
+  (* Cli.debug_print @@ Format.asprintf "free variable in the program : [%a]" (Format.pp_print_list
+     Print.format_var) (free_vars_list_scopes (Bindlib.unbox result)); *)
+  result
--- a/compiler/dcalc/binded_representation.mli
+++ b/compiler/dcalc/binded_representation.mli
@ -0,0 +1,63 @@
+(* This file is part of the Catala compiler, a specification language for tax and social benefits
+   computation rules. Copyright (C) 2020-2022 Inria, contributor: Alain Delaët-Tixeuil
+   <alain.delaet--tixeuil@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
+   in compliance with the License. You may obtain a copy of the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software distributed under the License
+   is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
+   or implied. See the License for the specific language governing permissions and limitations under
+   the License. *)
+
+module D = Ast
+
+(** Alternative representation of the Dcalc Ast. It is currently used in the transformation without
+    exceptions. We make heavy use of bindlib, binding each scope-let-variable and each scope
+    explicitly. *)
+
+(** In [Ast], [Ast.scope_lets] is defined as a list of kind, var, and boxed expression. This
+    representation binds using bindlib the tail of the list with the variable defined in the let. *)
+type scope_lets =
+  | Result of D.expr Utils.Pos.marked
+  | ScopeLet of {
+      scope_let_kind : D.scope_let_kind;
+      scope_let_typ : D.typ Utils.Pos.marked;
+      scope_let_expr : D.expr Utils.Pos.marked;
+      scope_let_next : (D.expr, scope_lets) Bindlib.binder;
+      scope_let_pos : Utils.Pos.t;
+    }
+
+type scope_body = {
+  scope_body_input_struct : D.StructName.t;
+  scope_body_output_struct : D.StructName.t;
+  scope_body_result : (D.expr, scope_lets) Bindlib.binder;
+}
+(** As a consequence, the scope_body contains only a result and input/output signature, as the other
+    elements are stored inside the scope_let. The binder present is the argument of type
+    [scope_body_input_struct]. *)
+
+(** Finally, we do the same transformation for the whole program for the kinded lets. This permit us
+    to use bindlib variables for scopes names. *)
+type scopes =
+  | Nil
+  | ScopeDef of {
+      scope_name : D.ScopeName.t;
+      scope_body : scope_body;
+      scope_next : (D.expr, scopes) Bindlib.binder;
+    }
+
+val free_vars_list_scope_lets : scope_lets -> D.Var.t list
+(** List of variables not binded inside a scope_lets *)
+
+val free_vars_list_scope_body : scope_body -> D.Var.t list
+(** List of variables not binded inside a scope_body. *)
+
+val free_vars_list_scopes : scopes -> D.Var.t list
+(** List of variables not binded inside scopes*)
+
+val bind_scopes : (D.ScopeName.t * D.expr Bindlib.var * D.scope_body) list -> scopes Bindlib.box
+(** Transform a list of scopes into our representation of scopes. It requires that scopes are
+    topologically-well-ordered, and ensure there is no free variables in the returned [scopes] *)
--- a/compiler/dcalc/optimizations.ml
+++ b/compiler/dcalc/optimizations.ml
@ -123,9 +123,11 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
              ((ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ])), _),
              _ ) ->
              (ELit LEmptyError, pos)
-          | [], just, cons ->
+          | [], just, cons when not !Cli.avoid_exceptions_flag ->
              (* without exceptions, a default is just an [if then else] raising an error in the
-                 else case *)
+                 else case. This exception is only valid in the context of
+                 compilation_with_exceptions, so we desactivate with a global flag to know if we
+                 will be compiling using exceptions or the option monad. *)
              (EIfThenElse (just, cons, (ELit LEmptyError, pos)), pos)
          | exceptions, just, cons -> (EDefault (exceptions, just, cons), pos))
        (List.map rec_helper exceptions |> Bindlib.box_list)
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@ -26,15 +26,17 @@ let extensions = [ (".catala_fr", "fr"); (".catala_en", "en"); (".catala_pl", "p
 (** Entry function for the executable. Returns a negative number in case of error. Usage:
    [driver source_file debug dcalc unstyled wrap_weaved_output backend language max_prec_digits trace optimize scope_to_execute output_file]*)
 let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
-    (wrap_weaved_output : bool) (backend : string) (language : string option)
-    (max_prec_digits : int option) (trace : bool) (disable_counterexamples : bool) (optimize : bool)
-    (ex_scope : string option) (output_file : string option) : int =
+    (wrap_weaved_output : bool) (avoid_exceptions : bool) (backend : string)
+    (language : string option) (max_prec_digits : int option) (trace : bool)
+    (disable_counterexamples : bool) (optimize : bool) (ex_scope : string option)
+    (output_file : string option) : int =
  try
    Cli.debug_flag := debug;
    Cli.style_flag := not unstyled;
    Cli.trace_flag := trace;
    Cli.optimize_flag := optimize;
    Cli.disable_counterexamples := disable_counterexamples;
+    Cli.avoid_exceptions_flag := avoid_exceptions;
    Cli.debug_print "Reading files...";
    let filename = ref "" in
    (match source_file with FileName f -> filename := f | Contents c -> Cli.contents := c);
@ -255,7 +257,10 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
            0
        | Cli.OCaml | Cli.Python | Cli.Lcalc | Cli.Scalc ->
            Cli.debug_print "Compiling program into lambda calculus...";
-            let prgm = Lcalc.Compile_with_exceptions.translate_program prgm in
+            let prgm =
+              if avoid_exceptions then Lcalc.Compile_without_exceptions.translate_program prgm
+              else Lcalc.Compile_with_exceptions.translate_program prgm
+            in
            let prgm =
              if optimize then begin
                Cli.debug_print "Optimizing lambda calculus...";
@ -355,7 +360,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
      -1

 let main () =
-  let return_code =
-    Cmdliner.Cmd.eval' (Cmdliner.Cmd.v Cli.info (Cli.catala_t (fun f -> driver (FileName f))))
-  in
-  exit return_code
+  let return_code = Cmdliner.Term.eval (Cli.catala_t (fun f -> driver (FileName f)), Cli.info) in
+  match return_code with
+  | `Ok 0 -> Cmdliner.Term.exit (`Ok 0)
+  | _ -> Cmdliner.Term.exit (`Error `Term)
--- a/compiler/lcalc/ast.ml
+++ b/compiler/lcalc/ast.ml
@ -74,18 +74,63 @@ let make_app (e : expr Pos.marked Bindlib.box) (u : expr Pos.marked Bindlib.box

 let make_let_in (x : Var.t) (tau : D.typ Pos.marked) (e1 : expr Pos.marked Bindlib.box)
    (e2 : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
-  Bindlib.box_apply2
-    (fun e u -> (EApp (e, u), Pos.get_position (Bindlib.unbox e2)))
-    (make_abs
-       (Array.of_list [ x ])
-       e2
-       (Pos.get_position (Bindlib.unbox e2))
-       [ tau ]
-       (Pos.get_position (Bindlib.unbox e2)))
-    (Bindlib.box_list [ e1 ])
+  let pos = Pos.get_position (Bindlib.unbox e2) in
+
+  make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] pos) [ e1 ] pos
+
+let ( let+ ) x f = Bindlib.box_apply f x
+
+let ( and+ ) x y = Bindlib.box_pair x y
+
+let option_enum : D.EnumName.t = D.EnumName.fresh ("eoption", Pos.no_pos)
+
+let none_constr : D.EnumConstructor.t = D.EnumConstructor.fresh ("ENone", Pos.no_pos)
+
+let some_constr : D.EnumConstructor.t = D.EnumConstructor.fresh ("ESome", Pos.no_pos)
+
+let option_enum_config : (D.EnumConstructor.t * D.typ Pos.marked) list =
+  [ (none_constr, (D.TLit D.TUnit, Pos.no_pos)); (some_constr, (D.TAny, Pos.no_pos)) ]
+
+let make_none (pos : Pos.t) : expr Pos.marked Bindlib.box =
+  let mark : 'a -> 'a Pos.marked = Pos.mark pos in
+  Bindlib.box @@ mark
+  @@ EInj (mark @@ ELit LUnit, 0, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ])
+
+let make_some (e : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
+  let pos = Pos.get_position @@ Bindlib.unbox e in
+  let mark : 'a -> 'a Pos.marked = Pos.mark pos in
+  let+ e = e in
+  mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ])
+
+(** [make_matchopt_with_abs_arms arg e_none e_some] build an expression
+    [match arg with |None -> e_none | Some -> e_some] and requires e_some and e_none to be in the
+    form [EAbs ...].*)
+let make_matchopt_with_abs_arms (arg : expr Pos.marked Bindlib.box)
+    (e_none : expr Pos.marked Bindlib.box) (e_some : expr Pos.marked Bindlib.box) :
+    expr Pos.marked Bindlib.box =
+  let pos = Pos.get_position @@ Bindlib.unbox arg in
+  let mark : 'a -> 'a Pos.marked = Pos.mark pos in
+
+  let+ arg = arg and+ e_none = e_none and+ e_some = e_some in
+
+  mark @@ EMatch (arg, [ e_none; e_some ], option_enum)
+
+(** [make_matchopt pos v tau arg e_none e_some] builds an expression
+    [match arg with | None () -> e_none | Some v -> e_some]. It binds v to e_some, permitting it to
+    be used inside the expression. There is no requirements on the form of both e_some and e_none. *)
+let make_matchopt (pos : Pos.t) (v : Var.t) (tau : D.typ Pos.marked)
+    (arg : expr Pos.marked Bindlib.box) (e_none : expr Pos.marked Bindlib.box)
+    (e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
+  let x = Var.make ("_", pos) in
+
+  make_matchopt_with_abs_arms arg
+    (make_abs (Array.of_list [ x ]) e_none pos [ (D.TLit D.TUnit, pos) ] pos)
+    (make_abs (Array.of_list [ v ]) e_some pos [ tau ] pos)

 let handle_default = Var.make ("handle_default", Pos.no_pos)

+let handle_default_opt = Var.make ("handle_default_opt", Pos.no_pos)
+
 type binder = (expr, expr Pos.marked) Bindlib.binder

 type scope_body = {
--- a/compiler/lcalc/ast.mli
+++ b/compiler/lcalc/ast.mli
@ -90,8 +90,39 @@ val make_let_in :
  expr Pos.marked Bindlib.box ->
  expr Pos.marked Bindlib.box

+val option_enum : Dcalc.Ast.EnumName.t
+
+val none_constr : Dcalc.Ast.EnumConstructor.t
+
+val some_constr : Dcalc.Ast.EnumConstructor.t
+
+val option_enum_config : (Dcalc.Ast.EnumConstructor.t * Dcalc.Ast.typ Pos.marked) list
+
+val make_none : Pos.t -> expr Pos.marked Bindlib.box
+
+val make_some : expr Pos.marked Bindlib.box -> expr Pos.marked Bindlib.box
+
+val make_matchopt_with_abs_arms :
+  expr Pos.marked Bindlib.box ->
+  expr Pos.marked Bindlib.box ->
+  expr Pos.marked Bindlib.box ->
+  expr Pos.marked Bindlib.box
+
+val make_matchopt :
+  Pos.t ->
+  Var.t ->
+  Dcalc.Ast.typ Pos.marked ->
+  expr Pos.marked Bindlib.box ->
+  expr Pos.marked Bindlib.box ->
+  expr Pos.marked Bindlib.box ->
+  expr Pos.marked Bindlib.box
+(** [e' = make_matchopt'' pos v e e_none e_some] Builds the term corresponding to
+    [match e with | None -> fun () -> e_none |Some -> fun v -> e_some]. *)
+
 val handle_default : Var.t

+val handle_default_opt : Var.t
+
 type binder = (expr, expr Pos.marked) Bindlib.binder

 type scope_body = {
--- a/compiler/lcalc/compile_with_exceptions.mli
+++ b/compiler/lcalc/compile_with_exceptions.mli
@ -12,6 +12,7 @@
   or implied. See the License for the specific language governing permissions and limitations under
   the License. *)

-(** Translation from the default calculus to the lambda calculus *)
+(** Translation from the default calculus to the lambda calculus. This translation uses exceptions
+    handle empty default terms. *)

 val translate_program : Dcalc.Ast.program -> Ast.program
--- a/compiler/lcalc/compile_without_exceptions.ml
+++ b/compiler/lcalc/compile_without_exceptions.ml
@ -0,0 +1,481 @@
+(* This file is part of the Catala compiler, a specification language for tax and social benefits
+   computation rules. Copyright (C) 2020-2022 Inria, contributor: Alain Delaët-Tixeuil
+   <alain.delaet--tixeuil@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
+   in compliance with the License. You may obtain a copy of the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software distributed under the License
+   is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
+   or implied. See the License for the specific language governing permissions and limitations under
+   the License. *)
+
+open Utils
+module D = Dcalc.Ast
+module A = Ast
+open Dcalc.Binded_representation
+
+(** The main idea around this pass is to compile Dcalc to Lcalc without using [raise EmptyError] nor
+    [try _ with EmptyError -> _]. To do so, we use the same technique as in rust or erlang to handle
+    this kind of exceptions. Each [raise EmptyError] will be translated as [None] and each
+    [try e1 with EmtpyError -> e2] as [match e1 with | None -> e2 | Some x -> x].
+
+    When doing this naively, this requires to add matches and Some constructor everywhere. We apply
+    here an other technique where we generate what we call `hoists`. Hoists are expression whom
+    could minimally [raise EmptyError]. For instance in
+    [let x = <e1, e2, ..., en| e_just :- e_cons> * 3 in x + 1], the sub-expression
+    [<e1, e2, ..., en| e_just :- e_cons>] can produce an empty error. So we make a hoist with a new
+    variable [y] linked to the Dcalc expression [<e1, e2, ..., en| e_just :- e_cons>], and we return
+    as the translated expression [let x = y * 3 in x + 1].
+
+    The compilation of expressions is found in the functions [translate_and_hoist ctx e] and
+    [translate_expr ctx e]. Every option-generating expression when calling [translate_and_hoist]
+    will be hoisted and later handled by the [translate_expr] function. Every other cases is found
+    in the translate_and_hoist function. *)
+
+type hoists = D.expr Pos.marked A.VarMap.t
+(** Hoists definition. It represent bindings between [A.Var.t] and [D.expr]. *)
+
+type info = { expr : A.expr Pos.marked Bindlib.box; var : A.expr Bindlib.var; is_pure : bool }
+(** Information about each encontered Dcalc variable is stored inside a context : what is the
+    corresponding LCalc variable; an expression corresponding to the variable build correctly using
+    Bindlib, and a boolean `is_pure` indicating whenever the variable can be an EmptyError and hence
+    should be matched (false) or if it never can be EmptyError (true). *)
+
+let pp_info (fmt : Format.formatter) (info : info) =
+  Format.fprintf fmt "{var: %a; is_pure: %b}" Print.format_var info.var info.is_pure
+
+type ctx = {
+  decl_ctx : D.decl_ctx;
+  vars : info D.VarMap.t;  (** information context about variables in the current scope *)
+}
+
+let _pp_ctx (fmt : Format.formatter) (ctx : ctx) =
+  let pp_binding (fmt : Format.formatter) ((v, info) : D.Var.t * info) =
+    Format.fprintf fmt "%a: %a" Dcalc.Print.format_var v pp_info info
+  in
+
+  let pp_bindings =
+    Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt "; ") pp_binding
+  in
+
+  Format.fprintf fmt "@[<2>[%a]@]" pp_bindings (D.VarMap.bindings ctx.vars)
+
+(** [find ~info n ctx] is a warpper to ocaml's Map.find that handle errors in a slightly better way. *)
+let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info =
+  (* let _ = Format.asprintf "Searching for variable %a inside context %a" Dcalc.Print.format_var n
+     pp_ctx ctx |> Cli.debug_print in *)
+  try D.VarMap.find n ctx.vars
+  with Not_found ->
+    Errors.raise_spanned_error
+      (Format.asprintf
+         "Internal Error: Variable %a was not found in the current environment. Additional \
+          informations : %s."
+         Dcalc.Print.format_var n info)
+      Pos.no_pos
+
+(** [add_var pos var is_pure ctx] add to the context [ctx] the Dcalc variable var, creating a unique
+    corresponding variable in Lcalc, with the corresponding expression, and the boolean is_pure. It
+    is usefull for debuging purposes as it printing each of the Dcalc/Lcalc variable pairs. *)
+let add_var (pos : Pos.t) (var : D.Var.t) (is_pure : bool) (ctx : ctx) : ctx =
+  let new_var = A.Var.make (Bindlib.name_of var, pos) in
+  let expr = A.make_var (new_var, pos) in
+
+  (* Cli.debug_print @@ Format.asprintf "D.%a |-> A.%a" Dcalc.Print.format_var var Print.format_var
+     new_var; *)
+  { ctx with vars = D.VarMap.update var (fun _ -> Some { expr; var = new_var; is_pure }) ctx.vars }
+
+(** [tau' = translate_typ tau] translate the a dcalc type into a lcalc type.
+
+    Since positions where there is thunked expressions is exactly where we will put option
+    expressions. Hence, the transformation simply reduce [unit -> 'a] into ['a option] recursivly.
+    There is no polymorphism inside catala. *)
+let rec translate_typ (tau : D.typ Pos.marked) : D.typ Pos.marked =
+  (Fun.flip Pos.same_pos_as) tau
+    begin
+      match Pos.unmark tau with
+      | D.TLit l -> D.TLit l
+      | D.TTuple (ts, s) -> D.TTuple (List.map translate_typ ts, s)
+      | D.TEnum (ts, en) -> D.TEnum (List.map translate_typ ts, en)
+      | D.TAny -> D.TAny
+      | D.TArray ts -> D.TArray (translate_typ ts)
+      (* catala is not polymorphic*)
+      | D.TArrow ((D.TLit D.TUnit, _), t2) ->
+          D.TEnum ([ translate_typ t2 ], A.option_enum) (* D.TAny *)
+      | D.TArrow (t1, t2) -> D.TArrow (translate_typ t1, translate_typ t2)
+    end
+
+let translate_lit (l : D.lit) (pos : Pos.t) : A.lit =
+  match l with
+  | D.LBool l -> A.LBool l
+  | D.LInt i -> A.LInt i
+  | D.LRat r -> A.LRat r
+  | D.LMoney m -> A.LMoney m
+  | D.LUnit -> A.LUnit
+  | D.LDate d -> A.LDate d
+  | D.LDuration d -> A.LDuration d
+  | D.LEmptyError ->
+      Errors.raise_spanned_error
+        "Internal Error: An empty error was found in a place that shouldn't be possible." pos
+
+(** [c = disjoint_union_maps cs] Compute the disjoint union of multiple maps. Raises an internal
+    error if there is two identicals keys in differnts parts. *)
+let disjoint_union_maps (pos : Pos.t) (cs : 'a A.VarMap.t list) : 'a A.VarMap.t =
+  let disjoint_union =
+    A.VarMap.union (fun _ _ _ ->
+        Errors.raise_spanned_error
+          "Internal Error: Two supposed to be disjoints maps have one shared key." pos)
+  in
+
+  List.fold_left disjoint_union A.VarMap.empty cs
+
+(** [e' = translate_and_hoist ctx e ] Translate the Dcalc expression e into an expression in Lcalc,
+    given we translate each hoists correctly. It ensures the equivalence between the execution of e
+    and the execution of e' are equivalent in an environement where each variable v, where (v, e_v)
+    is in hoists, has the non-empty value in e_v. *)
+let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
+    A.expr Pos.marked Bindlib.box * hoists =
+  let pos = Pos.get_position e in
+  match Pos.unmark e with
+  (* empty-producing/using terms. We hoist those. (D.EVar in some cases, EApp(D.EVar _, [ELit
+     LUnit]), EDefault _, ELit LEmptyDefault) I'm unsure about assert. *)
+  | D.EVar v ->
+      (* todo: for now, every unpure (such that [is_pure] is [false] in the current context) is
+         thunked, hence matched in the next case. This assumption can change in the future, and this
+         case is here for this reason. *)
+      let v, pos_v = v in
+      if not (find ~info:"search for a variable" v ctx).is_pure then
+        let v' = A.Var.make (Bindlib.name_of v, pos_v) in
+        (* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a, created a variable %a to
+           replace it" Dcalc.Print.format_var v Print.format_var v'; *)
+        (A.make_var (v', pos), A.VarMap.singleton v' e)
+      else ((find ~info:"should never happend" v ctx).expr, A.VarMap.empty)
+  | D.EApp ((D.EVar (v, pos_v), p), [ (D.ELit D.LUnit, _) ]) ->
+      if not (find ~info:"search for a variable" v ctx).is_pure then
+        let v' = A.Var.make (Bindlib.name_of v, pos_v) in
+        (* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a, created a variable %a to
+           replace it" Dcalc.Print.format_var v Print.format_var v'; *)
+        (A.make_var (v', pos), A.VarMap.singleton v' (D.EVar (v, pos_v), p))
+      else
+        Errors.raise_spanned_error
+          "Internal error: an pure variable was found in an unpure environment." pos
+  | D.EDefault (_exceptions, _just, _cons) ->
+      let v' = A.Var.make ("default_term", pos) in
+      (A.make_var (v', pos), A.VarMap.singleton v' e)
+  | D.ELit D.LEmptyError ->
+      let v' = A.Var.make ("empty_litteral", pos) in
+      (A.make_var (v', pos), A.VarMap.singleton v' e)
+  (* This one is a very special case. It transform an unpure expression environement to a pure
+     expression. *)
+  | ErrorOnEmpty arg ->
+      (* [ match arg with | None -> raise NoValueProvided | Some v -> {{ v }} ] *)
+      let silent_var = A.Var.make ("_", pos) in
+      let x = A.Var.make ("non_empty_argument", pos) in
+
+      let arg' = translate_expr ctx arg in
+
+      ( A.make_matchopt_with_abs_arms arg'
+          (A.make_abs [| silent_var |]
+             (Bindlib.box (A.ERaise A.NoValueProvided, pos))
+             pos [ (D.TAny, pos) ] pos)
+          (A.make_abs [| x |] (A.make_var (x, pos)) pos [ (D.TAny, pos) ] pos),
+        A.VarMap.empty )
+  (* pure terms *)
+  | D.ELit l -> (Bindlib.box (A.ELit (translate_lit l pos), pos), A.VarMap.empty)
+  | D.EIfThenElse (e1, e2, e3) ->
+      let e1', h1 = translate_and_hoist ctx e1 in
+      let e2', h2 = translate_and_hoist ctx e2 in
+      let e3', h3 = translate_and_hoist ctx e3 in
+
+      let e' =
+        Bindlib.box_apply3 (fun e1' e2' e3' -> (A.EIfThenElse (e1', e2', e3'), pos)) e1' e2' e3'
+      in
+
+      (*(* equivalent code : *) let e' = let+ e1' = e1' and+ e2' = e2' and+ e3' = e3' in
+        (A.EIfThenElse (e1', e2', e3'), pos) in *)
+      (e', disjoint_union_maps pos [ h1; h2; h3 ])
+  | D.EAssert e1 ->
+      (* same behavior as in the ICFP paper: if e1 is empty, then no error is raised. *)
+      let e1', h1 = translate_and_hoist ctx e1 in
+      (Bindlib.box_apply (fun e1' -> (A.EAssert e1', pos)) e1', h1)
+  | D.EAbs ((binder, pos_binder), ts) ->
+      let vars, body = Bindlib.unmbind binder in
+      let ctx, lc_vars =
+        ArrayLabels.fold_right vars ~init:(ctx, []) ~f:(fun var (ctx, lc_vars) ->
+            (* we suppose the invariant that when applying a function, its arguments cannot be of
+               the type "option".
+
+               The code should behave correctly in the without this assumption if we put here an
+               is_pure=false, but the types are more compilcated. (unimplemented for now) *)
+            let ctx = add_var pos var true ctx in
+            let lc_var = (find var ctx).var in
+            (ctx, lc_var :: lc_vars))
+      in
+      let lc_vars = Array.of_list lc_vars in
+
+      (* here we take the guess that if we cannot build the closure because one of the variable is
+         empty, then we cannot build the function. *)
+      let new_body, hoists = translate_and_hoist ctx body in
+      let new_binder = Bindlib.bind_mvar lc_vars new_body in
+
+      ( Bindlib.box_apply
+          (fun new_binder -> (A.EAbs ((new_binder, pos_binder), List.map translate_typ ts), pos))
+          new_binder,
+        hoists )
+  | EApp (e1, args) ->
+      let e1', h1 = translate_and_hoist ctx e1 in
+      let args', h_args = args |> List.map (translate_and_hoist ctx) |> List.split in
+
+      let hoists = disjoint_union_maps pos (h1 :: h_args) in
+      let e' =
+        Bindlib.box_apply2
+          (fun e1' args' -> (A.EApp (e1', args'), pos))
+          e1' (Bindlib.box_list args')
+      in
+      (e', hoists)
+  | ETuple (args, s) ->
+      let args', h_args = args |> List.map (translate_and_hoist ctx) |> List.split in
+
+      let hoists = disjoint_union_maps pos h_args in
+      (Bindlib.box_apply (fun args' -> (A.ETuple (args', s), pos)) (Bindlib.box_list args'), hoists)
+  | ETupleAccess (e1, i, s, ts) ->
+      let e1', hoists = translate_and_hoist ctx e1 in
+      let e1' = Bindlib.box_apply (fun e1' -> (A.ETupleAccess (e1', i, s, ts), pos)) e1' in
+      (e1', hoists)
+  | EInj (e1, i, en, ts) ->
+      let e1', hoists = translate_and_hoist ctx e1 in
+      let e1' = Bindlib.box_apply (fun e1' -> (A.EInj (e1', i, en, ts), pos)) e1' in
+      (e1', hoists)
+  | EMatch (e1, cases, en) ->
+      let e1', h1 = translate_and_hoist ctx e1 in
+      let cases', h_cases = cases |> List.map (translate_and_hoist ctx) |> List.split in
+
+      let hoists = disjoint_union_maps pos (h1 :: h_cases) in
+      let e' =
+        Bindlib.box_apply2
+          (fun e1' cases' -> (A.EMatch (e1', cases', en), pos))
+          e1' (Bindlib.box_list cases')
+      in
+      (e', hoists)
+  | EArray es ->
+      let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in
+
+      ( Bindlib.box_apply (fun es' -> (A.EArray es', pos)) (Bindlib.box_list es'),
+        disjoint_union_maps pos hoists )
+  | EOp op -> (Bindlib.box (A.EOp op, pos), A.VarMap.empty)
+
+and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Pos.marked) :
+    A.expr Pos.marked Bindlib.box =
+  let e', hoists = translate_and_hoist ctx e in
+  let hoists = A.VarMap.bindings hoists in
+
+  let _pos = Pos.get_position e in
+
+  (* build the hoists *)
+  (* Cli.debug_print @@ Format.asprintf "hoist for the expression: [%a]" (Format.pp_print_list
+     Print.format_var) (List.map fst hoists); *)
+  ListLabels.fold_left hoists
+    ~init:(if append_esome then A.make_some e' else e')
+    ~f:(fun acc (v, (hoist, pos_hoist)) ->
+      (* Cli.debug_print @@ Format.asprintf "hoist using A.%a" Print.format_var v; *)
+      let c' : A.expr Pos.marked Bindlib.box =
+        match hoist with
+        (* Here we have to handle only the cases appearing in hoists, as defined the
+           [translate_and_hoist] function. *)
+        | D.EVar v -> (find ~info:"should never happend" (Pos.unmark v) ctx).expr
+        | D.EDefault (excep, just, cons) ->
+            let excep' = List.map (translate_expr ctx) excep in
+            let just' = translate_expr ctx just in
+            let cons' = translate_expr ctx cons in
+            (* calls handle_option. *)
+            A.make_app
+              (A.make_var (A.handle_default_opt, pos_hoist))
+              [
+                Bindlib.box_apply
+                  (fun excep' -> (A.EArray excep', pos_hoist))
+                  (Bindlib.box_list excep');
+                just';
+                cons';
+              ]
+              pos_hoist
+        | D.ELit D.LEmptyError -> A.make_none pos_hoist
+        | D.EAssert arg ->
+            let arg' = translate_expr ctx arg in
+
+            (* [ match arg with | None -> raise NoValueProvided | Some v -> assert {{ v }} ] *)
+            let silent_var = A.Var.make ("_", pos_hoist) in
+            let x = A.Var.make ("assertion_argument", pos_hoist) in
+
+            A.make_matchopt_with_abs_arms arg'
+              (A.make_abs [| silent_var |]
+                 (Bindlib.box (A.ERaise A.NoValueProvided, pos_hoist))
+                 pos_hoist [ (D.TAny, pos_hoist) ] pos_hoist)
+              (A.make_abs [| x |]
+                 (Bindlib.box_apply
+                    (fun arg -> (A.EAssert arg, pos_hoist))
+                    (A.make_var (x, pos_hoist)))
+                 pos_hoist [ (D.TAny, pos_hoist) ] pos_hoist)
+        | _ ->
+            Errors.raise_spanned_error
+              "Internal Error: An term was found in a position where it should not be" pos_hoist
+      in
+
+      (* [ match {{ c' }} with | None -> None | Some {{ v }} -> {{ acc }} end ] *)
+      (* Cli.debug_print @@ Format.asprintf "build matchopt using %a" Print.format_var v; *)
+      A.make_matchopt pos_hoist v (D.TAny, pos_hoist) c' (A.make_none pos_hoist) acc)
+
+let rec translate_scope_let (ctx : ctx) (lets : scope_lets) =
+  match lets with
+  | Result e -> translate_expr ~append_esome:false ctx e
+  | ScopeLet
+      {
+        scope_let_kind = SubScopeVarDefinition;
+        scope_let_typ = typ;
+        scope_let_expr = D.EAbs ((binder, _), _), _pos;
+        scope_let_next = next;
+        scope_let_pos = pos;
+      } ->
+      (* special case : the subscope variable is thunked (context i/o). We remove this thunking. *)
+      let _, expr = Bindlib.unmbind binder in
+
+      let var_is_pure = true in
+      let var, next = Bindlib.unbind next in
+      (* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *)
+      let ctx' = add_var pos var var_is_pure ctx in
+      let new_var = (find ~info:"variable that was just created" var ctx').var in
+      A.make_let_in new_var (translate_typ typ)
+        (translate_expr ctx ~append_esome:false expr)
+        (translate_scope_let ctx' next)
+  | ScopeLet
+      {
+        scope_let_kind = SubScopeVarDefinition;
+        scope_let_typ = typ;
+        scope_let_expr = (D.ErrorOnEmpty _, _) as expr;
+        scope_let_next = next;
+        scope_let_pos = pos;
+      } ->
+      (* special case: regular input to the subscope *)
+      let var_is_pure = true in
+      let var, next = Bindlib.unbind next in
+      (* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *)
+      let ctx' = add_var pos var var_is_pure ctx in
+      let new_var = (find ~info:"variable that was just created" var ctx').var in
+      A.make_let_in new_var (translate_typ typ)
+        (translate_expr ctx ~append_esome:false expr)
+        (translate_scope_let ctx' next)
+  | ScopeLet
+      { scope_let_kind = SubScopeVarDefinition; scope_let_pos = pos; scope_let_expr = expr; _ } ->
+      Errors.raise_spanned_error
+        (Format.asprintf
+           "Internal Error: found an SubScopeVarDefinition that does not satisfy the invariants \
+            when translating Dcalc to Lcalc without exceptions: @[<hov 2>%a@]"
+           (Dcalc.Print.format_expr ctx.decl_ctx)
+           expr)
+        pos
+  | ScopeLet
+      {
+        scope_let_kind = kind;
+        scope_let_typ = typ;
+        scope_let_expr = expr;
+        scope_let_next = next;
+        scope_let_pos = pos;
+      } ->
+      let var_is_pure =
+        match kind with
+        | DestructuringInputStruct -> (
+            (* Here, we have to distinguish between context and input variables. We can do so by
+               looking at the typ of the destructuring: if it's thunked, then the variable is
+               context. If it's not thunked, it's a regular input. *)
+            match Pos.unmark typ with D.TArrow ((D.TLit D.TUnit, _), _) -> false | _ -> true)
+        | ScopeVarDefinition | SubScopeVarDefinition | CallingSubScope
+        | DestructuringSubScopeResults | Assertion ->
+            true
+      in
+      let var, next = Bindlib.unbind next in
+      (* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *)
+      let ctx' = add_var pos var var_is_pure ctx in
+      let new_var = (find ~info:"variable that was just created" var ctx').var in
+      A.make_let_in new_var (translate_typ typ)
+        (translate_expr ctx ~append_esome:false expr)
+        (translate_scope_let ctx' next)
+
+let translate_scope_body (scope_pos : Pos.t) (ctx : ctx) (body : scope_body) :
+    A.expr Pos.marked Bindlib.box =
+  match body with
+  | {
+   scope_body_result = result;
+   scope_body_input_struct = input_struct;
+   scope_body_output_struct = _output_struct;
+  } ->
+      let v, lets = Bindlib.unbind result in
+      let ctx' = add_var scope_pos v true ctx in
+      let v' = (find ~info:"variable that was just created" v ctx').var in
+
+      A.make_abs [| v' |] (translate_scope_let ctx' lets) Pos.no_pos
+        [ (D.TTuple ([], Some input_struct), Pos.no_pos) ]
+        Pos.no_pos
+
+let rec translate_scopes (ctx : ctx) (scopes : scopes) : Ast.scope_body list Bindlib.box =
+  match scopes with
+  | Nil -> Bindlib.box []
+  | ScopeDef { scope_name; scope_body; scope_next } ->
+      let scope_var, next = Bindlib.unbind scope_next in
+      let new_ctx = add_var Pos.no_pos scope_var true ctx in
+      let new_scope_name = (find ~info:"variable that was just created" scope_var new_ctx).var in
+
+      let scope_pos = Pos.get_position (D.ScopeName.get_info scope_name) in
+
+      let new_body = translate_scope_body scope_pos ctx scope_body in
+      let tail = translate_scopes new_ctx next in
+
+      Bindlib.box_apply2
+        (fun body tail ->
+          {
+            Ast.scope_body_var = new_scope_name;
+            scope_body_name = scope_name;
+            scope_body_expr = body;
+          }
+          :: tail)
+        new_body tail
+
+let translate_scopes (ctx : ctx) (scopes : scopes) : Ast.scope_body list =
+  Bindlib.unbox (translate_scopes ctx scopes)
+
+let translate_program (prgm : D.program) : A.program =
+  let inputs_structs =
+    ListLabels.fold_left prgm.scopes ~init:[] ~f:(fun acc (_, _, body) ->
+        body.D.scope_body_input_struct :: acc)
+  in
+
+  (* Cli.debug_print @@ Format.asprintf "List of structs to modify: [%a]" (Format.pp_print_list
+     D.StructName.format_t) inputs_structs; *)
+  let decl_ctx =
+    {
+      prgm.decl_ctx with
+      D.ctx_enums = prgm.decl_ctx.ctx_enums |> D.EnumMap.add A.option_enum A.option_enum_config;
+    }
+  in
+  let decl_ctx =
+    {
+      decl_ctx with
+      D.ctx_structs =
+        prgm.decl_ctx.ctx_structs
+        |> D.StructMap.mapi (fun n l ->
+               if List.mem n inputs_structs then
+                 ListLabels.map l ~f:(fun (n, tau) ->
+                     (* Cli.debug_print @@ Format.asprintf "Input type: %a" (Dcalc.Print.format_typ
+                        decl_ctx) tau; Cli.debug_print @@ Format.asprintf "Output type: %a"
+                        (Dcalc.Print.format_typ decl_ctx) (translate_typ tau); *)
+                     (n, translate_typ tau))
+               else l);
+    }
+  in
+
+  let scopes =
+    prgm.scopes |> bind_scopes |> Bindlib.unbox
+    |> translate_scopes { decl_ctx; vars = D.VarMap.empty }
+  in
+
+  { scopes; decl_ctx }
--- a/compiler/lcalc/compile_without_exceptions.mli
+++ b/compiler/lcalc/compile_without_exceptions.mli
@ -0,0 +1,19 @@
+(* This file is part of the Catala compiler, a specification language for tax and social benefits
+   computation rules. Copyright (C) 2020-2022 Inria, contributor: Alain Delaët-Tixeuil
+   <alain.delaet--tixeuil@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
+   in compliance with the License. You may obtain a copy of the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software distributed under the License
+   is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
+   or implied. See the License for the specific language governing permissions and limitations under
+   the License. *)
+
+(** Translation from the default calculus to the lambda calculus. This translation uses an option
+    monad to handle empty defaults terms. This transformation is one piece to permit to compile
+    toward legacy languages that does not contains exceptions. *)
+
+val translate_program : Dcalc.Ast.program -> Ast.program
--- a/compiler/lcalc/dune
+++ b/compiler/lcalc/dune
@ -1,7 +1,9 @@
 (library
 (name lcalc)
 (public_name catala.lcalc)
- (libraries bindlib dcalc scopelang runtime))
+ (libraries bindlib dcalc scopelang runtime)
+ (preprocess
+  (pps visitors.ppx)))

 (documentation
 (package catala)
--- a/compiler/lcalc/optimizations.ml
+++ b/compiler/lcalc/optimizations.ml
@ -14,58 +14,124 @@
 open Utils
 open Ast

-let rec peephole_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
+let ( let+ ) x f = Bindlib.box_apply f x
+
+let ( and+ ) x y = Bindlib.box_pair x y
+
+let visitor_map (t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box) (ctx : 'a)
+    (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
+  (* calls [t ctx] on every direct childs of [e], then rebuild an abstract syntax tree modified.
+     Used in other transformations. *)
+  let default_mark e' = Pos.same_pos_as e' e in
  match Pos.unmark e with
-  | EVar (v, pos) -> Bindlib.box_apply (fun v -> (v, pos)) (Bindlib.box_var v)
+  | EVar (v, pos) ->
+      let+ v = Bindlib.box_var v in
+      (v, pos)
  | ETuple (args, n) ->
-      Bindlib.box_apply
-        (fun args -> (ETuple (args, n), Pos.get_position e))
-        (Bindlib.box_list (List.map peephole_expr args))
+      let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
+      default_mark @@ ETuple (args, n)
  | ETupleAccess (e1, i, n, ts) ->
-      Bindlib.box_apply
-        (fun e1 -> (ETupleAccess (e1, i, n, ts), Pos.get_position e))
-        (peephole_expr e1)
+      let+ e1 = t ctx e1 in
+      default_mark @@ ETupleAccess (e1, i, n, ts)
  | EInj (e1, i, n, ts) ->
-      Bindlib.box_apply (fun e1 -> (EInj (e1, i, n, ts), Pos.get_position e)) (peephole_expr e1)
+      let+ e1 = t ctx e1 in
+      default_mark @@ EInj (e1, i, n, ts)
  | EMatch (arg, cases, n) ->
-      Bindlib.box_apply2
-        (fun arg cases -> (EMatch (arg, cases, n), Pos.get_position e))
-        (peephole_expr arg)
-        (Bindlib.box_list (List.map peephole_expr cases))
+      let+ arg = t ctx arg and+ cases = cases |> List.map (t ctx) |> Bindlib.box_list in
+      default_mark @@ EMatch (arg, cases, n)
  | EArray args ->
-      Bindlib.box_apply
-        (fun args -> (EArray args, Pos.get_position e))
-        (Bindlib.box_list (List.map peephole_expr args))
+      let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
+      default_mark @@ EArray args
  | EAbs ((binder, pos_binder), ts) ->
      let vars, body = Bindlib.unmbind binder in
-      let body = peephole_expr body in
-      Bindlib.box_apply
-        (fun binder -> (EAbs ((binder, pos_binder), ts), Pos.get_position e))
-        (Bindlib.bind_mvar vars body)
+      let body = t ctx body in
+      let+ binder = Bindlib.bind_mvar vars body in
+      default_mark @@ EAbs ((binder, pos_binder), ts)
  | EApp (e1, args) ->
-      Bindlib.box_apply2
-        (fun e1 args -> (EApp (e1, args), Pos.get_position e))
-        (peephole_expr e1)
-        (Bindlib.box_list (List.map peephole_expr args))
-  | EAssert e1 -> Bindlib.box_apply (fun e1 -> (EAssert e1, Pos.get_position e)) (peephole_expr e1)
+      let+ e1 = t ctx e1 and+ args = args |> List.map (t ctx) |> Bindlib.box_list in
+      default_mark @@ EApp (e1, args)
+  | EAssert e1 ->
+      let+ e1 = t ctx e1 in
+      default_mark @@ EAssert e1
  | EIfThenElse (e1, e2, e3) ->
-      Bindlib.box_apply3
-        (fun e1 e2 e3 ->
-          match Pos.unmark e1 with
-          | ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]) -> e2
-          | ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) -> e3
-          | _ -> (EIfThenElse (e1, e2, e3), Pos.get_position e))
-        (peephole_expr e1) (peephole_expr e2) (peephole_expr e3)
+      let+ e1 = t ctx e1 and+ e2 = t ctx e2 and+ e3 = t ctx e3 in
+      default_mark @@ EIfThenElse (e1, e2, e3)
  | ECatch (e1, exn, e2) ->
-      Bindlib.box_apply2
-        (fun e1 e2 ->
-          ( (match Pos.unmark e2 with
-            | ERaise exn2 when exn2 = exn -> Pos.unmark e1
-            | _ -> ECatch (e1, exn, e2)),
-            Pos.get_position e ))
-        (peephole_expr e1) (peephole_expr e2)
+      let+ e1 = t ctx e1 and+ e2 = t ctx e2 in
+      default_mark @@ ECatch (e1, exn, e2)
  | ERaise _ | ELit _ | EOp _ -> Bindlib.box e

+let rec iota_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
+  let default_mark e' = Pos.mark (Pos.get_position e) e' in
+  match Pos.unmark e with
+  | EMatch ((EInj (e1, i, n', _ts), _), cases, n) when Dcalc.Ast.EnumName.compare n n' = 0 ->
+      let+ e1 = visitor_map iota_expr () e1
+      and+ case = visitor_map iota_expr () (List.nth cases i) in
+      default_mark @@ EApp (case, [ e1 ])
+  | EMatch (e', cases, n)
+    when cases
+         |> List.mapi (fun i (case, _pos) ->
+                match case with
+                | EInj (_ei, i', n', _ts') ->
+                    i = i' && (* n = n' *) Dcalc.Ast.EnumName.compare n n' = 0
+                | _ -> false)
+         |> List.for_all Fun.id ->
+      visitor_map iota_expr () e'
+  | _ -> visitor_map iota_expr () e
+
+let rec beta_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
+  let default_mark e' = Pos.same_pos_as e' e in
+  match Pos.unmark e with
+  | EApp (e1, args) -> (
+      let+ e1 = beta_expr () e1 and+ args = List.map (beta_expr ()) args |> Bindlib.box_list in
+      match Pos.unmark e1 with
+      | EAbs ((binder, _pos_binder), _ts) ->
+          let (_ : (_, _) Bindlib.mbinder) = binder in
+          Bindlib.msubst binder (List.map fst args |> Array.of_list)
+      | _ -> default_mark @@ EApp (e1, args))
+  | _ -> visitor_map beta_expr () e
+
+let iota_optimizations (p : program) : program =
+  {
+    p with
+    scopes =
+      List.map
+        (fun scope_body ->
+          {
+            scope_body with
+            scope_body_expr = Bindlib.unbox (iota_expr () scope_body.scope_body_expr);
+          })
+        p.scopes;
+  }
+
+(* TODO: beta optimizations apply inlining of the program. We left the inclusion of
+   beta-optimization as future work since its produce code that is harder to read, and can produce
+   exponential blowup of the size of the generated program. *)
+let _beta_optimizations (p : program) : program =
+  {
+    p with
+    scopes =
+      List.map
+        (fun scope_body ->
+          {
+            scope_body with
+            scope_body_expr = Bindlib.unbox (beta_expr () scope_body.scope_body_expr);
+          })
+        p.scopes;
+  }
+
+let rec peephole_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
+  let default_mark e' = Pos.mark (Pos.get_position e) e' in
+
+  match Pos.unmark e with
+  | EIfThenElse (e1, e2, e3) -> (
+      let+ e1 = peephole_expr () e1 and+ e2 = peephole_expr () e2 and+ e3 = peephole_expr () e3 in
+      match Pos.unmark e1 with
+      | ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]) -> e2
+      | ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) -> e3
+      | _ -> default_mark @@ EIfThenElse (e1, e2, e3))
+  | _ -> visitor_map peephole_expr () e
+
 let peephole_optimizations (p : program) : program =
  {
    p with
@ -74,9 +140,9 @@ let peephole_optimizations (p : program) : program =
        (fun scope_body ->
          {
            scope_body with
-            scope_body_expr = Bindlib.unbox (peephole_expr scope_body.scope_body_expr);
+            scope_body_expr = Bindlib.unbox (peephole_expr () scope_body.scope_body_expr);
          })
        p.scopes;
  }

-let optimize_program (p : program) : program = peephole_optimizations p
+let optimize_program (p : program) : program = p |> iota_optimizations |> peephole_optimizations
--- a/compiler/lcalc/print.ml
+++ b/compiler/lcalc/print.ml
@ -63,7 +63,7 @@ let needs_parens (e : expr Pos.marked) : bool =
  match Pos.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false

 let format_var (fmt : Format.formatter) (v : Var.t) : unit =
-  Format.fprintf fmt "%s" (Bindlib.name_of v)
+  Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)

 let rec format_expr (ctx : Dcalc.Ast.decl_ctx) ?(debug : bool = false) (fmt : Format.formatter)
    (e : expr Pos.marked) : unit =
@ -111,7 +111,7 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) ?(debug : bool = false) (fmt : Fo
        (fst (List.nth (Dcalc.Ast.EnumMap.find en ctx.ctx_enums) n))
        format_expr e
  | EMatch (e, es, e_name) ->
-      Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]" format_keyword "match" format_expr e
+      Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@]" format_keyword "match" format_expr e
        format_keyword "with"
        (Format.pp_print_list
           ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
--- a/compiler/lcalc/to_ocaml.ml
+++ b/compiler/lcalc/to_ocaml.ml
@ -17,6 +17,26 @@ open Ast
 open Backends
 module D = Dcalc.Ast

+let find_struct (s : D.StructName.t) (ctx : D.decl_ctx) :
+    (D.StructFieldName.t * D.typ Pos.marked) list =
+  try D.StructMap.find s ctx.D.ctx_structs
+  with Not_found ->
+    let s_name, pos = D.StructName.get_info s in
+    Errors.raise_spanned_error
+      (Format.asprintf "Internal Error: Structure %s was not found in the current environment."
+         s_name)
+      pos
+
+let find_enum (en : D.EnumName.t) (ctx : D.decl_ctx) : (D.EnumConstructor.t * D.typ Pos.marked) list
+    =
+  try D.EnumMap.find en ctx.D.ctx_enums
+  with Not_found ->
+    let en_name, pos = D.EnumName.get_info en in
+    Errors.raise_spanned_error
+      (Format.asprintf "Internal Error: Enumeration %s was not found in the current environment."
+         en_name)
+      pos
+
 let format_lit (fmt : Format.formatter) (l : lit Pos.marked) : unit =
  match Pos.unmark l with
  | LBool b -> Dcalc.Print.format_lit fmt (Pos.same_pos_as (Dcalc.Ast.LBool b) l)
@ -41,14 +61,6 @@ let format_op_kind (fmt : Format.formatter) (k : Dcalc.Ast.op_kind) =
  Format.fprintf fmt "%s"
    (match k with KInt -> "!" | KRat -> "&" | KMoney -> "$" | KDate -> "@" | KDuration -> "^")

-let format_log_entry (fmt : Format.formatter) (entry : Dcalc.Ast.log_entry) : unit =
-  Format.fprintf fmt "%s"
-    (match entry with
-    | VarDef _ -> ":="
-    | BeginCall -> "→ "
-    | EndCall -> "← "
-    | PosRecordIfTrueBool -> "☛ ")
-
 let format_binop (fmt : Format.formatter) (op : Dcalc.Ast.binop Pos.marked) : unit =
  match Pos.unmark op with
  | Add k -> Format.fprintf fmt "+%a" format_op_kind k
@ -88,9 +100,10 @@ let format_unop (fmt : Format.formatter) (op : Dcalc.Ast.unop Pos.marked) : unit
  match Pos.unmark op with
  | Minus k -> Format.fprintf fmt "~-%a" format_op_kind k
  | Not -> Format.fprintf fmt "%s" "not"
-  | Log (entry, infos) ->
-      Format.fprintf fmt "@[<hov 2>log_entry@ \"%a|%a\"@]" format_log_entry entry format_uid_list
-        infos
+  | Log (_entry, _infos) ->
+      Errors.raise_spanned_error
+        "Internal error: a log operator has not been caught by the expression match"
+        (Pos.get_position op)
  | Length -> Format.fprintf fmt "%s" "array_length"
  | IntToRat -> Format.fprintf fmt "%s" "decimal_of_integer"
  | GetDay -> Format.fprintf fmt "%s" "day_of_month_of_date"
@ -158,10 +171,16 @@ let rec format_typ (fmt : Format.formatter) (typ : Dcalc.Ast.typ Pos.marked) : u
      Format.fprintf fmt "@[<hov 2>(%a)@]"
        (Format.pp_print_list
           ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ *@ ")
-           (fun fmt t -> Format.fprintf fmt "%a" format_typ_with_parens t))
+           format_typ_with_parens)
        ts
  | TTuple (_, Some s) -> Format.fprintf fmt "%a" format_struct_name s
-  | TEnum (_, e) -> Format.fprintf fmt "%a" format_enum_name e
+  | TEnum ([ t ], e) when D.EnumName.compare e Ast.option_enum = 0 ->
+      Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t format_enum_name e
+  | TEnum (_, e) when D.EnumName.compare e Ast.option_enum = 0 ->
+      Errors.raise_spanned_error
+        "Internal Error: found an typing parameter for an eoption type of the wrong lenght."
+        (Pos.get_position typ)
+  | TEnum (_ts, e) -> Format.fprintf fmt "%a" format_enum_name e
  | TArrow (t1, t2) ->
      Format.fprintf fmt "@[<hov 2>%a ->@ %a@]" format_typ_with_parens t1 format_typ_with_parens t2
  | TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ_with_parens t1
@ -173,8 +192,10 @@ let format_var (fmt : Format.formatter) (v : Var.t) : unit =
    Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\\.") ~subst:(fun _ -> "_dot_") lowercase_name
  in
  let lowercase_name = avoid_keywords (to_ascii lowercase_name) in
-  if lowercase_name = "handle_default" || Dcalc.Print.begins_with_uppercase (Bindlib.name_of v) then
-    Format.fprintf fmt "%s" lowercase_name
+  if
+    List.mem lowercase_name [ "handle_default"; "handle_default_opt" ]
+    || Dcalc.Print.begins_with_uppercase (Bindlib.name_of v)
+  then Format.fprintf fmt "%s" lowercase_name
  else if lowercase_name = "_" then Format.fprintf fmt "%s" lowercase_name
  else Format.fprintf fmt "%s_" lowercase_name

@ -220,7 +241,7 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
             (fun fmt (e, struct_field) ->
               Format.fprintf fmt "@[<hov 2>%a =@ %a@]" format_struct_field_name struct_field
                 format_with_parens e))
-          (List.combine es (List.map fst (Dcalc.Ast.StructMap.find s ctx.ctx_structs)))
+          (List.combine es (List.map fst (find_struct s ctx)))
  | EArray es ->
      Format.fprintf fmt "@[<hov 2>[|%a|]@]"
        (Format.pp_print_list
@ -238,10 +259,10 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
            format_with_parens e1
      | Some s ->
          Format.fprintf fmt "%a.%a" format_with_parens e1 format_struct_field_name
-            (fst (List.nth (Dcalc.Ast.StructMap.find s ctx.ctx_structs) n)))
+            (fst (List.nth (find_struct s ctx) n)))
  | EInj (e, n, en, _ts) ->
      Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_enum_cons_name
-        (fst (List.nth (Dcalc.Ast.EnumMap.find en ctx.ctx_enums) n))
+        (fst (List.nth (find_enum en ctx) n))
        format_with_parens e
  | EMatch (e, es, e_name) ->
      Format.fprintf fmt "@[<hov 2>match@ %a@]@ with@\n%a" format_with_parens e
@ -261,13 +282,13 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
                 | _ -> assert false
                 (* should not happen *))
               e))
-        (List.combine es (List.map fst (Dcalc.Ast.EnumMap.find e_name ctx.ctx_enums)))
+        (List.combine es (List.map fst (find_enum e_name ctx)))
  | ELit l -> Format.fprintf fmt "%a" format_lit (Pos.same_pos_as l e)
  | EApp ((EAbs ((binder, _), taus), _), args) ->
      let xs, body = Bindlib.unmbind binder in
      let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
      let xs_tau_arg = List.map2 (fun (x, tau) arg -> (x, tau, arg)) xs_tau args in
-      Format.fprintf fmt "%a%a"
+      Format.fprintf fmt "(%a%a)"
        (Format.pp_print_list
           ~pp_sep:(fun fmt () -> Format.fprintf fmt "")
           (fun fmt (x, tau, arg) ->
@ -410,11 +431,9 @@ let format_ctx (type_ordering : Scopelang.Dependency.TVertex.t list) (fmt : Form
    (fun struct_or_enum ->
      match struct_or_enum with
      | Scopelang.Dependency.TVertex.Struct s ->
-          Format.fprintf fmt "%a@\n@\n" format_struct_decl
-            (s, Dcalc.Ast.StructMap.find s ctx.Dcalc.Ast.ctx_structs)
+          Format.fprintf fmt "%a@\n@\n" format_struct_decl (s, find_struct s ctx)
      | Scopelang.Dependency.TVertex.Enum e ->
-          Format.fprintf fmt "%a@\n@\n" format_enum_decl
-            (e, Dcalc.Ast.EnumMap.find e ctx.Dcalc.Ast.ctx_enums))
+          Format.fprintf fmt "%a@\n@\n" format_enum_decl (e, find_enum e ctx))
    (type_ordering @ scope_structs)

 let format_program (fmt : Format.formatter) (p : Ast.program)
--- a/compiler/runtime.ml
+++ b/compiler/runtime.ml
@ -31,6 +31,8 @@ type source_position = {
  law_headings : string list;
 }

+type 'a eoption = ENone of unit | ESome of 'a
+
 exception EmptyError

 exception AssertionFailed
@ -213,6 +215,21 @@ let handle_default : 'a. (unit -> 'a) array -> (unit -> bool) -> (unit -> 'a) ->
  in
  match except with Some x -> x | None -> if just () then cons () else raise EmptyError

+let handle_default_opt (exceptions : 'a eoption array) (just : bool eoption) (cons : 'a eoption) :
+    'a eoption =
+  let except =
+    Array.fold_left
+      (fun acc except ->
+        match (acc, except) with
+        | ENone _, _ -> except
+        | ESome _, ENone _ -> acc
+        | ESome _, ESome _ -> raise ConflictError)
+      (ENone ()) exceptions
+  in
+  match except with
+  | ESome _ -> except
+  | ENone _ -> ( match just with ESome b -> if b then cons else ENone () | ENone _ -> ENone ())
+
 let no_input : unit -> 'a = fun _ -> raise EmptyError

 let ( *$ ) (i1 : money) (i2 : decimal) : money =
--- a/compiler/runtime.mli
+++ b/compiler/runtime.mli
@ -33,6 +33,8 @@ type source_position = {
  law_headings : string list;
 }

+type 'a eoption = ENone of unit | ESome of 'a
+
 (** {1 Exceptions} *)

 exception EmptyError
@ -173,6 +175,9 @@ val handle_default : (unit -> 'a) array -> (unit -> bool) -> (unit -> 'a) -> 'a
 (** @raise EmptyError
    @raise ConflictError *)

+val handle_default_opt : 'a eoption array -> bool eoption -> 'a eoption -> 'a eoption
+(** @raise ConflictError *)
+
 val no_input : unit -> 'a

 (**{1 Operators} *)
--- a/compiler/scopelang/scope_to_dcalc.ml
+++ b/compiler/scopelang/scope_to_dcalc.ml
@ -530,7 +530,14 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
              (Dcalc.Ast.Var.make ("_", Pos.get_position e), Pos.get_position e);
            Dcalc.Ast.scope_let_typ = (Dcalc.Ast.TLit TUnit, Pos.get_position e);
            Dcalc.Ast.scope_let_expr =
-              Bindlib.box_apply (fun new_e -> Pos.same_pos_as (Dcalc.Ast.EAssert new_e) e) new_e;
+              (* To ensure that we throw an error if the value is not defined, we add an check
+                 "ErrorOnEmpty" here. *)
+              Bindlib.box_apply
+                (fun new_e ->
+                  Pos.same_pos_as
+                    (Dcalc.Ast.EAssert (Dcalc.Ast.ErrorOnEmpty new_e, Pos.get_position e))
+                    e)
+                new_e;
            Dcalc.Ast.scope_let_kind = Dcalc.Ast.Assertion;
          };
        ],
--- a/compiler/utils/cli.ml
+++ b/compiler/utils/cli.ml
@ -36,6 +36,8 @@ let optimize_flag = ref false

 let disable_counterexamples = ref false

+let avoid_exceptions_flag = ref false
+
 open Cmdliner

 let file =
@ -61,6 +63,11 @@ let trace_opt =
          "Displays a trace of the interpreter's computation or generates logging instructions in \
           translate programs.")

+let avoid_exceptions =
+  Arg.(
+    value & flag
+    & info [ "avoid_exceptions" ] ~doc:"Compiles the default calculus without exceptions")
+
 let wrap_weaved_output =
  Arg.(
    value & flag
@ -126,7 +133,7 @@ let output =

 let catala_t f =
  Term.(
-    const f $ file $ debug $ unstyled $ wrap_weaved_output $ backend $ language
+    const f $ file $ debug $ unstyled $ wrap_weaved_output $ avoid_exceptions $ backend $ language
    $ max_prec_digits_opt $ trace_opt $ disable_counterexamples_opt $ optimize $ ex_scope $ output)

 let version = "0.5.0"
@ -190,8 +197,8 @@ let info =
      `P "Please file bug reports at https://github.com/CatalaLang/catala/issues";
    ]
  in
-  let exits = Cmd.Exit.defaults @ [ Cmd.Exit.info ~doc:"on error." 1 ] in
-  Cmd.info "catala" ~version ~doc ~exits ~man
+  let exits = Term.default_exits @ [ Term.exit_info ~doc:"on error." 1 ] in
+  Term.info "catala" ~version ~doc ~exits ~man

 (**{1 Terminal formatting}*)

--- a/compiler/utils/cli.mli
+++ b/compiler/utils/cli.mli
@ -38,6 +38,9 @@ val trace_flag : bool ref
 val disable_counterexamples : bool ref
 (** Disables model-generated counterexamples for proofs that fail. *)

+val avoid_exceptions_flag : bool ref
+(** Avoids using [try ... with] exceptions when compiling the default calculus. *)
+
 (** {2 CLI terms} *)

 val file : string Cmdliner.Term.t
@ -79,6 +82,7 @@ val catala_t :
  bool ->
  bool ->
  bool ->
+  bool ->
  string ->
  string option ->
  int option ->
@ -90,11 +94,11 @@ val catala_t :
  'a) ->
  'a Cmdliner.Term.t
 (** Main entry point:
-    [catala_t file debug unstyled wrap_weaved_output backend language max_prec_digits_opt trace_opt disable_counterexamples optimize ex_scope output] *)
+    [catala_t file debug unstyled wrap_weaved_output avoid_exceptions backend language max_prec_digits_opt trace_opt disable_counterexamples optimize ex_scope output] *)

 val version : string

-val info : Cmdliner.Cmd.info
+val info : Cmdliner.Term.info

 (**{1 Terminal formatting}*)

--- a/compiler/utils/pos.ml
+++ b/compiler/utils/pos.ml
@ -175,6 +175,8 @@ let no_pos : t =
  in
  { code_pos = (zero_pos, zero_pos); law_pos = [] }

+let mark pos e : 'a marked = (e, pos)
+
 let unmark ((x, _) : 'a marked) : 'a = x

 let get_position ((_, x) : 'a marked) : t = x
--- a/compiler/utils/pos.mli
+++ b/compiler/utils/pos.mli
@ -64,6 +64,8 @@ type 'a marked = 'a * t
 val no_pos : t
 (** Placeholder position *)

+val mark : t -> 'a -> 'a marked
+
 val unmark : 'a marked -> 'a

 val get_position : 'a marked -> t
--- a/compiler/verification/z3backend.ml
+++ b/compiler/verification/z3backend.ml
@ -41,8 +41,11 @@ type context = {
  (* A map from Catala temporary variables, generated when translating a match, to the corresponding
     enum accessor call as a Z3 expression *)
  ctx_z3structs : Sort.sort StructMap.t;
-      (* A map from Catala struct names to the corresponding Z3 sort, from which we can retrieve the
-         constructor and the accessors *)
+  (* A map from Catala struct names to the corresponding Z3 sort, from which we can retrieve the
+     constructor and the accessors *)
+  ctx_z3unit : Sort.sort * Expr.expr;
+      (* A pair containing the Z3 encodings of the unit type, encoded as a tuple of 0 elements, and
+         the unit value *)
 }
 (** The context contains all the required information to encode a VC represented as a Catala term to
    Z3. The fields [ctx_decl] and [ctx_var] are computed before starting the translation to Z3, and
@ -108,9 +111,11 @@ let rec print_z3model_expr (ctx : context) (ty : typ Pos.marked) (e : Expr.expr)
    match ty with
    (* TODO: Print boolean according to current language *)
    | TBool -> Expr.to_string e
-    | TUnit -> failwith "[Z3 model]: Pretty-printing of unit literals not supported"
+    (* TUnit is only used for the absence of an enum constructor argument. Hence, when
+       pretty-printing, we print nothing to remain closer from Catala sources *)
+    | TUnit -> ""
    | TInt -> Expr.to_string e
-    | TRat -> failwith "[Z3 model]: Pretty-printing of rational literals not supported"
+    | TRat -> Arithmetic.Real.to_decimal_string e !Cli.max_prec_digits
    (* TODO: Print the right money symbol according to language *)
    | TMoney ->
        let z3_str = Expr.to_string e in
@ -173,29 +178,42 @@ let print_model (ctx : context) (model : Model.model) : string =
    (Format.pp_print_list
       ~pp_sep:(fun fmt () -> Format.fprintf fmt "\n")
       (fun fmt d ->
-         match Model.get_const_interp model d with
-         (* TODO: Better handling of this case *)
-         | None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
-         (* Prints "name : value\n" *)
-         | Some e ->
-             if FuncDecl.get_arity d = 0 then
-               (* Constant case *)
+         if FuncDecl.get_arity d = 0 then
+           (* Constant case *)
+           match Model.get_const_interp model d with
+           (* TODO: Better handling of this case *)
+           | None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
+           (* Print "name : value\n" *)
+           | Some e ->
               let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
               let v = StringMap.find symbol_name ctx.ctx_z3vars in
               Format.fprintf fmt "%s %s : %s"
                 (Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
                 (Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
                 (print_z3model_expr ctx (VarMap.find v ctx.ctx_var) e)
-             else failwith "[Z3 model]: Printing of functions is not yet supported"))
+         else
+           (* Declaration d is a function *)
+           match Model.get_func_interp model d with
+           (* TODO: Better handling of this case *)
+           | None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
+           (* Print "name : value\n" *)
+           | Some f ->
+               let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
+               let v = StringMap.find symbol_name ctx.ctx_z3vars in
+               Format.fprintf fmt "%s %s : %s"
+                 (Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
+                 (Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
+                 (* TODO: Model of a Z3 function should be pretty-printed *)
+                 (Model.FuncInterp.to_string f)))
    decls

 (** [translate_typ_lit] returns the Z3 sort corresponding to the Catala literal type [t] **)
 let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort =
  match t with
  | TBool -> Boolean.mk_sort ctx.ctx_z3
-  | TUnit -> failwith "[Z3 encoding] TUnit type not supported"
+  | TUnit -> fst ctx.ctx_z3unit
  | TInt -> Arithmetic.Integer.mk_sort ctx.ctx_z3
-  | TRat -> failwith "[Z3 encoding] TRat type not supported"
+  | TRat -> Arithmetic.Real.mk_sort ctx.ctx_z3
  | TMoney -> Arithmetic.Integer.mk_sort ctx.ctx_z3
  (* Dates are encoded as integers, corresponding to the number of days since Jan 1, 1900 *)
  | TDate -> Arithmetic.Integer.mk_sort ctx.ctx_z3
@ -284,7 +302,7 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr =
  | LBool b -> if b then Boolean.mk_true ctx.ctx_z3 else Boolean.mk_false ctx.ctx_z3
  | LEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
  | LInt n -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.integer_to_int n)
-  | LRat _ -> failwith "[Z3 encoding] LRat literals not supported"
+  | LRat r -> Arithmetic.Real.mk_numeral_s ctx.ctx_z3 (string_of_float (Runtime.decimal_to_float r))
  | LMoney m ->
      let z3_m = Runtime.integer_to_int (Runtime.money_to_cents m) in
      Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 z3_m
@ -311,6 +329,9 @@ let find_or_create_funcdecl (ctx : context) (v : Var.t) : context * FuncDecl.fun
          let ctx = add_funcdecl v fd ctx in
          let ctx = add_z3var name v ctx in
          (ctx, fd)
+      | TAny ->
+          failwith
+            "[Z3 Encoding] A function being applied has type TAny, the type was not fully inferred"
      | _ ->
          failwith
            "[Z3 Encoding] Ill-formed VC, a function application does not have a function type")
@ -389,32 +410,32 @@ let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked lis
          | And -> (ctx, Boolean.mk_and ctx.ctx_z3 [ e1; e2 ])
          | Or -> (ctx, Boolean.mk_or ctx.ctx_z3 [ e1; e2 ])
          | Xor -> (ctx, Boolean.mk_xor ctx.ctx_z3 e1 e2)
-          | Add KInt -> (ctx, Arithmetic.mk_add ctx.ctx_z3 [ e1; e2 ])
+          | Add KInt | Add KRat | Add KMoney -> (ctx, Arithmetic.mk_add ctx.ctx_z3 [ e1; e2 ])
          | Add _ ->
              failwith "[Z3 encoding] application of non-integer binary operator Add not supported"
-          | Sub KInt -> (ctx, Arithmetic.mk_sub ctx.ctx_z3 [ e1; e2 ])
+          | Sub KInt | Sub KRat | Sub KMoney -> (ctx, Arithmetic.mk_sub ctx.ctx_z3 [ e1; e2 ])
          | Sub _ ->
              failwith "[Z3 encoding] application of non-integer binary operator Sub not supported"
-          | Mult KInt -> (ctx, Arithmetic.mk_mul ctx.ctx_z3 [ e1; e2 ])
+          | Mult KInt | Mult KRat | Mult KMoney -> (ctx, Arithmetic.mk_mul ctx.ctx_z3 [ e1; e2 ])
          | Mult _ ->
              failwith "[Z3 encoding] application of non-integer binary operator Mult not supported"
-          | Div KInt -> (ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2)
+          | Div KInt | Div KRat | Div KMoney -> (ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2)
          | Div _ ->
              failwith "[Z3 encoding] application of non-integer binary operator Div not supported"
-          | Lt KInt | Lt KMoney | Lt KDate -> (ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
+          | Lt KInt | Lt KRat | Lt KMoney | Lt KDate -> (ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
          | Lt _ ->
              failwith
                "[Z3 encoding] application of non-integer or money binary operator Lt not supported"
-          | Lte KInt | Lte KMoney | Lte KDate -> (ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
+          | Lte KInt | Lte KRat | Lte KMoney | Lte KDate -> (ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
          | Lte _ ->
              failwith
                "[Z3 encoding] application of non-integer or money binary operator Lte not \
                 supported"
-          | Gt KInt | Gt KMoney | Gt KDate -> (ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
+          | Gt KInt | Gt KRat | Gt KMoney | Gt KDate -> (ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
          | Gt _ ->
              failwith
                "[Z3 encoding] application of non-integer or money binary operator Gt not supported"
-          | Gte KInt | Gte KMoney | Gte KDate -> (ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
+          | Gte KInt | Gte KRat | Gte KMoney | Gte KDate -> (ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
          | Gte _ ->
              failwith
                "[Z3 encoding] application of non-integer or money binary operator Gte not \
@ -557,6 +578,14 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
          ] )
  | ErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"

+(** [create_z3unit] creates a Z3 sort and expression corresponding to the unit type and value
+    respectively. Concretely, we represent unit as a tuple with 0 elements **)
+let create_z3unit (ctx : Z3.context) : Z3.context * (Sort.sort * Expr.expr) =
+  let unit_sort = Tuple.mk_sort ctx (Symbol.mk_string ctx "unit") [] [] in
+  let mk_unit = Tuple.get_mk_decl unit_sort in
+  let unit_val = Expr.mk_app ctx mk_unit [] in
+  (ctx, (unit_sort, unit_val))
+
 module Backend = struct
  type backend_context = context

@ -590,6 +619,7 @@ module Backend = struct
      (if !Cli.disable_counterexamples then [] else [ ("model", "true") ]) @ [ ("proof", "false") ]
    in
    let z3_ctx = mk_context cfg in
+    let z3_ctx, z3unit = create_z3unit z3_ctx in
    {
      ctx_z3 = z3_ctx;
      ctx_decl = decl_ctx;
@ -599,6 +629,7 @@ module Backend = struct
      ctx_z3datatypes = EnumMap.empty;
      ctx_z3matchsubsts = VarMap.empty;
      ctx_z3structs = StructMap.empty;
+      ctx_z3unit = z3unit;
    }
 end

--- a/default.nix
+++ b/default.nix
@ -19,15 +19,16 @@
 , js_of_ocaml-ppx
 , camomile
 , cppo
+, ppx_deriving
 , z3
 , menhirLib ? null #for nixos-unstable compatibility.
 }:

 buildDunePackage rec {
  pname = "catala";
-  version = "0.3.0";
+  version = "0.5.0";

-  minimumOCamlVersion = "4.08";
+  minimumOCamlVersion = "4.11";

  src = ./.;

@ -54,6 +55,8 @@ buildDunePackage rec {

    pkgs.z3

+    ppx_deriving
+
    unionfind
    bindlib
  ] ++ (if isNull menhirLib then [ ] else [ menhirLib ]);
@ -68,4 +71,4 @@ buildDunePackage rec {
    license = licenses.asl20;
    maintainers = with maintainers; [ ];
  };
-}
+}
--- a/2
+++ b/2
@ -43,7 +43,7 @@
  (bindlib
   (>= 5.0.1))
  (cmdliner
-   (>= 1.1.0))
+   (= 1.0.4))
  (re
   (>= 1.9.0))
  (zarith
--- a/french_law/js/french_law.js
+++ b/french_law/js/french_law.js
--- a/french_law/js/package-lock.json
+++ b/french_law/js/package-lock.json
@ -1,8 +1,40 @@
 {
  "name": "french_law",
  "version": "0.5.0",
-  "lockfileVersion": 1,
+  "lockfileVersion": 2,
  "requires": true,
+  "packages": {
+    "": {
+      "name": "french_law",
+      "version": "0.5.0",
+      "license": "Apache-2.0",
+      "dependencies": {
+        "benchmark": "^2.1.4",
+        "lodash": "^4.17.21",
+        "platform": "^1.3.6"
+      },
+      "devDependencies": {}
+    },
+    "node_modules/benchmark": {
+      "version": "2.1.4",
+      "resolved": "https://registry.npmjs.org/benchmark/-/benchmark-2.1.4.tgz",
+      "integrity": "sha1-CfPeMckWQl1JjMLuVloOvzwqVik=",
+      "dependencies": {
+        "lodash": "^4.17.4",
+        "platform": "^1.3.3"
+      }
+    },
+    "node_modules/lodash": {
+      "version": "4.17.21",
+      "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.21.tgz",
+      "integrity": "sha512-v2kDEe57lecTulaDIuNTPy3Ry4gLGJ6Z1O3vE1krgXZNrsQ+LFTGHVxVjcXPs17LhbZVGedAJv8XZ1tvj5FvSg=="
+    },
+    "node_modules/platform": {
+      "version": "1.3.6",
+      "resolved": "https://registry.npmjs.org/platform/-/platform-1.3.6.tgz",
+      "integrity": "sha512-fnWVljUchTro6RiCFvCXBbNhJc2NijN7oIQxbwsyL0buWJPG85v81ehlHI9fXrJsMNgTofEoWIQeClKpgxFLrg=="
+    }
+  },
  "dependencies": {
    "benchmark": {
      "version": "2.1.4",
--- a/french_law/ocaml/law_source/allocations_familiales.ml
+++ b/french_law/ocaml/law_source/allocations_familiales.ml
--- a/french_law/python/src/allocations_familiales.py
+++ b/french_law/python/src/allocations_familiales.py
--- a/release.nix
+++ b/release.nix
@ -4,5 +4,4 @@ with pkgs;
 ocamlPackages.callPackage ./. {
  bindlib = ocamlPackages.callPackage ./.nix/bindlib.nix { };
  unionfind = ocamlPackages.callPackage ./.nix/unionfind.nix { };
-  cmdliner = ocamlPackages.callPackage ./.nix/cmdliner.nix { };
 }
--- a/shell.nix
+++ b/shell.nix
@ -5,7 +5,6 @@ let
  pkg = ocamlPackages.callPackage ./. {
    bindlib = ocamlPackages.callPackage ./.nix/bindlib.nix { };
    unionfind = ocamlPackages.callPackage ./.nix/unionfind.nix { };
-    cmdliner = ocamlPackages.callPackage ./.nix/cmdliner.nix { };
  };
 in mkShell {
  inputsFrom = [ pkg ];
--- a/tests/test_bool/good/output/test_bool.catala_en.Dcalc
+++ b/tests/test_bool/good/output/test_bool.catala_en.Dcalc
@ -1,18 +1,18 @@
-let TestBool_6 :
+let TestBool_7 :
  TestBool_in{"foo_in": unit → bool; "bar_in": unit → integer} →
    TestBool_out{"foo_out": bool; "bar_out": integer} =
-  λ (TestBool_in_7: TestBool_in{"foo_in": unit → bool; "bar_in":
+  λ (TestBool_in_8: TestBool_in{"foo_in": unit → bool; "bar_in":
                       unit → integer}) →
-    let foo_8 : unit → bool = TestBool_in_7."foo_in" in
-    let bar_9 : unit → integer = TestBool_in_7."bar_in" in
-    let bar_10 : integer = error_empty
-      ⟨bar_9 () | true ⊢
+    let foo_9 : unit → bool = TestBool_in_8."foo_in" in
+    let bar_10 : unit → integer = TestBool_in_8."bar_in" in
+    let bar_11 : integer = error_empty
+      ⟨bar_10 () | true ⊢
        ⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
          ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
-    let foo_11 : bool = error_empty
-      ⟨foo_8 () | true ⊢
-        ⟨⟨true ⊢ ⟨⟨bar_10 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
-          ⟨true ⊢ ⟨⟨bar_10 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
+    let foo_12 : bool = error_empty
+      ⟨foo_9 () | true ⊢
+        ⟨⟨true ⊢ ⟨⟨bar_11 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
+          ⟨true ⊢ ⟨⟨bar_11 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
          true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
-    TestBool_out {"foo_out"= foo_11; "bar_out"= bar_10} in
-TestBool_6
+    TestBool_out {"foo_out"= foo_12; "bar_out"= bar_11} in
+TestBool_7
--- a/tests/test_io/good/output/all_io.catala_en.A.Dcalc
+++ b/tests/test_io/good/output/all_io.catala_en.A.Dcalc
@ -1,23 +1,23 @@
 let A =
-  λ (A_in_10: A_in{"c_in": integer; "d_in": integer; "e_in":
+  λ (A_in_11: A_in{"c_in": integer; "d_in": integer; "e_in":
                 unit → integer; "f_in": unit → integer}) →
-    let c_11 : integer = A_in_10."c_in" in
-    let d_12 : integer = A_in_10."d_in" in
-    let e_13 : unit → integer = A_in_10."e_in" in
-    let f_14 : unit → integer = A_in_10."f_in" in
-    let a_15 : integer = error_empty
+    let c_12 : integer = A_in_11."c_in" in
+    let d_13 : integer = A_in_11."d_in" in
+    let e_14 : unit → integer = A_in_11."e_in" in
+    let f_15 : unit → integer = A_in_11."f_in" in
+    let a_16 : integer = error_empty
      ⟨⟨true ⊢ ⟨⟨true ⊢ 0⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
        ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
-    let b_16 : integer = error_empty
-      ⟨⟨true ⊢ ⟨⟨true ⊢ a_15 + 1⟩ | false ⊢ ∅ ⟩⟩ | true
+    let b_17 : integer = error_empty
+      ⟨⟨true ⊢ ⟨⟨true ⊢ a_16 + 1⟩ | false ⊢ ∅ ⟩⟩ | true
        ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
-    let e_17 : integer = error_empty
-      ⟨e_13 () | true ⊢
+    let e_18 : integer = error_empty
+      ⟨e_14 () | true ⊢
        ⟨⟨true ⊢
-             ⟨⟨true ⊢ b_16 + c_11 + d_12 + 1⟩ | false ⊢ ∅ ⟩⟩
+             ⟨⟨true ⊢ b_17 + c_12 + d_13 + 1⟩ | false ⊢ ∅ ⟩⟩
          | true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
-    let f_18 : integer = error_empty
-      ⟨f_14 () | true ⊢
-        ⟨⟨true ⊢ ⟨⟨true ⊢ e_17 + 1⟩ | false ⊢ ∅ ⟩⟩ |
+    let f_19 : integer = error_empty
+      ⟨f_15 () | true ⊢
+        ⟨⟨true ⊢ ⟨⟨true ⊢ e_18 + 1⟩ | false ⊢ ∅ ⟩⟩ |
          true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
-    A_out {"b_out"= b_16; "d_out"= d_12; "f_out"= f_18}
+    A_out {"b_out"= b_17; "d_out"= d_13; "f_out"= f_19}
--- a/tests/test_io/good/output/condition_only_input.catala_en.B.Dcalc
+++ b/tests/test_io/good/output/condition_only_input.catala_en.B.Dcalc
@ -1,8 +1,8 @@
 let B =
-  λ (B_in_13: B_in{}) →
-    let a.x_14 : bool = error_empty
+  λ (B_in_14: B_in{}) →
+    let a.x_15 : bool = error_empty
      ⟨true ⊢ ⟨⟨true ⊢ false⟩ | false ⊢ ∅ ⟩⟩ in
-    let result_15 : A_out{"y_out": integer} = A_2 (A_in {"x_in"= a.x_14}) in
-    let a.y_16 : integer = result_15."y_out" in
-    let __17 : unit = assert (a.y_16 = 1) in
+    let result_16 : A_out{"y_out": integer} = A_3 (A_in {"x_in"= a.x_15}) in
+    let a.y_17 : integer = result_16."y_out" in
+    let __18 : unit = assert (error_empty a.y_17 = 1) in
    B_out {}
--- a/tests/test_io/good/output/condition_only_input.catala_en.B.Interpret
+++ b/tests/test_io/good/output/condition_only_input.catala_en.B.Interpret
@ -1 +1 @@
-[RESULT] Computation successful!
+[RESULT] Computation successful!
--- a/tests/test_io/good/output/subscope.catala_en.B.Dcalc
+++ b/tests/test_io/good/output/subscope.catala_en.B.Dcalc
@ -1,11 +1,11 @@
 let B =
-  λ (B_in_17: B_in{}) →
-    let a.a_18 : unit → integer = λ (__19: unit) → ∅  in
-    let a.b_20 : integer = error_empty
+  λ (B_in_18: B_in{}) →
+    let a.a_19 : unit → integer = λ (__20: unit) → ∅  in
+    let a.b_21 : integer = error_empty
      ⟨⟨true ⊢ ⟨⟨true ⊢ 2⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
        ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
-    let result_21 : A_out{"c_out": integer} =
-      A_2 (A_in {"a_in"= a.a_18; "b_in"= a.b_20}) in
-    let a.c_22 : integer = result_21."c_out" in
-    let __23 : unit = assert (a.c_22 = 1) in
+    let result_22 : A_out{"c_out": integer} =
+      A_3 (A_in {"a_in"= a.a_19; "b_in"= a.b_21}) in
+    let a.c_23 : integer = result_22."c_out" in
+    let __24 : unit = assert (error_empty a.c_23 = 1) in
    B_out {}
--- a/tests/test_proof/bad/enums_unit-empty.catala_en
+++ b/tests/test_proof/bad/enums_unit-empty.catala_en
@ -0,0 +1,20 @@
+## Article
+
+```catala
+declaration enumeration E:
+  -- Case1 content integer
+  -- Case2
+
+declaration scope A:
+  context x content E
+  context y content integer
+
+scope A:
+  definition x equals Case1 content 2
+  definition y under condition match x with pattern
+    -- Case1 of i : i > 0
+    -- Case2 : false consequence equals 2
+  definition y under condition match x with pattern
+    -- Case1 of i : false
+    -- Case2 : true consequence equals 2
+```
--- a/tests/test_proof/bad/enums_unit-overlap.catala_en
+++ b/tests/test_proof/bad/enums_unit-overlap.catala_en
@ -0,0 +1,20 @@
+## Article
+
+```catala
+declaration enumeration E:
+  -- Case1 content integer
+  -- Case2
+
+declaration scope A:
+  context x content E
+  context y content integer
+
+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
+  definition y under condition match x with pattern
+    -- Case1 of i : false
+    -- Case2 : true consequence equals 2
+```
--- a/tests/test_proof/bad/output/enums_unit-empty.catala_en.Proof
+++ b/tests/test_proof/bad/output/enums_unit-empty.catala_en.Proof
@ -0,0 +1,10 @@
+[ERROR] [A.y] This variable might return an empty error:
+  --> tests/test_proof/bad/enums_unit-empty.catala_en
+   | 
+10 |   context y content integer
+   |           ^
+   + Article
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
--- a/tests/test_proof/bad/output/enums_unit-overlap.catala_en.Proof
+++ b/tests/test_proof/bad/output/enums_unit-overlap.catala_en.Proof
@ -0,0 +1,10 @@
+[RESULT] [A.y] This variable never returns an empty error
+[ERROR] [A.y] At least two exceptions overlap for this variable:
+  --> tests/test_proof/bad/enums_unit-overlap.catala_en
+   | 
+10 |   context y content integer
+   |           ^
+   + Article
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
--- a/tests/test_proof/bad/output/rationals-empty.catala_en.Proof
+++ b/tests/test_proof/bad/output/rationals-empty.catala_en.Proof
@ -0,0 +1,10 @@
+[ERROR] [A.y] This variable might return an empty error:
+ --> tests/test_proof/bad/rationals-empty.catala_en
+  | 
+6 |   context y content boolean
+  |           ^
+  + Test
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
--- a/tests/test_proof/bad/output/rationals-overlap.catala_en.Proof
+++ b/tests/test_proof/bad/output/rationals-overlap.catala_en.Proof
@ -0,0 +1,10 @@
+[RESULT] [A.y] This variable never returns an empty error
+[ERROR] [A.y] At least two exceptions overlap for this variable:
+ --> tests/test_proof/bad/rationals-overlap.catala_en
+  | 
+6 |   context y content boolean
+  |           ^
+  + Test
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
--- a/tests/test_proof/bad/rationals-empty.catala_en
+++ b/tests/test_proof/bad/rationals-empty.catala_en
@ -0,0 +1,11 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content decimal
+  context y content boolean
+
+scope A:
+  definition x equals 1.
+  definition y under condition x >. 1./.3. consequence equals true
+```
--- a/tests/test_proof/bad/rationals-overlap.catala_en
+++ b/tests/test_proof/bad/rationals-overlap.catala_en
@ -0,0 +1,12 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content decimal
+  context y content boolean
+
+scope A:
+  definition x equals 1.
+  definition y under condition x >=. 1./.3. consequence equals true
+  definition y under condition x <=. 1./.3. consequence equals false
+```
--- a/tests/test_proof/good/enums_unit.catala_en
+++ b/tests/test_proof/good/enums_unit.catala_en
@ -0,0 +1,20 @@
+## Article
+
+```catala
+declaration enumeration E:
+  -- Case1 content integer
+  -- Case2
+
+declaration scope A:
+  context x content E
+  context y content integer
+
+scope A:
+  definition x equals Case1 content 2
+  definition y under condition match x with pattern
+    -- Case1 of i : true
+    -- Case2 : false consequence equals 2
+  definition y under condition match x with pattern
+    -- Case1 of i : false
+    -- Case2 : true consequence equals 2
+```
--- a/tests/test_proof/good/output/enums_unit.catala_en.Proof
+++ b/tests/test_proof/good/output/enums_unit.catala_en.Proof
@ -0,0 +1,4 @@
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
--- a/tests/test_proof/good/output/rationals.catala_en.Proof
+++ b/tests/test_proof/good/output/rationals.catala_en.Proof
@ -0,0 +1,4 @@
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
--- a/tests/test_proof/good/rationals.catala_en
+++ b/tests/test_proof/good/rationals.catala_en
@ -0,0 +1,12 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content decimal
+  context y content boolean
+
+scope A:
+  definition x equals 1.
+  definition y under condition x >. 1./.3. consequence equals true
+  definition y under condition x <=. 1./.3. consequence equals false
+```