[skip ci] reorganized desugared to scope encoding, broke some invariants

WIP: fixed some bugs and provided documentations but one thing missing

compiler/dcalc/ast.ml

@@ -181,6 +181,14 @@ let make_let_in (x : Var.t) (tau : typ Pos.marked) (e1 : expr Pos.marked Bindlib
     (e2 : expr Pos.marked Bindlib.box) (pos : Pos.t) : expr Pos.marked Bindlib.box =
   make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] pos) [ e1 ] pos
 
+let empty_thunked_term : expr Pos.marked =
+  let silent = Var.make ("_", Pos.no_pos) in
+  Bindlib.unbox
+    (make_abs
+       (Array.of_list [ silent ])
+       (Bindlib.box (ELit LEmptyError, Pos.no_pos))
+       Pos.no_pos [ (TLit TUnit, Pos.no_pos) ] Pos.no_pos)
+
 let build_whole_scope_expr (ctx : decl_ctx) (body : scope_body) (pos_scope : Pos.t) =
   let body_expr =
     List.fold_right

compiler/dcalc/ast.mli

@@ -206,6 +206,8 @@ val make_let_in :
   Pos.t ->
   expr Pos.marked Bindlib.box
 
+val empty_thunked_term : expr Pos.marked
+
 (** {1 AST manipulation helpers}*)
 
 val build_whole_scope_expr : decl_ctx -> scope_body -> Pos.t -> expr Pos.marked Bindlib.box

compiler/dcalc/interpreter.ml

@@ -22,16 +22,6 @@ module A = Ast
 let is_empty_error (e : A.expr Pos.marked) : bool =
   match Pos.unmark e with ELit LEmptyError -> true | _ -> false
 
-let empty_thunked_term : Ast.expr Pos.marked =
-  let silent = Ast.Var.make ("_", Pos.no_pos) in
-  Bindlib.unbox
-    (Ast.make_abs
-       (Array.of_list [ silent ])
-       (Bindlib.box (Ast.ELit Ast.LEmptyError, Pos.no_pos))
-       Pos.no_pos
-       [ (Ast.TLit Ast.TUnit, Pos.no_pos) ]
-       Pos.no_pos)
-
 let log_indent = ref 0
 
 (** {1 Evaluation} *)
