The thing compiles

This commit is contained in:
Denis Merigoux 2023-05-30 16:22:05 +02:00 committed by Louis Gesbert
parent 4e6efe08da
commit d1210cc0e4
9 changed files with 51 additions and 47 deletions

View File

@ -942,9 +942,7 @@ let driver
in
Messages.emit_debug "executing '%s'..." ninja_cmd;
Sys.command ninja_cmd
| exception Sys_error e ->
Cli.error_print "can not write in %s" e;
return_err)
| exception Sys_error e -> Messages.raise_error "can not write in %s" e)
| "run" -> (
match scope with
| Some scope ->
@ -955,20 +953,16 @@ let driver
in
if 0 <> res then return_err else return_ok
| None ->
Cli.error_print "Please provide a scope to run with the -s option";
return_err)
Messages.raise_error "Please provide a scope to run with the -s option")
| "runtest" -> (
match files_or_folders with
| [f] ->
run_inline_tests ~reset:reset_test_outputs f catala_exe
(List.filter (( <> ) "") (String.split_on_char ' ' catala_opts));
0
| _ ->
Cli.error_print "Please specify a single catala file to test";
return_err)
| _ -> Messages.raise_error "Please specify a single catala file to test")
| _ ->
Cli.error_print "The command \"%s\" is unknown to clerk." command;
return_err
Messages.raise_error "The command \"%s\" is unknown to clerk." command
with Messages.CompilerError content ->
let bt = Printexc.get_raw_backtrace () in
Messages.emit_content content Error;

View File

