From 8a2b50289e7e88b0fe8d37e3d51c48d82a6420fa Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Sat, 15 Apr 2023 15:43:03 +0200 Subject: [PATCH 1/7] Printer: add some missing boxes --- compiler/shared_ast/print.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index 77c27a9a..666c7880 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -431,12 +431,13 @@ let rec expr_aux : Format.fprintf fmt "@[%a@ %a@ %a@]" operator op (lhs exprc) arg1 (rhs exprc) arg2 | EApp { f = EOp { op = (And | Or) as op; _ }, _; args = [arg1; arg2] } -> - Format.fprintf fmt "%a@ %a %a" (lhs exprc) arg1 operator op (rhs exprc) arg2 + Format.fprintf fmt "@[%a@ %a %a@]" (lhs exprc) arg1 operator op + (rhs exprc) arg2 | EApp { f = EOp { op; _ }, _; args = [arg1; arg2] } -> Format.fprintf fmt "@[%a@ %a %a@]" (lhs exprc) arg1 operator op (rhs exprc) arg2 | EApp { f = EOp { op; _ }, _; args = [arg1] } -> - Format.fprintf fmt "%a %a" operator op (rhs exprc) arg1 + Format.fprintf fmt "@[%a@ %a@]" operator op (rhs exprc) arg1 | EApp { f; args } -> Format.fprintf fmt "@[%a@ %a@]" (lhs exprc) f (Format.pp_print_list @@ -473,8 +474,8 @@ let rec expr_aux : Format.fprintf fmt "@[%a@ %a@]" keyword "raise" except exn | ELocation loc -> location fmt loc | EDStructAccess { e; field; _ } -> - Format.fprintf fmt "%a%a%a%a%a" (lhs exprc) e punctuation "." punctuation - "\"" IdentName.format_t field punctuation "\"" + Format.fprintf fmt "@[%a%a@,%a%a%a@]" (lhs exprc) e punctuation "." + punctuation "\"" IdentName.format_t field punctuation "\"" | EStruct { name; fields } -> Format.fprintf fmt "@[@[%a@,@[%a@]@]@,%a%a@]" punctuation "{" @@ -487,10 +488,11 @@ let rec expr_aux : (StructField.Map.bindings fields) punctuation "}_" StructName.format_t name | EStructAccess { e; field; _ } -> - Format.fprintf fmt "%a%a%a%a%a" (lhs exprc) e punctuation "." punctuation - "\"" StructField.format_t field punctuation "\"" + Format.fprintf fmt "@[%a%a@,%a%a%a@]" (lhs exprc) e punctuation "." + punctuation "\"" StructField.format_t field punctuation "\"" | EInj { e; cons; _ } -> - Format.fprintf fmt "%a@ %a" EnumConstructor.format_t cons (rhs exprc) e + Format.fprintf fmt "@[%a@ %a@]" EnumConstructor.format_t cons + (rhs exprc) e | EMatch { e; cases; _ } -> Format.fprintf fmt "@[@[%a@ %a@]@ %a@ %a@]" keyword "match" (lhs exprc) e keyword "with" From cec52d47dee9656ce5573fc95aeed9cefef0ffc9 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Mon, 17 Apr 2023 12:23:54 +0200 Subject: [PATCH 2/7] Printer: flatten "else if" --- compiler/shared_ast/print.ml | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index 666c7880..4b2ac627 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -444,10 +444,20 @@ let rec expr_aux : ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") (rhs exprc)) args - | EIfThenElse { cond; etrue; efalse } -> - Format.fprintf fmt - "@[@[%a@ %a@]@ @[%a@ %a@]@ @[%a@ %a@]@]" keyword - "if" expr cond keyword "then" expr etrue keyword "else" (rhs exprc) efalse + | EIfThenElse _ -> + Format.pp_open_hvbox fmt 0; + let rec pr els fmt = function + | EIfThenElse { cond; etrue; efalse }, _ -> + Format.fprintf fmt + "@[%a@ %a@]@ @[%a@ %a@]@ %a@]" + keyword (if els then "else if" else "if") + expr cond keyword "then" expr etrue + (pr true) efalse + | e -> + Format.fprintf fmt "@[%a@ %a@]" keyword "else" (rhs exprc) e + in + pr false fmt e; + Format.pp_close_box fmt () | EOp { op; _ } -> operator fmt op | EDefault { excepts; just; cons } -> if List.length excepts = 0 then From 3e7a2a34abd68a8eebffec56987b741c106684b4 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Mon, 17 Apr 2023 15:10:47 +0200 Subject: [PATCH 3/7] More printer improvements --- compiler/shared_ast/print.ml | 145 ++++++++++++------ compiler/shared_ast/print.mli | 4 + tests/test_array/good/aggregation_2.catala_en | 26 ++-- tests/test_array/good/aggregation_3.catala_en | 70 ++++----- tests/test_bool/good/test_bool.catala_en | 28 ++-- .../good/grouped_exceptions.catala_en | 4 +- .../good/groups_of_exceptions.catala_en | 6 +- tests/test_func/good/context_func.catala_en | 20 ++- tests/test_io/good/all_io.catala_en | 29 +++- .../good/condition_only_input.catala_en | 8 +- tests/test_io/good/subscope.catala_en | 8 +- .../good/let_in.catala_en | 18 +-- .../good/out_of_order.catala_en | 15 +- .../good/toplevel_defs.catala_en | 14 +- tests/test_scope/good/scope_call2.catala_en | 8 +- tests/test_scope/good/scope_call3.catala_en | 46 +++--- tests/test_scope/good/simple.catala_en | 4 +- tests/test_struct/good/nested3.catala_en | 32 ++-- .../good/same_name_fields.catala_en | 4 +- tests/test_struct/good/simple.catala_en | 4 +- 20 files changed, 276 insertions(+), 217 deletions(-) diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index 4b2ac627..c7f55348 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -40,7 +40,7 @@ let base_type (fmt : Format.formatter) (s : string) : unit = Cli.format_with_style [ANSITerminal.yellow] fmt s let punctuation (fmt : Format.formatter) (s : string) : unit = - Cli.format_with_style [ANSITerminal.cyan] fmt s + Format.pp_print_as fmt 1 (Cli.with_style [ANSITerminal.cyan] "%s" s) let op_style (fmt : Format.formatter) (s : string) : unit = Cli.format_with_style [ANSITerminal.green] fmt s @@ -72,6 +72,10 @@ let enum_constructor (fmt : Format.formatter) (c : EnumConstructor.t) : unit = Cli.format_with_style [ANSITerminal.magenta] fmt (Format.asprintf "%a" EnumConstructor.format_t c) +let struct_field (fmt : Format.formatter) (c : StructField.t) : unit = + Cli.format_with_style [ANSITerminal.magenta] fmt + (Format.asprintf "%a" StructField.format_t c) + let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit = let typ = typ ctx in let typ_with_parens (fmt : Format.formatter) (t : typ) = @@ -82,11 +86,35 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit = | TTuple ts -> Format.fprintf fmt "@[(%a)@]" (Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " op_style "*") + ~pp_sep:(fun fmt () -> Format.fprintf fmt " %a@ " op_style "*") typ) ts - | TStruct s -> Format.fprintf fmt "@[%a@]" StructName.format_t s - | TEnum e -> Format.fprintf fmt "@[%a@]" EnumName.format_t e + | TStruct s -> ( + match ctx with + | None -> StructName.format_t fmt s + | Some ctx -> + Format.fprintf fmt "@[%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) -> + Format.fprintf fmt "%a%a@ %a" struct_field field punctuation ":" + typ mty)) + (StructField.Map.bindings (StructName.Map.find s ctx.ctx_structs)) + punctuation "}") + | TEnum e -> ( + match ctx with + | None -> Format.fprintf fmt "@[%a@]" EnumName.format_t e + | Some ctx -> + Format.fprintf fmt "@[%a%a%a%a@]" EnumName.format_t e punctuation + "[" + (Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " punctuation "|") + (fun fmt (case, mty) -> + Format.fprintf fmt "%a%a@ %a" enum_constructor case punctuation ":" + typ mty)) + (EnumConstructor.Map.bindings (EnumName.Map.find e ctx.ctx_enums)) + punctuation "]") | TOption t -> Format.fprintf fmt "@[%a@ %a@]" base_type "option" typ t | TArrow ([t1], t2) -> Format.fprintf fmt "@[%a@ %a@ %a@]" typ_with_parens t1 op_style "→" @@ -326,7 +354,7 @@ module Precedence = struct let needs_parens ~context ?(rhs = false) e = match expr context, expr e with | _, Contained -> false - | Dot, Dot -> not rhs + | Dot, Dot -> rhs | _, Dot -> false | Dot, _ -> true | App, App -> not rhs @@ -347,7 +375,7 @@ module Precedence = struct | (Mul | Div), (Add | Sub) -> true | Mul, (Mul | Div) -> false | Div, (Mul | Div) -> rhs) - | Op _, App -> false + | Op _, App -> not rhs | Op _, _ -> true | Contained, _ -> false end @@ -412,30 +440,48 @@ let rec expr_aux : ~pp_sep:(fun fmt () -> Format.fprintf fmt "") (fun fmt (x, tau, arg) -> Format.fprintf fmt - "@[@[@[%a@ %a@ %a@ %a@ %a@]@ %a@]@ %a@]@\n" - keyword "let" var x punctuation ":" (typ ctx) tau punctuation "=" + "@[@[%a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]@\n" keyword + "let" var x punctuation ":" (typ None) tau punctuation "=" (expr colors) arg keyword "in")) xs_tau_arg (rhs expr) body | EAbs { binder; tys } -> let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in let expr = exprb bnd_ctx in let xs_tau = List.mapi (fun i tau -> xs.(i), tau) tys in - Format.fprintf fmt "@[%a @[%a@] %a@ %a@]" punctuation "λ" - (Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") - (fun fmt (x, tau) -> - Format.fprintf fmt "%a%a%a %a%a" punctuation "(" var x punctuation - ":" (typ ctx) tau punctuation ")")) + Format.fprintf fmt "@[@[%a @[%a@]@ @]%a@ %a@]" punctuation + "λ" + (Format.pp_print_list ~pp_sep:Format.pp_print_space (fun fmt (x, tau) -> + punctuation fmt "("; + Format.pp_open_hvbox fmt 2; + var fmt x; + punctuation fmt ":"; + Format.pp_print_space fmt (); + typ None fmt tau; + Format.pp_close_box fmt (); + punctuation fmt ")")) xs_tau punctuation "→" (rhs expr) body | EApp { f = EOp { op = (Map | Filter) as op; _ }, _; args = [arg1; arg2] } -> - Format.fprintf fmt "@[%a@ %a@ %a@]" operator op (lhs exprc) arg1 - (rhs exprc) arg2 - | EApp { f = EOp { op = (And | Or) as op; _ }, _; args = [arg1; arg2] } -> - Format.fprintf fmt "@[%a@ %a %a@]" (lhs exprc) arg1 operator op - (rhs exprc) arg2 - | EApp { f = EOp { op; _ }, _; args = [arg1; arg2] } -> - Format.fprintf fmt "@[%a@ %a %a@]" (lhs exprc) arg1 operator op + Format.fprintf fmt "@[%a %a@ %a@]" operator op (lhs exprc) arg1 (rhs exprc) arg2 + | EApp { f = EOp { op = op0; _ }, _; args = [_; _] } -> + let prec = Precedence.expr e in + let rec pr colors fmt = function + (* Flatten sequences of the same associative op *) + | EApp { f = EOp { op; _ }, _; args = [arg1; arg2] }, _ when op = op0 -> ( + (match prec with + | Op (And | Or | Mul | Add | Div | Sub) -> lhs pr fmt arg1 + | _ -> lhs exprc fmt arg1); + Format.pp_print_space fmt (); + operator fmt op; + Format.pp_print_char fmt ' '; + match prec with + | Op (And | Or | Mul | Add) -> rhs pr fmt arg2 + | _ -> rhs exprc fmt arg2) + | e -> exprc colors fmt e + in + Format.pp_open_hvbox fmt 0; + pr colors fmt e; + Format.pp_close_box fmt () | EApp { f = EOp { op; _ }, _; args = [arg1] } -> Format.fprintf fmt "@[%a@ %a@]" operator op (rhs exprc) arg1 | EApp { f; args } -> @@ -445,23 +491,20 @@ let rec expr_aux : (rhs exprc)) args | EIfThenElse _ -> - Format.pp_open_hvbox fmt 0; let rec pr els fmt = function | EIfThenElse { cond; etrue; efalse }, _ -> - Format.fprintf fmt - "@[%a@ %a@]@ @[%a@ %a@]@ %a@]" - keyword (if els then "else if" else "if") - expr cond keyword "then" expr etrue - (pr true) efalse - | e -> - Format.fprintf fmt "@[%a@ %a@]" keyword "else" (rhs exprc) e + Format.fprintf fmt "@[%a@ %a@]@ @[%a@ %a@]@ %a" keyword + (if els then "else if" else "if") + expr cond keyword "then" expr etrue (pr true) efalse + | e -> Format.fprintf fmt "@[%a@ %a@]" keyword "else" (rhs exprc) e in + Format.pp_open_hvbox fmt 0; pr false fmt e; Format.pp_close_box fmt () | EOp { op; _ } -> operator fmt op | EDefault { excepts; just; cons } -> if List.length excepts = 0 then - Format.fprintf fmt "@[%a%a@ %a@ %a%a@]" punctuation "⟨" expr just + Format.fprintf fmt "@[%a%a@ %a %a%a@]" punctuation "⟨" expr just punctuation "⊢" expr cons punctuation "⟩" else Format.fprintf fmt @@ -487,30 +530,42 @@ let rec expr_aux : Format.fprintf fmt "@[%a%a@,%a%a%a@]" (lhs exprc) e punctuation "." punctuation "\"" IdentName.format_t field punctuation "\"" | EStruct { name; fields } -> - Format.fprintf fmt "@[@[%a@,@[%a@]@]@,%a%a@]" punctuation - "{" - (Format.pp_print_list - ~pp_sep:(fun fmt () -> punctuation fmt ";") - (fun fmt (field_name, field_expr) -> - Format.fprintf fmt "@ @[%a%a%a %a@ %a@]" punctuation "\"" - StructField.format_t field_name punctuation "\"" punctuation "=" - (lhs exprc) field_expr)) - (StructField.Map.bindings fields) - punctuation "}_" StructName.format_t name + if StructField.Map.is_empty fields then ( + punctuation fmt "{"; + StructName.format_t fmt name; + punctuation fmt "}") + else + Format.fprintf fmt "@[%a %a@ %a@;<1 -2>%a@]" punctuation "{" + StructName.format_t name + (Format.pp_print_list ~pp_sep:Format.pp_print_space + (fun fmt (field_name, field_expr) -> + Format.fprintf fmt "@[%a %a@ %a%a@]" struct_field field_name + punctuation "=" (lhs exprc) field_expr punctuation ";")) + (StructField.Map.bindings fields) + punctuation "}" | EStructAccess { e; field; _ } -> - Format.fprintf fmt "@[%a%a@,%a%a%a@]" (lhs exprc) e punctuation "." - punctuation "\"" StructField.format_t field punctuation "\"" + Format.fprintf fmt "@[%a%a@,%a@]" (lhs exprc) e punctuation "." + struct_field field | EInj { e; cons; _ } -> Format.fprintf fmt "@[%a@ %a@]" EnumConstructor.format_t cons (rhs exprc) e | EMatch { e; cases; _ } -> - Format.fprintf fmt "@[@[%a@ %a@]@ %a@ %a@]" keyword "match" + Format.fprintf fmt "@[@[%a@ %a@ %a@]@ %a@]" keyword "match" (lhs exprc) e keyword "with" (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n") (fun fmt (cons_name, case_expr) -> - Format.fprintf fmt "@[%a %a@ %a@ %a@]" punctuation "|" - enum_constructor cons_name punctuation "→" (rhs exprc) case_expr)) + match case_expr with + | EAbs { binder; _ }, _ -> + let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in + let expr = exprb bnd_ctx in + Format.fprintf fmt "@[%a %a@ %a@ %a@ %a@]" punctuation "|" + enum_constructor cons_name + (Format.pp_print_seq ~pp_sep:Format.pp_print_space var) + (Array.to_seq xs) punctuation "→" (rhs expr) body + | e -> + Format.fprintf fmt "@[%a %a@ %a@ %a@]" punctuation "|" + enum_constructor cons_name punctuation "→" (rhs exprc) e)) (EnumConstructor.Map.bindings cases) | EScopeCall { scope; args } -> Format.pp_open_hovbox fmt 2; diff --git a/compiler/shared_ast/print.mli b/compiler/shared_ast/print.mli index f23726c8..617d13f0 100644 --- a/compiler/shared_ast/print.mli +++ b/compiler/shared_ast/print.mli @@ -23,7 +23,11 @@ open Definitions val base_type : Format.formatter -> string -> unit val keyword : Format.formatter -> string -> unit + val punctuation : Format.formatter -> string -> unit +(** The argument is assumed to be 1-column wide (but can be a multi-char utf8 + character) *) + val op_style : Format.formatter -> string -> unit val lit_style : Format.formatter -> string -> unit diff --git a/tests/test_array/good/aggregation_2.catala_en b/tests/test_array/good/aggregation_2.catala_en index a19bf596..f2883507 100644 --- a/tests/test_array/good/aggregation_2.catala_en +++ b/tests/test_array/good/aggregation_2.catala_en @@ -33,31 +33,29 @@ scope B: $ catala Interpret -s A [RESULT] Computation successful! Results: [RESULT] x = - [ { "id" = 0; "income" = $0.00}_S; - { "id" = 1; "income" = $9.00}_S; - { "id" = 2; "income" = $5.20}_S ] + [ { S id = 0; income = $0.00; }; + { S id = 1; income = $9.00; }; + { S id = 2; income = $5.20; } ] ``` ```catala-test-inline $ catala Interpret -s B [RESULT] Computation successful! Results: -[RESULT] argmax = { "id" = 1; "income" = $9.00}_S -[RESULT] argmin = { "id" = 0; "income" = $0.00}_S +[RESULT] argmax = { S id = 1; income = $9.00; } +[RESULT] argmin = { S id = 0; income = $0.00; } ``` ```catala-test-inline $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] x = ESome - [ ESome - { "id" = ESome 0; "income" = ESome $0.00}_S; - ESome - { "id" = ESome 1; "income" = ESome $9.00}_S; - ESome - { "id" = ESome 2; "income" = ESome $5.20}_S ] +[RESULT] x = + ESome + [ ESome { S id = ESome 0; income = ESome $0.00; }; + ESome { S id = ESome 1; income = ESome $9.00; }; + ESome { S id = ESome 2; income = ESome $5.20; } ] ``` ```catala-test-inline $ catala Interpret_Lcalc -s B --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] argmax = ESome { "id" = ESome 1; "income" = ESome $9.00}_S -[RESULT] argmin = ESome { "id" = ESome 0; "income" = ESome $0.00}_S +[RESULT] argmax = ESome { S id = ESome 1; income = ESome $9.00; } +[RESULT] argmin = ESome { S id = ESome 0; income = ESome $0.00; } ``` diff --git a/tests/test_array/good/aggregation_3.catala_en b/tests/test_array/good/aggregation_3.catala_en index ef2ec4cd..b3924ff5 100644 --- a/tests/test_array/good/aggregation_3.catala_en +++ b/tests/test_array/good/aggregation_3.catala_en @@ -35,47 +35,47 @@ scope S: $ catala scopelang -s S let scope S (x: integer|internal|output) = let x : integer = ⟨true ⊢ 0⟩; - assert reduce - (λ (i_1: integer) (i_2: integer) → - if - let i : integer = i_1 in - to_rat_int ((2 -! i) *! (2 -! i)) - <. let i : integer = i_2 in - to_rat_int ((2 -! i) *! (2 -! i)) - then i_1 - else i_2), - 42, - [ 1; 2; 3 ] + assert (reduce + (λ (i_1: integer) (i_2: integer) → + if + (let i : integer = i_1 in + to_rat_int ((2 -! i) *! (2 -! i))) + <. let i : integer = i_2 in + to_rat_int ((2 -! i) *! (2 -! i)) + then i_1 + else i_2), + 42, + [ 1; 2; 3 ]) = 2; - assert reduce - (λ (max1: decimal) (max2: decimal) → - if max1 >. max2 then max1 else max2), - 10., - map (λ (i: integer) → to_rat_int i) [ 1; 2; 3 ] + assert (reduce + (λ (max1: decimal) (max2: decimal) → + if max1 >. max2 then max1 else max2), + 10., + map (λ (i: integer) → to_rat_int i) [ 1; 2; 3 ]) = 3.; - assert reduce - (λ (max1: integer) (max2: integer) → - if max1 >! max2 then max1 else max2), - 10, - [ 1; 2; 3 ] + assert (reduce + (λ (max1: integer) (max2: integer) → + if max1 >! max2 then max1 else max2), + 10, + [ 1; 2; 3 ]) = 3; - assert length filter (λ (i: integer) → i >=! 2) [ 1; 2; 3 ] = 2; - assert length [ 1; 2; 3 ] = 3; - assert reduce - (λ (sum1: integer) (sum2: integer) → sum1 +! sum2), - 0, - map (λ (i: integer) → i +! 2) [ 1; 2; 3 ] + assert (length filter (λ (i: integer) → i >=! 2) [ 1; 2; 3 ]) = 2; + assert (length [ 1; 2; 3 ]) = 3; + assert (reduce + (λ (sum1: integer) (sum2: integer) → sum1 +! sum2), + 0, + map (λ (i: integer) → i +! 2) [ 1; 2; 3 ]) = 12; - assert reduce - (λ (sum1: integer) (sum2: integer) → sum1 +! sum2), - 0, - [ 1; 2; 3 ] + assert (reduce + (λ (sum1: integer) (sum2: integer) → sum1 +! sum2), + 0, + [ 1; 2; 3 ]) = 6; - assert map (λ (i: integer) → i +! 2) - filter (λ (i: integer) → i >! 2) [ 1; 2; 3 ] + assert (map (λ (i: integer) → i +! 2) + filter (λ (i: integer) → i >! 2) [ 1; 2; 3 ]) = [ 5 ]; - assert filter (λ (i: integer) → i >=! 2) [ 1; 2; 3 ] = [ 2; 3 ]; - assert map (λ (i: integer) → i +! 2) [ 1; 2; 3 ] = [ 3; 4; 5 ] + assert (filter (λ (i: integer) → i >=! 2) [ 1; 2; 3 ]) = [ 2; 3 ]; + assert (map (λ (i: integer) → i +! 2) [ 1; 2; 3 ]) = [ 3; 4; 5 ] ``` ```catala-test-inline diff --git a/tests/test_bool/good/test_bool.catala_en b/tests/test_bool/good/test_bool.catala_en index a93f3690..623dc41a 100644 --- a/tests/test_bool/good/test_bool.catala_en +++ b/tests/test_bool/good/test_bool.catala_en @@ -15,20 +15,16 @@ scope TestBool: $ catala Dcalc let TestBool : TestBool_in → TestBool = λ (TestBool_in: TestBool_in) → - let foo : unit → bool = TestBool_in."foo_in" in - let bar : unit → integer = TestBool_in."bar_in" in - let bar1 : integer = - error_empty ⟨ bar () | true ⊢ ⟨true ⊢ 1⟩ ⟩ - in - let foo1 : bool = - error_empty - ⟨ foo () - | true - ⊢ ⟨true ⊢ - ⟨ ⟨bar1 >=! 0 ⊢ true⟩, ⟨bar1 =! 0 ⊢ true⟩, ⟨bar1 =! 0 ⊢ true⟩, ⟨bar =! 0 ⊢ true⟩, ⟨bar ! 0 ⊢ x -! 1⟩; + let a.f : integer → integer = λ (x: integer) → ⟨b && x >! 0 ⊢ x -! 1⟩; call A[a] ``` @@ -39,12 +38,11 @@ $ catala Dcalc -s A 5 │ context f content integer depends on x content integer │ ‾ └─ Test -let scope A (A_in: A_in): A = - let get f : integer → integer = A_in."f_in" in +let scope A (A_in: A_in {f_in: integer → integer}): A {} = + let get f : integer → integer = A_in.f_in in let set f : integer → integer = - λ (x: integer) → - error_empty ⟨ f x | true ⊢ ⟨true ⊢ x +! 1⟩ ⟩ in - return {}_A + λ (x: integer) → error_empty ⟨ f x | true ⊢ ⟨true ⊢ x +! 1⟩ ⟩ in + return {A} ``` ```catala-test-inline @@ -56,10 +54,10 @@ $ catala Dcalc -s B 5 │ context f content integer depends on x content integer │ ‾ └─ Test -let scope B (B_in: B_in): B = - let get b : bool = B_in."b_in" in +let scope B (B_in: B_in {b_in: bool}): B {} = + let get b : bool = B_in.b_in in let sub_set a.f : integer → integer = λ (x: integer) → ⟨b && x >! 0 ⊢ x -! 1⟩ in - let call result : A = A { "f_in" = a.f}_A_in in - return {}_B + let call result : A {} = A { A_in f_in = a.f; } in + return {B} ``` diff --git a/tests/test_io/good/all_io.catala_en b/tests/test_io/good/all_io.catala_en index af7ba186..a0216541 100644 --- a/tests/test_io/good/all_io.catala_en +++ b/tests/test_io/good/all_io.catala_en @@ -19,18 +19,31 @@ scope A: ```catala-test-inline $ catala Dcalc -s A -let scope A (A_in: A_in): A = - let get c : integer = A_in."c_in" in - let get d : integer = A_in."d_in" in - let get e : unit → integer = A_in."e_in" in - let get f : unit → integer = A_in."f_in" in +let scope A (A_in: A_in + {c_in: + integer; + d_in: + integer; + e_in: + unit → integer; + f_in: + unit → integer}): A + {b: + integer; + d: + integer; + f: + integer} = + let get c : integer = A_in.c_in in + let get d : integer = A_in.d_in in + let get e : unit → integer = A_in.e_in in + let get f : unit → integer = A_in.f_in in let set a : integer = error_empty ⟨true ⊢ 0⟩ in let set b : integer = error_empty ⟨true ⊢ a +! 1⟩ in let set e : integer = error_empty ⟨ e () | true ⊢ ⟨true ⊢ b +! c +! d +! 1⟩ ⟩ in - let set f : integer = - error_empty ⟨ f () | true ⊢ ⟨true ⊢ e +! 1⟩ ⟩ in - return { "b" = b; "d" = d; "f" = f}_A + let set f : integer = error_empty ⟨ f () | true ⊢ ⟨true ⊢ e +! 1⟩ ⟩ in + return { A b = b; d = d; f = f; } ``` ```catala-test-inline diff --git a/tests/test_io/good/condition_only_input.catala_en b/tests/test_io/good/condition_only_input.catala_en index cc72e1bc..4a1782b5 100644 --- a/tests/test_io/good/condition_only_input.catala_en +++ b/tests/test_io/good/condition_only_input.catala_en @@ -16,12 +16,12 @@ scope B: ``` ```catala-test-inline $ catala Dcalc -s B -let scope B (B_in: B_in): B = +let scope B (B_in: B_in {}): B {} = let sub_set a.x : bool = error_empty ⟨true ⊢ false⟩ in - let call result : A = A { "x_in" = a.x}_A_in in - let sub_get a.y : integer = result."y" in + let call result : A {y: integer} = A { A_in x_in = a.x; } in + let sub_get a.y : integer = result.y in let assert _ : unit = assert (error_empty (a.y = 1)) in - return {}_B + return {B} ``` ```catala-test-inline diff --git a/tests/test_io/good/subscope.catala_en b/tests/test_io/good/subscope.catala_en index 9abf989a..8efd0827 100644 --- a/tests/test_io/good/subscope.catala_en +++ b/tests/test_io/good/subscope.catala_en @@ -22,13 +22,13 @@ scope B: ```catala-test-inline $ catala Dcalc -s B -let scope B (B_in: B_in): B = +let scope B (B_in: B_in {}): B {} = let sub_set a.a : unit → integer = λ (_: unit) → ∅ in let sub_set a.b : integer = error_empty ⟨true ⊢ 2⟩ in - let call result : A = A { "a_in" = a.a; "b_in" = a.b}_A_in in - let sub_get a.c : integer = result."c" in + let call result : A {c: integer} = A { A_in a_in = a.a; b_in = a.b; } in + let sub_get a.c : integer = result.c in let assert _ : unit = assert (error_empty (a.c = 1)) in - return {}_B + return {B} ``` ```catala-test-inline diff --git a/tests/test_name_resolution/good/let_in.catala_en b/tests/test_name_resolution/good/let_in.catala_en index 8ac58740..a62f107b 100644 --- a/tests/test_name_resolution/good/let_in.catala_en +++ b/tests/test_name_resolution/good/let_in.catala_en @@ -28,8 +28,8 @@ scope S: ```catala-test-inline $ catala Interpret -s S [RESULT] Computation successful! Results: -[RESULT] a = { "x" = -2.; "y" = { "y" = false; "z" = -1.}_B}_A -[RESULT] b = { "y" = true; "z" = 42.}_B +[RESULT] a = { A x = -2.; y = { B y = false; z = -1.; }; } +[RESULT] b = { B y = true; z = 42.; } ``` ## Check scope of let-in vs scope variable @@ -53,13 +53,13 @@ $ catala Interpret -s S2 ```catala-test-inline $ catala Interpret_Lcalc -s S --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] a = ESome - { - - "x" = ESome -2.; - "y" = ESome { "y" = ESome false; "z" = ESome -1.}_B - }_A -[RESULT] b = ESome { "y" = ESome true; "z" = ESome 42.}_B +[RESULT] a = + ESome + { A + x = ESome -2.; + y = ESome { B y = ESome false; z = ESome -1.; }; + } +[RESULT] b = ESome { B y = ESome true; z = ESome 42.; } ``` ```catala-test-inline $ catala Interpret_Lcalc -s S2 --avoid_exceptions --optimize diff --git a/tests/test_name_resolution/good/out_of_order.catala_en b/tests/test_name_resolution/good/out_of_order.catala_en index 53488d35..94fdead6 100644 --- a/tests/test_name_resolution/good/out_of_order.catala_en +++ b/tests/test_name_resolution/good/out_of_order.catala_en @@ -21,14 +21,17 @@ scope S: ```catala-test-inline $ catala Interpret -s S [RESULT] Computation successful! Results: -[RESULT] a = { "x" = 0; "y" = { "y" = true; "z" = 0.}_B}_A -[RESULT] b = { "y" = true; "z" = 0.}_B +[RESULT] a = { A x = 0; y = { B y = true; z = 0.; }; } +[RESULT] b = { B y = true; z = 0.; } ``` ```catala-test-inline $ catala Interpret_Lcalc -s S --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] a = ESome - { "x" = ESome 0; "y" = ESome { "y" = ESome true; "z" = ESome 0.}_B - }_A -[RESULT] b = ESome { "y" = ESome true; "z" = ESome 0.}_B +[RESULT] a = + ESome + { A + x = ESome 0; + y = ESome { B y = ESome true; z = ESome 0.; }; + } +[RESULT] b = ESome { B y = ESome true; z = ESome 0.; } ``` diff --git a/tests/test_name_resolution/good/toplevel_defs.catala_en b/tests/test_name_resolution/good/toplevel_defs.catala_en index 3bf4fb11..9125aaeb 100644 --- a/tests/test_name_resolution/good/toplevel_defs.catala_en +++ b/tests/test_name_resolution/good/toplevel_defs.catala_en @@ -23,7 +23,7 @@ scope S: $ catala Interpret -s S [RESULT] Computation successful! Results: [RESULT] a = 1946.5744 -[RESULT] b = { "y" = true; "z" = 2091.}_A +[RESULT] b = { A y = true; z = 2091.; } ``` ## Test toplevel function defs @@ -109,7 +109,7 @@ let glob5_6 = glob5_aux_5 () let glob2_10 = A {"y": glob1_2 >=. 30., "z": 123. *. 17.} -let S2_6 (S2_in_11: S2_in) = +let S2_6 (S2_in_11: S2_in {}) = decl temp_a_13 : any; try: decl temp_a_16 : any; @@ -126,7 +126,7 @@ let S2_6 (S2_in_11: S2_in) = a_12 = temp_a_13; return S2 {"a": a_12} -let S3_7 (S3_in_18: S3_in) = +let S3_7 (S3_in_18: S3_in {}) = decl temp_a_20 : any; try: decl temp_a_23 : any; @@ -143,7 +143,7 @@ let S3_7 (S3_in_18: S3_in) = a_19 = temp_a_20; return S3 {"a": a_19} -let S4_8 (S4_in_25: S4_in) = +let S4_8 (S4_in_25: S4_in {}) = decl temp_a_27 : any; try: decl temp_a_30 : any; @@ -160,7 +160,7 @@ let S4_8 (S4_in_25: S4_in) = a_26 = temp_a_27; return S4 {"a": a_26} -let S_9 (S_in_32: S_in) = +let S_9 (S_in_32: S_in {}) = decl temp_a_40 : any; try: decl temp_a_43 : any; @@ -187,7 +187,7 @@ let S_9 (S_in_32: S_in) = with EmptyError: temp_b_35 = dead_value_1; raise NoValueProvided; - decl b_34 : A; + decl b_34 : A {y: bool; z: decimal}; b_34 = temp_b_35; return S {"a": a_33, "b": b_34} ``` @@ -466,7 +466,7 @@ def s(s_in:SIn): $ catala Interpret_Lcalc -s S --avoid_exceptions --optimize [RESULT] Computation successful! Results: [RESULT] a = ESome 1946.5744 -[RESULT] b = ESome { "y" = ESome true; "z" = ESome 2091.}_A +[RESULT] b = ESome { A y = ESome true; z = ESome 2091.; } ``` ```catala-test-inline $ catala Interpret_Lcalc -s S2 --avoid_exceptions --optimize diff --git a/tests/test_scope/good/scope_call2.catala_en b/tests/test_scope/good/scope_call2.catala_en index 82f7920c..c9a86929 100644 --- a/tests/test_scope/good/scope_call2.catala_en +++ b/tests/test_scope/good/scope_call2.catala_en @@ -21,12 +21,12 @@ scope Titi: ```catala-test-inline $ catala Interpret -s Titi [RESULT] Computation successful! Results: -[RESULT] fizz = { "foo" = 1213}_Toto -[RESULT] fuzz = { "foo" = 1323}_Toto +[RESULT] fizz = { Toto foo = 1213; } +[RESULT] fuzz = { Toto foo = 1323; } ``` ```catala-test-inline $ catala Interpret_Lcalc -s Titi --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] fizz = ESome { "foo" = ESome 1213}_Toto -[RESULT] fuzz = ESome { "foo" = ESome 1323}_Toto +[RESULT] fizz = ESome { Toto foo = ESome 1213; } +[RESULT] fuzz = ESome { Toto foo = ESome 1323; } ``` diff --git a/tests/test_scope/good/scope_call3.catala_en b/tests/test_scope/good/scope_call3.catala_en index d037ac42..34a7aab0 100644 --- a/tests/test_scope/good/scope_call3.catala_en +++ b/tests/test_scope/good/scope_call3.catala_en @@ -34,7 +34,7 @@ $ catala Interpret -t -s HousingComputation │ ‾ [LOG] → RentComputation.direct -[LOG] ≔ RentComputation.direct.input: {}_RentComputation_in +[LOG] ≔ RentComputation.direct.input: {RentComputation_in} [LOG] ≔ RentComputation.g: [LOG] ≔ RentComputation.f: [LOG] ☛ Definition applied: @@ -43,7 +43,7 @@ $ catala Interpret -t -s HousingComputation 7 │ definition f of x equals (output of RentComputation).f of x │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾ -[LOG] ≔ RentComputation.direct.output: { "f" = λ (param0: integer) → { "f" = λ (x: integer) → error_empty ⟨true ⊢ (λ (x1: integer) → error_empty ⟨true ⊢ x1 +! 1⟩) (x +! 1)⟩ }_RentComputation."f" param0 }_RentComputation +[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0: integer) → { RentComputation f = λ (x: integer) → error_empty ⟨true ⊢ (λ (x1: integer) → error_empty ⟨true ⊢ x1 +! 1⟩) (x +! 1)⟩; }. f param0; } [LOG] ← RentComputation.direct [LOG] → RentComputation.f [LOG] ≔ RentComputation.f.input0: 1 @@ -71,26 +71,26 @@ $ catala Interpret -t -s HousingComputation [RESULT] Computation successful! Results: [RESULT] f = λ (x: integer) → - error_empty - ⟨true ⊢ - (let result : RentComputation = - (λ (RentComputation_in: RentComputation_in) → - let g : integer → integer = - λ (x1: integer) → - error_empty ⟨true ⊢ x1 +! 1⟩ - in - let f : integer → integer = - λ (x1: integer) → - error_empty ⟨true ⊢ g (x1 +! 1)⟩ - in - { "f" = f}_RentComputation) - {}_RentComputation_in - in - let result1 : RentComputation = - { "f" = λ (param0: integer) → result."f" param0 - }_RentComputation - in - if true then result1 else result1)."f" - x⟩ + error_empty + ⟨true + ⊢ (let result : RentComputation = + (λ (RentComputation_in: RentComputation_in) → + let g : integer → integer = + λ (x1: integer) → error_empty ⟨true ⊢ x1 +! 1⟩ + in + let f : integer → integer = + λ (x1: integer) → error_empty ⟨true ⊢ g (x1 +! 1)⟩ + in + { RentComputation f = f; }) + {RentComputation_in} + in + let result1 : RentComputation = + { RentComputation + f = λ (param0: integer) → result.f param0; + } + in + if true then result1 else result1). + f + x⟩ [RESULT] result = 3 ``` diff --git a/tests/test_scope/good/simple.catala_en b/tests/test_scope/good/simple.catala_en index 17bd294a..dc68e0fb 100644 --- a/tests/test_scope/good/simple.catala_en +++ b/tests/test_scope/good/simple.catala_en @@ -10,9 +10,9 @@ scope Foo: ```catala-test-inline $ catala Lcalc -s Foo -let scope Foo (Foo_in: Foo_in): Foo = +let scope Foo (Foo_in: Foo_in {}): Foo {bar: integer} = let set bar : integer = try handle_default [ ], (λ (_: unit) → true), (λ (_: unit) → 0) with EmptyError -> raise NoValueProvided in - return { "bar" = bar}_Foo + return { Foo bar = bar; } ``` diff --git a/tests/test_struct/good/nested3.catala_en b/tests/test_struct/good/nested3.catala_en index cdc5912a..fd87218f 100644 --- a/tests/test_struct/good/nested3.catala_en +++ b/tests/test_struct/good/nested3.catala_en @@ -37,37 +37,33 @@ scope B: ```catala-test-inline $ catala Interpret -s A [RESULT] Computation successful! Results: -[RESULT] t = - { "a" = { "x" = 0; "y" = false}_S; "b" = { "x" = 1; "y" = true}_S - }_T +[RESULT] t = { T a = { S x = 0; y = false; }; b = { S x = 1; y = true; }; } ``` ```catala-test-inline $ catala Interpret -s B [RESULT] Computation successful! Results: [RESULT] out = 1 -[RESULT] t = - { "a" = { "x" = 0; "y" = false}_S; "b" = { "x" = 1; "y" = true}_S - }_T +[RESULT] t = { T a = { S x = 0; y = false; }; b = { S x = 1; y = true; }; } ``` ```catala-test-inline $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] t = ESome - { - - "a" = ESome { "x" = ESome 0; "y" = ESome false}_S; - "b" = ESome { "x" = ESome 1; "y" = ESome true}_S - }_T +[RESULT] t = + ESome + { T + a = ESome { S x = ESome 0; y = ESome false; }; + b = ESome { S x = ESome 1; y = ESome true; }; + } ``` ```catala-test-inline $ catala Interpret_Lcalc -s B --avoid_exceptions --optimize [RESULT] Computation successful! Results: [RESULT] out = ESome 1 -[RESULT] t = ESome - { - - "a" = ESome { "x" = ESome 0; "y" = ESome false}_S; - "b" = ESome { "x" = ESome 1; "y" = ESome true}_S - }_T +[RESULT] t = + ESome + { T + a = ESome { S x = ESome 0; y = ESome false; }; + b = ESome { S x = ESome 1; y = ESome true; }; + } ``` diff --git a/tests/test_struct/good/same_name_fields.catala_en b/tests/test_struct/good/same_name_fields.catala_en index 81afc769..f203b939 100644 --- a/tests/test_struct/good/same_name_fields.catala_en +++ b/tests/test_struct/good/same_name_fields.catala_en @@ -26,7 +26,7 @@ $ catala Interpret -s A │ ‾‾‾ └─ Article [RESULT] Computation successful! Results: -[RESULT] x = { "f" = 1}_Foo +[RESULT] x = { Foo f = 1; } [RESULT] y = 1 ``` ```catala-test-inline @@ -39,6 +39,6 @@ $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize │ ‾‾‾ └─ Article [RESULT] Computation successful! Results: -[RESULT] x = ESome { "f" = ESome 1}_Foo +[RESULT] x = ESome { Foo f = ESome 1; } [RESULT] y = ESome 1 ``` diff --git a/tests/test_struct/good/simple.catala_en b/tests/test_struct/good/simple.catala_en index 44ce2f27..8532f6fb 100644 --- a/tests/test_struct/good/simple.catala_en +++ b/tests/test_struct/good/simple.catala_en @@ -20,12 +20,12 @@ scope A: ```catala-test-inline $ catala Interpret -s A [RESULT] Computation successful! Results: -[RESULT] s = { "x" = 1; "y" = 2}_S +[RESULT] s = { S x = 1; y = 2; } [RESULT] z = 3 ``` ```catala-test-inline $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] s = ESome { "x" = ESome 1; "y" = ESome 2}_S +[RESULT] s = ESome { S x = ESome 1; y = ESome 2; } [RESULT] z = ESome 3 ``` From c249cef3cc4eedf802bd6647ee55c150d824b820 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Tue, 18 Apr 2023 10:09:58 +0200 Subject: [PATCH 4/7] Printer: flatten nested let-ins too --- compiler/shared_ast/print.ml | 39 ++++++----- tests/test_array/good/concatenation.catala_en | 41 +++++------- tests/test_array/good/fold.catala_en | 26 ++++---- .../good/infinite_precision.catala_en | 5 +- tests/test_func/good/context_func.catala_en | 8 +-- tests/test_scope/good/nothing.catala_en | 2 +- tests/test_scope/good/scope_call3.catala_en | 9 +-- tests/test_scope/good/scope_call4.catala_en | 64 +++++++++---------- 8 files changed, 96 insertions(+), 98 deletions(-) diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index c7f55348..febafa08 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -430,26 +430,33 @@ let rec expr_aux : punctuation fmt "."; Format.pp_print_int fmt index | ELit l -> lit fmt l - | EApp { f = EAbs { binder; tys }, _; args } -> - let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in - let expr = exprb bnd_ctx in - let xs_tau = List.mapi (fun i tau -> xs.(i), tau) tys in - let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in - Format.fprintf fmt "@[%a%a@]" - (Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.fprintf fmt "") - (fun fmt (x, tau, arg) -> - Format.fprintf fmt - "@[@[%a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]@\n" keyword - "let" var x punctuation ":" (typ None) tau punctuation "=" - (expr colors) arg keyword "in")) - xs_tau_arg (rhs expr) body + | EApp { f = EAbs _, _; _ } -> + let rec pr bnd_ctx colors fmt = function + | EApp { f = EAbs { binder; tys }, _; args }, _ -> + let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in + let xs_tau = List.mapi (fun i tau -> xs.(i), tau) tys in + let xs_tau_arg = + List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args + in + Format.pp_print_list + (fun fmt (x, tau, arg) -> + Format.fprintf fmt + "@[@[%a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]" keyword + "let" var x punctuation ":" (typ None) tau punctuation "=" + (exprc colors) arg keyword "in") + fmt xs_tau_arg; + Format.pp_print_cut fmt (); + rhs (pr bnd_ctx) fmt body + | e -> rhs (exprb bnd_ctx) fmt e + in + Format.pp_open_vbox fmt 0; + pr bnd_ctx colors fmt e; + Format.pp_close_box fmt () | EAbs { binder; tys } -> let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in let expr = exprb bnd_ctx in let xs_tau = List.mapi (fun i tau -> xs.(i), tau) tys in - Format.fprintf fmt "@[@[%a @[%a@]@ @]%a@ %a@]" punctuation - "λ" + Format.fprintf fmt "@[%a @[%a@]@ @]%a@ %a" punctuation "λ" (Format.pp_print_list ~pp_sep:Format.pp_print_space (fun fmt (x, tau) -> punctuation fmt "("; Format.pp_open_hvbox fmt 2; diff --git a/tests/test_array/good/concatenation.catala_en b/tests/test_array/good/concatenation.catala_en index 950176a2..b784a07f 100644 --- a/tests/test_array/good/concatenation.catala_en +++ b/tests/test_array/good/concatenation.catala_en @@ -19,29 +19,20 @@ $ catala Interpret -s A ```catala-test-inline $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] x = ESome - [ ESome 0; ESome 1; ESome 2; ESome 3; ESome 4; ESome 5; ESome 6 ] -[RESULT] y = ESome - [ ESome - 0; - ESome - 1; - ESome - 2; - ESome - 3; - ESome - 4; - ESome - 5; - ESome - 6; - ESome - 7; - ESome - 8; - ESome - 9; - ESome - 10 ] +[RESULT] x = + ESome + [ ESome 0; ESome 1; ESome 2; ESome 3; ESome 4; ESome 5; ESome 6 ] +[RESULT] y = + ESome + [ ESome 0; + ESome 1; + ESome 2; + ESome 3; + ESome 4; + ESome 5; + ESome 6; + ESome 7; + ESome 8; + ESome 9; + ESome 10 ] ``` diff --git a/tests/test_array/good/fold.catala_en b/tests/test_array/good/fold.catala_en index a19bf596..f2883507 100644 --- a/tests/test_array/good/fold.catala_en +++ b/tests/test_array/good/fold.catala_en @@ -33,31 +33,29 @@ scope B: $ catala Interpret -s A [RESULT] Computation successful! Results: [RESULT] x = - [ { "id" = 0; "income" = $0.00}_S; - { "id" = 1; "income" = $9.00}_S; - { "id" = 2; "income" = $5.20}_S ] + [ { S id = 0; income = $0.00; }; + { S id = 1; income = $9.00; }; + { S id = 2; income = $5.20; } ] ``` ```catala-test-inline $ catala Interpret -s B [RESULT] Computation successful! Results: -[RESULT] argmax = { "id" = 1; "income" = $9.00}_S -[RESULT] argmin = { "id" = 0; "income" = $0.00}_S +[RESULT] argmax = { S id = 1; income = $9.00; } +[RESULT] argmin = { S id = 0; income = $0.00; } ``` ```catala-test-inline $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] x = ESome - [ ESome - { "id" = ESome 0; "income" = ESome $0.00}_S; - ESome - { "id" = ESome 1; "income" = ESome $9.00}_S; - ESome - { "id" = ESome 2; "income" = ESome $5.20}_S ] +[RESULT] x = + ESome + [ ESome { S id = ESome 0; income = ESome $0.00; }; + ESome { S id = ESome 1; income = ESome $9.00; }; + ESome { S id = ESome 2; income = ESome $5.20; } ] ``` ```catala-test-inline $ catala Interpret_Lcalc -s B --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] argmax = ESome { "id" = ESome 1; "income" = ESome $9.00}_S -[RESULT] argmin = ESome { "id" = ESome 0; "income" = ESome $0.00}_S +[RESULT] argmax = ESome { S id = ESome 1; income = ESome $9.00; } +[RESULT] argmin = ESome { S id = ESome 0; income = ESome $0.00; } ``` diff --git a/tests/test_dec/good/infinite_precision.catala_en b/tests/test_dec/good/infinite_precision.catala_en index 3bd6bba0..c5b3b32c 100644 --- a/tests/test_dec/good/infinite_precision.catala_en +++ b/tests/test_dec/good/infinite_precision.catala_en @@ -26,8 +26,9 @@ $ catala Interpret -s A ```catala-test-inline $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] a = ESome - -0.000000000000000000000000000000000000000000000000000000000078695580959228473468… +[RESULT] a = + ESome + -0.000000000000000000000000000000000000000000000000000000000078695580959228473468… [RESULT] x = ESome 84.64866565265689623 [RESULT] y = ESome -4.3682977870532065498 [RESULT] z = ESome 654265429805103220650980650.570540510654 diff --git a/tests/test_func/good/context_func.catala_en b/tests/test_func/good/context_func.catala_en index 5276a49d..0af5e05c 100644 --- a/tests/test_func/good/context_func.catala_en +++ b/tests/test_func/good/context_func.catala_en @@ -40,8 +40,8 @@ $ catala Dcalc -s A └─ Test let scope A (A_in: A_in {f_in: integer → integer}): A {} = let get f : integer → integer = A_in.f_in in - let set f : integer → integer = - λ (x: integer) → error_empty ⟨ f x | true ⊢ ⟨true ⊢ x +! 1⟩ ⟩ in + let set f : integer → integer = λ (x: integer) → + error_empty ⟨ f x | true ⊢ ⟨true ⊢ x +! 1⟩ ⟩ in return {A} ``` @@ -56,8 +56,8 @@ $ catala Dcalc -s B └─ Test let scope B (B_in: B_in {b_in: bool}): B {} = let get b : bool = B_in.b_in in - let sub_set a.f : integer → integer = - λ (x: integer) → ⟨b && x >! 0 ⊢ x -! 1⟩ in + let sub_set a.f : integer → integer = λ (x: integer) → + ⟨b && x >! 0 ⊢ x -! 1⟩ in let call result : A {} = A { A_in f_in = a.f; } in return {B} ``` diff --git a/tests/test_scope/good/nothing.catala_en b/tests/test_scope/good/nothing.catala_en index 03d2350a..401371bc 100644 --- a/tests/test_scope/good/nothing.catala_en +++ b/tests/test_scope/good/nothing.catala_en @@ -14,7 +14,7 @@ $ catala Scalc -s Foo2 -O -t 5 │ output bar content integer │ ‾‾‾ └─ Test -let Foo2_3 (Foo2_in_2: Foo2_in) = +let Foo2_3 (Foo2_in_2: Foo2_in {}) = decl temp_bar_4 : any; temp_bar_4 = dead_value_1; raise NoValueProvided; diff --git a/tests/test_scope/good/scope_call3.catala_en b/tests/test_scope/good/scope_call3.catala_en index 34a7aab0..a44b3d2b 100644 --- a/tests/test_scope/good/scope_call3.catala_en +++ b/tests/test_scope/good/scope_call3.catala_en @@ -69,17 +69,18 @@ $ catala Interpret -t -s HousingComputation [LOG] ← HousingComputation.f [LOG] ≔ HousingComputation.result: 3 [RESULT] Computation successful! Results: -[RESULT] f = - λ (x: integer) → +[RESULT] f = λ (x: integer) → error_empty ⟨true ⊢ (let result : RentComputation = (λ (RentComputation_in: RentComputation_in) → let g : integer → integer = - λ (x1: integer) → error_empty ⟨true ⊢ x1 +! 1⟩ + λ (x1: integer) → + error_empty ⟨true ⊢ x1 +! 1⟩ in let f : integer → integer = - λ (x1: integer) → error_empty ⟨true ⊢ g (x1 +! 1)⟩ + λ (x1: integer) → + error_empty ⟨true ⊢ g (x1 +! 1)⟩ in { RentComputation f = f; }) {RentComputation_in} diff --git a/tests/test_scope/good/scope_call4.catala_en b/tests/test_scope/good/scope_call4.catala_en index 77807ab0..5c17ed6d 100644 --- a/tests/test_scope/good/scope_call4.catala_en +++ b/tests/test_scope/good/scope_call4.catala_en @@ -25,41 +25,41 @@ scope RentComputation: ```catala-test-inline $ catala Interpret -s RentComputation [RESULT] Computation successful! Results: -[RESULT] f1 = - λ (x: integer) → - error_empty - ⟨true ⊢ - let x1 : integer = x +! 1 in - error_empty ⟨true ⊢ x1 +! 1⟩⟩ -[RESULT] f2 = - λ (x: integer) → - error_empty - ⟨true ⊢ - let x1 : integer = x +! 1 in - error_empty ⟨true ⊢ x1 +! 1⟩⟩ +[RESULT] f1 = λ (x: integer) → + error_empty + ⟨true + ⊢ let x1 : integer = x +! 1 in + error_empty ⟨true ⊢ x1 +! 1⟩⟩ +[RESULT] f2 = λ (x: integer) → + error_empty + ⟨true + ⊢ let x1 : integer = x +! 1 in + error_empty ⟨true ⊢ x1 +! 1⟩⟩ ``` ```catala-test-inline $ catala Interpret_Lcalc -s RentComputation --avoid_exceptions --optimize [RESULT] Computation successful! Results: -[RESULT] f1 = ESome - (λ (x: integer) → ESome - match - (match (ESome (λ (x1: integer) → ESome (x1 +! 1))) - with - | ENone → (λ (_: unit) → ENone _) - | ESome → (λ (f1: any) → f1 (x +! 1))) - with - | ENone → (λ (f1: any) → raise NoValueProvided) - | ESome → (λ (x1: any) → x1)) -[RESULT] f2 = ESome - (λ (x: integer) → ESome - match - (match (ESome (λ (x1: integer) → ESome (x1 +! 1))) - with - | ENone → (λ (_: unit) → ENone _) - | ESome → (λ (f2: any) → f2 (x +! 1))) - with - | ENone → (λ (f2: any) → raise NoValueProvided) - | ESome → (λ (x1: any) → x1)) +[RESULT] f1 = + ESome + (λ (x: integer) → + ESome + match + (match (ESome (λ (x1: integer) → ESome (x1 +! 1))) with + | ENone _ → ENone _ + | ESome f1 → f1 (x +! 1)) + with + | ENone f1 → raise NoValueProvided + | ESome x1 → x1) +[RESULT] f2 = + ESome + (λ (x: integer) → + ESome + match + (match (ESome (λ (x1: integer) → ESome (x1 +! 1))) with + | ENone _ → ENone _ + | ESome f2 → f2 (x +! 1)) + with + | ENone f2 → raise NoValueProvided + | ESome x1 → x1) ``` From 83e7a845fe8ac093b80c0ff24cd05a5e109fdb73 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Tue, 2 May 2023 11:59:39 +0200 Subject: [PATCH 5/7] Cleanup expr printer interface - `Print.expr` no longer needs the context - This removes the need for `expr ~debug` + `expr_debug` ; use `Print.expr` for normal (non-debug) output, and `Print.expr' ?debug ()` for possibly debug output. - This improves consistency of debug expr output in many places - Prints simplified operators (without type suffix) in non-verbose mode (this patch also fixes some cases of `Expr.skip_wrappers` and leverages the binder equality provided by Bindlib) --- compiler/dcalc/invariants.ml | 3 +- compiler/driver.ml | 6 +- compiler/lcalc/compile_without_exceptions.ml | 3 +- compiler/lcalc/to_ocaml.ml | 3 +- compiler/plugins/lazy_interp.ml | 35 ++++---- compiler/scalc/print.ml | 10 +-- compiler/scopelang/print.ml | 12 +-- compiler/shared_ast/expr.ml | 23 ++++-- compiler/shared_ast/expr.mli | 2 +- compiler/shared_ast/interpreter.ml | 40 ++++----- compiler/shared_ast/interpreter.mli | 1 - compiler/shared_ast/operator.ml | 3 +- compiler/shared_ast/optimizations.ml | 12 +-- compiler/shared_ast/print.ml | 82 +++++++++++++++---- compiler/shared_ast/print.mli | 18 ++-- compiler/shared_ast/typing.ml | 2 +- compiler/verification/conditions.ml | 9 +- compiler/verification/io.ml | 2 +- compiler/verification/z3backend.real.ml | 2 +- tests/test_array/good/aggregation_3.catala_en | 28 +++---- tests/test_bool/good/test_bool.catala_en | 4 +- tests/test_func/good/context_func.catala_en | 6 +- tests/test_io/good/all_io.catala_en | 8 +- .../good/toplevel_defs.catala_en | 18 ++-- tests/test_scope/good/scope_call3.catala_en | 6 +- tests/test_scope/good/scope_call4.catala_en | 18 ++-- .../good/subscope.catala_en | 4 +- 27 files changed, 194 insertions(+), 166 deletions(-) diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index d8927285..68b055c6 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -39,8 +39,7 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) : bool = | Fail -> Cli.error_format "%s failed in %s.\n\n %a" name (Pos.to_string_short (Expr.pos e)) - (Print.expr ~debug:true p.decl_ctx) - e; + (Print.expr' ()) e; incr total; false | Pass -> diff --git a/compiler/driver.ml b/compiler/driver.ml index e2e243a7..4f8d215b 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -361,7 +361,7 @@ let driver source_file (options : Cli.options) : int = Shared_ast.Expr.unbox (Shared_ast.Program.to_expr prgm scope_uid) in Format.fprintf fmt "%a\n" - (Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx) + (Shared_ast.Expr.format ~debug:options.debug ()) prgrm_dcalc_expr | ( `Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof | `Plugin _ | `Interpret_Lcalc ) as backend -> ( @@ -408,7 +408,7 @@ let driver source_file (options : Cli.options) : int = List.iter (fun ((var, _), result) -> Cli.result_format "@[%s@ =@ %a@]" var - (Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx) + (Shared_ast.Expr.format ~debug:options.debug ()) result) results | `Plugin (Plugin.Dcalc p) -> @@ -496,7 +496,7 @@ let driver source_file (options : Cli.options) : int = List.iter (fun ((var, _), result) -> Cli.result_format "@[%s@ =@ %a@]" var - (Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx) + (Shared_ast.Expr.format ~debug:options.debug ()) result) results | (`OCaml | `Python | `Scalc | `Plugin _) as backend -> ( diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index f4b9c1d6..1e09b72c 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -342,7 +342,8 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : Errors.raise_internal_error "List operator %a was not fully determined: some partial evaluation was \ found while compiling." - Print.operator op + (Print.operator ~debug:false) + op | EApp { f = EOp { op; tys }, opmark; args } -> let res = Ast.OptionMonad.mmap ~var_name:ctx.ctx_context_name diff --git a/compiler/lcalc/to_ocaml.ml b/compiler/lcalc/to_ocaml.ml index 7ca1f974..bf4fdaf2 100644 --- a/compiler/lcalc/to_ocaml.ml +++ b/compiler/lcalc/to_ocaml.ml @@ -342,7 +342,8 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) : Format.fprintf fmt "@[%a@ @[{filename = \"%s\";@ start_line=%d;@ \ start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a@]" - Print.operator op + (Print.operator ~debug:true) + op (Pos.get_file (Expr.mark_pos pos)) (Pos.get_start_line (Expr.mark_pos pos)) (Pos.get_start_column (Expr.mark_pos pos)) diff --git a/compiler/plugins/lazy_interp.ml b/compiler/plugins/lazy_interp.ml index 1d854242..56e2e625 100644 --- a/compiler/plugins/lazy_interp.ml +++ b/compiler/plugins/lazy_interp.ml @@ -84,9 +84,9 @@ let rec lazy_eval : let r, env1 = lazy_eval ctx env1 llevel e in if not (Expr.equal e r) then ( log "@[{{%a =@ [%a]@ ==> [%a]}}@]" Print.var_debug v - (Print.expr ~debug:true ctx) + (Print.expr' ~debug:true ()) e - (Print.expr ~debug:true ctx) + (Print.expr' ~debug:true ()) r; v_env := r, env1); r, Env.join env env1 @@ -105,12 +105,12 @@ let rec lazy_eval : Seq.fold_left2 (fun env1 var e -> log "@[LET %a = %a@]@ " Print.var_debug var - (Print.expr ~debug:true ctx) + (Print.expr' ~debug:true ()) e; Env.add var e env env1) env (Array.to_seq vars) (List.to_seq args) in - log "@]@[IN [%a]@]" (Print.expr ~debug:true ctx) body; + log "@]@[IN [%a]@]" (Print.expr' ~debug:true ()) body; let e, env = lazy_eval ctx env llevel body in log "@]}"; e, env @@ -131,9 +131,9 @@ let rec lazy_eval : renv := env; e in - Interpreter.evaluate_operator eval ctx op m args, !renv + Interpreter.evaluate_operator eval op m args, !renv (* fixme: this forwards eempty *) - | e, _ -> error e "Invalid apply on %a" (Print.expr ctx) e) + | e, _ -> error e "Invalid apply on %a" Print.expr e) | (EAbs _ | ELit _ | EOp _ | EEmptyError), _ -> e0, env (* these are values *) | (EStruct _ | ETuple _ | EInj _ | EArray _), _ -> if not llevel.eval_struct then e0, env @@ -152,14 +152,14 @@ let rec lazy_eval : match eval_to_value env e with | (EStruct { name = n; fields }, _), env when StructName.equal name n -> lazy_eval ctx env llevel (StructField.Map.find field fields) - | e, _ -> error e "Invalid field access on %a" (Print.expr ctx) e) + | e, _ -> error e "Invalid field access on %a" Print.expr e) | ETupleAccess { e; index; size }, _ -> ( if not llevel.eval_default then e0, env else match eval_to_value env e with | (ETuple es, _), env when List.length es = size -> lazy_eval ctx env llevel (List.nth es index) - | e, _ -> error e "Invalid tuple access on %a" (Print.expr ctx) e) + | e, _ -> error e "Invalid tuple access on %a" Print.expr e) | EMatch { e; name; cases }, _ -> ( if not llevel.eval_default then e0, env else @@ -167,7 +167,7 @@ let rec lazy_eval : | (EInj { name = n; cons; e }, m), env when EnumName.equal name n -> lazy_eval ctx env llevel (EApp { f = EnumConstructor.Map.find cons cases; args = [e] }, m) - | e, _ -> error e "Invalid match argument %a" (Print.expr ctx) e) + | e, _ -> error e "Invalid match argument %a" Print.expr e) | EDefault { excepts; just; cons }, m -> ( let excs = List.filter_map @@ -182,9 +182,9 @@ let rec lazy_eval : match eval_to_value env just with | (ELit (LBool true), _), _ -> lazy_eval ctx env llevel cons | (ELit (LBool false), _), _ -> (EEmptyError, m), env - | e, _ -> error e "Invalid exception justification %a" (Print.expr ctx) e) + | e, _ -> error e "Invalid exception justification %a" Print.expr e) | [(e, env)] -> - log "@[EVAL %a@]" (Print.expr ctx) e; + log "@[EVAL %a@]" Print.expr e; lazy_eval ctx env llevel e | _ :: _ :: _ -> Errors.raise_multispanned_error @@ -195,21 +195,20 @@ let rec lazy_eval : match eval_to_value env cond with | (ELit (LBool true), _), _ -> lazy_eval ctx env llevel etrue | (ELit (LBool false), _), _ -> lazy_eval ctx env llevel efalse - | e, _ -> error e "Invalid condition %a" (Print.expr ctx) e) + | e, _ -> error e "Invalid condition %a" Print.expr e) | EErrorOnEmpty e, _ -> ( match eval_to_value env e ~eval_default:false with | ((EEmptyError, _) as e'), _ -> (* This does _not_ match the eager semantics ! *) - error e' "This value is undefined %a" (Print.expr ctx) e + error e' "This value is undefined %a" Print.expr e | e, env -> lazy_eval ctx env llevel e) | EAssert e, m -> ( if noassert then (ELit LUnit, m), env else match eval_to_value env e with | (ELit (LBool true), m), env -> (ELit LUnit, m), env - | (ELit (LBool false), _), _ -> - error e "Assert failure (%a)" (Print.expr ctx) e - | _ -> error e "Invalid assertion condition %a" (Print.expr ctx) e) + | (ELit (LBool false), _), _ -> error e "Assert failure (%a)" Print.expr e + | _ -> error e "Invalid assertion condition %a" Print.expr e) | _ -> . let interpret_program @@ -230,7 +229,7 @@ let interpret_program let { contents = e, env } = Env.find scope_v all_env in let e = Expr.unbox (Expr.remove_logging_calls e) in log "====================="; - log "%a" (Print.expr ~debug:true ctx) e; + log "%a" (Print.expr' ~debug:true ()) e; log "====================="; let m = Marked.get_mark e in let application_arg = @@ -268,6 +267,6 @@ let apply ~source_file ~output_file ~scope prg _type_ordering = ignore output_file; let fmt = Format.std_formatter in let result_expr, _env = interpret_program prg scope in - Print.expr prg.decl_ctx fmt result_expr + Print.expr fmt result_expr let () = Driver.Plugin.register_dcalc ~name ~extension apply diff --git a/compiler/scalc/print.ml b/compiler/scalc/print.ml index 625de1f9..3487d5f1 100644 --- a/compiler/scalc/print.ml +++ b/compiler/scalc/print.ml @@ -68,16 +68,16 @@ let rec format_expr format_expr e | ELit l -> Print.lit fmt l | EApp ((EOp ((Map | Filter) as op), _), [arg1; arg2]) -> - Format.fprintf fmt "@[%a@ %a@ %a@]" Print.operator op + Format.fprintf fmt "@[%a@ %a@ %a@]" (Print.operator ~debug) op format_with_parens arg1 format_with_parens arg2 | EApp ((EOp op, _), [arg1; arg2]) -> Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1 - Print.operator op format_with_parens arg2 + (Print.operator ~debug) op format_with_parens arg2 | EApp ((EOp (Log _), _), [arg1]) when not debug -> Format.fprintf fmt "%a" format_with_parens arg1 | EApp ((EOp op, _), [arg1]) -> - Format.fprintf fmt "@[%a@ %a@]" Print.operator op format_with_parens - arg1 + Format.fprintf fmt "@[%a@ %a@]" (Print.operator ~debug) op + format_with_parens arg1 | EApp (f, []) -> Format.fprintf fmt "@[%a@ ()@]" format_expr f | EApp (f, args) -> Format.fprintf fmt "@[%a@ %a@]" format_expr f @@ -85,7 +85,7 @@ let rec format_expr ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") format_with_parens) args - | EOp op -> Format.fprintf fmt "%a" Print.operator op + | EOp op -> Print.operator ~debug fmt op let rec format_statement (decl_ctx : decl_ctx) diff --git a/compiler/scopelang/print.ml b/compiler/scopelang/print.ml index b7a8c57e..94161fe3 100644 --- a/compiler/scopelang/print.ml +++ b/compiler/scopelang/print.ml @@ -48,7 +48,7 @@ let enum (Print.typ ctx) typ)) (EnumConstructor.Map.bindings cases) -let scope ?(debug = false) ctx fmt (name, decl) = +let scope ?debug ctx fmt (name, decl) = Format.fprintf fmt "@[%a@ %a@ %a@ %a@ %a@]@\n@[ %a@]" Print.keyword "let" Print.keyword "scope" ScopeName.format_t name (Format.pp_print_list ~pp_sep:Format.pp_print_space @@ -77,7 +77,7 @@ let scope ?(debug = false) ctx fmt (name, decl) = (Print.typ ctx) typ Print.punctuation "=" (fun fmt e -> match Marked.unmark loc with - | SubScopeVar _ | ToplevelVar _ -> Print.expr ctx fmt e + | SubScopeVar _ | ToplevelVar _ -> Print.expr' () fmt e | ScopelangScopeVar v -> ( match Marked.unmark @@ -86,12 +86,12 @@ let scope ?(debug = false) ctx fmt (name, decl) = with | Reentrant -> Format.fprintf fmt "%a@ %a" Print.op_style - "reentrant or by default" (Print.expr ~debug ctx) e - | _ -> Format.fprintf fmt "%a" (Print.expr ~debug ctx) e)) + "reentrant or by default" (Print.expr' ?debug ()) e + | _ -> Format.fprintf fmt "%a" (Print.expr' ?debug ()) e)) e | Assertion e -> Format.fprintf fmt "%a %a" Print.keyword "assert" - (Print.expr ~debug ctx) e + (Print.expr' ?debug ()) e | Call (scope_name, subscope_name, _) -> Format.fprintf fmt "%a %a%a%a%a" Print.keyword "call" ScopeName.format_t scope_name Print.punctuation "[" @@ -113,7 +113,7 @@ let print_topdef ctx ppf name (e, ty) = Format.pp_close_box ppf () in Format.pp_print_cut ppf (); - Print.expr ctx ppf e; + Print.expr' () ppf e; Format.pp_close_box ppf () let program ?(debug : bool = false) (fmt : Format.formatter) (p : 'm program) : diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml index a4c859cc..6e4cffea 100644 --- a/compiler/shared_ast/expr.ml +++ b/compiler/shared_ast/expr.ml @@ -536,11 +536,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool = | EArray es1, EArray es2 -> equal_list es1 es2 | ELit l1, ELit l2 -> l1 = l2 | EAbs { binder = b1; tys = tys1 }, EAbs { binder = b2; tys = tys2 } -> - Type.equal_list tys1 tys2 - && - let vars1, body1 = Bindlib.unmbind b1 in - let body2 = Bindlib.msubst b2 (Array.map (fun x -> EVar x) vars1) in - equal body1 body2 + Type.equal_list tys1 tys2 && Bindlib.eq_mbinder equal b1 b2 | EApp { f = e1; args = args1 }, EApp { f = e2; args = args2 } -> equal e1 e2 && equal_list args1 args2 | EAssert e1, EAssert e2 -> equal e1 e2 @@ -702,18 +698,27 @@ let rec free_vars : ('a, 't) gexpr -> ('a, 't) gexpr Var.Set.t = function let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function | EApp { f = EOp { op = Log _; _ }, _; args = [e] }, _ -> skip_wrappers e + | EApp { f = EApp { f = EOp { op = Log _; _ }, _; args = [f] }, _; args }, m + -> + skip_wrappers (EApp { f; args }, m) | EErrorOnEmpty e, _ -> skip_wrappers e + | EDefault { excepts = []; just = ELit (LBool true), _; cons = e }, _ -> + skip_wrappers e | e -> e let remove_logging_calls e = let rec f e = - match Marked.unmark e with - | EApp { f = EOp { op = Log _; _ }, _; args = [arg] } -> map ~f arg - | _ -> map ~f e + let e, m = map ~f e in + ( Bindlib.box_apply + (function + | EApp { f = EOp { op = Log _; _ }, _; args = [(arg, _)] } -> arg + | e -> e) + e, + m ) in f e -let format ?debug decl_ctx ppf e = Print.expr ?debug decl_ctx ppf e +let format ?debug () ppf e = Print.expr' ?debug () ppf e let rec size : type a. (a, 't) gexpr -> int = fun e -> diff --git a/compiler/shared_ast/expr.mli b/compiler/shared_ast/expr.mli index ab4b84b8..6d3e0971 100644 --- a/compiler/shared_ast/expr.mli +++ b/compiler/shared_ast/expr.mli @@ -342,7 +342,7 @@ val remove_logging_calls : val format : ?debug:bool (** [true] for debug printing *) -> - decl_ctx -> + unit -> Format.formatter -> (_, _ mark) gexpr -> unit diff --git a/compiler/shared_ast/interpreter.ml b/compiler/shared_ast/interpreter.ml index 086d4e18..1ea0f751 100644 --- a/compiler/shared_ast/interpreter.ml +++ b/compiler/shared_ast/interpreter.ml @@ -49,7 +49,7 @@ let log_indent = ref 0 different backends: python, ocaml, javascript, and interpreter *) (** {1 Evaluation} *) -let print_log ctx entry infos pos e = +let print_log entry infos pos e = if !Cli.trace_flag then match entry with | VarDef _ -> @@ -60,9 +60,7 @@ let print_log ctx entry infos pos e = (match Marked.unmark e with | EAbs _ -> Cli.with_style [ANSITerminal.green] "" | _ -> - let expr_str = - Format.asprintf "%a" (Expr.format ctx ~debug:false) e - in + let expr_str = Format.asprintf "%a" (Expr.format ()) e in let expr_str = Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*") ~subst:(fun _ -> " ") @@ -91,7 +89,7 @@ exception CatalaException of except (* Todo: this should be handled early when resolving overloads. Here we have proper structural equality, but the OCaml backend for example uses the builtin equality function instead of this. *) -let handle_eq evaluate_operator ctx pos e1 e2 = +let handle_eq evaluate_operator pos e1 e2 = let open Runtime.Oper in match e1, e2 with | ELit LUnit, ELit LUnit -> true @@ -105,7 +103,7 @@ let handle_eq evaluate_operator ctx pos e1 e2 = try List.for_all2 (fun e1 e2 -> - match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with + match Marked.unmark (evaluate_operator Eq pos [e1; e2]) with | ELit (LBool b) -> b | _ -> assert false (* should not happen *)) @@ -115,7 +113,7 @@ let handle_eq evaluate_operator ctx pos e1 e2 = StructName.equal s1 s2 && StructField.Map.equal (fun e1 e2 -> - match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with + match Marked.unmark (evaluate_operator Eq pos [e1; e2]) with | ELit (LBool b) -> b | _ -> assert false (* should not happen *)) @@ -126,7 +124,7 @@ let handle_eq evaluate_operator ctx pos e1 e2 = EnumName.equal en1 en2 && EnumConstructor.equal i1 i2 && - match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with + match Marked.unmark (evaluate_operator Eq pos [e1; e2]) with | ELit (LBool b) -> b | _ -> assert false (* should not happen *) @@ -136,7 +134,6 @@ let handle_eq evaluate_operator ctx pos e1 e2 = (* Call-by-value: the arguments are expected to be already evaluated here *) let rec evaluate_operator evaluate_expr - ctx (op : < overloaded : no ; .. > operator) m args = @@ -167,8 +164,7 @@ let rec evaluate_operator (fun i arg -> ( Some (Format.asprintf "Argument n°%d, value %a" (i + 1) - (Expr.format ctx ~debug:true) - arg), + (Expr.format ()) arg), Expr.pos arg )) args) "Operator applied to the wrong arguments\n\ @@ -183,10 +179,10 @@ let rec evaluate_operator | Length, [(EArray es, _)] -> ELit (LInt (Runtime.integer_of_int (List.length es))) | Log (entry, infos), [e'] -> - print_log ctx entry infos pos e'; + print_log entry infos pos e'; Marked.unmark e' | Eq, [(e1, _); (e2, _)] -> - ELit (LBool (handle_eq (evaluate_operator evaluate_expr) ctx m e1 e2)) + ELit (LBool (handle_eq (evaluate_operator evaluate_expr) m e1 e2)) | Map, [f; (EArray es, _)] -> EArray (List.map @@ -422,7 +418,7 @@ let rec evaluate_expr : "wrong function call, expected %d arguments, got %d" (Bindlib.mbinder_arity binder) (List.length args) - | EOp { op; _ } -> evaluate_operator (evaluate_expr ctx) ctx op m args + | EOp { op; _ } -> evaluate_operator (evaluate_expr ctx) op m args | _ -> Errors.raise_spanned_error pos "function has not been reduced to a lambda at evaluation (should not \ @@ -462,8 +458,7 @@ let rec evaluate_expr : Errors.raise_spanned_error (Expr.pos e) "The expression %a should be a struct %a but is not (should not happen \ if the term was well-typed)" - (Expr.format ctx ~debug:true) - e StructName.format_t s) + (Expr.format ()) e StructName.format_t s) | ETuple es -> Marked.mark m (ETuple (List.map (evaluate_expr ctx) es)) | ETupleAccess { e = e1; index; size } -> ( match evaluate_expr ctx e1 with @@ -472,8 +467,7 @@ let rec evaluate_expr : Errors.raise_spanned_error (Expr.pos e) "The expression %a was expected to be a tuple of size %d (should not \ happen if the term was well-typed)" - (Expr.format ctx ~debug:true) - e size) + (Expr.format ()) e size) | EInj { e; name; cons } -> propagate_empty_error (evaluate_expr ctx e) @@ fun e -> Marked.mark m (EInj { e; name; cons }) @@ -526,13 +520,11 @@ let rec evaluate_expr : args = [((ELit _, _) as e1); ((ELit _, _) as e2)]; } -> Errors.raise_spanned_error (Expr.pos e') - "Assertion failed: %a %a %a" - (Expr.format ctx ~debug:false) - e1 Print.operator op - (Expr.format ctx ~debug:false) - e2 + "Assertion failed: %a %a %a" (Expr.format ()) e1 + (Print.operator ~debug:!Cli.debug_flag) + op (Expr.format ()) e2 | _ -> - Cli.debug_format "%a" (Expr.format ctx) e'; + Cli.debug_format "%a" (Expr.format ()) e'; Errors.raise_spanned_error (Expr.mark_pos m) "Assertion failed") | _ -> Errors.raise_spanned_error (Expr.pos e') diff --git a/compiler/shared_ast/interpreter.mli b/compiler/shared_ast/interpreter.mli index e2a2f872..c78f5760 100644 --- a/compiler/shared_ast/interpreter.mli +++ b/compiler/shared_ast/interpreter.mli @@ -22,7 +22,6 @@ open Definitions val evaluate_operator : ((((_, _) dcalc_lcalc as 'a), 'm mark) gexpr -> ('a, 'm mark) gexpr) -> - decl_ctx -> 'a operator -> 'm mark -> ('a, 'm mark) gexpr list -> diff --git a/compiler/shared_ast/operator.ml b/compiler/shared_ast/operator.ml index 722a798d..6ce21682 100644 --- a/compiler/shared_ast/operator.ml +++ b/compiler/shared_ast/operator.ml @@ -533,7 +533,8 @@ let resolve_overload ctx (op : overloaded t Marked.pos) (operands : typ list) : (Print.typ ctx) ty), Marked.get_mark ty )) operands) - "I don't know how to apply operator %a on types %a" Print.operator + "I don't know how to apply operator %a on types %a" + (Print.operator ~debug:true) (Marked.unmark op) (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf " and@ ") diff --git a/compiler/shared_ast/optimizations.ml b/compiler/shared_ast/optimizations.ml index 33889bd8..909887d4 100644 --- a/compiler/shared_ast/optimizations.ml +++ b/compiler/shared_ast/optimizations.ml @@ -342,10 +342,8 @@ let test_iota_reduction_1 () = \ | B → (λ (x: any) → D x)\n\ after=C\n\ x" - (Format.asprintf "before=%a\nafter=%a" - (Print.expr_debug ~debug:false) - (Expr.unbox matchA) - (Print.expr_debug ~debug:false) + (Format.asprintf "before=%a\nafter=%a" Print.expr (Expr.unbox matchA) + Print.expr (Expr.unbox (optimize_expr { @@ -416,10 +414,8 @@ let test_iota_reduction_2 () = \ with\n\ \ | A → (λ (x: any) → C 20)\n\ \ | B → (λ (x: any) → D B x)\n" - (Format.asprintf "before=@[%a@]@.after=%a@." - (Print.expr_debug ~debug:false) - (Expr.unbox matchA) - (Print.expr_debug ~debug:false) + (Format.asprintf "before=@[%a@]@.after=%a@." Print.expr + (Expr.unbox matchA) Print.expr (Expr.unbox (optimize_expr { diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index febafa08..8c29da62 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -247,8 +247,50 @@ let operator_to_string : type a. a Op.t -> string = | HandleDefault -> "handle_default" | HandleDefaultOpt -> "handle_default_opt" -let operator : type a. Format.formatter -> a operator -> unit = - fun fmt op -> +let operator_to_shorter_string : type a. a Op.t -> string = + let open Op in + function + | Not -> "~" + | Length -> "length" + | GetDay -> "get_day" + | GetMonth -> "get_month" + | GetYear -> "get_year" + | FirstDayOfMonth -> "first_day_of_month" + | LastDayOfMonth -> "last_day_of_month" + | ToRat_int | ToRat_mon | ToRat -> "to_rat" + | ToMoney_rat | ToMoney -> "to_mon" + | Round_rat | Round_mon | Round -> "round" + | Log _ -> "Log" + | Minus_int | Minus_rat | Minus_mon | Minus_dur | Minus -> "-" + | And -> "&&" + | Or -> "||" + | Xor -> "xor" + | Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dur_dur | Eq_dat_dat | Eq -> "=" + | Map -> "map" + | Reduce -> "reduce" + | Concat -> "++" + | Filter -> "filter" + | Add_int_int | Add_rat_rat | Add_mon_mon | Add_dat_dur _ | Add_dur_dur | Add + -> + "+" + | Sub_int_int | Sub_rat_rat | Sub_mon_mon | Sub_dat_dat | Sub_dat_dur + | Sub_dur_dur | Sub -> + "-" + | Mult_int_int | Mult_rat_rat | Mult_mon_rat | Mult_dur_int | Mult -> "*" + | Div_int_int | Div_rat_rat | Div_mon_mon | Div_mon_rat | Div_dur_dur | Div -> + "/" + | Lt_int_int | Lt_rat_rat | Lt_mon_mon | Lt_dur_dur | Lt_dat_dat | Lt -> "<" + | Lte_int_int | Lte_rat_rat | Lte_mon_mon | Lte_dur_dur | Lte_dat_dat | Lte -> + "<=" + | Gt_int_int | Gt_rat_rat | Gt_mon_mon | Gt_dur_dur | Gt_dat_dat | Gt -> ">" + | Gte_int_int | Gte_rat_rat | Gte_mon_mon | Gte_dur_dur | Gte_dat_dat | Gte -> + ">=" + | Fold -> "fold" + | HandleDefault -> "handle_default" + | HandleDefaultOpt -> "handle_default_opt" + +let operator : type a. ?debug:bool -> Format.formatter -> a operator -> unit = + fun ?(debug = true) fmt op -> let open Op in match op with | Log (entry, infos) -> @@ -263,7 +305,9 @@ let operator : type a. Format.formatter -> a operator -> unit = infos (Cli.format_with_style [ANSITerminal.blue]) "}" - | op -> Format.fprintf fmt "%a" op_style (operator_to_string op) + | op -> + op_style fmt + (if debug then operator_to_string op else operator_to_shorter_string op) let except (fmt : Format.formatter) (exn : except) : unit = op_style fmt @@ -382,15 +426,14 @@ end let rec expr_aux : type a. - ?debug:bool -> - decl_ctx option -> + debug:bool -> Bindlib.ctxt -> ANSITerminal.style list -> Format.formatter -> (a, 't) gexpr -> unit = - fun ?(debug = false) ctx bnd_ctx colors fmt e -> - let exprb bnd_ctx colors e = expr_aux ~debug ctx bnd_ctx colors e in + fun ~debug bnd_ctx colors fmt e -> + let exprb bnd_ctx colors e = expr_aux ~debug bnd_ctx colors e in let exprc colors e = exprb bnd_ctx colors e in let expr e = exprc colors e in let var = if debug then var_debug else var in @@ -468,8 +511,10 @@ let rec expr_aux : punctuation fmt ")")) xs_tau punctuation "→" (rhs expr) body | EApp { f = EOp { op = (Map | Filter) as op; _ }, _; args = [arg1; arg2] } -> - Format.fprintf fmt "@[%a %a@ %a@]" operator op (lhs exprc) arg1 - (rhs exprc) arg2 + Format.fprintf fmt "@[%a %a@ %a@]" (operator ~debug) op (lhs exprc) + arg1 (rhs exprc) arg2 + | EApp { f = EOp { op = Log _ as op; _ }, _; args = [arg1] } -> + Format.fprintf fmt "@[%a@ %a@]" (operator ~debug) op (rhs exprc) arg1 | EApp { f = EOp { op = op0; _ }, _; args = [_; _] } -> let prec = Precedence.expr e in let rec pr colors fmt = function @@ -479,7 +524,7 @@ let rec expr_aux : | Op (And | Or | Mul | Add | Div | Sub) -> lhs pr fmt arg1 | _ -> lhs exprc fmt arg1); Format.pp_print_space fmt (); - operator fmt op; + (operator ~debug) fmt op; Format.pp_print_char fmt ' '; match prec with | Op (And | Or | Mul | Add) -> rhs pr fmt arg2 @@ -490,7 +535,7 @@ let rec expr_aux : pr colors fmt e; Format.pp_close_box fmt () | EApp { f = EOp { op; _ }, _; args = [arg1] } -> - Format.fprintf fmt "@[%a@ %a@]" operator op (rhs exprc) arg1 + Format.fprintf fmt "@[%a@ %a@]" (operator ~debug) op (rhs exprc) arg1 | EApp { f; args } -> Format.fprintf fmt "@[%a@ %a@]" (lhs exprc) f (Format.pp_print_list @@ -508,7 +553,7 @@ let rec expr_aux : Format.pp_open_hvbox fmt 0; pr false fmt e; Format.pp_close_box fmt () - | EOp { op; _ } -> operator fmt op + | EOp { op; _ } -> operator ~debug fmt op | EDefault { excepts; just; cons } -> if List.length excepts = 0 then Format.fprintf fmt "@[%a%a@ %a %a%a@]" punctuation "⟨" expr just @@ -604,8 +649,11 @@ let rec colors = let typ_debug = typ None let typ ctx = typ (Some ctx) -let expr_debug ?debug = expr_aux ?debug None Bindlib.empty_ctxt colors -let expr ?debug ctx = expr_aux ?debug (Some ctx) Bindlib.empty_ctxt colors + +let expr' ?(debug = !Cli.debug_flag) () ppf e = + expr_aux ~debug Bindlib.empty_ctxt colors ppf e + +let expr ppf e = expr' ~debug:false () ppf e let scope_let_kind ?debug:(_debug = true) _ctx fmt k = match k with @@ -618,7 +666,7 @@ let scope_let_kind ?debug:(_debug = true) _ctx fmt k = let rec scope_body_expr ?(debug = false) ctx fmt b : unit = match b with - | Result e -> Format.fprintf fmt "%a %a" keyword "return" (expr ~debug ctx) e + | Result e -> Format.fprintf fmt "%a %a" keyword "return" (expr' ~debug ()) e | ScopeLet { scope_let_kind = kind; @@ -633,7 +681,7 @@ let rec scope_body_expr ?(debug = false) ctx fmt b : unit = kind (if debug then var_debug else var) x punctuation ":" (typ ctx) scope_let_typ punctuation "=" - (expr ~debug ctx) scope_let_expr keyword "in" + (expr' ~debug ()) scope_let_expr keyword "in" (scope_body_expr ~debug ctx) next @@ -734,7 +782,7 @@ let code_item ?(debug = false) decl_ctx fmt c = | Topdef (n, ty, e) -> Format.fprintf fmt "@[%a %a %a %a %a %a @]" keyword "let topval" TopdefName.format_t n op_style ":" (typ decl_ctx) ty op_style "=" - (expr ~debug decl_ctx) e + (expr' ~debug ()) e let rec code_item_list ?(debug = false) decl_ctx fmt c = match c with diff --git a/compiler/shared_ast/print.mli b/compiler/shared_ast/print.mli index 617d13f0..96727801 100644 --- a/compiler/shared_ast/print.mli +++ b/compiler/shared_ast/print.mli @@ -39,27 +39,19 @@ val tlit : Format.formatter -> typ_lit -> unit val location : Format.formatter -> 'a glocation -> unit val typ : decl_ctx -> Format.formatter -> typ -> unit val lit : Format.formatter -> lit -> unit -val operator : Format.formatter -> 'a operator -> unit +val operator : ?debug:bool -> Format.formatter -> 'a operator -> unit val log_entry : Format.formatter -> log_entry -> unit val except : Format.formatter -> except -> unit val var : Format.formatter -> 'e Var.t -> unit val var_debug : Format.formatter -> 'e Var.t -> unit +val expr : Format.formatter -> ('a, 'm mark) gexpr -> unit -val expr : - ?debug:bool (** [true] for debug printing *) -> - decl_ctx -> - Format.formatter -> - ('a, 'm mark) gexpr -> - unit +val expr' : + ?debug:bool -> unit -> Format.formatter -> ('a, 'm mark) gexpr -> unit +(** Same as [expr], but with a debug flag that defaults to [!Cli.debug_flag] *) (** {1 Debugging versions that don't require a context} *) -val expr_debug : - ?debug:bool (** [true] for debug printing *) -> - Format.formatter -> - ('a, 'm mark) gexpr -> - unit - val typ_debug : Format.formatter -> typ -> unit val scope : diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml index 577ae689..4565927c 100644 --- a/compiler/shared_ast/typing.ml +++ b/compiler/shared_ast/typing.ml @@ -394,7 +394,7 @@ and typecheck_expr_top_down : | Some ty -> ty | None -> Errors.raise_spanned_error pos_e "Reference to %a not found" - (Expr.format ctx) e + (Expr.format ()) e in Expr.elocation loc (mark_with_tau_and_unify (ast_to_typ ty)) | A.EStruct { name; fields } -> diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index 1c899772..614e5ee9 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -139,8 +139,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) : "Internal error: this expression does not have the structure expected \ by the VC generator:\n\ %a" - (Expr.format ~debug:true ctx.decl) - e) + (Expr.format ()) e) | EErrorOnEmpty d -> d (* input subscope variables and non-input scope variable *) | _ -> @@ -148,8 +147,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) : "Internal error: this expression does not have the structure expected by \ the VC generator:\n\ %a" - (Expr.format ~debug:true ctx.decl) - e + (Expr.format ()) e (** {1 Verification conditions generator}*) @@ -334,8 +332,7 @@ let rec generate_verification_conditions_scope_body_expr "Internal error: this assertion does not have the structure \ expected by the VC generator:\n\ %a" - (Expr.format ~debug:true ctx.decl) - e) + (Expr.format ()) e) | DestructuringInputStruct -> { ctx with input_vars = scope_let_var :: ctx.input_vars }, [], [] | ScopeVarDefinition | SubScopeVarDefinition -> diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml index 68a3bcd5..7a4c6cdd 100644 --- a/compiler/verification/io.ml +++ b/compiler/verification/io.ml @@ -154,7 +154,7 @@ module MakeBackendIO (B : Backend) = struct | Conditions.NoEmptyError -> "the variable definition never to return an empty error" | NoOverlappingExceptions -> "no two exceptions to ever overlap") - (Expr.format decl_ctx) vc.vc_guard (Expr.format decl_ctx) vc.vc_asserts; + (Expr.format ()) vc.vc_guard (Expr.format ()) vc.vc_asserts; match z3_vc with | Success (encoding, backend_ctx) -> ( diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index c4674d75..ef9e9955 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -434,7 +434,7 @@ let rec translate_op : let ill_formed () = Format.kasprintf failwith "[Z3 encoding] Ill-formed operator application: %a" - (Shared_ast.Expr.format ctx.ctx_decl) + (Shared_ast.Expr.format ()) (Shared_ast.Expr.eapp (Shared_ast.Expr.eop op [] (Untyped { pos = Pos.no_pos })) (List.map Shared_ast.Expr.untype args) diff --git a/tests/test_array/good/aggregation_3.catala_en b/tests/test_array/good/aggregation_3.catala_en index b3924ff5..a052dd5b 100644 --- a/tests/test_array/good/aggregation_3.catala_en +++ b/tests/test_array/good/aggregation_3.catala_en @@ -39,9 +39,9 @@ let scope S (x: integer|internal|output) = (λ (i_1: integer) (i_2: integer) → if (let i : integer = i_1 in - to_rat_int ((2 -! i) *! (2 -! i))) - <. let i : integer = i_2 in - to_rat_int ((2 -! i) *! (2 -! i)) + to_rat ((2 - i) * (2 - i))) + < let i : integer = i_2 in + to_rat ((2 - i) * (2 - i)) then i_1 else i_2), 42, @@ -49,33 +49,33 @@ let scope S (x: integer|internal|output) = = 2; assert (reduce (λ (max1: decimal) (max2: decimal) → - if max1 >. max2 then max1 else max2), + if max1 > max2 then max1 else max2), 10., - map (λ (i: integer) → to_rat_int i) [ 1; 2; 3 ]) + map (λ (i: integer) → to_rat i) [ 1; 2; 3 ]) = 3.; assert (reduce (λ (max1: integer) (max2: integer) → - if max1 >! max2 then max1 else max2), + if max1 > max2 then max1 else max2), 10, [ 1; 2; 3 ]) = 3; - assert (length filter (λ (i: integer) → i >=! 2) [ 1; 2; 3 ]) = 2; + assert (length filter (λ (i: integer) → i >= 2) [ 1; 2; 3 ]) = 2; assert (length [ 1; 2; 3 ]) = 3; assert (reduce - (λ (sum1: integer) (sum2: integer) → sum1 +! sum2), + (λ (sum1: integer) (sum2: integer) → sum1 + sum2), 0, - map (λ (i: integer) → i +! 2) [ 1; 2; 3 ]) + map (λ (i: integer) → i + 2) [ 1; 2; 3 ]) = 12; assert (reduce - (λ (sum1: integer) (sum2: integer) → sum1 +! sum2), + (λ (sum1: integer) (sum2: integer) → sum1 + sum2), 0, [ 1; 2; 3 ]) = 6; - assert (map (λ (i: integer) → i +! 2) - filter (λ (i: integer) → i >! 2) [ 1; 2; 3 ]) + assert (map (λ (i: integer) → i + 2) + filter (λ (i: integer) → i > 2) [ 1; 2; 3 ]) = [ 5 ]; - assert (filter (λ (i: integer) → i >=! 2) [ 1; 2; 3 ]) = [ 2; 3 ]; - assert (map (λ (i: integer) → i +! 2) [ 1; 2; 3 ]) = [ 3; 4; 5 ] + assert (filter (λ (i: integer) → i >= 2) [ 1; 2; 3 ]) = [ 2; 3 ]; + assert (map (λ (i: integer) → i + 2) [ 1; 2; 3 ]) = [ 3; 4; 5 ] ``` ```catala-test-inline diff --git a/tests/test_bool/good/test_bool.catala_en b/tests/test_bool/good/test_bool.catala_en index 623dc41a..a3fcc3b1 100644 --- a/tests/test_bool/good/test_bool.catala_en +++ b/tests/test_bool/good/test_bool.catala_en @@ -22,7 +22,7 @@ let TestBool : TestBool_in → TestBool = error_empty ⟨ foo () | true - ⊢ ⟨true ⊢ ⟨ ⟨bar1 >=! 0 ⊢ true⟩, ⟨bar1 = 0 ⊢ true⟩, ⟨bar1 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩ ⟩ in { TestBool foo = foo1; bar = bar1; } in @@ -46,7 +46,7 @@ struct TestBool = { let scope TestBool (foo: bool|context|output) (bar: integer|context|output) = let bar : integer = reentrant or by default ⟨true ⊢ 1⟩; let foo : bool = reentrant or by default - ⟨true ⊢ ⟨ ⟨bar >=! 0 ⊢ true⟩, ⟨bar = 0 ⊢ true⟩, ⟨bar < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩ ``` ```catala-test-inline $ catala Interpret_Lcalc -s TestBool --avoid_exceptions --optimize diff --git a/tests/test_func/good/context_func.catala_en b/tests/test_func/good/context_func.catala_en index 0af5e05c..783e12ae 100644 --- a/tests/test_func/good/context_func.catala_en +++ b/tests/test_func/good/context_func.catala_en @@ -25,7 +25,7 @@ $ catala Scopelang -s B │ ‾ └─ Test let scope B (b: bool|input) = - let a.f : integer → integer = λ (x: integer) → ⟨b && x >! 0 ⊢ x -! 1⟩; + let a.f : integer → integer = λ (x: integer) → ⟨b && x > 0 ⊢ x - 1⟩; call A[a] ``` @@ -41,7 +41,7 @@ $ catala Dcalc -s A let scope A (A_in: A_in {f_in: integer → integer}): A {} = let get f : integer → integer = A_in.f_in in let set f : integer → integer = λ (x: integer) → - error_empty ⟨ f x | true ⊢ ⟨true ⊢ x +! 1⟩ ⟩ in + error_empty ⟨ f x | true ⊢ ⟨true ⊢ x + 1⟩ ⟩ in return {A} ``` @@ -57,7 +57,7 @@ $ catala Dcalc -s B let scope B (B_in: B_in {b_in: bool}): B {} = let get b : bool = B_in.b_in in let sub_set a.f : integer → integer = λ (x: integer) → - ⟨b && x >! 0 ⊢ x -! 1⟩ in + ⟨b && x > 0 ⊢ x - 1⟩ in let call result : A {} = A { A_in f_in = a.f; } in return {B} ``` diff --git a/tests/test_io/good/all_io.catala_en b/tests/test_io/good/all_io.catala_en index a0216541..9914ed09 100644 --- a/tests/test_io/good/all_io.catala_en +++ b/tests/test_io/good/all_io.catala_en @@ -39,10 +39,10 @@ let scope A (A_in: A_in let get e : unit → integer = A_in.e_in in let get f : unit → integer = A_in.f_in in let set a : integer = error_empty ⟨true ⊢ 0⟩ in - let set b : integer = error_empty ⟨true ⊢ a +! 1⟩ in - let set e : integer = - error_empty ⟨ e () | true ⊢ ⟨true ⊢ b +! c +! d +! 1⟩ ⟩ in - let set f : integer = error_empty ⟨ f () | true ⊢ ⟨true ⊢ e +! 1⟩ ⟩ in + let set b : integer = error_empty ⟨true ⊢ a + 1⟩ in + let set e : integer = error_empty ⟨ e () | true ⊢ ⟨true ⊢ b + c + d + 1⟩ ⟩ + in + let set f : integer = error_empty ⟨ f () | true ⊢ ⟨true ⊢ e + 1⟩ ⟩ in return { A b = b; d = d; f = f; } ``` diff --git a/tests/test_name_resolution/good/toplevel_defs.catala_en b/tests/test_name_resolution/good/toplevel_defs.catala_en index 9125aaeb..4bb45cef 100644 --- a/tests/test_name_resolution/good/toplevel_defs.catala_en +++ b/tests/test_name_resolution/good/toplevel_defs.catala_en @@ -93,28 +93,28 @@ $ catala Interpret -s S4 $ catala scalc let glob1_2 = 44.12 -let glob3_3 (x_3: money) = return to_rat_mon x_3 +. 10. +let glob3_3 (x_3: money) = return to_rat x_3 + 10. -let glob4_4 (x_4: money) (y_5: decimal) = return to_rat_mon x_4 *. y_5 +. 10. +let glob4_4 (x_4: money) (y_5: decimal) = return to_rat x_4 * y_5 + 10. let glob5_aux_5 = decl glob5_7 : any; let glob5_7 (x_8 : decimal) = decl y_9 : decimal; y_9 = 1000.; - return x_8 *. y_9; - return glob5_7 to_rat_int 2 *. 3. + return x_8 * y_9; + return glob5_7 to_rat 2 * 3. let glob5_6 = glob5_aux_5 () -let glob2_10 = A {"y": glob1_2 >=. 30., "z": 123. *. 17.} +let glob2_10 = A {"y": glob1_2 >= 30., "z": 123. * 17.} let S2_6 (S2_in_11: S2_in {}) = decl temp_a_13 : any; try: decl temp_a_16 : any; let temp_a_16 (__17 : unit) = - return glob3_3 $44.00 +. 100.; + return glob3_3 $44.00 + 100.; decl temp_a_14 : any; let temp_a_14 (__15 : unit) = return true; @@ -131,7 +131,7 @@ let S3_7 (S3_in_18: S3_in {}) = try: decl temp_a_23 : any; let temp_a_23 (__24 : unit) = - return 50. +. glob4_4 $44.00 55.; + return 50. + glob4_4 $44.00 55.; decl temp_a_21 : any; let temp_a_21 (__22 : unit) = return true; @@ -148,7 +148,7 @@ let S4_8 (S4_in_25: S4_in {}) = try: decl temp_a_30 : any; let temp_a_30 (__31 : unit) = - return glob5_6 +. 1.; + return glob5_6 + 1.; decl temp_a_28 : any; let temp_a_28 (__29 : unit) = return true; @@ -165,7 +165,7 @@ let S_9 (S_in_32: S_in {}) = try: decl temp_a_43 : any; let temp_a_43 (__44 : unit) = - return glob1_2 *. glob1_2; + return glob1_2 * glob1_2; decl temp_a_41 : any; let temp_a_41 (__42 : unit) = return true; diff --git a/tests/test_scope/good/scope_call3.catala_en b/tests/test_scope/good/scope_call3.catala_en index a44b3d2b..3152c996 100644 --- a/tests/test_scope/good/scope_call3.catala_en +++ b/tests/test_scope/good/scope_call3.catala_en @@ -43,7 +43,7 @@ $ catala Interpret -t -s HousingComputation 7 │ definition f of x equals (output of RentComputation).f of x │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾ -[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0: integer) → { RentComputation f = λ (x: integer) → error_empty ⟨true ⊢ (λ (x1: integer) → error_empty ⟨true ⊢ x1 +! 1⟩) (x +! 1)⟩; }. f param0; } +[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0: integer) → { RentComputation f = λ (x: integer) → error_empty ⟨true ⊢ (λ (x1: integer) → error_empty ⟨true ⊢ x1 + 1⟩) (x + 1)⟩; }. f param0; } [LOG] ← RentComputation.direct [LOG] → RentComputation.f [LOG] ≔ RentComputation.f.input0: 1 @@ -76,11 +76,11 @@ $ catala Interpret -t -s HousingComputation (λ (RentComputation_in: RentComputation_in) → let g : integer → integer = λ (x1: integer) → - error_empty ⟨true ⊢ x1 +! 1⟩ + error_empty ⟨true ⊢ x1 + 1⟩ in let f : integer → integer = λ (x1: integer) → - error_empty ⟨true ⊢ g (x1 +! 1)⟩ + error_empty ⟨true ⊢ g (x1 + 1)⟩ in { RentComputation f = f; }) {RentComputation_in} diff --git a/tests/test_scope/good/scope_call4.catala_en b/tests/test_scope/good/scope_call4.catala_en index 5c17ed6d..d9f97c02 100644 --- a/tests/test_scope/good/scope_call4.catala_en +++ b/tests/test_scope/good/scope_call4.catala_en @@ -27,14 +27,12 @@ $ catala Interpret -s RentComputation [RESULT] Computation successful! Results: [RESULT] f1 = λ (x: integer) → error_empty - ⟨true - ⊢ let x1 : integer = x +! 1 in - error_empty ⟨true ⊢ x1 +! 1⟩⟩ + ⟨true ⊢ let x1 : integer = x + 1 in + error_empty ⟨true ⊢ x1 + 1⟩⟩ [RESULT] f2 = λ (x: integer) → error_empty - ⟨true - ⊢ let x1 : integer = x +! 1 in - error_empty ⟨true ⊢ x1 +! 1⟩⟩ + ⟨true ⊢ let x1 : integer = x + 1 in + error_empty ⟨true ⊢ x1 + 1⟩⟩ ``` ```catala-test-inline @@ -45,9 +43,9 @@ $ catala Interpret_Lcalc -s RentComputation --avoid_exceptions --optimize (λ (x: integer) → ESome match - (match (ESome (λ (x1: integer) → ESome (x1 +! 1))) with + (match (ESome (λ (x1: integer) → ESome (x1 + 1))) with | ENone _ → ENone _ - | ESome f1 → f1 (x +! 1)) + | ESome f1 → f1 (x + 1)) with | ENone f1 → raise NoValueProvided | ESome x1 → x1) @@ -56,9 +54,9 @@ $ catala Interpret_Lcalc -s RentComputation --avoid_exceptions --optimize (λ (x: integer) → ESome match - (match (ESome (λ (x1: integer) → ESome (x1 +! 1))) with + (match (ESome (λ (x1: integer) → ESome (x1 + 1))) with | ENone _ → ENone _ - | ESome f2 → f2 (x +! 1)) + | ESome f2 → f2 (x + 1)) with | ENone f2 → raise NoValueProvided | ESome x1 → x1) diff --git a/tests/test_variable_state/good/subscope.catala_en b/tests/test_variable_state/good/subscope.catala_en index 7b1bc2e8..029e1c7e 100644 --- a/tests/test_variable_state/good/subscope.catala_en +++ b/tests/test_variable_state/good/subscope.catala_en @@ -35,8 +35,8 @@ $ catala Scopelang -s A let scope A (foo_bar: integer|context) (foo_baz: integer|internal) (foo_fizz: integer|internal|output) = let foo_bar : integer = reentrant or by default ⟨true ⊢ 1⟩; - let foo_baz : integer = ⟨true ⊢ foo_bar +! 1⟩; - let foo_fizz : integer = ⟨true ⊢ foo_baz +! 1⟩ + let foo_baz : integer = ⟨true ⊢ foo_bar + 1⟩; + let foo_fizz : integer = ⟨true ⊢ foo_baz + 1⟩ ``` ```catala-test-inline From 5e26c5c83d57c8736f117a1bdbadf30e96fa6903 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Tue, 2 May 2023 16:33:23 +0200 Subject: [PATCH 6/7] Yet more printer improvements - Fix the printer for scopes - Improve the printer for struct types - Remove `Print.expr'`. Use `Expr.format` as the function with simplified arguments instead. --- compiler/dcalc/invariants.ml | 2 +- compiler/driver.ml | 6 +- compiler/lcalc/compile_without_exceptions.ml | 2 +- compiler/plugins/lazy_interp.ml | 33 +++---- compiler/scopelang/print.ml | 10 +- compiler/shared_ast/expr.ml | 2 +- compiler/shared_ast/expr.mli | 9 +- compiler/shared_ast/interpreter.ml | 14 +-- compiler/shared_ast/optimizations.ml | 8 +- compiler/shared_ast/print.ml | 96 ++++++++++++------- compiler/shared_ast/print.mli | 3 +- compiler/shared_ast/typing.ml | 2 +- compiler/verification/conditions.ml | 6 +- compiler/verification/io.ml | 4 +- compiler/verification/z3backend.real.ml | 3 +- tests/test_func/good/context_func.catala_en | 18 ++-- tests/test_io/good/all_io.catala_en | 30 +++--- .../good/condition_only_input.catala_en | 2 +- tests/test_io/good/subscope.catala_en | 2 +- .../good/toplevel_defs.catala_en | 8 +- tests/test_scope/good/nothing.catala_en | 2 +- tests/test_scope/good/simple.catala_en | 5 +- 22 files changed, 143 insertions(+), 124 deletions(-) diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index 68b055c6..f47a86d3 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -39,7 +39,7 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) : bool = | Fail -> Cli.error_format "%s failed in %s.\n\n %a" name (Pos.to_string_short (Expr.pos e)) - (Print.expr' ()) e; + (Print.expr ()) e; incr total; false | Pass -> diff --git a/compiler/driver.ml b/compiler/driver.ml index 4f8d215b..e57e3648 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -361,7 +361,7 @@ let driver source_file (options : Cli.options) : int = Shared_ast.Expr.unbox (Shared_ast.Program.to_expr prgm scope_uid) in Format.fprintf fmt "%a\n" - (Shared_ast.Expr.format ~debug:options.debug ()) + (Shared_ast.Print.expr ~debug:options.debug ()) prgrm_dcalc_expr | ( `Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof | `Plugin _ | `Interpret_Lcalc ) as backend -> ( @@ -408,7 +408,7 @@ let driver source_file (options : Cli.options) : int = List.iter (fun ((var, _), result) -> Cli.result_format "@[%s@ =@ %a@]" var - (Shared_ast.Expr.format ~debug:options.debug ()) + (Shared_ast.Print.expr ~debug:options.debug ()) result) results | `Plugin (Plugin.Dcalc p) -> @@ -496,7 +496,7 @@ let driver source_file (options : Cli.options) : int = List.iter (fun ((var, _), result) -> Cli.result_format "@[%s@ =@ %a@]" var - (Shared_ast.Expr.format ~debug:options.debug ()) + (Shared_ast.Print.expr ~debug:options.debug ()) result) results | (`OCaml | `Python | `Scalc | `Plugin _) as backend -> ( diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index 1e09b72c..6aaef647 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -103,7 +103,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : let m = Marked.get_mark e in let mark = m in let pos = Expr.pos e in - (* Cli.debug_format "%a" (Print.expr_debug ~debug:true) e; *) + (* Cli.debug_format "%a" (Print.expr ~debug:true ()) e; *) match Marked.unmark e with | EVar x -> if (Var.Map.find x ctx.ctx_vars).info_pure then diff --git a/compiler/plugins/lazy_interp.ml b/compiler/plugins/lazy_interp.ml index 56e2e625..6348707f 100644 --- a/compiler/plugins/lazy_interp.ml +++ b/compiler/plugins/lazy_interp.ml @@ -84,9 +84,9 @@ let rec lazy_eval : let r, env1 = lazy_eval ctx env1 llevel e in if not (Expr.equal e r) then ( log "@[{{%a =@ [%a]@ ==> [%a]}}@]" Print.var_debug v - (Print.expr' ~debug:true ()) + (Print.expr ~debug:true ()) e - (Print.expr' ~debug:true ()) + (Print.expr ~debug:true ()) r; v_env := r, env1); r, Env.join env env1 @@ -105,12 +105,12 @@ let rec lazy_eval : Seq.fold_left2 (fun env1 var e -> log "@[LET %a = %a@]@ " Print.var_debug var - (Print.expr' ~debug:true ()) + (Print.expr ~debug:true ()) e; Env.add var e env env1) env (Array.to_seq vars) (List.to_seq args) in - log "@]@[IN [%a]@]" (Print.expr' ~debug:true ()) body; + log "@]@[IN [%a]@]" (Print.expr ~debug:true ()) body; let e, env = lazy_eval ctx env llevel body in log "@]}"; e, env @@ -133,7 +133,7 @@ let rec lazy_eval : in Interpreter.evaluate_operator eval op m args, !renv (* fixme: this forwards eempty *) - | e, _ -> error e "Invalid apply on %a" Print.expr e) + | e, _ -> error e "Invalid apply on %a" Expr.format e) | (EAbs _ | ELit _ | EOp _ | EEmptyError), _ -> e0, env (* these are values *) | (EStruct _ | ETuple _ | EInj _ | EArray _), _ -> if not llevel.eval_struct then e0, env @@ -152,14 +152,14 @@ let rec lazy_eval : match eval_to_value env e with | (EStruct { name = n; fields }, _), env when StructName.equal name n -> lazy_eval ctx env llevel (StructField.Map.find field fields) - | e, _ -> error e "Invalid field access on %a" Print.expr e) + | e, _ -> error e "Invalid field access on %a" Expr.format e) | ETupleAccess { e; index; size }, _ -> ( if not llevel.eval_default then e0, env else match eval_to_value env e with | (ETuple es, _), env when List.length es = size -> lazy_eval ctx env llevel (List.nth es index) - | e, _ -> error e "Invalid tuple access on %a" Print.expr e) + | e, _ -> error e "Invalid tuple access on %a" Expr.format e) | EMatch { e; name; cases }, _ -> ( if not llevel.eval_default then e0, env else @@ -167,7 +167,7 @@ let rec lazy_eval : | (EInj { name = n; cons; e }, m), env when EnumName.equal name n -> lazy_eval ctx env llevel (EApp { f = EnumConstructor.Map.find cons cases; args = [e] }, m) - | e, _ -> error e "Invalid match argument %a" Print.expr e) + | e, _ -> error e "Invalid match argument %a" Expr.format e) | EDefault { excepts; just; cons }, m -> ( let excs = List.filter_map @@ -182,9 +182,9 @@ let rec lazy_eval : match eval_to_value env just with | (ELit (LBool true), _), _ -> lazy_eval ctx env llevel cons | (ELit (LBool false), _), _ -> (EEmptyError, m), env - | e, _ -> error e "Invalid exception justification %a" Print.expr e) + | e, _ -> error e "Invalid exception justification %a" Expr.format e) | [(e, env)] -> - log "@[EVAL %a@]" Print.expr e; + log "@[EVAL %a@]" Expr.format e; lazy_eval ctx env llevel e | _ :: _ :: _ -> Errors.raise_multispanned_error @@ -195,20 +195,21 @@ let rec lazy_eval : match eval_to_value env cond with | (ELit (LBool true), _), _ -> lazy_eval ctx env llevel etrue | (ELit (LBool false), _), _ -> lazy_eval ctx env llevel efalse - | e, _ -> error e "Invalid condition %a" Print.expr e) + | e, _ -> error e "Invalid condition %a" Expr.format e) | EErrorOnEmpty e, _ -> ( match eval_to_value env e ~eval_default:false with | ((EEmptyError, _) as e'), _ -> (* This does _not_ match the eager semantics ! *) - error e' "This value is undefined %a" Print.expr e + error e' "This value is undefined %a" Expr.format e | e, env -> lazy_eval ctx env llevel e) | EAssert e, m -> ( if noassert then (ELit LUnit, m), env else match eval_to_value env e with | (ELit (LBool true), m), env -> (ELit LUnit, m), env - | (ELit (LBool false), _), _ -> error e "Assert failure (%a)" Print.expr e - | _ -> error e "Invalid assertion condition %a" Print.expr e) + | (ELit (LBool false), _), _ -> + error e "Assert failure (%a)" Expr.format e + | _ -> error e "Invalid assertion condition %a" Expr.format e) | _ -> . let interpret_program @@ -229,7 +230,7 @@ let interpret_program let { contents = e, env } = Env.find scope_v all_env in let e = Expr.unbox (Expr.remove_logging_calls e) in log "====================="; - log "%a" (Print.expr' ~debug:true ()) e; + log "%a" (Print.expr ~debug:true ()) e; log "====================="; let m = Marked.get_mark e in let application_arg = @@ -267,6 +268,6 @@ let apply ~source_file ~output_file ~scope prg _type_ordering = ignore output_file; let fmt = Format.std_formatter in let result_expr, _env = interpret_program prg scope in - Print.expr fmt result_expr + Expr.format fmt result_expr let () = Driver.Plugin.register_dcalc ~name ~extension apply diff --git a/compiler/scopelang/print.ml b/compiler/scopelang/print.ml index 94161fe3..1beaa529 100644 --- a/compiler/scopelang/print.ml +++ b/compiler/scopelang/print.ml @@ -77,7 +77,7 @@ let scope ?debug ctx fmt (name, decl) = (Print.typ ctx) typ Print.punctuation "=" (fun fmt e -> match Marked.unmark loc with - | SubScopeVar _ | ToplevelVar _ -> Print.expr' () fmt e + | SubScopeVar _ | ToplevelVar _ -> Print.expr () fmt e | ScopelangScopeVar v -> ( match Marked.unmark @@ -86,12 +86,12 @@ let scope ?debug ctx fmt (name, decl) = with | Reentrant -> Format.fprintf fmt "%a@ %a" Print.op_style - "reentrant or by default" (Print.expr' ?debug ()) e - | _ -> Format.fprintf fmt "%a" (Print.expr' ?debug ()) e)) + "reentrant or by default" (Print.expr ?debug ()) e + | _ -> Format.fprintf fmt "%a" (Print.expr ?debug ()) e)) e | Assertion e -> Format.fprintf fmt "%a %a" Print.keyword "assert" - (Print.expr' ?debug ()) e + (Print.expr ?debug ()) e | Call (scope_name, subscope_name, _) -> Format.fprintf fmt "%a %a%a%a%a" Print.keyword "call" ScopeName.format_t scope_name Print.punctuation "[" @@ -113,7 +113,7 @@ let print_topdef ctx ppf name (e, ty) = Format.pp_close_box ppf () in Format.pp_print_cut ppf (); - Print.expr' () ppf e; + Print.expr () ppf e; Format.pp_close_box ppf () let program ?(debug : bool = false) (fmt : Format.formatter) (p : 'm program) : diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml index 6e4cffea..03d691cd 100644 --- a/compiler/shared_ast/expr.ml +++ b/compiler/shared_ast/expr.ml @@ -718,7 +718,7 @@ let remove_logging_calls e = in f e -let format ?debug () ppf e = Print.expr' ?debug () ppf e +let format ppf e = Print.expr ~debug:false () ppf e let rec size : type a. (a, 't) gexpr -> int = fun e -> diff --git a/compiler/shared_ast/expr.mli b/compiler/shared_ast/expr.mli index 6d3e0971..f0a194bc 100644 --- a/compiler/shared_ast/expr.mli +++ b/compiler/shared_ast/expr.mli @@ -340,12 +340,9 @@ val remove_logging_calls : (** Removes all calls to [Log] unary operators in the AST, replacing them by their argument. *) -val format : - ?debug:bool (** [true] for debug printing *) -> - unit -> - Format.formatter -> - (_, _ mark) gexpr -> - unit +val format : Format.formatter -> ('a, 'm mark) gexpr -> unit +(** Simple printing without debug, use [Print.expr ()] instead to follow the + command-line debug setting *) (** {2 Analysis and tests} *) diff --git a/compiler/shared_ast/interpreter.ml b/compiler/shared_ast/interpreter.ml index 1ea0f751..9cc54d9d 100644 --- a/compiler/shared_ast/interpreter.ml +++ b/compiler/shared_ast/interpreter.ml @@ -60,7 +60,7 @@ let print_log entry infos pos e = (match Marked.unmark e with | EAbs _ -> Cli.with_style [ANSITerminal.green] "" | _ -> - let expr_str = Format.asprintf "%a" (Expr.format ()) e in + let expr_str = Format.asprintf "%a" (Print.expr ()) e in let expr_str = Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*") ~subst:(fun _ -> " ") @@ -164,7 +164,7 @@ let rec evaluate_operator (fun i arg -> ( Some (Format.asprintf "Argument n°%d, value %a" (i + 1) - (Expr.format ()) arg), + (Print.expr ()) arg), Expr.pos arg )) args) "Operator applied to the wrong arguments\n\ @@ -458,7 +458,7 @@ let rec evaluate_expr : Errors.raise_spanned_error (Expr.pos e) "The expression %a should be a struct %a but is not (should not happen \ if the term was well-typed)" - (Expr.format ()) e StructName.format_t s) + (Print.expr ()) e StructName.format_t s) | ETuple es -> Marked.mark m (ETuple (List.map (evaluate_expr ctx) es)) | ETupleAccess { e = e1; index; size } -> ( match evaluate_expr ctx e1 with @@ -467,7 +467,7 @@ let rec evaluate_expr : Errors.raise_spanned_error (Expr.pos e) "The expression %a was expected to be a tuple of size %d (should not \ happen if the term was well-typed)" - (Expr.format ()) e size) + (Print.expr ()) e size) | EInj { e; name; cons } -> propagate_empty_error (evaluate_expr ctx e) @@ fun e -> Marked.mark m (EInj { e; name; cons }) @@ -520,11 +520,11 @@ let rec evaluate_expr : args = [((ELit _, _) as e1); ((ELit _, _) as e2)]; } -> Errors.raise_spanned_error (Expr.pos e') - "Assertion failed: %a %a %a" (Expr.format ()) e1 + "Assertion failed: %a %a %a" (Print.expr ()) e1 (Print.operator ~debug:!Cli.debug_flag) - op (Expr.format ()) e2 + op (Print.expr ()) e2 | _ -> - Cli.debug_format "%a" (Expr.format ()) e'; + Cli.debug_format "%a" (Print.expr ()) e'; Errors.raise_spanned_error (Expr.mark_pos m) "Assertion failed") | _ -> Errors.raise_spanned_error (Expr.pos e') diff --git a/compiler/shared_ast/optimizations.ml b/compiler/shared_ast/optimizations.ml index 909887d4..de897aa1 100644 --- a/compiler/shared_ast/optimizations.ml +++ b/compiler/shared_ast/optimizations.ml @@ -342,8 +342,8 @@ let test_iota_reduction_1 () = \ | B → (λ (x: any) → D x)\n\ after=C\n\ x" - (Format.asprintf "before=%a\nafter=%a" Print.expr (Expr.unbox matchA) - Print.expr + (Format.asprintf "before=%a\nafter=%a" Expr.format (Expr.unbox matchA) + Expr.format (Expr.unbox (optimize_expr { @@ -414,8 +414,8 @@ let test_iota_reduction_2 () = \ with\n\ \ | A → (λ (x: any) → C 20)\n\ \ | B → (λ (x: any) → D B x)\n" - (Format.asprintf "before=@[%a@]@.after=%a@." Print.expr - (Expr.unbox matchA) Print.expr + (Format.asprintf "before=@[%a@]@.after=%a@." Expr.format + (Expr.unbox matchA) Expr.format (Expr.unbox (optimize_expr { diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index 8c29da62..f3790590 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -93,15 +93,20 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit = match ctx with | None -> StructName.format_t fmt s | Some ctx -> - Format.fprintf fmt "@[%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) -> - Format.fprintf fmt "%a%a@ %a" struct_field field punctuation ":" - typ mty)) - (StructField.Map.bindings (StructName.Map.find s ctx.ctx_structs)) - punctuation "}") + let fields = StructName.Map.find s ctx.ctx_structs in + if StructField.Map.is_empty fields then StructName.format_t fmt s + else + Format.fprintf fmt "@[%a %a@,%a@;<0 -2>%a@]" StructName.format_t s + punctuation "{" + (Format.pp_print_list + ~pp_sep:(fun fmt () -> + punctuation fmt ";"; + Format.pp_print_space fmt ()) + (fun fmt (field_name, field_typ) -> + Format.fprintf fmt "@[%a%a@ %a@]" struct_field field_name + punctuation ":" typ field_typ)) + (StructField.Map.bindings fields) + punctuation "}") | TEnum e -> ( match ctx with | None -> Format.fprintf fmt "@[%a@]" EnumName.format_t e @@ -650,11 +655,9 @@ let rec colors = let typ_debug = typ None let typ ctx = typ (Some ctx) -let expr' ?(debug = !Cli.debug_flag) () ppf e = +let expr ?(debug = !Cli.debug_flag) () ppf e = expr_aux ~debug Bindlib.empty_ctxt colors ppf e -let expr ppf e = expr' ~debug:false () ppf e - let scope_let_kind ?debug:(_debug = true) _ctx fmt k = match k with | DestructuringInputStruct -> keyword fmt "get" @@ -664,9 +667,10 @@ let scope_let_kind ?debug:(_debug = true) _ctx fmt k = | DestructuringSubScopeResults -> keyword fmt "sub_get" | Assertion -> keyword fmt "assert" -let rec scope_body_expr ?(debug = false) ctx fmt b : unit = +let[@ocamlformat "disable"] rec + scope_body_expr ?(debug = false) ctx fmt b : unit = match b with - | Result e -> Format.fprintf fmt "%a %a" keyword "return" (expr' ~debug ()) e + | Result e -> Format.fprintf fmt "%a %a" keyword "return" (expr ~debug ()) e | ScopeLet { scope_let_kind = kind; @@ -676,14 +680,17 @@ let rec scope_body_expr ?(debug = false) ctx fmt b : unit = _; } -> let x, next = Bindlib.unbind scope_let_next in - Format.fprintf fmt "@[%a %a %a %a %a %a@;%a@;%a @]@,%a" keyword "let" - (scope_let_kind ~debug ctx) - kind - (if debug then var_debug else var) - x punctuation ":" (typ ctx) scope_let_typ punctuation "=" - (expr' ~debug ()) scope_let_expr keyword "in" - (scope_body_expr ~debug ctx) - next + Format.fprintf fmt + "@[@[%a %a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]@,%a" + keyword "let" + (scope_let_kind ~debug ctx) kind + (if debug then var_debug else var) x + punctuation ":" + (typ ctx) scope_let_typ + punctuation "=" + (expr ~debug ()) scope_let_expr + keyword "in" + (scope_body_expr ~debug ctx) next let scope_body ?(debug = false) ctx fmt (n, l) : unit = let { @@ -699,23 +706,36 @@ let scope_body ?(debug = false) ctx fmt (n, l) : unit = let x, body = Bindlib.unbind body in - let _ = + let () = Format.pp_open_vbox fmt 2; - let _ = - Format.pp_open_hbox fmt (); - keyword fmt "let scope"; - Format.pp_print_space fmt (); - ScopeName.format_t fmt n; + let () = + Format.pp_open_hvbox fmt 2; + let () = + Format.pp_open_hovbox fmt 4; + keyword fmt "let scope"; + Format.pp_print_space fmt (); + ScopeName.format_t fmt n; + Format.pp_close_box fmt () + in Format.pp_print_space fmt (); punctuation fmt "("; - (if debug then var_debug else var) fmt x; + let () = + Format.pp_open_hvbox fmt 2; + (if debug then var_debug else var) fmt x; + punctuation fmt ":"; + Format.pp_print_space fmt (); + (if debug then typ_debug else typ ctx) fmt input_typ; + punctuation fmt ")"; + Format.pp_close_box fmt () + in + Format.pp_print_cut fmt (); punctuation fmt ":"; - Format.pp_print_space fmt (); - (if debug then typ_debug else typ ctx) fmt input_typ; - punctuation fmt ")"; - punctuation fmt ":"; - Format.pp_print_space fmt (); - (if debug then typ_debug else typ ctx) fmt output_typ; + Format.pp_print_string fmt " "; + let () = + Format.pp_open_hvbox fmt 2; + (if debug then typ_debug else typ ctx) fmt output_typ; + Format.pp_close_box fmt () + in Format.pp_print_space fmt (); punctuation fmt "="; Format.pp_close_box fmt () @@ -774,7 +794,9 @@ let scope (ctx : decl_ctx) (fmt : Format.formatter) ((n, s) : ScopeName.t * 'm scope_body) : unit = - scope_body ~debug ctx fmt (n, s) + Format.pp_open_vbox fmt 0; + scope_body ~debug ctx fmt (n, s); + Format.pp_close_box fmt () let code_item ?(debug = false) decl_ctx fmt c = match c with @@ -782,7 +804,7 @@ let code_item ?(debug = false) decl_ctx fmt c = | Topdef (n, ty, e) -> Format.fprintf fmt "@[%a %a %a %a %a %a @]" keyword "let topval" TopdefName.format_t n op_style ":" (typ decl_ctx) ty op_style "=" - (expr' ~debug ()) e + (expr ~debug ()) e let rec code_item_list ?(debug = false) decl_ctx fmt c = match c with diff --git a/compiler/shared_ast/print.mli b/compiler/shared_ast/print.mli index 96727801..9a175ce3 100644 --- a/compiler/shared_ast/print.mli +++ b/compiler/shared_ast/print.mli @@ -44,9 +44,8 @@ val log_entry : Format.formatter -> log_entry -> unit val except : Format.formatter -> except -> unit val var : Format.formatter -> 'e Var.t -> unit val var_debug : Format.formatter -> 'e Var.t -> unit -val expr : Format.formatter -> ('a, 'm mark) gexpr -> unit -val expr' : +val expr : ?debug:bool -> unit -> Format.formatter -> ('a, 'm mark) gexpr -> unit (** Same as [expr], but with a debug flag that defaults to [!Cli.debug_flag] *) diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml index 4565927c..f657c247 100644 --- a/compiler/shared_ast/typing.ml +++ b/compiler/shared_ast/typing.ml @@ -394,7 +394,7 @@ and typecheck_expr_top_down : | Some ty -> ty | None -> Errors.raise_spanned_error pos_e "Reference to %a not found" - (Expr.format ()) e + (Print.expr ()) e in Expr.elocation loc (mark_with_tau_and_unify (ast_to_typ ty)) | A.EStruct { name; fields } -> diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index 614e5ee9..1e3318a0 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -139,7 +139,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) : "Internal error: this expression does not have the structure expected \ by the VC generator:\n\ %a" - (Expr.format ()) e) + (Print.expr ()) e) | EErrorOnEmpty d -> d (* input subscope variables and non-input scope variable *) | _ -> @@ -147,7 +147,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) : "Internal error: this expression does not have the structure expected by \ the VC generator:\n\ %a" - (Expr.format ()) e + (Print.expr ()) e (** {1 Verification conditions generator}*) @@ -332,7 +332,7 @@ let rec generate_verification_conditions_scope_body_expr "Internal error: this assertion does not have the structure \ expected by the VC generator:\n\ %a" - (Expr.format ()) e) + (Print.expr ()) e) | DestructuringInputStruct -> { ctx with input_vars = scope_let_var :: ctx.input_vars }, [], [] | ScopeVarDefinition | SubScopeVarDefinition -> diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml index 7a4c6cdd..aaf0914d 100644 --- a/compiler/verification/io.ml +++ b/compiler/verification/io.ml @@ -138,7 +138,7 @@ module MakeBackendIO (B : Backend) = struct | Some counterexample -> "\n" ^ counterexample let encode_and_check_vc - (decl_ctx : decl_ctx) + (_decl_ctx : decl_ctx) (vc : Conditions.verification_condition * vc_encoding_result) : bool = let vc, z3_vc = vc in @@ -154,7 +154,7 @@ module MakeBackendIO (B : Backend) = struct | Conditions.NoEmptyError -> "the variable definition never to return an empty error" | NoOverlappingExceptions -> "no two exceptions to ever overlap") - (Expr.format ()) vc.vc_guard (Expr.format ()) vc.vc_asserts; + (Print.expr ()) vc.vc_guard (Print.expr ()) vc.vc_asserts; match z3_vc with | Success (encoding, backend_ctx) -> ( diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index ef9e9955..10bf1f68 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -433,8 +433,7 @@ let rec translate_op : fun ctx op args -> let ill_formed () = Format.kasprintf failwith - "[Z3 encoding] Ill-formed operator application: %a" - (Shared_ast.Expr.format ()) + "[Z3 encoding] Ill-formed operator application: %a" Shared_ast.Expr.format (Shared_ast.Expr.eapp (Shared_ast.Expr.eop op [] (Untyped { pos = Pos.no_pos })) (List.map Shared_ast.Expr.untype args) diff --git a/tests/test_func/good/context_func.catala_en b/tests/test_func/good/context_func.catala_en index 783e12ae..93ff53eb 100644 --- a/tests/test_func/good/context_func.catala_en +++ b/tests/test_func/good/context_func.catala_en @@ -38,10 +38,12 @@ $ catala Dcalc -s A 5 │ context f content integer depends on x content integer │ ‾ └─ Test -let scope A (A_in: A_in {f_in: integer → integer}): A {} = +let scope A (A_in: A_in {f_in: integer → integer}): A = let get f : integer → integer = A_in.f_in in - let set f : integer → integer = λ (x: integer) → - error_empty ⟨ f x | true ⊢ ⟨true ⊢ x + 1⟩ ⟩ in + let set f : integer → integer = + λ (x: integer) → + error_empty ⟨ f x | true ⊢ ⟨true ⊢ x + 1⟩ ⟩ + in return {A} ``` @@ -54,10 +56,12 @@ $ catala Dcalc -s B 5 │ context f content integer depends on x content integer │ ‾ └─ Test -let scope B (B_in: B_in {b_in: bool}): B {} = +let scope B (B_in: B_in {b_in: bool}): B = let get b : bool = B_in.b_in in - let sub_set a.f : integer → integer = λ (x: integer) → - ⟨b && x > 0 ⊢ x - 1⟩ in - let call result : A {} = A { A_in f_in = a.f; } in + let sub_set a.f : integer → integer = + λ (x: integer) → + ⟨b && x > 0 ⊢ x - 1⟩ + in + let call result : A = A { A_in f_in = a.f; } in return {B} ``` diff --git a/tests/test_io/good/all_io.catala_en b/tests/test_io/good/all_io.catala_en index 9914ed09..43781973 100644 --- a/tests/test_io/good/all_io.catala_en +++ b/tests/test_io/good/all_io.catala_en @@ -19,29 +19,25 @@ scope A: ```catala-test-inline $ catala Dcalc -s A -let scope A (A_in: A_in - {c_in: - integer; - d_in: - integer; - e_in: - unit → integer; - f_in: - unit → integer}): A - {b: - integer; - d: - integer; - f: - integer} = +let scope A + (A_in: + A_in { + c_in: integer; + d_in: integer; + e_in: unit → integer; + f_in: unit → integer + }) + : A {b: integer; d: integer; f: integer} + = let get c : integer = A_in.c_in in let get d : integer = A_in.d_in in let get e : unit → integer = A_in.e_in in let get f : unit → integer = A_in.f_in in let set a : integer = error_empty ⟨true ⊢ 0⟩ in let set b : integer = error_empty ⟨true ⊢ a + 1⟩ in - let set e : integer = error_empty ⟨ e () | true ⊢ ⟨true ⊢ b + c + d + 1⟩ ⟩ - in + let set e : integer = + error_empty ⟨ e () | true ⊢ ⟨true ⊢ b + c + d + 1⟩ ⟩ + in let set f : integer = error_empty ⟨ f () | true ⊢ ⟨true ⊢ e + 1⟩ ⟩ in return { A b = b; d = d; f = f; } ``` diff --git a/tests/test_io/good/condition_only_input.catala_en b/tests/test_io/good/condition_only_input.catala_en index 4a1782b5..cd3d99a2 100644 --- a/tests/test_io/good/condition_only_input.catala_en +++ b/tests/test_io/good/condition_only_input.catala_en @@ -16,7 +16,7 @@ scope B: ``` ```catala-test-inline $ catala Dcalc -s B -let scope B (B_in: B_in {}): B {} = +let scope B (B_in: B_in): B = let sub_set a.x : bool = error_empty ⟨true ⊢ false⟩ in let call result : A {y: integer} = A { A_in x_in = a.x; } in let sub_get a.y : integer = result.y in diff --git a/tests/test_io/good/subscope.catala_en b/tests/test_io/good/subscope.catala_en index 8efd0827..9f0d620a 100644 --- a/tests/test_io/good/subscope.catala_en +++ b/tests/test_io/good/subscope.catala_en @@ -22,7 +22,7 @@ scope B: ```catala-test-inline $ catala Dcalc -s B -let scope B (B_in: B_in {}): B {} = +let scope B (B_in: B_in): B = let sub_set a.a : unit → integer = λ (_: unit) → ∅ in let sub_set a.b : integer = error_empty ⟨true ⊢ 2⟩ in let call result : A {c: integer} = A { A_in a_in = a.a; b_in = a.b; } in diff --git a/tests/test_name_resolution/good/toplevel_defs.catala_en b/tests/test_name_resolution/good/toplevel_defs.catala_en index 4bb45cef..585a692b 100644 --- a/tests/test_name_resolution/good/toplevel_defs.catala_en +++ b/tests/test_name_resolution/good/toplevel_defs.catala_en @@ -109,7 +109,7 @@ let glob5_6 = glob5_aux_5 () let glob2_10 = A {"y": glob1_2 >= 30., "z": 123. * 17.} -let S2_6 (S2_in_11: S2_in {}) = +let S2_6 (S2_in_11: S2_in) = decl temp_a_13 : any; try: decl temp_a_16 : any; @@ -126,7 +126,7 @@ let S2_6 (S2_in_11: S2_in {}) = a_12 = temp_a_13; return S2 {"a": a_12} -let S3_7 (S3_in_18: S3_in {}) = +let S3_7 (S3_in_18: S3_in) = decl temp_a_20 : any; try: decl temp_a_23 : any; @@ -143,7 +143,7 @@ let S3_7 (S3_in_18: S3_in {}) = a_19 = temp_a_20; return S3 {"a": a_19} -let S4_8 (S4_in_25: S4_in {}) = +let S4_8 (S4_in_25: S4_in) = decl temp_a_27 : any; try: decl temp_a_30 : any; @@ -160,7 +160,7 @@ let S4_8 (S4_in_25: S4_in {}) = a_26 = temp_a_27; return S4 {"a": a_26} -let S_9 (S_in_32: S_in {}) = +let S_9 (S_in_32: S_in) = decl temp_a_40 : any; try: decl temp_a_43 : any; diff --git a/tests/test_scope/good/nothing.catala_en b/tests/test_scope/good/nothing.catala_en index 401371bc..03d2350a 100644 --- a/tests/test_scope/good/nothing.catala_en +++ b/tests/test_scope/good/nothing.catala_en @@ -14,7 +14,7 @@ $ catala Scalc -s Foo2 -O -t 5 │ output bar content integer │ ‾‾‾ └─ Test -let Foo2_3 (Foo2_in_2: Foo2_in {}) = +let Foo2_3 (Foo2_in_2: Foo2_in) = decl temp_bar_4 : any; temp_bar_4 = dead_value_1; raise NoValueProvided; diff --git a/tests/test_scope/good/simple.catala_en b/tests/test_scope/good/simple.catala_en index dc68e0fb..ae458fb1 100644 --- a/tests/test_scope/good/simple.catala_en +++ b/tests/test_scope/good/simple.catala_en @@ -10,9 +10,10 @@ scope Foo: ```catala-test-inline $ catala Lcalc -s Foo -let scope Foo (Foo_in: Foo_in {}): Foo {bar: integer} = +let scope Foo (Foo_in: Foo_in): Foo {bar: integer} = let set bar : integer = try handle_default [ ], (λ (_: unit) → true), (λ (_: unit) → 0) - with EmptyError -> raise NoValueProvided in + with EmptyError -> raise NoValueProvided + in return { Foo bar = bar; } ``` From b1955bd9d4d83d2cc04b9d42bef8e96eeac0d109 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Tue, 2 May 2023 16:46:36 +0200 Subject: [PATCH 7/7] Don't use a debug printing function for OCaml output --- compiler/lcalc/to_ocaml.ml | 5 ++--- compiler/shared_ast/print.mli | 6 ++++++ 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/compiler/lcalc/to_ocaml.ml b/compiler/lcalc/to_ocaml.ml index bf4fdaf2..3a52c540 100644 --- a/compiler/lcalc/to_ocaml.ml +++ b/compiler/lcalc/to_ocaml.ml @@ -340,10 +340,9 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) : args; } -> Format.fprintf fmt - "@[%a@ @[{filename = \"%s\";@ start_line=%d;@ \ + "@[%s@ @[{filename = \"%s\";@ start_line=%d;@ \ start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a@]" - (Print.operator ~debug:true) - op + (Print.operator_to_string op) (Pos.get_file (Expr.mark_pos pos)) (Pos.get_start_line (Expr.mark_pos pos)) (Pos.get_start_column (Expr.mark_pos pos)) diff --git a/compiler/shared_ast/print.mli b/compiler/shared_ast/print.mli index 9a175ce3..5cdbff9e 100644 --- a/compiler/shared_ast/print.mli +++ b/compiler/shared_ast/print.mli @@ -31,6 +31,12 @@ val punctuation : Format.formatter -> string -> unit val op_style : Format.formatter -> string -> unit val lit_style : Format.formatter -> string -> unit +(** {1 Some basic stringifiers} *) + +val operator_to_string : 'a operator -> string +(** Prints the operator symbols with kind suffixes, as expected by the OCaml + backend (e.g. "+^", "+$", etc.) *) + (** {1 Formatters} *) val uid_list : Format.formatter -> Uid.MarkedString.info list -> unit