@@ -439,7 +429,7 @@ let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Pos.marked) :
     (Uid.MarkedString.info * Ast.expr Pos.marked) list =
   match Pos.unmark (evaluate_expr ctx e) with
   | Ast.EAbs (_, [ (Ast.TTuple (taus, Some s_in), _) ]) -> (
-      let application_term = List.map (fun _ -> empty_thunked_term) taus in
+      let application_term = List.map (fun _ -> Ast.empty_thunked_term) taus in
       let to_interpret =
         (Ast.EApp (e, [ (Ast.ETuple (application_term, Some s_in), Pos.no_pos) ]), Pos.no_pos)
       in

compiler/dcalc/interpreter.mli

@@ -16,8 +16,6 @@
 
 open Utils
 
-val empty_thunked_term : Ast.expr Pos.marked
-
 val interpret_program :
   Ast.decl_ctx -> Ast.expr Pos.marked -> (Uid.MarkedString.info * Ast.expr Pos.marked) list
 (** Interpret a program. This function expects an expression typed as a function whose argument are

compiler/dcalc/print.ml

@@ -79,8 +79,8 @@ let rec format_typ (ctx : Ast.decl_ctx) (fmt : Format.formatter) (typ : typ Pos.
            (fun fmt t -> Format.fprintf fmt "%a" format_typ t))
         ts
   | TTuple (args, Some s) ->
-      Format.fprintf fmt "%a [%a]" Ast.StructName.format_t s
-        (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ") format_typ)
+      Format.fprintf fmt "%a {%a}" Ast.StructName.format_t s
+        (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ;@ ") format_typ)
         args
   | TEnum (_, e) -> Format.fprintf fmt "%a" Ast.EnumName.format_t e
   | TArrow (t1, t2) ->

compiler/desugared/ast.ml

@@ -118,6 +118,7 @@ type scope_def = {
   scope_def_rules : rule RuleMap.t;
   scope_def_typ : Scopelang.Ast.typ Pos.marked;
   scope_def_is_condition : bool;
+  scope_def_visibility : Scopelang.Ast.visibility;
   scope_def_label_groups : RuleSet.t LabelMap.t;
 }
 

compiler/desugared/ast.mli

@@ -79,6 +79,7 @@ type scope_def = {
   scope_def_rules : rule RuleMap.t;
   scope_def_typ : Scopelang.Ast.typ Pos.marked;
   scope_def_is_condition : bool;
+  scope_def_visibility : Scopelang.Ast.visibility;
   scope_def_label_groups : RuleSet.t LabelMap.t;
 }
 

compiler/desugared/desugared_to_scope.ml

@@ -124,13 +124,15 @@ let rec rule_tree_to_expr ~(toplevel : bool) (def_pos : Pos.t)
 (** Translates a definition inside a scope, the resulting expression should be an {!constructor:
     Dcalc.Ast.EDefault} *)
 let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t)
-    (typ : Scopelang.Ast.typ Pos.marked) (is_cond : bool) : Scopelang.Ast.expr Pos.marked =
+    (typ : Scopelang.Ast.typ Pos.marked) ~(is_cond : bool) ~(is_subscope_var : bool) :
+    Scopelang.Ast.expr Pos.marked =
   (* Here, we have to transform this list of rules into a default tree. *)
-  let is_func _ (r : Ast.rule) : bool = Option.is_some r.Ast.rule_parameter in
-  let all_rules_func = Ast.RuleMap.for_all is_func def in
-  let all_rules_not_func = Ast.RuleMap.for_all (fun n r -> not (is_func n r)) def in
-  let is_def_func : Scopelang.Ast.typ Pos.marked option =
-    if all_rules_func && Ast.RuleMap.cardinal def > 0 then
+  let is_def_func = match Pos.unmark typ with Scopelang.Ast.TArrow (_, _) -> true | _ -> false in
+  let is_rule_func _ (r : Ast.rule) : bool = Option.is_some r.Ast.rule_parameter in
+  let all_rules_func = Ast.RuleMap.for_all is_rule_func def in
+  let all_rules_not_func = Ast.RuleMap.for_all (fun n r -> not (is_rule_func n r)) def in
+  let is_def_func_param_typ : Scopelang.Ast.typ Pos.marked option =
+    if is_def_func && all_rules_func then
       match Pos.unmark typ with
       | Scopelang.Ast.TArrow (t_param, _) -> Some t_param
       | _ ->
@@ -139,7 +141,7 @@ let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t)
                "The definitions of %a are function but its type, %a, is not a function type"
                Ast.ScopeDef.format_t def_info Scopelang.Print.format_typ typ)
             (Pos.get_position typ)
-    else if all_rules_not_func then None
+    else if (not is_def_func) && all_rules_not_func then None
     else
       Errors.raise_multispanned_error
         "some definitions of the same variable are functions while others aren't"
@@ -147,26 +149,43 @@ let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t)
            (fun (_, r) ->
              ( Some "This definition is a function:",
                Pos.get_position (Bindlib.unbox r.Ast.rule_cons) ))
-           (Ast.RuleMap.bindings (Ast.RuleMap.filter is_func def))
+           (Ast.RuleMap.bindings (Ast.RuleMap.filter is_rule_func def))
         @ List.map
             (fun (_, r) ->
               ( Some "This definition is not a function:",
                 Pos.get_position (Bindlib.unbox r.Ast.rule_cons) ))
-            (Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_func n r)) def)))
+            (Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_rule_func n r)) def)))
   in
   let top_list = def_map_to_tree def_info def in
   let top_value =
-    (if is_cond then Ast.always_false_rule else Ast.empty_rule) Pos.no_pos is_def_func
+    (if is_cond then Ast.always_false_rule else Ast.empty_rule) Pos.no_pos is_def_func_param_typ
   in
