feat(compiler): Compiling Dcalc into Lcalc without using ∅ errors

.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))

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))

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 =

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

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
+   <[email protected]>
+
+   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

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
+   <[email protected]>
+
+   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] *)

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)

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...";