@ -84,20 +84,24 @@ let log_format format =
(** {1 Message content} *)
type message_position = { message : string option; position : Pos.t }
type message_content = { message : string; positions : message_position list }
module Content = struct
type position = { message : string option; position : Pos.t }
type t = { message : string; positions : position list }
let of_message (s : string) : t = { message = s; positions = [] }
end
let internal_error_prefix =
"Internal Error, please report to \
https://github.com/CatalaLang/catala/issues: "
let to_internal_error (content : message_content) : message_content =
let to_internal_error (content : Content.t) : Content.t =
{ content with message = internal_error_prefix ^ content.message }
type content_type = Error | Warning | Debug | Log | Result
let emit_content (content : message_content) (typ : content_type) : unit =
let { message = msg; positions = pos } = content in
let emit_content (content : Content.t) (typ : content_type) : unit =
let { Content.message = msg; positions = pos } = content in
match !Cli.message_format_flag with
| Cli.Human ->
(match typ with
@ -110,7 +114,7 @@ let emit_content (content : message_content) (typ : content_type) : unit =
(if pos = [] then "" else "\n\n")
(String.concat "\n\n"
(List.map
(fun (pos : message_position) ->
(fun (pos : Content.position) ->
Printf.sprintf "%s%s"
(match pos.message with None -> "" | Some msg -> msg ^ "\n")
(Pos.retrieve_loc_text pos.position))
@ -144,7 +148,7 @@ let emit_content (content : message_content) (typ : content_type) : unit =
(if
pos != []
&& List.for_all
(fun (pos' : message_position) -> Option.is_some pos'.message)
(fun (pos' : Content.position) -> Option.is_some pos'.message)
pos
then
Format.asprintf "%a: %s %s\n"
@ -157,7 +161,7 @@ let emit_content (content : message_content) (typ : content_type) : unit =
(fun pos' ->
Format.asprintf "%a: %s %s"
(Cli.format_with_style [ANSITerminal.blue])
(Pos.to_string_short pos'.position)
(Pos.to_string_short pos'.Content.position)
severity
(match pos'.message with
| None -> remove_new_lines msg
@ -166,7 +170,7 @@ let emit_content (content : message_content) (typ : content_type) : unit =
(** {1 Error exception} *)
exception CompilerError of message_content
exception CompilerError of Content.t
(** {1 Error printing} *)
@ -189,7 +193,9 @@ let raise_multispanned_error (spans : (string option * Pos.t) list) format =
{
message = msg;
positions =
List.map (fun (message, position) -> { message; position }) spans;
List.map
(fun (message, position) -> { Content.message; position })
spans;
}))
format
@ -214,7 +220,9 @@ let emit_multispanned_warning (pos : (string option * Pos.t) list) format =
{
message = msg;
positions =
List.map (fun (msg, pos) -> { message = msg; position = pos }) pos;
List.map
(fun (msg, pos) -> { Content.message = msg; position = pos })
pos;
}
Warning)
format

View File

@ -18,18 +18,23 @@
(** {1 Message content} *)
type message_content
module Content : sig
type t
val of_message : string -> t
end
val to_internal_error : Content.t -> Content.t
type content_type = Error | Warning | Debug | Log | Result
val to_internal_error : message_content -> message_content
val emit_content : message_content -> content_type -> unit
val emit_content : Content.t -> content_type -> unit
(** This functions emits the message according to the emission type defined by
[Cli.message_format_flag]. *)
(** {1 Error exception} *)
exception CompilerError of message_content
exception CompilerError of Content.t
(** {1 Common error raising} *)

View File

@ -37,11 +37,8 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) : bool =
match inv e with
| Ignore -> true
| Fail ->
Cli.error_format "%s failed in %s.\n\n %a" name
(Pos.to_string_short (Expr.pos e))
(Print.expr ()) e;
incr total;
false
Messages.raise_spanned_error (Expr.pos e) "%s failed\n\n%a" name
(Print.expr ()) e
| Pass ->
incr ok;
incr total;

View File

@ -569,7 +569,9 @@ let driver source_file (options : Cli.options) : int =
-1
| Sys_error msg ->
let bt = Printexc.get_raw_backtrace () in
Cli.error_print "System error: %s" msg;
Messages.emit_content
(Messages.Content.of_message ("System error: " ^ msg))
Error;
if Printexc.backtrace_status () then Printexc.print_raw_backtrace stderr bt;
-1

View File

@ -248,7 +248,7 @@ module To_jsoo = struct
(fun fmt (cname, typ) ->
match Mark.remove typ with
| TTuple _ ->
Cli.error_print
Messages.raise_spanned_error (Mark.get typ)
"Tuples aren't supported yet in the conversion to JS"
| _ ->
Format.fprintf fmt
@ -273,7 +273,7 @@ module To_jsoo = struct
(fun fmt (cname, typ) ->
match Mark.remove typ with
| TTuple _ ->
Cli.error_print
Messages.raise_spanned_error (Mark.get typ)
"Tuples aren't yet supported in the conversion to JS..."
| TLit TUnit ->
Format.fprintf fmt "@[<hv 2>| \"%a\" ->@ %a.%a ()@]"

View File

@ -230,6 +230,7 @@ let apply
ScopeName.format_t s
(Option.value ~default:"stdout" output_file);
To_json.format_program fmt s prgm)
| None -> Cli.error_print "A scope must be specified for the plugin: %s" name
| None ->
Messages.raise_error "A scope must be specified for the plugin: %s" name
let () = Driver.Plugin.register_lcalc ~name ~extension apply

View File

@ -163,11 +163,11 @@ module MakeBackendIO (B : Backend) = struct
match B.solve_vc_encoding backend_ctx encoding with
| ProvenTrue -> true
| ProvenFalse model ->
Cli.error_print "%s" (print_negative_result vc backend_ctx model);
Messages.emit_warning "%s" (print_negative_result vc backend_ctx model);
false
| Unknown -> failwith "The solver failed at proving or disproving the VC")
| Fail msg ->
Cli.error_print "%s The translation to Z3 failed:\n%s"
Messages.emit_warning "%s The translation to Z3 failed:\n%s"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Mark.remove vc.vc_variable)))

View File

@ -121,7 +121,7 @@ let run_request (request : unit -> (string * string) Lwt.t) :
if resp = "200 OK" then
try body |> Yojson.Basic.from_string with
| Yojson.Basic.Util.Type_error (msg, obj) ->
Cli.error_print
Messages.raise_error
"Error while parsing JSON answer from API: %s\n\
Specific JSON:\n\
%s\n\
@ -129,8 +129,7 @@ let run_request (request : unit -> (string * string) Lwt.t) :
%s"
msg
(Yojson.Basic.to_string obj)
body;
exit (-1)
body
| _ -> raise (Failure "")
else raise (Failure "")
in
@ -142,11 +141,10 @@ let run_request (request : unit -> (string * string) Lwt.t) :
Unix.sleep 2;
Messages.emit_debug "Retrying request...";
try_n_times (n - 1))
else (
Cli.error_print
else
Messages.raise_error
"The API request went wrong ; status is %s and the body is\n%s" resp
body;
exit (-1))
body
in
try_n_times 5
@ -191,7 +189,7 @@ let raise_article_parsing_error
(json : Yojson.Basic.t)
(msg : string)
(obj : Yojson.Basic.t) =
Cli.error_print
Messages.raise_error
"Error while manipulating JSON answer from API: %s\n\
Specific JSON:\n\
%s\n\
@ -199,8 +197,7 @@ let raise_article_parsing_error
%s"
msg
(Yojson.Basic.to_string obj)
(Yojson.Basic.to_string json);
exit 1
(Yojson.Basic.to_string json)
let get_article_id (article : article) : string =
try