-  Bindlib.unbox
-    (rule_tree_to_expr ~toplevel:true
-       (Ast.ScopeDef.get_position def_info)
-       (Option.map (fun _ -> Scopelang.Ast.Var.make ("param", Pos.no_pos)) is_def_func)
-       (match top_list with
-       | [] ->
-           (* In this case, there are no rules to define the expression *)
-           Leaf [ top_value ]
-       | _ -> Node (top_list, [ top_value ])))
+  if
+    Ast.RuleMap.cardinal def = 0 && is_def_func && is_subscope_var
+    (* Here we have a special case for the empty definitions. Indeed, we could use the code for the
+       regular case below that would create a convoluted default always returning empty error, and
+       this would be correct. But it gets more complicated with functions. Indeed, if we create an
+       empty definition for a subscope argument whose type is a function, we get something like [fun
+       () -> (fun real_param -> < ... >)] that is passed as an argument to the subscope. The
+       sub-scope de-thunks but the de-thunking does not return empty error, signalling there is not
+       reentrant variable, because functions are values! So the subscope does not see that there is
+       not reentrant variable and does not pick its internal definition instead. See
+       [test/test_scope/subscope_function_arg_not_defined.catala_en] for a test case exercising that
+       subtlety.
+
+       To avoid this complication we special case here and put an empty error whether the type of
+       the subscope argument is a function or not. *)
+  then (ELit LEmptyError, Pos.no_pos)
+  else
+    Bindlib.unbox
+      (rule_tree_to_expr ~toplevel:true
+         (Ast.ScopeDef.get_position def_info)
+         (Option.map (fun _ -> Scopelang.Ast.Var.make ("param", Pos.no_pos)) is_def_func_param_typ)
+         (match top_list with
+         | [] ->
+             (* In this case, there are no rules to define the expression *)
+             Leaf [ top_value ]
+         | _ -> Node (top_list, [ top_value ])))
 
 (** Translates a scope *)
 let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =
@@ -183,7 +202,10 @@ let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =
                let var_def = scope_def.scope_def_rules in
                let var_typ = scope_def.scope_def_typ in
                let is_cond = scope_def.scope_def_is_condition in
