Callable scopes: fixes following review

2024-11-08 07:51:43 +03:00 · 2022-11-03 15:18:51 +01:00 · 2022-11-03 15:18:51 +01:00 · 3e004551fc
commit 3e004551fc
parent 47a1258648
13 changed files with 36 additions and 35 deletions
--- a/compiler/desugared/desugared_to_scope.ml
+++ b/compiler/desugared/desugared_to_scope.ml
@ -89,7 +89,10 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr) :
           let v' =
             match ScopeVarMap.find v ctx.scope_var_mapping with
             | WholeVar v' -> v'
-             | States ((_, v') :: _) -> v'
+             | States ((_, v') :: _) ->
+               (* When there are multiple states, the input is always the first
+                  one *)
+               v'
             | States [] -> assert false
           in
           ScopeVarMap.add v' (translate_expr ctx e) fields')
--- a/compiler/scopelang/scope_to_dcalc.ml
+++ b/compiler/scopelang/scope_to_dcalc.ml
@ -33,8 +33,7 @@ type 'm scope_sig_ctx = {
  scope_sig_output_struct : StructName.t;  (** Scope output *)
  scope_sig_in_fields :
    (StructFieldName.t * Ast.io_input Marked.pos) ScopeVarMap.t;
-      (** Mapping between the input scope variables and the input struct fields.
-          The boolean is true for 'context' variables which need to be thunked. *)
+      (** Mapping between the input scope variables and the input struct fields. *)
 }

 type 'm scope_sigs_ctx = 'm scope_sig_ctx ScopeMap.t
@ -147,6 +146,9 @@ let collapse_similar_outcomes (type m) (excepts : m Ast.expr list) :
  excepts

 let thunk_scope_arg io_in e =
+  (* For "context" (or reentrant) variables, we thunk them as [(fun () -> e)] so
+     that we can put them in default terms at the initialisation of the function
+     body, allowing an empty error to recover the default value. *)
  let silent_var = Var.make "_" in
  let pos = Marked.get_mark io_in in
  match Marked.unmark io_in with
--- a/compiler/shared_ast/print.ml
+++ b/compiler/shared_ast/print.ml
@ -88,8 +88,8 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
    match ctx with
    | None -> Format.fprintf fmt "@[<hov 2>%a@]" StructName.format_t s
    | Some ctx ->
-      Format.fprintf fmt "@[<hov 2>%a%a%a%a@]" StructName.format_t s punctuation
-        "{"
+      Format.fprintf fmt "@[<hov 2>%a@ %a%a%a@]" StructName.format_t s
+        punctuation "{"
        (Format.pp_print_list
           ~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ";")
           (fun fmt (field, mty) ->
--- a/compiler/shared_ast/typing.ml
+++ b/compiler/shared_ast/typing.ml
@ -61,7 +61,8 @@ let rec typ_to_ast (ty : unionfind_typ) : A.typ =
    (* No polymorphism in Catala: type inference should return full types
       without wildcards, and this function is used to recover the types after
       typing. *)
-    assert false
+    Errors.raise_spanned_error pos
+      "Internal error: typing at this point could not be resolved"

 let rec ast_to_typ (ty : A.typ) : unionfind_typ =
  let ty' =
--- a/compiler/surface/desugaring.ml
+++ b/compiler/surface/desugaring.ml
@ -55,15 +55,6 @@ let translate_binop (op : Ast.binop) : binop =
 let translate_unop (op : Ast.unop) : unop =
  match op with Not -> Not | Minus l -> Minus (translate_op_kind l)

-(** The two modules below help performing operations on map with the {!type:
-    Bindlib.box}. Indeed, Catala uses the {{:https://lepigre.fr/ocaml-bindlib/}
-    Bindlib} library to represent bound variables in the AST. In this
-    translation, bound variables are used to represent function parameters or
-    pattern macthing bindings. *)
-
-module LiftStructFieldMap = Bindlib.Lift (StructFieldMap)
-module LiftEnumConstructorMap = Bindlib.Lift (EnumConstructorMap)
-
 let disambiguate_constructor
    (ctxt : Name_resolution.context)
    (constructor : (string Marked.pos option * string Marked.pos) list)
@ -332,12 +323,12 @@ let rec translate_expr
                [
                  None, Marked.get_mark fld_id;
                  ( Some
-                      (Format.asprintf "Scope '%a' declared here"
+                      (Format.asprintf "Scope %a declared here"
                         ScopeName.format_t called_scope),
                    Marked.get_mark (ScopeName.get_info called_scope) );
                ]
-                "Scope '%a' has no input variable '%s'" ScopeName.format_t
-                called_scope (Marked.unmark fld_id)
+                "Scope %a has no input variable %a" ScopeName.format_t
+                called_scope Print.lit_style (Marked.unmark fld_id)
          in
          ScopeVarMap.update var
            (function
@ -1150,7 +1141,11 @@ let attribute_to_io (attr : Ast.scope_decl_context_io) : Scopelang.Ast.io =
        attr.scope_decl_context_io_input;
  }

-let init_scope_defs ctxt scope_idmap =
+let init_scope_defs
+    (ctxt : Name_resolution.context)
+    (scope_idmap :
+      Name_resolution.scope_var_or_subscope Desugared.Ast.IdentMap.t) :
+    Desugared.Ast.scope_def Desugared.Ast.ScopeDefMap.t =
  (* Initializing the definitions of all scopes and subscope vars, with no rules
     yet inside *)
  let add_def _ v scope_def_map =
--- a/compiler/surface/name_resolution.ml
+++ b/compiler/surface/name_resolution.ml
@ -676,11 +676,11 @@ let get_def_key
      | Some (SubScope (v, u)) -> v, u
      | Some _ ->
        Errors.raise_spanned_error pos
-          "Invalid access to input variable, '%s' is not a subscope"
-          (Marked.unmark y)
+          "Invalid access to input variable, %a is not a subscope"
+          Print.lit_style (Marked.unmark y)
      | None ->
-        Errors.raise_spanned_error pos "No definition found for subscope '%s'"
-          (Marked.unmark y)
+        Errors.raise_spanned_error pos "No definition found for subscope %a"
+          Print.lit_style (Marked.unmark y)
    in
    let x_uid = get_var_uid subscope_real_uid ctxt x in
    Desugared.Ast.ScopeDef.SubScopeVar (subscope_uid, x_uid, pos)
--- a/tests/test_bool/good/test_bool.catala_en
+++ b/tests/test_bool/good/test_bool.catala_en
@ -14,9 +14,9 @@ scope TestBool:
 ```catala-test-inline
 $ catala Dcalc 
 let TestBool :
-  TestBool_in{"foo_in": unit → bool; "bar_in": unit → integer} →
-    TestBool{"foo": bool; "bar": integer} =
-  λ (TestBool_in: TestBool_in{"foo_in": unit → bool; "bar_in":
+  TestBool_in {"foo_in": unit → bool; "bar_in": unit → integer} →
+    TestBool {"foo": bool; "bar": integer} =
+  λ (TestBool_in: TestBool_in {"foo_in": unit → bool; "bar_in":
                     unit → integer}) →
    let foo : unit → bool = TestBool_in."foo_in" in
    let bar : unit → integer = TestBool_in."bar_in" in
--- a/tests/test_io/good/all_io.catala_en
+++ b/tests/test_io/good/all_io.catala_en
@ -20,7 +20,7 @@ scope A:
 ```catala-test-inline
 $ catala Dcalc -s A
 let A =
-  λ (A_in: A_in{"c_in": integer; "d_in": integer; "e_in": unit → integer;
+  λ (A_in: A_in {"c_in": integer; "d_in": integer; "e_in": unit → integer;
              "f_in": unit → integer}) →
    let c : integer = A_in."c_in" in
    let d : integer = A_in."d_in" in
--- a/tests/test_io/good/condition_only_input.catala_en
+++ b/tests/test_io/good/condition_only_input.catala_en
@ -17,9 +17,9 @@ scope B:
 ```catala-test-inline
 $ catala Dcalc -s B
 let B =
-  λ (B_in: B_in{}) →
+  λ (B_in: B_in {}) →
    let a.x : bool = error_empty ⟨true ⊢ false⟩ in
-    let result : A{"y": integer} = A (A_in {"x_in"= a.x}) in
+    let result : A {"y": integer} = A (A_in {"x_in"= a.x}) in
    let a.y : integer = result."y" in
    let _ : unit = assert (error_empty a.y = 1) in
    B {}
--- a/tests/test_io/good/subscope.catala_en
+++ b/tests/test_io/good/subscope.catala_en
@ -23,10 +23,10 @@ scope B:
 ```catala-test-inline
 $ catala Dcalc -s B
 let B =
-  λ (B_in: B_in{}) →
+  λ (B_in: B_in {}) →
    let a.a : unit → integer = λ (_: unit) → ∅  in
    let a.b : integer = error_empty ⟨true ⊢ 2⟩ in
-    let result : A{"c": integer} = A (A_in {"a_in"= a.a; "b_in"= a.b}) in
+    let result : A {"c": integer} = A (A_in {"a_in"= a.a; "b_in"= a.b}) in
    let a.c : integer = result."c" in
    let _ : unit = assert (error_empty a.c = 1) in
    B {}
--- a/tests/test_scope/bad/scope_call_extra.catala_en
+++ b/tests/test_scope/bad/scope_call_extra.catala_en
@ -16,7 +16,7 @@ scope Titi:

 ```catala-test-inline
 $ catala dcalc -s Titi
-[ERROR] Scope 'Toto' has no input variable 'biz'
+[ERROR] Scope Toto has no input variable biz

  --> tests/test_scope/bad/scope_call_extra.catala_en
   |
@ -24,7 +24,7 @@ $ catala dcalc -s Titi
   |                                     ^^^
   +

-Scope 'Toto' declared here
+Scope Toto declared here
 --> tests/test_scope/bad/scope_call_extra.catala_en
  |
 2 | declaration scope Toto:
--- a/tests/test_scope/good/nothing.catala_en
+++ b/tests/test_scope/good/nothing.catala_en
@ -7,7 +7,7 @@ declaration scope Foo2:

 ```catala-test-inline
 $ catala Scalc -s Foo2 -O -t
-let Foo2 (Foo2_in : Foo2_in{}) =
+let Foo2 (Foo2_in : Foo2_in {}) =
  decl temp_bar : any;
  temp_bar = dead_value_1;
  raise NoValueProvided;
--- a/tests/test_scope/good/simple.catala_en
+++ b/tests/test_scope/good/simple.catala_en
@ -11,7 +11,7 @@ scope Foo:
 ```catala-test-inline
 $ catala Lcalc -s Foo
 let Foo =
-  λ (Foo_in: Foo_in{}) →
+  λ (Foo_in: Foo_in {}) →
    let bar : integer =
      try handle_default [] (λ (_: unit) → true) (λ (_: unit) → 0) with
        EmptyError -> raise NoValueProvided in