Unify traces between interpreter and runtime (#615)

This commit is contained in:
Louis Gesbert 2024-05-15 10:59:15 +02:00 committed by GitHub
commit bd30fe8d50
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 136 additions and 38 deletions

View File

@ -935,7 +935,16 @@ let ninja_cmdline ninja_flags nin_file targets =
let run_ninja ~clean_up_env cmdline =
let cmd = List.hd cmdline in
let env = if clean_up_env then cleaned_up_env () else Unix.environment () in
Unix.execvpe cmd (Array.of_list cmdline) env
let npid =
Unix.create_process_env cmd (Array.of_list cmdline) env Unix.stdin
Unix.stdout Unix.stderr
in
let return_code =
match Unix.waitpid [] npid with
| _, Unix.WEXITED n -> n
| _, (Unix.WSIGNALED n | Unix.WSTOPPED n) -> 128 - n
in
raise (Catala_utils.Cli.Exit_with return_code)
open Cmdliner

View File

@ -34,30 +34,88 @@ let is_empty_error : type a. (a, 'm) gexpr -> bool =
let indent_str = ref ""
(** {1 Evaluation} *)
let print_log lang entry infos pos e =
if Global.options.trace then
match entry with
| VarDef _ ->
Message.log "%s%a %a: @{<green>%s@}" !indent_str Print.log_entry entry
Print.uid_list infos
(Message.unformat (fun ppf ->
(if Global.options.debug then Print.expr ~debug:true ()
else Print.UserFacing.expr lang)
ppf e))
| PosRecordIfTrueBool -> (
match pos <> Pos.no_pos, Mark.remove e with
| true, ELit (LBool true) ->
Message.log "%s@[<v>%a@{<green>Definition applied@}:@,%a@]" !indent_str
Print.log_entry entry Pos.format_loc_text pos
| _ -> ())
| BeginCall ->
Message.log "%s%a %a" !indent_str Print.log_entry entry Print.uid_list
infos;
indent_str := !indent_str ^ " "
| EndCall ->
indent_str := String.sub !indent_str 0 (String.length !indent_str - 2);
Message.log "%s%a %a" !indent_str Print.log_entry entry Print.uid_list
infos
let rec format_runtime_value lang ppf = function
| Runtime.Unit -> Print.UserFacing.unit lang ppf ()
| Runtime.Bool b -> Print.UserFacing.bool lang ppf b
| Runtime.Money m -> Print.UserFacing.money lang ppf m
| Runtime.Integer i -> Print.UserFacing.integer lang ppf i
| Runtime.Decimal d -> Print.UserFacing.decimal lang ppf d
| Runtime.Date t -> Print.UserFacing.date lang ppf t
| Runtime.Duration dt -> Print.UserFacing.duration lang ppf dt
| Runtime.Enum (name, (constr, v)) ->
Format.fprintf ppf "@[<hov 2>%s.%s@ (%a)@]" name constr
(format_runtime_value lang)
v
| Runtime.Struct (name, fields) ->
Format.fprintf ppf "@[<hv 2>%s {@ %a@;<1 -2>}@]" name
(Format.pp_print_list ~pp_sep:Format.pp_print_space (fun ppf (fld, v) ->
Format.fprintf ppf "@[<hov 2>-- %s:@ %a@]" fld
(format_runtime_value lang)
v))
fields
| Runtime.Array elts ->
Format.fprintf ppf "@[<hv 2>[@,@[<hov>%a@]@;<0 -2>]@]"
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ")
(format_runtime_value lang))
(Array.to_list elts)
| Runtime.Unembeddable -> Format.pp_print_string ppf "<object>"
let print_log lang entry =
let pp_infos =
Format.(
pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf ".@,")
pp_print_string)
in
match entry with
| Runtime.BeginCall infos ->
Message.log "%s%a %a" !indent_str Print.log_entry BeginCall pp_infos infos;
indent_str := !indent_str ^ " "
| Runtime.EndCall infos ->
indent_str := String.sub !indent_str 0 (String.length !indent_str - 2);
Message.log "%s%a %a" !indent_str Print.log_entry EndCall pp_infos infos
| Runtime.VariableDefinition (infos, io, value) ->
Message.log "%s%a %a: @{<green>%s@}" !indent_str Print.log_entry
(VarDef
{
log_typ = TAny;
log_io_input = io.Runtime.io_input;
log_io_output = io.Runtime.io_output;
})
pp_infos infos
(Message.unformat (fun ppf -> format_runtime_value lang ppf value))
| Runtime.DecisionTaken rtpos ->
let pos = Expr.runtime_to_pos rtpos in
Message.log "%s@[<v>%a@{<green>Definition applied@}:@,%a@]" !indent_str
Print.log_entry PosRecordIfTrueBool Pos.format_loc_text pos
let rec value_to_runtime_embedded = function
| ELit LUnit -> Runtime.Unit
| ELit (LBool b) -> Runtime.Bool b
| ELit (LMoney m) -> Runtime.Money m
| ELit (LInt i) -> Runtime.Integer i
| ELit (LRat r) -> Runtime.Decimal r
| ELit (LDate d) -> Runtime.Date d
| ELit (LDuration dt) -> Runtime.Duration dt
| EInj { name; cons; e } ->
Runtime.Enum
( EnumName.to_string name,
( EnumConstructor.to_string cons,
value_to_runtime_embedded (Mark.remove e) ) )
| EStruct { name; fields } ->
Runtime.Struct
( StructName.to_string name,
List.map
(fun (f, e) ->
StructField.to_string f, value_to_runtime_embedded (Mark.remove e))
(StructField.Map.bindings fields) )
| EArray el ->
Runtime.Array
(Array.of_list
(List.map (fun e -> value_to_runtime_embedded (Mark.remove e)) el))
| _ -> Runtime.Unembeddable
(* Todo: this should be handled early when resolving overloads. Here we have
proper structural equality, but the OCaml backend for example uses the
@ -147,9 +205,22 @@ let rec evaluate_operator
match op, args with
| Length, [(EArray es, _)] ->
ELit (LInt (Runtime.integer_of_int (List.length es)))
| Log (entry, infos), [e'] ->
print_log lang entry infos pos e';
Mark.remove e'
| Log (entry, infos), [(e, _)] when Global.options.trace -> (
let rtinfos = List.map Uid.MarkedString.to_string infos in
match entry with
| BeginCall -> Runtime.log_begin_call rtinfos e
| EndCall -> Runtime.log_end_call rtinfos e
| PosRecordIfTrueBool ->
(match e with
| ELit (LBool b) ->
Runtime.log_decision_taken (Expr.pos_to_runtime pos) b |> ignore
| _ -> ());
e
| VarDef def ->
Runtime.log_variable_definition rtinfos
{ Runtime.io_input = def.log_io_input; io_output = def.log_io_output }
value_to_runtime_embedded e)
| Log _, [(e', _)] -> e'
| (FromClosureEnv | ToClosureEnv), [e'] ->
(* [FromClosureEnv] and [ToClosureEnv] are just there to bypass the need for
existential types when typing code after closure conversion. There are
@ -840,6 +911,22 @@ and partially_evaluate_expr_for_assertion_failure_message :
Mark.get e )
| _ -> evaluate_expr ctx lang e
let evaluate_expr_trace :
type d e.
decl_ctx ->
Global.backend_lang ->
((d, e, yes) interpr_kind, 't) gexpr ->
((d, e, yes) interpr_kind, 't) gexpr =
fun ctx lang e ->
Fun.protect
(fun () -> evaluate_expr ctx lang e)
~finally:(fun () ->
if Global.options.trace then
let trace = Runtime.retrieve_log () in
List.iter (print_log lang) trace
(* TODO: [Runtime.pp_events ~is_first_call:true Format.err_formatter
(Runtime.EventParser.parse_raw_events trace)] fais here, check why *))
let evaluate_expr_safe :
type d e.
decl_ctx ->
@ -847,7 +934,7 @@ let evaluate_expr_safe :
((d, e, yes) interpr_kind, 't) gexpr ->
((d, e, yes) interpr_kind, 't) gexpr =
fun ctx lang e ->
try evaluate_expr ctx lang e
try evaluate_expr_trace ctx lang e
with Runtime.Error (err, rpos) ->
Message.error
~extra_pos:(List.map (fun rp -> "", Expr.runtime_to_pos rp) rpos)

View File

@ -79,7 +79,7 @@ let raise_parser_error
| None -> "Error token", error_loc
| Some last_good_loc -> "Last good token", last_good_loc);
]
"Syntax error at %a@\n%t"
"@[<hov>Syntax error at %a:@ %t@]"
(fun ppf string -> Format.fprintf ppf "@{<yellow>\"%s\"@}" string)
token msg
@ -131,10 +131,11 @@ module ParserAux (LocalisedLexer : Lexer_common.LocalisedLexer) = struct
(match Parser_errors.message (state env) with
| exception Not_found -> Format.fprintf ppf "@{<yellow>unexpected token@}"
| msg ->
Format.fprintf ppf "@{<yellow>@<1>»@} @[<hov>%a@]" Format.pp_print_text
Format.fprintf ppf "@{<yellow>@<1>%s@} @[<hov>%a@]" "»"
Format.pp_print_text
(String.trim (String.uncapitalize_ascii msg)));
if acceptable_tokens <> [] then
Format.fprintf ppf "@,@[<hov>Those are valid at this point:@ %a@]"
Format.fprintf ppf "@\n@[<hov>Those are valid at this point:@ %a@]"
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf ",@ ")
(fun ppf string -> Format.fprintf ppf "@{<yellow>\"%s\"@}" string))

View File

@ -13,7 +13,7 @@ scope A:
$ catala test-scope A
┌─[ERROR]─
│ Syntax error at "="
│ Syntax error at "=":
│ » expected 'under condition' followed by a condition, 'equals' followed by
│ the definition body, or the rest of the variable qualified name
│ Those are valid at this point: "of", "state", "equals", "under condition",

View File

@ -44,7 +44,7 @@ $ catala Interpret -t -s HousingComputation --debug
[DEBUG] Translating to default calculus...
[DEBUG] Typechecking again...
[DEBUG] Starting interpretation...
[LOG] ≔ HousingComputation.f: λ (x_67: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨(let result_68 : RentComputation = (#{→ RentComputation.direct} (λ (RentComputation_in_69: RentComputation_in) → let g_70 : integer → integer = #{≔ RentComputation.g} (λ (x1_71: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_71 +! 1⟩⟩ | false ⊢ ∅ ⟩) in let f_72 : integer → integer = #{≔ RentComputation.f} (λ (x1_73: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} g_70) #{≔ RentComputation.g.input0} (x1_73 +! 1)⟩⟩ | false ⊢ ∅ ⟩) in { RentComputation f = f_72; })) #{≔ RentComputation.direct.input} {RentComputation_in} in let result1_74 : RentComputation = { RentComputation f = λ (param0_75: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} result_68.f) #{≔ RentComputation.f.input0} param0_75; } in #{← RentComputation.direct} #{≔ RentComputation.direct.output} if #{☛ RentComputation.direct.output} true then result1_74 else result1_74).f x_67⟩⟩ | false ⊢ ∅ ⟩
[LOG] ≔ HousingComputation.f: <object>
[LOG] ☛ Definition applied:
─➤ tests/scope/good/scope_call3.catala_en:8.14-8.20:
@ -58,15 +58,16 @@ $ catala Interpret -t -s HousingComputation --debug
7 │ definition f of x equals (output of RentComputation).f of x
│ ‾
[LOG] → RentComputation.direct
[LOG] ≔ RentComputation.direct.input: {RentComputation_in}
[LOG] ≔ RentComputation.g: λ (x_76: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x_76 +! 1⟩⟩ | false ⊢ ∅ ⟩
[LOG] ≔ RentComputation.f: λ (x_77: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_78: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_78 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_77 +! 1)⟩⟩ | false ⊢ ∅ ⟩
[LOG] ≔ RentComputation.direct.input: RentComputation_in { }
[LOG] ≔ RentComputation.g: <object>
[LOG] ≔ RentComputation.f: <object>
[LOG] ☛ Definition applied:
─➤ tests/scope/good/scope_call3.catala_en:7.29-7.54:
7 │ definition f of x equals (output of RentComputation).f of x
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0_79: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} { RentComputation f = λ (x_80: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_81: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_81 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_80 +! 1)⟩⟩ | false ⊢ ∅ ⟩; }.f) #{≔ RentComputation.f.input0} param0_79; }
[LOG] ≔ RentComputation.direct.
output: RentComputation { -- f: <object> }
[LOG] ← RentComputation.direct
[LOG] → RentComputation.f
[LOG] ≔ RentComputation.f.input0: 1