-               let expr_def = translate_def (Ast.ScopeDef.Var var) var_def var_typ is_cond in
+               let expr_def =
+                 translate_def (Ast.ScopeDef.Var var) var_def var_typ ~is_cond
+                   ~is_subscope_var:false
+               in
                [
                  Scopelang.Ast.Definition
                    ( ( Scopelang.Ast.ScopeVar
@@ -207,7 +229,9 @@ let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =
                      match def_key with
                      | Ast.ScopeDef.Var _ -> assert false (* should not happen *)
                      | Ast.ScopeDef.SubScopeVar (_, sub_scope_var) ->
-                         let expr_def = translate_def def_key def def_typ is_cond in
+                         let expr_def =
+                           translate_def def_key def def_typ ~is_cond ~is_subscope_var:true
+                         in
                          let subscop_real_name =
                            Scopelang.Ast.SubScopeMap.find sub_scope_index scope.scope_sub_scopes
                          in

compiler/scopelang/ast.ml

@@ -123,6 +123,8 @@ type rule =
   | Assertion of expr Pos.marked
   | Call of ScopeName.t * SubScopeName.t
 
+type visibility = { visibility_output : bool; visibility_input : bool }
+
 type scope_decl = {
   scope_decl_name : ScopeName.t;
   scope_sig : typ Pos.marked ScopeVarMap.t;

compiler/scopelang/ast.mli

@@ -89,6 +89,11 @@ type rule =
   | Assertion of expr Pos.marked
   | Call of ScopeName.t * SubScopeName.t
 
+type visibility = {
+  visibility_output : bool;  (** True if present in the scope's output *)
+  visibility_input : bool;  (** True if present in the scope's input (reentrant) *)
+}
+
 type scope_decl = {
   scope_decl_name : ScopeName.t;
   scope_sig : typ Pos.marked ScopeVarMap.t;

compiler/scopelang/scope_to_dcalc.ml

@@ -378,7 +378,10 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
         List.map
           (fun (subvar, _) ->
             if subscope_var_not_yet_defined subvar then
-              Bindlib.box Dcalc.Interpreter.empty_thunked_term
+              (* This is a redundant check. Normally, all subscope varaibles should have been
+                 defined (even an empty definition, if they're not defined by any rule in the source
+                 code) by the translation from desugared to the scope language. *)
+              Bindlib.box Dcalc.Ast.empty_thunked_term
             else
               let a_var, _ = Ast.ScopeVarMap.find subvar subscope_vars_defined in
               Dcalc.Ast.make_var (a_var, pos_call))

compiler/surface/desugaring.ml

@@ -927,17 +927,7 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
         (Some (Pos.same_pos_as param_var param), ctxt)
   in
   let scope_updated =
-    let scope_def =
-      {
-        Desugared.Ast.scope_def_rules =
-          (match Desugared.Ast.ScopeDefMap.find_opt def_key scope.scope_defs with
-          | Some def -> def.scope_def_rules
-          | None -> Desugared.Ast.RuleMap.empty);
-        scope_def_typ = Name_resolution.get_def_typ ctxt def_key;
-        scope_def_is_condition = Name_resolution.is_def_cond ctxt def_key;
-        scope_def_label_groups = Name_resolution.label_groups ctxt scope_uid def_key;
-      }
-    in
+    let scope_def = Desugared.Ast.ScopeDefMap.find def_key scope.scope_defs in
     let rule_name = def.definition_id in
     let parent_rules =
       match def.Ast.definition_exception_to with
@@ -945,7 +935,7 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
       | UnlabeledException -> (
           match scope_def_ctxt.default_exception_rulename with
           (* This should have been caught previously by check_unlabeled_exception *)
-          | None | Some (Name_resolution.Ambiguous _) -> assert false
+          | None | Some (Name_resolution.Ambiguous _) -> assert false (* should not happen *)
           | Some (Name_resolution.Unique (name, pos)) -> (Desugared.Ast.RuleSet.singleton name, pos)
           )
       | ExceptionToLabel label -> (
@@ -1099,18 +1089,57 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) : Desu
                   s_context.Name_resolution.var_idmap Scopelang.Ast.ScopeVarSet.empty;
               Desugared.Ast.scope_sub_scopes = s_context.Name_resolution.sub_scopes;
               Desugared.Ast.scope_defs =
-                Desugared.Ast.IdentMap.fold
-                  (fun _ v acc ->
-                    let x, y = Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs in
-                    Desugared.Ast.ScopeDefMap.add (Desugared.Ast.ScopeDef.Var v)
-                      {
-                        Desugared.Ast.scope_def_rules = Desugared.Ast.RuleMap.empty;
-                        Desugared.Ast.scope_def_typ = x;
-                        Desugared.Ast.scope_def_label_groups = Desugared.Ast.LabelMap.empty;
-                        Desugared.Ast.scope_def_is_condition = y;
-                      }
-                      acc)
-                  s_context.Name_resolution.var_idmap Desugared.Ast.ScopeDefMap.empty;
+                (* Initializing the definitions of all scopes and subscope vars, with no rules yet
+                   inside *)
+                (let scope_vars_defs =
+                   Desugared.Ast.IdentMap.fold
+                     (fun _ v acc ->
+                       let x, y = Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs in
+                       let def_key = Desugared.Ast.ScopeDef.Var v in
+                       Desugared.Ast.ScopeDefMap.add def_key
+                         {
+                           Desugared.Ast.scope_def_rules = Desugared.Ast.RuleMap.empty;
+                           Desugared.Ast.scope_def_typ = x;
+                           Desugared.Ast.scope_def_label_groups =
+                             Name_resolution.label_groups ctxt s_uid def_key;
+                           Desugared.Ast.scope_def_is_condition = y;
+                           Desugared.Ast.scope_def_visibility =
+                             {
+                               Scopelang.Ast.visibility_input = true;
+                               Scopelang.Ast.visibility_output = true;
+                             };
+                         }
+                         acc)
+                     s_context.Name_resolution.var_idmap Desugared.Ast.ScopeDefMap.empty
+                 in
+                 let scope_and_subscope_vars_defs =
+                   Scopelang.Ast.SubScopeMap.fold
+                     (fun subscope_name subscope_uid acc ->
+                       Desugared.Ast.IdentMap.fold
+                         (fun _ v acc ->
+                           let x, y =
+                             Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs
+                           in
+                           let def_key = Desugared.Ast.ScopeDef.SubScopeVar (subscope_name, v) in
+                           Desugared.Ast.ScopeDefMap.add def_key
+                             {
+                               Desugared.Ast.scope_def_rules = Desugared.Ast.RuleMap.empty;
+                               Desugared.Ast.scope_def_typ = x;
+                               Desugared.Ast.scope_def_label_groups =
+                                 Name_resolution.label_groups ctxt subscope_uid def_key;
+                               Desugared.Ast.scope_def_is_condition = y;
+                               Desugared.Ast.scope_def_visibility =
+                                 {
+                                   Scopelang.Ast.visibility_input = true;
+                                   Scopelang.Ast.visibility_output = true;
+                                 };
+                             }
+                             acc)
+                         (Scopelang.Ast.ScopeMap.find subscope_uid ctxt.Name_resolution.scopes)
+                           .Name_resolution.var_idmap acc)
+                     s_context.sub_scopes scope_vars_defs
+                 in
+                 scope_and_subscope_vars_defs);
               Desugared.Ast.scope_assertions = [];
               Desugared.Ast.scope_meta_assertions = [];
               Desugared.Ast.scope_uid = s_uid;

compiler/surface/name_resolution.ml

@@ -143,9 +143,11 @@ let is_def_cond (ctxt : context) (def : Desugared.Ast.ScopeDef.t) : bool =
 
 let label_groups (ctxt : context) (s_uid : Scopelang.Ast.ScopeName.t)
     (def : Desugared.Ast.ScopeDef.t) : Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t =
-  (Desugared.Ast.ScopeDefMap.find def
-     (Scopelang.Ast.ScopeMap.find s_uid ctxt.scopes).scope_defs_contexts)
-    .label_groups
+  try
+    (Desugared.Ast.ScopeDefMap.find def
+       (Scopelang.Ast.ScopeMap.find s_uid ctxt.scopes).scope_defs_contexts)
+      .label_groups
+  with Not_found -> Desugared.Ast.LabelMap.empty
 
 (** {1 Declarations pass} *)
 

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

@@ -1,8 +1,8 @@
 let
   TestBool_6 :
-    TestBool_in [unit → bool | unit → integer] → TestBool_out [bool |
-      integer] =
-  λ (TestBool_in_7: TestBool_in [unit → bool | unit → integer]) →
+    TestBool_in {unit → bool ; unit → integer} → TestBool_out {bool ;
+      integer} =
+  λ (TestBool_in_7: TestBool_in {unit → bool ; unit → integer}) →
     let foo_8 : unit → bool = TestBool_in_7."foo_in"
     in
     let bar_9 : unit → integer = TestBool_in_7."bar_in"

tests/test_proof/bad/output/prolala_motivating_example.catala_en.Proof

@@ -10,6 +10,8 @@ The solver generated the following counterexample to explain the faulty behavior
 [RESULT] [Amount.amount] No two exceptions to ever overlap for this variable
 [RESULT] [Amount.correct_amount] This variable never returns an empty error
 [RESULT] [Amount.correct_amount] No two exceptions to ever overlap for this variable
+[RESULT] [Amount.eligibility.is_eligible_correct] No two exceptions to ever overlap for this variable
+[RESULT] [Amount.eligibility.is_eligible] No two exceptions to ever overlap for this variable
 [RESULT] [Amount.eligibility.is_professor] No two exceptions to ever overlap for this variable
 [RESULT] [Amount.eligibility.is_student] No two exceptions to ever overlap for this variable
 [RESULT] [Amount.number_of_advisors] This variable never returns an empty error

tests/test_scope/good/output/subscope_function_arg_not_defined.catala_en.Caller.Interpret

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

tests/test_scope/good/subscope_function_arg_not_defined.catala_en

@@ -0,0 +1,18 @@
+## Article
+
+```catala
+declaration scope Callee:
+  context input content integer depends on boolean
+  context output content integer
+
+declaration scope Caller:
+  context sub scope Callee
+  context y content integer
+
+scope Callee:
+  definition input of b equals if b then 0 else 1
+  definition output equals input of true + 1
+
+scope Caller:
+  definition y equals sub.output
+```