Understanding a limitation

This commit is contained in:
Denis Merigoux 2023-06-13 20:10:42 +02:00
parent 7072369b2d
commit 27bbe78438
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
5 changed files with 99 additions and 33 deletions

View File

@ -75,7 +75,7 @@ let print_time_marker =
time := new_time;
let delta = (new_time -. old_time) *. 1000. in
if delta > 50. then
Format.fprintf ppf "@{<bold;black>[TIME] %.0fms@}@," delta
Format.fprintf ppf "@{<bold;black>[TIME] %.0fms@}@\n" delta
let pp_marker target ppf =
let open Ocolor_types in
@ -105,22 +105,28 @@ module Content = struct
let of_string (s : string) : t =
{ message = (fun ppf -> Format.pp_print_string ppf s); positions = [] }
let internal_error_prefix =
"Internal Error, please report to \
https://github.com/CatalaLang/catala/issues: "
let prepend_message (content : t) prefix : t =
{
content with
message = (fun ppf -> Format.fprintf ppf "%t@,%t" prefix content.message);
}
let mark_as_internal_error (content : t) : t =
{
content with
message =
(fun ppf ->
Format.fprintf ppf "%s@,%t" internal_error_prefix content.message);
}
end
open Content
let internal_error_prefix =
"Internal Error, please report to \
https://github.com/CatalaLang/catala/issues: "
let to_internal_error (content : Content.t) : Content.t =
{
content with
message =
(fun ppf ->
Format.fprintf ppf "%s@,%t" internal_error_prefix content.message);
}
let emit_content (content : Content.t) (target : content_type) : unit =
let { message; positions } = content in
match !Cli.message_format_flag with

View File

@ -33,10 +33,10 @@ module Content : sig
val of_message : (Format.formatter -> unit) -> t
val of_string : string -> t
val mark_as_internal_error : t -> t
val prepend_message : t -> (Format.formatter -> unit) -> t
end
val to_internal_error : Content.t -> Content.t
type content_type = Error | Warning | Debug | Log | Result
val emit_content : Content.t -> content_type -> unit

View File

@ -319,7 +319,7 @@ let driver source_file (options : Cli.options) : int =
with Messages.CompilerError error_content ->
raise
(Messages.CompilerError
(Messages.to_internal_error error_content))
(Messages.Content.mark_as_internal_error error_content))
in
(* That's it! *)
Messages.emit_result "Typechecking successful!"
@ -355,7 +355,7 @@ let driver source_file (options : Cli.options) : int =
with Messages.CompilerError error_content ->
raise
(Messages.CompilerError
(Messages.to_internal_error error_content))
(Messages.Content.mark_as_internal_error error_content))
in
if !Cli.check_invariants_flag then (
Messages.emit_debug "Checking invariants...";
@ -445,11 +445,28 @@ let driver source_file (options : Cli.options) : int =
else prgm
in
Messages.emit_debug "Retyping lambda calculus...";
let prgm =
Shared_ast.Program.untype
(Shared_ast.Typing.program ~leave_unresolved:true prgm)
in
prgm)
try
let prgm =
Shared_ast.Program.untype
(Shared_ast.Typing.program ~leave_unresolved:true prgm)
in
prgm
with Messages.CompilerError content ->
raise
(Messages.CompilerError
(Messages.Content.prepend_message content (fun fmt ->
Format.fprintf fmt
"As part of the compilation process, one of the \
step (closure conversion) modified the Catala \
program and re-typing after this modification \
failed with the error message below. This \
re-typing error if not your fault, but is \
likely to indicate that the program you are \
trying to compile is incompatible with the \
current compilation scheme provided by the \
Catala compiler. Try to rewrite the program to \
avoid the problematic pattern or contact the \
compiler developers for help.@\n"))))
else prgm
in
match backend with

View File

@ -0,0 +1,54 @@
```catala
declaration structure Result:
data r content integer depends on z content integer
declaration scope SubFoo:
input x content integer
output y content integer depends on z content integer
declaration scope Foo:
internal r content Result
output z content integer
scope SubFoo:
definition y of z equals x + z
scope Foo:
definition r equals Result { --r: (output of SubFoo with { -- x: 10 }).y }
definition z equals r.r of 1
```
Closure conversion fails because the type of `Result` should change to reflect
the transformed closure but we don't allow our closure conversion to change
user-defined types.
```catala-test-inline
$ catala Lcalc --avoid_exceptions -O --closure_conversion
[ERROR] As part of the compilation process, one of the step (closure conversion) modified the Catala program and re-typing after this modification failed with the error message below. This re-typing error if not your fault, but is likely to indicate that the program you are trying to compile is incompatible with the current compilation scheme provided by the Catala compiler. Try to rewrite the program to avoid the problematic pattern or contact the compiler developers for help.
Error during typechecking, incompatible types:
┌─⯈ (<any> * <any>)
└─⯈ integer → option integer
Error coming from typechecking the following expression:
┌─⯈ tests/test_scope/bad/scope_call_func_struct_closure.catala_en:10.12-10.13:
└──┐
10 │ internal r content Result
│ ‾
Type (<any> * <any>) coming from expression:
┌─⯈ tests/test_scope/bad/scope_call_func_struct_closure.catala_en:10.12-10.13:
└──┐
10 │ internal r content Result
│ ‾
Type integer → option integer coming from expression:
┌─⯈ tests/test_scope/bad/scope_call_func_struct_closure.catala_en:3.18-3.25:
└─┐
3 │ data r content integer depends on z content integer
│ ‾‾‾‾‾‾‾
#return code 255#
```

View File

@ -1,8 +1,4 @@
```catala
declaration structure Test:
data z2 content integer
data z3 content integer
declaration scope SubFoo:
input x content integer
input y content integer
@ -26,13 +22,6 @@ scope Foo:
```catala-test-inline
$ catala interpret -s Foo
[WARNING] The structure "Test" is never used; maybe it's unnecessary?
┌─⯈ tests/test_scope/good/scope_call.catala_en:2.23-2.27:
└─┐
2 │ declaration structure Test:
│ ‾‾‾‾
[RESULT] Computation successful! Results:
[RESULT] example = -7
```