mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-08 07:51:43 +03:00
Use ocolor instead of ANSITerminal
This commit is contained in:
parent
7aa7bfb8fa
commit
deaf40761e
@ -919,10 +919,7 @@ let driver
|
||||
in
|
||||
if there_is_some_fails then
|
||||
List.iter
|
||||
(fun f ->
|
||||
f
|
||||
|> Cli.with_style [ANSITerminal.magenta] "%s"
|
||||
|> Messages.emit_warning "No test case found for %s")
|
||||
(Messages.emit_warning "No test case found for @{<magenta>%s@}")
|
||||
ctx.all_failed_names;
|
||||
if 0 = List.compare_lengths ctx.all_failed_names files_or_folders then
|
||||
return_ok
|
||||
|
@ -86,8 +86,10 @@ let contents : string ref = ref ""
|
||||
(** Prints debug information *)
|
||||
let debug_flag = ref false
|
||||
|
||||
type when_enum = Auto | Always | Never
|
||||
|
||||
(* Styles the terminal output *)
|
||||
let style_flag = ref true
|
||||
let style_flag = ref Auto
|
||||
|
||||
(* Max number of digits to show for decimal results *)
|
||||
let max_prec_digits = ref 20
|
||||
@ -113,8 +115,6 @@ let file =
|
||||
let debug =
|
||||
Arg.(value & flag & info ["debug"; "d"] ~doc:"Prints debug information.")
|
||||
|
||||
type when_enum = Auto | Always | Never
|
||||
|
||||
let when_opt = Arg.enum ["auto", Auto; "always", Always; "never", Never]
|
||||
|
||||
let color =
|
||||
@ -370,11 +370,7 @@ let catala_t f = Term.(const f $ file $ options)
|
||||
|
||||
let set_option_globals options : unit =
|
||||
debug_flag := options.debug;
|
||||
(style_flag :=
|
||||
match options.color with
|
||||
| Always -> true
|
||||
| Never -> false
|
||||
| Auto -> Unix.isatty Unix.stdout);
|
||||
style_flag := options.color;
|
||||
(match options.max_prec_digits with
|
||||
| None -> ()
|
||||
| Some i -> max_prec_digits := i);
|
||||
@ -479,42 +475,42 @@ let info =
|
||||
let exits = Cmd.Exit.defaults @ [Cmd.Exit.info ~doc:"on error." 1] in
|
||||
Cmd.info "catala" ~version ~doc ~exits ~man
|
||||
|
||||
let with_style
|
||||
(styles : ANSITerminal.style list)
|
||||
(str : ('a, unit, string) format) =
|
||||
if !style_flag then ANSITerminal.sprintf styles str else Printf.sprintf str
|
||||
|
||||
let format_with_style (styles : ANSITerminal.style list) fmt (str : string) =
|
||||
if !style_flag then
|
||||
Format.pp_print_as fmt (String.length str)
|
||||
(ANSITerminal.sprintf styles "%s" str)
|
||||
else Format.pp_print_string fmt str
|
||||
|
||||
let call_unstyled f =
|
||||
let prev = !style_flag in
|
||||
style_flag := false;
|
||||
let res = f () in
|
||||
style_flag := prev;
|
||||
res
|
||||
|
||||
let concat_with_line_depending_prefix_and_suffix
|
||||
(prefix : int -> string)
|
||||
(suffix : int -> string)
|
||||
(ss : string list) =
|
||||
match ss with
|
||||
| [] -> prefix 0
|
||||
| _ :: _ ->
|
||||
let len = List.length ss in
|
||||
let suffix i = if i < len - 1 then suffix i else "" in
|
||||
String.concat ""
|
||||
@@ List.concat
|
||||
@@ List.mapi
|
||||
(fun i s -> [prefix i; (if s = "" then "" else " "); s; suffix i])
|
||||
ss
|
||||
|
||||
(** The int argument of the prefix corresponds to the line number, starting at 0 *)
|
||||
let add_prefix_to_each_line (s : string) (prefix : int -> string) =
|
||||
concat_with_line_depending_prefix_and_suffix
|
||||
(fun i -> prefix i)
|
||||
(fun _ -> "\n")
|
||||
(String.split_on_char '\n' s)
|
||||
(* let with_style
|
||||
* (styles : ANSITerminal.style list)
|
||||
* (str : ('a, unit, string) format) =
|
||||
* if !style_flag then ANSITerminal.sprintf styles str else Printf.sprintf str
|
||||
*
|
||||
* let format_with_style (styles : ANSITerminal.style list) fmt (str : string) =
|
||||
* if !style_flag then
|
||||
* Format.pp_print_as fmt (String.length str)
|
||||
* (ANSITerminal.sprintf styles "%s" str)
|
||||
* else Format.pp_print_string fmt str
|
||||
*
|
||||
* let call_unstyled f =
|
||||
* let prev = !style_flag in
|
||||
* style_flag := false;
|
||||
* let res = f () in
|
||||
* style_flag := prev;
|
||||
* res
|
||||
*
|
||||
* let concat_with_line_depending_prefix_and_suffix
|
||||
* (prefix : int -> string)
|
||||
* (suffix : int -> string)
|
||||
* (ss : string list) =
|
||||
* match ss with
|
||||
* | [] -> prefix 0
|
||||
* | _ :: _ ->
|
||||
* let len = List.length ss in
|
||||
* let suffix i = if i < len - 1 then suffix i else "" in
|
||||
* String.concat ""
|
||||
* @@ List.concat
|
||||
* @@ List.mapi
|
||||
* (fun i s -> [prefix i; (if s = "" then "" else " "); s; suffix i])
|
||||
* ss
|
||||
*
|
||||
* (\** The int argument of the prefix corresponds to the line number, starting at 0 *\)
|
||||
* let add_prefix_to_each_line (s : string) (prefix : int -> string) =
|
||||
* concat_with_line_depending_prefix_and_suffix
|
||||
* (fun i -> prefix i)
|
||||
* (fun _ -> "\n")
|
||||
* (String.split_on_char '\n' s) *)
|
||||
|
@ -35,6 +35,9 @@ type backend_option_builtin =
|
||||
|
||||
type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
|
||||
|
||||
(** The usual auto/always/never option argument *)
|
||||
type when_enum = Auto | Always | Never
|
||||
|
||||
val languages : (string * backend_lang) list
|
||||
|
||||
val language_code : backend_lang -> string
|
||||
@ -57,7 +60,7 @@ val locale_lang : backend_lang ref
|
||||
val contents : string ref
|
||||
val debug_flag : bool ref
|
||||
|
||||
val style_flag : bool ref
|
||||
val style_flag : when_enum ref
|
||||
(** Styles the terminal output *)
|
||||
|
||||
val optimize_flag : bool ref
|
||||
@ -99,9 +102,6 @@ val max_prec_digits_opt : int option Cmdliner.Term.t
|
||||
val ex_scope : string option Cmdliner.Term.t
|
||||
val output : string option Cmdliner.Term.t
|
||||
|
||||
(** The usual auto/always/never option argument *)
|
||||
type when_enum = Auto | Always | Never
|
||||
|
||||
type options = {
|
||||
debug : bool;
|
||||
color : when_enum;
|
||||
@ -136,21 +136,10 @@ val info : Cmdliner.Cmd.info
|
||||
|
||||
(**{1 Terminal formatting}*)
|
||||
|
||||
(**{2 Markers}*)
|
||||
|
||||
val with_style : ANSITerminal.style list -> ('a, unit, string) format -> 'a
|
||||
|
||||
val format_with_style :
|
||||
ANSITerminal.style list -> Format.formatter -> string -> unit
|
||||
|
||||
val call_unstyled : (unit -> 'a) -> 'a
|
||||
(** [call_unstyled f] calls the function [f] with the [style_flag] set to false
|
||||
during the execution. *)
|
||||
|
||||
(**{2 Printers}*)
|
||||
|
||||
val concat_with_line_depending_prefix_and_suffix :
|
||||
(int -> string) -> (int -> string) -> string list -> string
|
||||
|
||||
val add_prefix_to_each_line : string -> (int -> string) -> string
|
||||
(** The int argument of the prefix corresponds to the line number, starting at 0 *)
|
||||
(* val concat_with_line_depending_prefix_and_suffix :
|
||||
* (int -> string) -> (int -> string) -> string list -> string
|
||||
*
|
||||
* val add_prefix_to_each_line : string -> (int -> string) -> string
|
||||
* (\** The int argument of the prefix corresponds to the line number, starting at 0 *\) *)
|
||||
|
@ -1,7 +1,7 @@
|
||||
(library
|
||||
(name catala_utils)
|
||||
(public_name catala.catala_utils)
|
||||
(libraries cmdliner ubase ANSITerminal re bindlib catala.runtime_ocaml))
|
||||
(libraries unix cmdliner ubase ocolor re bindlib catala.runtime_ocaml))
|
||||
|
||||
(documentation
|
||||
(package catala)
|
||||
|
@ -2,153 +2,175 @@
|
||||
|
||||
(**{1 Terminal formatting}*)
|
||||
|
||||
(**{2 Markers}*)
|
||||
(* Adds handling of color tags in the formatter *)
|
||||
let[@ocaml.warning "-32"] color_formatter ppf = Ocolor_format.prettify_formatter ppf; ppf
|
||||
|
||||
let time : float ref = ref (Unix.gettimeofday ())
|
||||
(* Sets handling of tags in the formatter to ignore them (don't print any color codes) *)
|
||||
let unstyle_formatter ppf =
|
||||
Format.pp_set_mark_tags ppf false; ppf
|
||||
(* Format.pp_set_formatter_stag_functions ppf {
|
||||
* Format.mark_open_stag = (fun _ -> "");
|
||||
* mark_close_stag = (fun _ -> "");
|
||||
* print_open_stag = ignore;
|
||||
* print_close_stag = ignore;
|
||||
* };
|
||||
* ppf *)
|
||||
|
||||
let time_marker ppf () =
|
||||
(* SIDE EFFECT AT MODULE LOAD: this turns on handling of tags in [Format.sprintf] etc. functions (ignoring them) *)
|
||||
let () = ignore (unstyle_formatter Format.str_formatter)
|
||||
(* Note: we could do the same for std_formatter, err_formatter... but we'd rather promote the use of the formatting functions of this module and the below std_ppf / err_ppf *)
|
||||
|
||||
let has_color unix_fd =
|
||||
match !Cli.style_flag with
|
||||
| Cli.Never -> false
|
||||
| Always -> true
|
||||
| Auto -> Unix.isatty unix_fd
|
||||
|
||||
(* Here we affect the Ocolor printers to stderr/stdout, which remain separate from the ones used by [Format.printf] / [Format.eprintf] (which remain unchanged) *)
|
||||
|
||||
let std_ppf = lazy (
|
||||
if has_color Unix.stdout
|
||||
then Ocolor_format.raw_std_formatter
|
||||
else unstyle_formatter (Ocolor_format.raw_std_formatter)
|
||||
)
|
||||
|
||||
let err_ppf = lazy (
|
||||
if has_color Unix.stderr
|
||||
then Ocolor_format.raw_err_formatter
|
||||
else unstyle_formatter (Ocolor_format.raw_err_formatter)
|
||||
)
|
||||
|
||||
let ignore_ppf = lazy (
|
||||
Format.make_formatter (fun _ _ _ -> ()) (fun () -> ())
|
||||
)
|
||||
|
||||
let unformat (f: Format.formatter -> unit) : string =
|
||||
let buf = Buffer.create 1024 in
|
||||
let ppf = unstyle_formatter (Format.formatter_of_buffer buf) in
|
||||
Format.pp_set_margin ppf max_int; (* We won't print newlines anyways, but better not have them in the first place (this wouldn't remove cuts in a vbox for example) *)
|
||||
let out_funs = Format.pp_get_formatter_out_functions ppf () in
|
||||
Format.pp_set_formatter_out_functions ppf
|
||||
{ out_funs
|
||||
with Format.out_newline = (fun () -> out_funs.out_string " " 0 1);
|
||||
Format.out_indent = (fun _ -> ()) };
|
||||
f ppf;
|
||||
Format.pp_print_flush ppf ();
|
||||
Buffer.contents buf
|
||||
|
||||
(**{2 Message types and output helpers *)
|
||||
|
||||
type content_type = Error | Warning | Debug | Log | Result
|
||||
|
||||
let get_ppf = function
|
||||
| Result -> Lazy.force std_ppf
|
||||
| Debug when not !Cli.debug_flag -> Lazy.force ignore_ppf
|
||||
| Warning when !Cli.disable_warnings_flag -> Lazy.force ignore_ppf
|
||||
| Error | Log | Debug | Warning -> Lazy.force err_ppf
|
||||
|
||||
(**{3 Markers}*)
|
||||
|
||||
let print_time_marker =
|
||||
let time : float ref = ref (Unix.gettimeofday ()) in
|
||||
fun ppf () ->
|
||||
let new_time = Unix.gettimeofday () in
|
||||
let old_time = !time in
|
||||
time := new_time;
|
||||
let delta = (new_time -. old_time) *. 1000. in
|
||||
if delta > 50. then
|
||||
Cli.format_with_style
|
||||
[ANSITerminal.Bold; ANSITerminal.black]
|
||||
ppf
|
||||
(Format.sprintf "[TIME] %.0fms@\n" delta)
|
||||
Format.fprintf ppf "@{<bold;black>[TIME] %.0fms@}@\n" delta
|
||||
|
||||
(** Prints [\[DEBUG\]] in purple on the terminal standard output *)
|
||||
let debug_marker ppf () =
|
||||
time_marker ppf ();
|
||||
Cli.format_with_style [ANSITerminal.Bold; ANSITerminal.magenta] ppf "[DEBUG] "
|
||||
|
||||
(** Prints [\[ERROR\]] in red on the terminal error output *)
|
||||
let error_marker ppf () =
|
||||
Cli.format_with_style [ANSITerminal.Bold; ANSITerminal.red] ppf "[ERROR] "
|
||||
|
||||
(** Prints [\[WARNING\]] in yellow on the terminal standard output *)
|
||||
let warning_marker ppf () =
|
||||
Cli.format_with_style
|
||||
[ANSITerminal.Bold; ANSITerminal.yellow]
|
||||
ppf "[WARNING] "
|
||||
|
||||
(** Prints [\[RESULT\]] in green on the terminal standard output *)
|
||||
let result_marker ppf () =
|
||||
Cli.format_with_style [ANSITerminal.Bold; ANSITerminal.green] ppf "[RESULT] "
|
||||
|
||||
(** Prints [\[LOG\]] in red on the terminal error output *)
|
||||
let log_marker ppf () =
|
||||
Cli.format_with_style [ANSITerminal.Bold; ANSITerminal.black] ppf "[LOG] "
|
||||
let pp_marker target ppf () =
|
||||
let open Ocolor_types in
|
||||
let tags, str = match target with
|
||||
| Debug -> [ Bold; Fg (C4 magenta) ], "[DEBUG]"
|
||||
| Error -> [ Bold; Fg (C4 red) ], "[ERROR]"
|
||||
| Warning -> [ Bold; Fg (C4 yellow) ], "[WARNING]"
|
||||
| Result -> [ Bold; Fg (C4 green) ], "[RESULT]"
|
||||
| Log -> [ Bold; Fg (C4 black) ], "[LOG]"
|
||||
in
|
||||
if target = Debug then print_time_marker ppf ();
|
||||
Format.pp_open_stag ppf (Ocolor_format.Ocolor_styles_tag tags);
|
||||
Format.pp_print_string ppf str;
|
||||
Format.pp_close_stag ppf ()
|
||||
|
||||
(**{2 Printers}*)
|
||||
|
||||
(** All the printers below print their argument after the correct marker *)
|
||||
|
||||
let debug_format (format : ('a, Format.formatter, unit) format) =
|
||||
if !Cli.debug_flag then
|
||||
Format.printf ("%a@[<hov>" ^^ format ^^ "@]@.") debug_marker ()
|
||||
else Format.ifprintf Format.std_formatter format
|
||||
|
||||
let error_format (format : ('a, Format.formatter, unit) format) =
|
||||
Format.print_flush ();
|
||||
(* Flushes previous warnings *)
|
||||
Format.printf ("%a" ^^ format ^^ "\n%!") error_marker ()
|
||||
|
||||
let warning_format format =
|
||||
if !Cli.disable_warnings_flag then Format.ifprintf Format.std_formatter format
|
||||
else Format.printf ("%a" ^^ format ^^ "\n%!") warning_marker ()
|
||||
|
||||
let result_format format =
|
||||
Format.printf ("%a" ^^ format ^^ "\n%!") result_marker ()
|
||||
|
||||
let log_format format =
|
||||
Format.printf ("%a@[<hov>" ^^ format ^^ "@]@.") log_marker ()
|
||||
(** Prints the argument after the correct marker and to the correct channel *)
|
||||
let format target format =
|
||||
let ppf = get_ppf target in
|
||||
pp_marker target ppf ();
|
||||
Format.pp_print_space ppf ();
|
||||
Format.pp_open_hovbox ppf 0;
|
||||
Format.kfprintf (fun ppf -> Format.pp_close_box ppf (); Format.pp_print_newline ppf ()) ppf format
|
||||
|
||||
(** {1 Message content} *)
|
||||
|
||||
module Content = struct
|
||||
type position = { message : string option; position : Pos.t }
|
||||
type t = { message : string; positions : position list }
|
||||
type message = Format.formatter -> unit
|
||||
|
||||
let of_message (s : string) : t = { message = s; positions = [] }
|
||||
type position = { pos_message : message option; pos : Pos.t }
|
||||
type t = { message : message; positions : position list }
|
||||
|
||||
let of_message (message : message) : t = { message; positions = [] }
|
||||
let of_string (s : string) : t = { message = (fun ppf -> Format.pp_print_string ppf s); positions = [] }
|
||||
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 = internal_error_prefix ^ content.message }
|
||||
{ content with message = (fun ppf -> Format.fprintf ppf "%s@\n%t" internal_error_prefix content.message)}
|
||||
|
||||
type content_type = Error | Warning | Debug | Log | Result
|
||||
|
||||
let emit_content (content : Content.t) (typ : content_type) : unit =
|
||||
let { Content.message = msg; positions = pos } = content in
|
||||
let emit_content (content : Content.t) (target : content_type) : unit =
|
||||
let { message; positions } = content in
|
||||
match !Cli.message_format_flag with
|
||||
| Cli.Human ->
|
||||
(match typ with
|
||||
| Warning -> warning_format
|
||||
| Error -> error_format
|
||||
| Debug -> debug_format
|
||||
| Log -> log_format
|
||||
| Result -> result_format)
|
||||
"%s%s%s" msg
|
||||
(if pos = [] then "" else "\n\n")
|
||||
(String.concat "\n\n"
|
||||
(List.map
|
||||
(fun (pos : Content.position) ->
|
||||
Printf.sprintf "%s%s"
|
||||
(match pos.message with None -> "" | Some msg -> msg ^ "\n")
|
||||
(Pos.retrieve_loc_text pos.position))
|
||||
pos))
|
||||
format target
|
||||
"@[<v>%t%a@]"
|
||||
message
|
||||
(fun ppf l -> Format.pp_print_list
|
||||
~pp_sep:(fun _ () -> ())
|
||||
(fun ppf pos ->
|
||||
Format.pp_print_cut ppf ();
|
||||
Format.pp_print_cut ppf ();
|
||||
Option.iter (fun msg -> Format.fprintf ppf "%t@," msg) pos.pos_message;
|
||||
Pos.format_loc_text ppf pos.pos)
|
||||
ppf l)
|
||||
positions
|
||||
| Cli.GNU ->
|
||||
let remove_new_lines s =
|
||||
Re.replace ~all:true
|
||||
(Re.compile (Re.seq [Re.char '\n'; Re.rep Re.blank]))
|
||||
~f:(fun _ -> " ")
|
||||
s
|
||||
in
|
||||
let severity =
|
||||
Format.asprintf "%a"
|
||||
(match typ with
|
||||
| Warning -> warning_marker
|
||||
| Error -> error_marker
|
||||
| Debug -> debug_marker
|
||||
| Log -> log_marker
|
||||
| Result -> result_marker)
|
||||
()
|
||||
in
|
||||
(* The top message doesn't come with a position, which is not something the
|
||||
GNU standard allows. So we look the position list and put the top message
|
||||
everywhere there is not a more precise message. If we can'r find a
|
||||
position without a more precise message, we just take the first position
|
||||
in the list to pair with the message. *)
|
||||
(match typ with
|
||||
| Error -> Format.eprintf
|
||||
| Warning | Log | Debug | Result -> Format.printf)
|
||||
"%s%s\n"
|
||||
(if
|
||||
pos != []
|
||||
&& List.for_all
|
||||
(fun (pos' : Content.position) -> Option.is_some pos'.message)
|
||||
pos
|
||||
let marker = pp_marker target in
|
||||
let ppf = get_ppf target in
|
||||
let () =
|
||||
if
|
||||
positions != []
|
||||
&& List.for_all
|
||||
(fun (pos' : Content.position) -> Option.is_some pos'.pos_message)
|
||||
positions
|
||||
then
|
||||
Format.asprintf "%a: %s %s\n"
|
||||
(Cli.format_with_style [ANSITerminal.blue])
|
||||
(Pos.to_string_short (List.hd pos).position)
|
||||
severity (remove_new_lines msg)
|
||||
else "")
|
||||
(String.concat "\n"
|
||||
(List.map
|
||||
(fun pos' ->
|
||||
Format.asprintf "%a: %s %s"
|
||||
(Cli.format_with_style [ANSITerminal.blue])
|
||||
(Pos.to_string_short pos'.Content.position)
|
||||
severity
|
||||
(match pos'.message with
|
||||
| None -> remove_new_lines msg
|
||||
| Some msg' -> remove_new_lines msg'))
|
||||
pos))
|
||||
Format.fprintf ppf ("@{<blue>%s@}: %a %s@\n")
|
||||
(Pos.to_string_short (List.hd positions).pos)
|
||||
marker ()
|
||||
(unformat message)
|
||||
in
|
||||
Format.pp_print_list
|
||||
~pp_sep:Format.pp_print_newline
|
||||
(fun ppf pos' ->
|
||||
Format.fprintf ppf ("@{<blue>%s@}: %a %s")
|
||||
(Pos.to_string_short pos'.pos)
|
||||
marker ()
|
||||
(match pos'.pos_message with
|
||||
| None -> unformat message
|
||||
| Some msg' -> unformat msg'))
|
||||
ppf
|
||||
positions
|
||||
|
||||
(** {1 Error exception} *)
|
||||
|
||||
@ -156,34 +178,39 @@ exception CompilerError of Content.t
|
||||
|
||||
(** {1 Error printing} *)
|
||||
|
||||
let raise_spanned_error ?(span_msg : string option) (span : Pos.t) format =
|
||||
Format.kasprintf
|
||||
(fun msg ->
|
||||
let raise_spanned_error ?(span_msg : Content.message option) (span : Pos.t) format =
|
||||
Format.kdprintf
|
||||
(fun message ->
|
||||
raise
|
||||
(CompilerError
|
||||
{
|
||||
message = msg;
|
||||
positions = [{ message = span_msg; position = span }];
|
||||
message;
|
||||
positions = [{ pos_message = span_msg; pos = span }];
|
||||
}))
|
||||
format
|
||||
|
||||
let raise_multispanned_error (spans : (string option * Pos.t) list) format =
|
||||
Format.kasprintf
|
||||
(fun msg ->
|
||||
let raise_multispanned_error_full (spans : (Content.message option * Pos.t) list) format =
|
||||
Format.kdprintf
|
||||
(fun message ->
|
||||
raise
|
||||
(CompilerError
|
||||
{
|
||||
message = msg;
|
||||
message;
|
||||
positions =
|
||||
List.map
|
||||
(fun (message, position) -> { Content.message; position })
|
||||
(fun (pos_message, pos) -> { pos_message; pos })
|
||||
spans;
|
||||
}))
|
||||
format
|
||||
|
||||
let raise_multispanned_error spans format =
|
||||
raise_multispanned_error_full
|
||||
(List.map (fun (msg, pos) -> Option.map (fun s ppf -> Format.pp_print_string ppf s) msg, pos) spans)
|
||||
format
|
||||
|
||||
let raise_error format =
|
||||
Format.kasprintf
|
||||
(fun msg -> raise (CompilerError { message = msg; positions = [] }))
|
||||
Format.kdprintf
|
||||
(fun message -> raise (CompilerError { message; positions = [] }))
|
||||
format
|
||||
|
||||
let raise_internal_error format =
|
||||
@ -195,36 +222,36 @@ let assert_internal_error condition fmt =
|
||||
if condition then raise_internal_error ("assertion failed: " ^^ fmt)
|
||||
else Format.ifprintf (Format.formatter_of_out_channel stdout) fmt
|
||||
|
||||
let emit_multispanned_warning (pos : (string option * Pos.t) list) format =
|
||||
Format.kasprintf
|
||||
(fun msg ->
|
||||
let emit_multispanned_warning (pos : (Content.message option * Pos.t) list) format =
|
||||
Format.kdprintf
|
||||
(fun message ->
|
||||
emit_content
|
||||
{
|
||||
message = msg;
|
||||
message;
|
||||
positions =
|
||||
List.map
|
||||
(fun (msg, pos) -> { Content.message = msg; position = pos })
|
||||
(fun (pos_message, pos) -> { pos_message; pos })
|
||||
pos;
|
||||
}
|
||||
Warning)
|
||||
format
|
||||
|
||||
let emit_spanned_warning ?(span_msg : string option) (span : Pos.t) format =
|
||||
let emit_spanned_warning ?(span_msg : Content.message option) (span : Pos.t) format =
|
||||
emit_multispanned_warning [span_msg, span] format
|
||||
|
||||
let emit_warning format = emit_multispanned_warning [] format
|
||||
|
||||
let emit_log format =
|
||||
Format.kasprintf
|
||||
(fun msg -> emit_content { message = msg; positions = [] } Log)
|
||||
Format.kdprintf
|
||||
(fun message -> emit_content { message; positions = [] } Log)
|
||||
format
|
||||
|
||||
let emit_debug format =
|
||||
Format.kasprintf
|
||||
(fun msg -> emit_content { message = msg; positions = [] } Debug)
|
||||
Format.kdprintf
|
||||
(fun message -> emit_content { message; positions = [] } Debug)
|
||||
format
|
||||
|
||||
let emit_result format =
|
||||
Format.kasprintf
|
||||
(fun msg -> emit_content { message = msg; positions = [] } Result)
|
||||
Format.kdprintf
|
||||
(fun message -> emit_content { message; positions = [] } Result)
|
||||
format
|
||||
|
@ -14,14 +14,21 @@
|
||||
License for the specific language governing permissions and limitations under
|
||||
the License. *)
|
||||
|
||||
(** Interface for emitting compiler messages *)
|
||||
(** Interface for emitting compiler messages.
|
||||
|
||||
All messages are expected to use the [Format] module. Flush, ["@?"], ["@."], ["%!"] etc. are not supposed to be used outside of this module.
|
||||
|
||||
WARNING: this module performs side-effects at load time, adding support for ocolor tags (e.g. ["@{<blue>text@}"]) to the standard string formatter used by e.g. [Format.sprintf]. (In this case, the tags are ignored, for color output you should use the functions of this module that toggle support depending on cli flags and terminal support).
|
||||
*)
|
||||
|
||||
(** {1 Message content} *)
|
||||
|
||||
module Content : sig
|
||||
type message = Format.formatter -> unit
|
||||
type t
|
||||
|
||||
val of_message : string -> t
|
||||
val of_message : (Format.formatter -> unit) -> t
|
||||
val of_string : string -> t
|
||||
end
|
||||
|
||||
val to_internal_error : Content.t -> Content.t
|
||||
@ -39,7 +46,10 @@ exception CompilerError of Content.t
|
||||
(** {1 Common error raising} *)
|
||||
|
||||
val raise_spanned_error :
|
||||
?span_msg:string -> Pos.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
|
||||
?span_msg:Content.message -> Pos.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
|
||||
|
||||
val raise_multispanned_error_full :
|
||||
(Content.message option * Pos.t) list -> ('a, Format.formatter, unit, 'b) format4 -> 'a
|
||||
|
||||
val raise_multispanned_error :
|
||||
(string option * Pos.t) list -> ('a, Format.formatter, unit, 'b) format4 -> 'a
|
||||
@ -53,10 +63,10 @@ val assert_internal_error :
|
||||
(** {1 Common warning emission}*)
|
||||
|
||||
val emit_multispanned_warning :
|
||||
(string option * Pos.t) list -> ('a, Format.formatter, unit) format -> 'a
|
||||
(Content.message option * Pos.t) list -> ('a, Format.formatter, unit) format -> 'a
|
||||
|
||||
val emit_spanned_warning :
|
||||
?span_msg:string -> Pos.t -> ('a, Format.formatter, unit) format -> 'a
|
||||
?span_msg:Content.message -> Pos.t -> ('a, Format.formatter, unit) format -> 'a
|
||||
|
||||
val emit_warning : ('a, Format.formatter, unit) format -> 'a
|
||||
|
||||
@ -71,3 +81,24 @@ val emit_debug : ('a, Format.formatter, unit) format -> 'a
|
||||
(* {1 Common result emission}*)
|
||||
|
||||
val emit_result : ('a, Format.formatter, unit) format -> 'a
|
||||
|
||||
(* {1 Some formatting helpers}*)
|
||||
|
||||
val unformat: (Format.formatter -> unit) -> string
|
||||
(* Converts [f] to a string, discarding formatting and skipping newlines and indents *)
|
||||
|
||||
|
||||
|
||||
(*
|
||||
(**{2 Markers}*)
|
||||
|
||||
val with_style : ANSITerminal.style list -> ('a, unit, string) format -> 'a
|
||||
|
||||
val format_with_style :
|
||||
ANSITerminal.style list -> Format.formatter -> string -> unit
|
||||
|
||||
val call_unstyled : (unit -> 'a) -> 'a
|
||||
(** [call_unstyled f] calls the function [f] with the [style_flag] set to false
|
||||
during the execution. *)
|
||||
|
||||
*)
|
||||
|
@ -136,15 +136,15 @@ let utf8_byte_index s ui0 =
|
||||
in
|
||||
aux 0 0
|
||||
|
||||
let retrieve_loc_text (pos : t) : string =
|
||||
let format_loc_text ppf (pos : t) =
|
||||
try
|
||||
let filename = get_file pos in
|
||||
let blue_style = [ANSITerminal.Bold; ANSITerminal.blue] in
|
||||
if filename = "" then "No position information"
|
||||
if filename = "" then
|
||||
Format.pp_print_string ppf "No position information"
|
||||
else
|
||||
let sline = get_start_line pos in
|
||||
let eline = get_end_line pos in
|
||||
let oc, input_line_opt =
|
||||
let ic, input_line_opt =
|
||||
if filename = "stdin" then
|
||||
let line_index = ref 0 in
|
||||
let lines = String.split_on_char '\n' !Cli.contents in
|
||||
@ -157,15 +157,36 @@ let retrieve_loc_text (pos : t) : string =
|
||||
in
|
||||
None, input_line_opt
|
||||
else
|
||||
let oc = open_in filename in
|
||||
let ic = open_in filename in
|
||||
let input_line_opt () : string option =
|
||||
try Some (input_line oc) with End_of_file -> None
|
||||
try Some (input_line ic) with End_of_file -> None
|
||||
in
|
||||
Some oc, input_line_opt
|
||||
Some ic, input_line_opt
|
||||
in
|
||||
let print_matched_line (line : string) (line_no : int) : string =
|
||||
let include_extra_count = 0 in
|
||||
let rec get_lines (n : int) : (int * string) list =
|
||||
match input_line_opt () with
|
||||
| Some line ->
|
||||
if n < sline - include_extra_count then get_lines (n + 1)
|
||||
else if
|
||||
n >= sline - include_extra_count && n <= eline + include_extra_count
|
||||
then (n, line) :: get_lines (n + 1)
|
||||
else []
|
||||
| None -> []
|
||||
in
|
||||
let pos_lines = get_lines 1 in
|
||||
let nspaces = int_of_float (log10 (float_of_int eline)) + 1 in
|
||||
let legal_pos_lines =
|
||||
List.rev_map
|
||||
(fun s ->
|
||||
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
|
||||
~subst:(fun _ -> " ")
|
||||
s)
|
||||
pos.law_pos
|
||||
in
|
||||
(match ic with None -> () | Some ic -> close_in ic);
|
||||
let print_matched_line ppf (line_no, line : int * string) =
|
||||
let line_indent = indent_number line in
|
||||
let error_indicator_style = [ANSITerminal.red; ANSITerminal.Bold] in
|
||||
let match_start_index =
|
||||
utf8_byte_index line
|
||||
(if line_no = sline then get_start_column pos - 1 else line_indent)
|
||||
@ -181,88 +202,28 @@ let retrieve_loc_text (pos : t) : string =
|
||||
in
|
||||
let match_start_col = string_columns unmatched_prefix in
|
||||
let match_num_cols = string_columns matched_substring in
|
||||
String.concat ""
|
||||
(line
|
||||
:: "\n"
|
||||
::
|
||||
(if line_no >= sline && line_no <= eline then
|
||||
[
|
||||
string_repeat match_start_col " ";
|
||||
Cli.with_style error_indicator_style "%s"
|
||||
(string_repeat match_num_cols "‾");
|
||||
]
|
||||
else []))
|
||||
Format.fprintf ppf "@{<bold;blue>%*d │@} %s@," nspaces line_no line;
|
||||
if line_no >= sline && line_no <= eline then
|
||||
Format.fprintf ppf "@{<bold;blue>%s │@} %s@{<bold;red>%s@}"
|
||||
(string_repeat nspaces " ")
|
||||
(string_repeat match_start_col " ")
|
||||
(string_repeat match_num_cols "‾")
|
||||
in
|
||||
let include_extra_count = 0 in
|
||||
let rec get_lines (n : int) : string list =
|
||||
match input_line_opt () with
|
||||
| Some line ->
|
||||
if n < sline - include_extra_count then get_lines (n + 1)
|
||||
else if
|
||||
n >= sline - include_extra_count && n <= eline + include_extra_count
|
||||
then print_matched_line line n :: get_lines (n + 1)
|
||||
else []
|
||||
| None -> []
|
||||
in
|
||||
let pos_lines = get_lines 1 in
|
||||
let spaces = int_of_float (log10 (float_of_int eline)) + 1 in
|
||||
let legal_pos_lines =
|
||||
List.rev
|
||||
(List.map
|
||||
(fun s ->
|
||||
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
|
||||
~subst:(fun _ -> " ")
|
||||
s)
|
||||
pos.law_pos)
|
||||
in
|
||||
(match oc with None -> () | Some oc -> close_in oc);
|
||||
let buf = Buffer.create 73 in
|
||||
Buffer.add_string buf
|
||||
(Cli.with_style blue_style "┌─⯈ %s:" (to_string_short pos));
|
||||
Buffer.add_char buf '\n';
|
||||
(* should be outside of [Cli.with_style] *)
|
||||
Buffer.add_string buf
|
||||
(Cli.with_style blue_style "└%s┐" (string_repeat spaces "─"));
|
||||
Buffer.add_char buf '\n';
|
||||
Buffer.add_string buf
|
||||
(Cli.add_prefix_to_each_line (String.concat "\n" pos_lines) (fun i ->
|
||||
let cur_line = sline - include_extra_count + i in
|
||||
if
|
||||
cur_line >= sline
|
||||
&& cur_line <= sline + (2 * (eline - sline))
|
||||
&& cur_line mod 2 = sline mod 2
|
||||
then
|
||||
Cli.with_style blue_style "%*d │" spaces
|
||||
(sline + ((cur_line - sline) / 2))
|
||||
else if cur_line >= sline - include_extra_count && cur_line < sline
|
||||
then Cli.with_style blue_style "%*d │" spaces (cur_line + 1)
|
||||
else if
|
||||
cur_line
|
||||
<= sline + (2 * (eline - sline)) + 1 + include_extra_count
|
||||
&& cur_line > sline + (2 * (eline - sline)) + 1
|
||||
then
|
||||
Cli.with_style blue_style "%*d │" spaces
|
||||
(cur_line - (eline - sline + 1))
|
||||
else Cli.with_style blue_style "%*s │" spaces ""));
|
||||
Buffer.add_char buf '\n';
|
||||
let () =
|
||||
match legal_pos_lines with
|
||||
Format.pp_open_vbox ppf 0;
|
||||
Format.fprintf ppf "@{<bold;blue>┌─⯈ %s:@}@," (to_string_short pos);
|
||||
Format.fprintf ppf "@{<bold;blue>└%s┐@}@," (string_repeat nspaces "─");
|
||||
Format.pp_print_list print_matched_line ppf pos_lines;
|
||||
Format.pp_print_cut ppf ();
|
||||
let rec pp_legal nspaces = function
|
||||
| [last] ->
|
||||
Format.fprintf ppf "@{<bold;blue>%*s└─ %s@}" nspaces "" last
|
||||
| l :: lines ->
|
||||
Format.fprintf ppf "@{<bold;blue>%*s└┬ %s@}" nspaces "" l;
|
||||
pp_legal (nspaces + 1) lines
|
||||
| [] -> ()
|
||||
| _ ->
|
||||
let last = List.length legal_pos_lines - 1 in
|
||||
Buffer.add_string buf
|
||||
(Cli.add_prefix_to_each_line
|
||||
(String.concat "\n"
|
||||
(List.map
|
||||
(fun l -> Cli.with_style blue_style "%s" l)
|
||||
legal_pos_lines))
|
||||
(fun i ->
|
||||
if i = last then
|
||||
Cli.with_style blue_style "%*s└─" (spaces + i + 1) ""
|
||||
else Cli.with_style blue_style "%*s└┬" (spaces + i + 1) ""))
|
||||
in
|
||||
Buffer.contents buf
|
||||
with Sys_error _ -> "Location:" ^ to_string pos
|
||||
pp_legal (nspaces + 1) legal_pos_lines
|
||||
with Sys_error _ -> Format.fprintf ppf "Location: %s" (to_string pos)
|
||||
|
||||
let no_pos : t =
|
||||
let zero_pos =
|
||||
|
@ -57,7 +57,7 @@ val to_string_short : t -> string
|
||||
{{:https://www.gnu.org/prep/standards/standards.html#Errors} GNU coding
|
||||
standards}. *)
|
||||
|
||||
val retrieve_loc_text : t -> string
|
||||
val format_loc_text : Format.formatter -> t -> unit
|
||||
(** Open the file corresponding to the position and retrieves the text concerned
|
||||
by the position *)
|
||||
|
||||
|
@ -35,12 +35,10 @@ let detect_empty_definitions (p : program) : unit =
|
||||
then
|
||||
Messages.emit_spanned_warning
|
||||
(ScopeDef.get_position scope_def_key)
|
||||
"In scope %a, the variable %a is declared but never defined; did \
|
||||
"In scope @{<yellow>\"%a\"@}, the variable @{<yellow>\"%a\"@} is declared but never defined; did \
|
||||
you forget something?"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" ScopeName.format_t scope_name)
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" Ast.ScopeDef.format_t scope_def_key))
|
||||
ScopeName.format_t scope_name
|
||||
Ast.ScopeDef.format_t scope_def_key)
|
||||
scope.scope_defs)
|
||||
p.program_scopes
|
||||
|
||||
@ -147,9 +145,8 @@ let detect_unused_struct_fields (p : program) : unit =
|
||||
then
|
||||
Messages.emit_spanned_warning
|
||||
(snd (StructName.get_info s_name))
|
||||
"The structure %a is never used; maybe it's unnecessary?"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" StructName.format_t s_name)
|
||||
"The structure @{<yellow>\"%a\"@} is never used; maybe it's unnecessary?"
|
||||
StructName.format_t s_name
|
||||
else
|
||||
StructField.Map.iter
|
||||
(fun field _ ->
|
||||
@ -159,12 +156,10 @@ let detect_unused_struct_fields (p : program) : unit =
|
||||
then
|
||||
Messages.emit_spanned_warning
|
||||
(snd (StructField.get_info field))
|
||||
"The field %a of struct %a is never used; maybe it's \
|
||||
"The field @{<yellow>\"%a\"@} of struct @{<yellow>\"%a\"@} is never used; maybe it's \
|
||||
unnecessary?"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" StructField.format_t field)
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" StructName.format_t s_name))
|
||||
StructField.format_t field
|
||||
StructName.format_t s_name)
|
||||
fields)
|
||||
p.program_ctx.ctx_structs
|
||||
|
||||
@ -203,9 +198,8 @@ let detect_unused_enum_constructors (p : program) : unit =
|
||||
then
|
||||
Messages.emit_spanned_warning
|
||||
(snd (EnumName.get_info e_name))
|
||||
"The enumeration %a is never used; maybe it's unnecessary?"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" EnumName.format_t e_name)
|
||||
"The enumeration @{<yellow>\"%a\"@} is never used; maybe it's unnecessary?"
|
||||
EnumName.format_t e_name
|
||||
else
|
||||
EnumConstructor.Map.iter
|
||||
(fun constructor _ ->
|
||||
@ -213,12 +207,10 @@ let detect_unused_enum_constructors (p : program) : unit =
|
||||
then
|
||||
Messages.emit_spanned_warning
|
||||
(snd (EnumConstructor.get_info constructor))
|
||||
"The constructor %a of enumeration %a is never used; maybe \
|
||||
"The constructor @{<yellow>\"%a\"@} of enumeration @{<yellow>\"%a\"@} is never used; maybe \
|
||||
it's unnecessary?"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" EnumConstructor.format_t constructor)
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" EnumName.format_t e_name))
|
||||
EnumConstructor.format_t constructor
|
||||
EnumName.format_t e_name)
|
||||
constructors)
|
||||
p.program_ctx.ctx_enums
|
||||
|
||||
@ -263,9 +255,8 @@ let detect_dead_code (p : program) : unit =
|
||||
Messages.emit_spanned_warning
|
||||
(Mark.get (ScopeVar.get_info var))
|
||||
"This variable is dead code; it does not contribute to computing \
|
||||
any of scope %a outputs. Did you forget something?"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ Mark.remove (ScopeName.get_info scope_name) ^ "\"")
|
||||
any of scope @{<yellow>\"%s\"@} outputs. Did you forget something?"
|
||||
(Mark.remove (ScopeName.get_info scope_name))
|
||||
in
|
||||
match states with
|
||||
| WholeVar ->
|
||||
|
@ -100,8 +100,9 @@ let raise_unsupported_feature (msg : string) (pos : Pos.t) =
|
||||
(** Function to call whenever an identifier used somewhere has not been declared
|
||||
in the program previously *)
|
||||
let raise_unknown_identifier (msg : string) (ident : IdentName.t Mark.pos) =
|
||||
Messages.raise_spanned_error (Mark.get ident) "\"%s\": unknown identifier %s"
|
||||
(Cli.with_style [ANSITerminal.yellow] "%s" (Mark.remove ident))
|
||||
Messages.raise_spanned_error (Mark.get ident)
|
||||
"@{<yellow>\"%s\"@}: unknown identifier %s"
|
||||
(Mark.remove ident)
|
||||
msg
|
||||
|
||||
(** Gets the type associated to an uid *)
|
||||
@ -259,8 +260,7 @@ let process_subscope_decl
|
||||
in
|
||||
Messages.raise_multispanned_error
|
||||
[Some "first use", Mark.get info; Some "second use", s_pos]
|
||||
"Subscope name \"%a\" already used"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
"Subscope name @{<yellow>\"%s\"@} already used"
|
||||
subscope
|
||||
| None ->
|
||||
let sub_scope_uid = SubScopeName.fresh (name, name_pos) in
|
||||
@ -314,8 +314,7 @@ let rec process_base_typ
|
||||
TStruct scope_str.out_struct_name, typ_pos
|
||||
| None ->
|
||||
Messages.raise_spanned_error typ_pos
|
||||
"Unknown type \"%a\", not a struct or enum previously declared"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
"Unknown type @{<yellow>\"%s\"@}, not a struct or enum previously declared"
|
||||
ident)
|
||||
| Surface.Ast.Named (_path, (_ident, _pos)) ->
|
||||
Messages.raise_spanned_error typ_pos
|
||||
@ -349,8 +348,7 @@ let process_data_decl
|
||||
in
|
||||
Messages.raise_multispanned_error
|
||||
[Some "First use:", Mark.get info; Some "Second use:", pos]
|
||||
"Variable name \"%a\" already used"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
"Variable name @{<yellow>\"%s\"@} already used"
|
||||
name
|
||||
| None ->
|
||||
let uid = ScopeVar.fresh (name, pos) in
|
||||
@ -366,17 +364,15 @@ let process_data_decl
|
||||
((states_idmap : StateName.t IdentName.Map.t), states_list) ->
|
||||
let state_id_name = Mark.remove state_id in
|
||||
if IdentName.Map.mem state_id_name states_idmap then
|
||||
Messages.raise_multispanned_error
|
||||
Messages.raise_multispanned_error_full
|
||||
[
|
||||
( Some
|
||||
(Format.asprintf "First instance of state %a:"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ state_id_name ^ "\"")),
|
||||
(fun ppf -> Format.fprintf ppf "First instance of state @{<yellow>\"%s\"@}:"
|
||||
state_id_name),
|
||||
Mark.get state_id );
|
||||
( Some
|
||||
(Format.asprintf "Second instance of state %a:"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ state_id_name ^ "\"")),
|
||||
(fun ppf -> Format.fprintf ppf "Second instance of state @{<yellow>\"%s\"@}:"
|
||||
state_id_name),
|
||||
Mark.get
|
||||
(IdentName.Map.find state_id_name states_idmap
|
||||
|> StateName.get_info) );
|
||||
@ -605,11 +601,10 @@ let typedef_info = function
|
||||
let process_name_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
|
||||
context =
|
||||
let raise_already_defined_error (use : Uid.MarkedString.info) name pos msg =
|
||||
Messages.raise_multispanned_error
|
||||
[Some "First definition:", Mark.get use; Some "Second definition:", pos]
|
||||
"%s name \"%a\" already defined" msg
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
name
|
||||
Messages.raise_multispanned_error_full
|
||||
[Some (fun ppf -> Format.pp_print_string ppf "First definition:"), Mark.get use;
|
||||
Some (fun ppf -> Format.pp_print_string ppf "Second definition:"), pos]
|
||||
"%s name @{<yellow>\"%s\"@} already defined" msg name
|
||||
in
|
||||
match Mark.remove item with
|
||||
| ScopeDecl decl ->
|
||||
@ -894,8 +889,7 @@ let process_scope_use (ctxt : context) (suse : Surface.Ast.scope_use) : context
|
||||
| _ ->
|
||||
Messages.raise_spanned_error
|
||||
(Mark.get suse.Surface.Ast.scope_use_name)
|
||||
"\"%a\": this scope has not been declared anywhere, is it a typo?"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
"@{<yellow>\"%s\"@}: this scope has not been declared anywhere, is it a typo?"
|
||||
(Mark.remove suse.Surface.Ast.scope_use_name)
|
||||
in
|
||||
List.fold_left
|
||||
|
@ -25,47 +25,42 @@ open Format
|
||||
|
||||
(* Original credits for this printing code: Jean-Christophe Filiâtre *)
|
||||
let format_exception_tree (fmt : Format.formatter) (t : exception_tree) =
|
||||
let blue s =
|
||||
Format.asprintf "%a" (Cli.format_with_style [ANSITerminal.blue]) s
|
||||
let blue fmt s =
|
||||
Format.fprintf fmt "@{<blue>%s@}" s
|
||||
in
|
||||
let rec print_node pref (t : exception_tree) =
|
||||
let (s, w), sons =
|
||||
let print_s s =
|
||||
( Format.asprintf "%a"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" LabelName.format_t
|
||||
s.Dependency.ExceptionVertex.label),
|
||||
String.length
|
||||
(Format.asprintf "\"%a\"" LabelName.format_t
|
||||
s.Dependency.ExceptionVertex.label) )
|
||||
in
|
||||
match t with Leaf s -> print_s s, [] | Node (sons, s) -> print_s s, sons
|
||||
let label, sons = match t with
|
||||
| Leaf l -> l.Dependency.ExceptionVertex.label, []
|
||||
| Node (sons, l) -> l.Dependency.ExceptionVertex.label, sons
|
||||
in
|
||||
pp_print_string fmt s;
|
||||
Format.fprintf fmt "@{<yellow>\"%a\"@}" LabelName.format_t label;
|
||||
let w = String.length (fst (LabelName.get_info label)) + 2 in
|
||||
if sons != [] then
|
||||
let pref' = pref ^ String.make (w + 1) ' ' in
|
||||
match sons with
|
||||
| [t'] ->
|
||||
pp_print_string fmt (blue "───");
|
||||
blue fmt "───";
|
||||
print_node (pref' ^ " ") t'
|
||||
| _ ->
|
||||
pp_print_string fmt (blue "──");
|
||||
blue fmt "──";
|
||||
print_sons pref' "─┬──" sons
|
||||
and print_sons pref start = function
|
||||
| [] -> assert false
|
||||
| [s] ->
|
||||
pp_print_string fmt (blue " └──");
|
||||
blue fmt " └──";
|
||||
print_node (pref ^ " ") s
|
||||
| s :: sons ->
|
||||
pp_print_string fmt (blue start);
|
||||
blue fmt start;
|
||||
print_node (pref ^ "| ") s;
|
||||
pp_force_newline fmt ();
|
||||
pp_print_string fmt (blue (pref ^ " │"));
|
||||
pp_force_newline fmt ();
|
||||
pp_print_string fmt (blue pref);
|
||||
pp_print_cut fmt ();
|
||||
blue fmt (pref ^ " │");
|
||||
pp_print_cut fmt ();
|
||||
blue fmt pref;
|
||||
print_sons pref " ├──" sons
|
||||
in
|
||||
print_node "" t
|
||||
Format.pp_open_vbox fmt 0;
|
||||
print_node "" t;
|
||||
Format.pp_close_box fmt ()
|
||||
|
||||
let build_exception_tree exc_graph =
|
||||
let base_cases =
|
||||
@ -91,22 +86,15 @@ let print_exceptions_graph
|
||||
(var : Ast.ScopeDef.t)
|
||||
(g : Dependency.ExceptionsDependencies.t) =
|
||||
Messages.emit_result
|
||||
"Printing the tree of exceptions for the definitions of variable %a of \
|
||||
scope %a."
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" Ast.ScopeDef.format_t var)
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" ScopeName.format_t scope);
|
||||
"Printing the tree of exceptions for the definitions of variable @{<yellow>\"%a\"@} of \
|
||||
scope @{<yellow>\"%a\"@}."
|
||||
Ast.ScopeDef.format_t var
|
||||
ScopeName.format_t scope;
|
||||
Dependency.ExceptionsDependencies.iter_vertex
|
||||
(fun ex ->
|
||||
Messages.emit_result "Definitions with label %a:\n%a"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" LabelName.format_t
|
||||
ex.Dependency.ExceptionVertex.label)
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n")
|
||||
(fun fmt (_, pos) ->
|
||||
Format.fprintf fmt "%s" (Pos.retrieve_loc_text pos)))
|
||||
Messages.emit_result "@[<v>Definitions with label @{<yellow>\"%a\"@}:@,%a@]"
|
||||
LabelName.format_t ex.Dependency.ExceptionVertex.label
|
||||
(Format.pp_print_list (fun fmt (_, pos) -> Pos.format_loc_text fmt pos))
|
||||
(RuleName.Map.bindings ex.Dependency.ExceptionVertex.rules))
|
||||
g;
|
||||
let tree = build_exception_tree g in
|
||||
|
@ -45,9 +45,7 @@ let get_scope_uid
|
||||
match Shared_ast.IdentName.Map.find_opt name ctxt.typedefs with
|
||||
| Some (Desugared.Name_resolution.TScope (uid, _)) -> uid
|
||||
| _ ->
|
||||
Messages.raise_error "There is no scope %a inside the program."
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ name ^ "\""))
|
||||
Messages.raise_error "There is no scope @{<yellow>\"%s\"@} inside the program." name)
|
||||
|
||||
let get_variable_uid
|
||||
(options : Cli.options)
|
||||
@ -80,24 +78,18 @@ let get_variable_uid
|
||||
(Shared_ast.ScopeName.Map.find scope_uid ctxt.scopes).var_idmap
|
||||
with
|
||||
| None ->
|
||||
Messages.raise_error "Variable %a not found inside scope %a"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ name ^ "\"")
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" Shared_ast.ScopeName.format_t scope_uid)
|
||||
Messages.raise_error "Variable @{<yellow>\"%s\"@} not found inside scope @{<yellow>\"%a\"@}"
|
||||
name Shared_ast.ScopeName.format_t scope_uid
|
||||
| Some
|
||||
(Desugared.Name_resolution.SubScope (subscope_var_name, subscope_name))
|
||||
-> (
|
||||
match second_part with
|
||||
| None ->
|
||||
Messages.raise_error
|
||||
"Subscope %a of scope %a cannot be selected by itself, please add \
|
||||
"Subscope @{<yellow>\"%a\"@} of scope @{<yellow>\"%a\"@} cannot be selected by itself, please add \
|
||||
\".<var>\" where <var> is a subscope variable."
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" Shared_ast.SubScopeName.format_t
|
||||
subscope_var_name)
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" Shared_ast.ScopeName.format_t scope_uid)
|
||||
Shared_ast.SubScopeName.format_t subscope_var_name
|
||||
Shared_ast.ScopeName.format_t scope_uid
|
||||
| Some second_part -> (
|
||||
match
|
||||
Shared_ast.IdentName.Map.find_opt second_part
|
||||
@ -109,15 +101,11 @@ let get_variable_uid
|
||||
(subscope_var_name, v, Pos.no_pos))
|
||||
| _ ->
|
||||
Messages.raise_error
|
||||
"Var %a of subscope %a in scope %a does not exist, please check \
|
||||
"Var @{<yellow>\"%s\"@} of subscope @{<yellow>\"%a\"@} in scope @{<yellow>\"%a\"@} does not exist, please check \
|
||||
your command line arguments."
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ second_part ^ "\"")
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" Shared_ast.SubScopeName.format_t
|
||||
subscope_var_name)
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" Shared_ast.ScopeName.format_t scope_uid)))
|
||||
second_part
|
||||
Shared_ast.SubScopeName.format_t subscope_var_name
|
||||
Shared_ast.ScopeName.format_t scope_uid))
|
||||
| Some (Desugared.Name_resolution.ScopeVar v) ->
|
||||
Some
|
||||
(Desugared.Ast.ScopeDef.Var
|
||||
@ -132,14 +120,10 @@ let get_variable_uid
|
||||
| Some state -> state
|
||||
| None ->
|
||||
Messages.raise_error
|
||||
"State %a is not found for variable %a of scope %a"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ second_part ^ "\"")
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ first_part ^ "\"")
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" Shared_ast.ScopeName.format_t
|
||||
scope_uid))
|
||||
"State @{<yellow>\"%s\"@} is not found for variable @{<yellow>\"%s\"@} of scope @{<yellow>\"%a\"@}"
|
||||
second_part
|
||||
first_part
|
||||
Shared_ast.ScopeName.format_t scope_uid)
|
||||
second_part )))
|
||||
|
||||
(** Entry function for the executable. Returns a negative number in case of
|
||||
@ -570,7 +554,7 @@ let driver source_file (options : Cli.options) : int =
|
||||
| Sys_error msg ->
|
||||
let bt = Printexc.get_raw_backtrace () in
|
||||
Messages.emit_content
|
||||
(Messages.Content.of_message ("System error: " ^ msg))
|
||||
(Messages.Content.of_string ("System error: " ^ msg))
|
||||
Error;
|
||||
if Printexc.backtrace_status () then Printexc.print_raw_backtrace stderr bt;
|
||||
-1
|
||||
|
@ -543,17 +543,16 @@ let format_program
|
||||
(fmt : Format.formatter)
|
||||
(p : 'm Ast.program)
|
||||
(type_ordering : Scopelang.Dependency.TVertex.t list) : unit =
|
||||
Cli.call_unstyled (fun _ ->
|
||||
Format.fprintf fmt
|
||||
"(** This file has been generated by the Catala compiler, do not edit! \
|
||||
*)@\n\
|
||||
@\n\
|
||||
open Runtime_ocaml.Runtime@\n\
|
||||
@\n\
|
||||
[@@@@@@ocaml.warning \"-4-26-27-32-41-42\"]@\n\
|
||||
@\n\
|
||||
%a%a@\n\
|
||||
@?"
|
||||
(format_ctx type_ordering) p.decl_ctx
|
||||
(format_code_items p.decl_ctx)
|
||||
p.code_items)
|
||||
Format.fprintf fmt
|
||||
"(** This file has been generated by the Catala compiler, do not edit! \
|
||||
*)@\n\
|
||||
@\n\
|
||||
open Runtime_ocaml.Runtime@\n\
|
||||
@\n\
|
||||
[@@@@@@ocaml.warning \"-4-26-27-32-41-42\"]@\n\
|
||||
@\n\
|
||||
%a%a@\n\
|
||||
@?"
|
||||
(format_ctx type_ordering) p.decl_ctx
|
||||
(format_code_items p.decl_ctx)
|
||||
p.code_items
|
||||
|
@ -112,18 +112,13 @@ let check_exceeding_lines
|
||||
Uutf.String.fold_utf_8 (fun (acc : int) _ _ -> acc + 1) 0 s
|
||||
in
|
||||
if len_s > max_len then (
|
||||
Messages.emit_warning "The line %s in %s is exceeding %s characters:"
|
||||
(Cli.with_style
|
||||
ANSITerminal.[Bold; yellow]
|
||||
"%d"
|
||||
(start_line + i + 1))
|
||||
(Cli.with_style ANSITerminal.[Bold; magenta] "%s" filename)
|
||||
(Cli.with_style ANSITerminal.[Bold; red] "%d" max_len);
|
||||
Messages.emit_warning "%s%s" (String.sub s 0 max_len)
|
||||
(Cli.with_style
|
||||
ANSITerminal.[red]
|
||||
"%s"
|
||||
String.(sub s max_len (len_s - max_len)))))
|
||||
Messages.emit_warning
|
||||
"@[<v>The line @{<bold;yellow>%d@} in @{<bold;magenta>%s@} is exceeding @{<bold;red}%d@} characters:@,%s@{<red>%s@}@]"
|
||||
(start_line + i + 1)
|
||||
filename
|
||||
max_len
|
||||
(String.sub s 0 max_len)
|
||||
(String.sub s max_len (len_s - max_len))))
|
||||
|
||||
let with_pygmentize_lexer lang f =
|
||||
let lexer_py =
|
||||
|
@ -402,32 +402,31 @@ module To_jsoo = struct
|
||||
module_name)
|
||||
in
|
||||
|
||||
Cli.call_unstyled (fun _ ->
|
||||
Format.fprintf fmt
|
||||
"(** This file has been generated by the Catala compiler, do not \
|
||||
edit! *)@\n\
|
||||
@\n\
|
||||
open Runtime_ocaml.Runtime@\n\
|
||||
open Runtime_jsoo.Runtime@\n\
|
||||
open Js_of_ocaml@\n\
|
||||
%s@\n\
|
||||
@\n\
|
||||
[@@@@@@ocaml.warning \"-4-26-27-32-41-42\"]@\n\
|
||||
@\n\
|
||||
(* Generated API *)@\n\
|
||||
@\n\
|
||||
%a@\n\
|
||||
%a@\n\
|
||||
@\n\
|
||||
@[<v 2>let _ =@ @[<hov 2> Js.export \"%a\"@\n\
|
||||
@[<v 2>(object%%js@ %a@]@\n\
|
||||
end)@]@]@?"
|
||||
(Option.fold ~none:"" ~some:(fun name -> name) module_name)
|
||||
(format_ctx type_ordering) prgm.decl_ctx
|
||||
(format_scopes_to_fun prgm.decl_ctx)
|
||||
prgm.code_items fmt_lib_name ()
|
||||
(format_scopes_to_callbacks prgm.decl_ctx)
|
||||
prgm.code_items)
|
||||
Format.fprintf fmt
|
||||
"(** This file has been generated by the Catala compiler, do not \
|
||||
edit! *)@\n\
|
||||
@\n\
|
||||
open Runtime_ocaml.Runtime@\n\
|
||||
open Runtime_jsoo.Runtime@\n\
|
||||
open Js_of_ocaml@\n\
|
||||
%s@\n\
|
||||
@\n\
|
||||
[@@@@@@ocaml.warning \"-4-26-27-32-41-42\"]@\n\
|
||||
@\n\
|
||||
(* Generated API *)@\n\
|
||||
@\n\
|
||||
%a@\n\
|
||||
%a@\n\
|
||||
@\n\
|
||||
@[<v 2>let _ =@ @[<hov 2> Js.export \"%a\"@\n\
|
||||
@[<v 2>(object%%js@ %a@]@\n\
|
||||
end)@]@]@?"
|
||||
(Option.fold ~none:"" ~some:(fun name -> name) module_name)
|
||||
(format_ctx type_ordering) prgm.decl_ctx
|
||||
(format_scopes_to_fun prgm.decl_ctx)
|
||||
prgm.code_items fmt_lib_name ()
|
||||
(format_scopes_to_callbacks prgm.decl_ctx)
|
||||
prgm.code_items
|
||||
end
|
||||
|
||||
let apply
|
||||
|
@ -197,20 +197,19 @@ module To_json = struct
|
||||
(scope : ScopeName.t)
|
||||
(prgm : 'm Lcalc.Ast.program) =
|
||||
let scope_body = Program.get_scope_body prgm scope in
|
||||
Cli.call_unstyled (fun _ ->
|
||||
Format.fprintf fmt
|
||||
"{@[<hov 2>@\n\
|
||||
\"type\": \"object\",@\n\
|
||||
\"@[<hov 2>definitions\": {%a@]@\n\
|
||||
},@\n\
|
||||
\"@[<hov 2>properties\": {@\n\
|
||||
%a@]@\n\
|
||||
}@]@\n\
|
||||
}"
|
||||
(fmt_definitions prgm.decl_ctx)
|
||||
(scope, scope_body)
|
||||
(fmt_struct_properties prgm.decl_ctx)
|
||||
scope_body.scope_body_input_struct)
|
||||
Format.fprintf fmt
|
||||
"{@[<hov 2>@\n\
|
||||
\"type\": \"object\",@\n\
|
||||
\"@[<hov 2>definitions\": {%a@]@\n\
|
||||
},@\n\
|
||||
\"@[<hov 2>properties\": {@\n\
|
||||
%a@]@\n\
|
||||
}@]@\n\
|
||||
}"
|
||||
(fmt_definitions prgm.decl_ctx)
|
||||
(scope, scope_body)
|
||||
(fmt_struct_properties prgm.decl_ctx)
|
||||
scope_body.scope_body_input_struct
|
||||
end
|
||||
|
||||
let apply
|
||||
|
@ -590,17 +590,16 @@ let format_program
|
||||
(* We disable the style flag in order to enjoy formatting from the
|
||||
pretty-printers of Dcalc and Lcalc but without the color terminal
|
||||
markers. *)
|
||||
Cli.call_unstyled (fun () ->
|
||||
Format.fprintf fmt
|
||||
"# This file has been generated by the Catala compiler, do not edit!\n\
|
||||
@\n\
|
||||
from catala.runtime import *@\n\
|
||||
from typing import Any, List, Callable, Tuple\n\
|
||||
from enum import Enum\n\
|
||||
@\n\
|
||||
@[<v>%a@]@\n\
|
||||
@\n\
|
||||
%a@?"
|
||||
"@[<v># This file has been generated by the Catala compiler, do not edit!@,\
|
||||
@,\
|
||||
from catala.runtime import *@,\
|
||||
from typing import Any, List, Callable, Tuple@,\
|
||||
from enum import Enum@,\
|
||||
@,\
|
||||
@[<v>%a@]@,\
|
||||
@,\
|
||||
%a@]@?"
|
||||
(format_ctx type_ordering) p.decl_ctx
|
||||
(Format.pp_print_list ~pp_sep:Format.pp_print_newline (fun fmt ->
|
||||
function
|
||||
@ -619,4 +618,4 @@ let format_program
|
||||
Format.fprintf fmt "%a:%a" format_var (Mark.remove var)
|
||||
format_typ typ))
|
||||
func_params (format_block p.decl_ctx) func_body))
|
||||
p.code_items)
|
||||
p.code_items
|
||||
|
@ -88,11 +88,9 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
|
||||
with Not_found ->
|
||||
(* Should not happen after disambiguation *)
|
||||
Messages.raise_spanned_error (Expr.mark_pos m)
|
||||
"Field %a does not belong to structure %a"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ field ^ "\"")
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" StructName.format_t name)
|
||||
"Field @{<yellow>\"%s\"@} does not belong to structure @{<yellow>\"%a\"@}"
|
||||
field
|
||||
StructName.format_t name
|
||||
in
|
||||
Expr.estructaccess e' field name m
|
||||
| ETuple es -> Expr.etuple (List.map (translate_expr ctx) es) m
|
||||
|
@ -43,8 +43,6 @@ let propagate_empty_error_list elist f =
|
||||
in
|
||||
aux [] elist
|
||||
|
||||
let log_indent = ref 0
|
||||
|
||||
(* TODO: we should provide a generic way to print logs, that work across the
|
||||
different backends: python, ocaml, javascript, and interpreter *)
|
||||
|
||||
@ -53,35 +51,22 @@ let print_log entry infos pos e =
|
||||
if !Cli.trace_flag then
|
||||
match entry with
|
||||
| VarDef _ ->
|
||||
(* TODO: this usage of Format is broken, Formatting requires that all is
|
||||
formatted in one pass, without going through intermediate "%s" *)
|
||||
Messages.emit_log "%*s%a %a: %s" (!log_indent * 2) "" Print.log_entry
|
||||
Messages.emit_log "@,%a %a: @{<green>%s@}" Print.log_entry
|
||||
entry Print.uid_list infos
|
||||
(let expr_str =
|
||||
Format.asprintf "%a" (Print.expr ~hide_function_body:true ()) e
|
||||
in
|
||||
let expr_str =
|
||||
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
|
||||
~subst:(fun _ -> " ")
|
||||
expr_str
|
||||
in
|
||||
Cli.with_style [ANSITerminal.green] "%s" expr_str)
|
||||
(Messages.unformat
|
||||
(fun ppf -> Print.expr ~hide_function_body:true () ppf e))
|
||||
| PosRecordIfTrueBool -> (
|
||||
match pos <> Pos.no_pos, Mark.remove e with
|
||||
| true, ELit (LBool true) ->
|
||||
Messages.emit_log "%*s%a%s:\n%s" (!log_indent * 2) "" Print.log_entry
|
||||
entry
|
||||
(Cli.with_style [ANSITerminal.green] "Definition applied")
|
||||
(Cli.add_prefix_to_each_line (Pos.retrieve_loc_text pos) (fun _ ->
|
||||
Format.asprintf "%*s" (!log_indent * 2) ""))
|
||||
Messages.emit_log "@,@[<v>%a@{<green>Definition applied@}:@,%a@]"
|
||||
Print.log_entry entry
|
||||
Pos.format_loc_text pos
|
||||
| _ -> ())
|
||||
| BeginCall ->
|
||||
Messages.emit_log "%*s%a %a" (!log_indent * 2) "" Print.log_entry entry
|
||||
Print.uid_list infos;
|
||||
log_indent := !log_indent + 1
|
||||
Messages.emit_log "@,[<v 2>%a %a" Print.log_entry entry
|
||||
Print.uid_list infos
|
||||
| EndCall ->
|
||||
log_indent := !log_indent - 1;
|
||||
Messages.emit_log "%*s%a %a" (!log_indent * 2) "" Print.log_entry entry
|
||||
Messages.emit_log "@]@,%a %a" Print.log_entry entry
|
||||
Print.uid_list infos
|
||||
|
||||
exception CatalaException of except
|
||||
|
@ -310,7 +310,6 @@ let optimize_program (p : 'm program) : 'm program =
|
||||
(Program.map_exprs ~f:(optimize_expr p.decl_ctx) ~varf:(fun v -> v) p)
|
||||
|
||||
let test_iota_reduction_1 () =
|
||||
Cli.call_unstyled (fun _ ->
|
||||
let x = Var.make "x" in
|
||||
let enumT = EnumName.fresh ("t", Pos.no_pos) in
|
||||
let consA = EnumConstructor.fresh ("A", Pos.no_pos) in
|
||||
@ -348,7 +347,7 @@ let test_iota_reduction_1 () =
|
||||
ctx_struct_fields = IdentName.Map.empty;
|
||||
ctx_scopes = ScopeName.Map.empty;
|
||||
}
|
||||
(Expr.unbox matchA)))))
|
||||
(Expr.unbox matchA))))
|
||||
|
||||
let cases_of_list l : ('a, 't) boxed_gexpr EnumConstructor.Map.t =
|
||||
EnumConstructor.Map.of_seq
|
||||
@ -362,62 +361,61 @@ let cases_of_list l : ('a, 't) boxed_gexpr EnumConstructor.Map.t =
|
||||
(Untyped { pos = Pos.no_pos }) ))
|
||||
|
||||
let test_iota_reduction_2 () =
|
||||
Cli.call_unstyled (fun _ ->
|
||||
let enumT = EnumName.fresh ("t", Pos.no_pos) in
|
||||
let consA = EnumConstructor.fresh ("A", Pos.no_pos) in
|
||||
let consB = EnumConstructor.fresh ("B", Pos.no_pos) in
|
||||
let consC = EnumConstructor.fresh ("C", Pos.no_pos) in
|
||||
let consD = EnumConstructor.fresh ("D", Pos.no_pos) in
|
||||
let enumT = EnumName.fresh ("t", Pos.no_pos) in
|
||||
let consA = EnumConstructor.fresh ("A", Pos.no_pos) in
|
||||
let consB = EnumConstructor.fresh ("B", Pos.no_pos) in
|
||||
let consC = EnumConstructor.fresh ("C", Pos.no_pos) in
|
||||
let consD = EnumConstructor.fresh ("D", Pos.no_pos) in
|
||||
|
||||
let nomark = Untyped { pos = Pos.no_pos } in
|
||||
let nomark = Untyped { pos = Pos.no_pos } in
|
||||
|
||||
let num n = Expr.elit (LInt (Runtime.integer_of_int n)) nomark in
|
||||
let num n = Expr.elit (LInt (Runtime.integer_of_int n)) nomark in
|
||||
|
||||
let injAe e = Expr.einj e consA enumT nomark in
|
||||
let injBe e = Expr.einj e consB enumT nomark in
|
||||
let injCe e = Expr.einj e consC enumT nomark in
|
||||
let injDe e = Expr.einj e consD enumT nomark in
|
||||
let injAe e = Expr.einj e consA enumT nomark in
|
||||
let injBe e = Expr.einj e consB enumT nomark in
|
||||
let injCe e = Expr.einj e consC enumT nomark in
|
||||
let injDe e = Expr.einj e consD enumT nomark in
|
||||
|
||||
(* let injA x = injAe (Expr.evar x nomark) in *)
|
||||
let injB x = injBe (Expr.evar x nomark) in
|
||||
let injC x = injCe (Expr.evar x nomark) in
|
||||
let injD x = injDe (Expr.evar x nomark) in
|
||||
(* let injA x = injAe (Expr.evar x nomark) in *)
|
||||
let injB x = injBe (Expr.evar x nomark) in
|
||||
let injC x = injCe (Expr.evar x nomark) in
|
||||
let injD x = injDe (Expr.evar x nomark) in
|
||||
|
||||
let matchA =
|
||||
Expr.ematch
|
||||
(Expr.ematch (num 1) enumT
|
||||
(cases_of_list
|
||||
[
|
||||
(consB, fun x -> injBe (injB x));
|
||||
(consA, fun _x -> injAe (num 20));
|
||||
])
|
||||
nomark)
|
||||
enumT
|
||||
(cases_of_list [consA, injC; consB, injD])
|
||||
nomark
|
||||
in
|
||||
Alcotest.(check string)
|
||||
"same string "
|
||||
"before=match\n\
|
||||
\ (match 1\n\
|
||||
\ with\n\
|
||||
\ | A → (λ (x: any) → A 20)\n\
|
||||
\ | B → (λ (x: any) → B B x))\n\
|
||||
\ with\n\
|
||||
\ | A → (λ (x: any) → C x)\n\
|
||||
\ | B → (λ (x: any) → D x)\n\
|
||||
after=match 1\n\
|
||||
\ with\n\
|
||||
\ | A → (λ (x: any) → C 20)\n\
|
||||
\ | B → (λ (x: any) → D B x)\n"
|
||||
(Format.asprintf "before=@[%a@]@.after=%a@." Expr.format
|
||||
(Expr.unbox matchA) Expr.format
|
||||
(Expr.unbox
|
||||
(optimize_expr
|
||||
{
|
||||
ctx_enums = EnumName.Map.empty;
|
||||
ctx_structs = StructName.Map.empty;
|
||||
ctx_struct_fields = IdentName.Map.empty;
|
||||
ctx_scopes = ScopeName.Map.empty;
|
||||
}
|
||||
(Expr.unbox matchA)))))
|
||||
let matchA =
|
||||
Expr.ematch
|
||||
(Expr.ematch (num 1) enumT
|
||||
(cases_of_list
|
||||
[
|
||||
(consB, fun x -> injBe (injB x));
|
||||
(consA, fun _x -> injAe (num 20));
|
||||
])
|
||||
nomark)
|
||||
enumT
|
||||
(cases_of_list [consA, injC; consB, injD])
|
||||
nomark
|
||||
in
|
||||
Alcotest.(check string)
|
||||
"same string "
|
||||
"before=match\n\
|
||||
\ (match 1\n\
|
||||
\ with\n\
|
||||
\ | A → (λ (x: any) → A 20)\n\
|
||||
\ | B → (λ (x: any) → B B x))\n\
|
||||
\ with\n\
|
||||
\ | A → (λ (x: any) → C x)\n\
|
||||
\ | B → (λ (x: any) → D x)\n\
|
||||
after=match 1\n\
|
||||
\ with\n\
|
||||
\ | A → (λ (x: any) → C 20)\n\
|
||||
\ | B → (λ (x: any) → D B x)\n"
|
||||
(Format.asprintf "before=@[%a@]@.after=%a@." Expr.format
|
||||
(Expr.unbox matchA) Expr.format
|
||||
(Expr.unbox
|
||||
(optimize_expr
|
||||
{
|
||||
ctx_enums = EnumName.Map.empty;
|
||||
ctx_structs = StructName.Map.empty;
|
||||
ctx_struct_fields = IdentName.Map.empty;
|
||||
ctx_scopes = ScopeName.Map.empty;
|
||||
}
|
||||
(Expr.unbox matchA))))
|
||||
|
@ -25,28 +25,36 @@ let uid_list (fmt : Format.formatter) (infos : Uid.MarkedString.info list) :
|
||||
Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.')
|
||||
(fun fmt info ->
|
||||
Cli.format_with_style
|
||||
(if String.begins_with_uppercase (Mark.remove info) then
|
||||
[ANSITerminal.red]
|
||||
else [])
|
||||
fmt
|
||||
(Uid.MarkedString.to_string info))
|
||||
Format.fprintf
|
||||
fmt
|
||||
(if String.begins_with_uppercase (Mark.remove info) then
|
||||
"@{<red>%s@}"
|
||||
else "%s")
|
||||
(Uid.MarkedString.to_string info))
|
||||
fmt infos
|
||||
|
||||
let with_color f color fmt x =
|
||||
(* equivalent to [Format.fprintf fmt "@{<color>%s@}" s] *)
|
||||
Format.pp_open_stag fmt Ocolor_format.(Ocolor_style_tag (Fg (C4 color)));
|
||||
f fmt x;
|
||||
Format.pp_close_stag fmt ()
|
||||
|
||||
let pp_color_string = with_color Format.pp_print_string
|
||||
|
||||
let keyword (fmt : Format.formatter) (s : string) : unit =
|
||||
Cli.format_with_style [ANSITerminal.red] fmt s
|
||||
pp_color_string Ocolor_types.red fmt s
|
||||
|
||||
let base_type (fmt : Format.formatter) (s : string) : unit =
|
||||
Cli.format_with_style [ANSITerminal.yellow] fmt s
|
||||
pp_color_string Ocolor_types.yellow fmt s
|
||||
|
||||
let punctuation (fmt : Format.formatter) (s : string) : unit =
|
||||
Format.pp_print_as fmt 1 (Cli.with_style [ANSITerminal.cyan] "%s" s)
|
||||
with_color (fun fmt -> Format.pp_print_as fmt 1) Ocolor_types.cyan fmt s
|
||||
|
||||
let op_style (fmt : Format.formatter) (s : string) : unit =
|
||||
Cli.format_with_style [ANSITerminal.green] fmt s
|
||||
pp_color_string Ocolor_types.green fmt s
|
||||
|
||||
let lit_style (fmt : Format.formatter) (s : string) : unit =
|
||||
Cli.format_with_style [ANSITerminal.yellow] fmt s
|
||||
pp_color_string Ocolor_types.yellow fmt s
|
||||
|
||||
let tlit (fmt : Format.formatter) (l : typ_lit) : unit =
|
||||
base_type fmt
|
||||
@ -69,12 +77,10 @@ let location (type a) (fmt : Format.formatter) (l : a glocation) : unit =
|
||||
| ToplevelVar v -> TopdefName.format_t fmt (Mark.remove v)
|
||||
|
||||
let enum_constructor (fmt : Format.formatter) (c : EnumConstructor.t) : unit =
|
||||
Cli.format_with_style [ANSITerminal.magenta] fmt
|
||||
(Format.asprintf "%a" EnumConstructor.format_t c)
|
||||
Format.fprintf fmt "@{<magenta>%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)
|
||||
Format.fprintf fmt "@{<magenta>%a@}" StructField.format_t c
|
||||
|
||||
let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
|
||||
let typ = typ ctx in
|
||||
@ -152,14 +158,11 @@ let lit (fmt : Format.formatter) (l : lit) : unit =
|
||||
| LDuration d -> lit_style fmt (Runtime.duration_to_string d)
|
||||
|
||||
let log_entry (fmt : Format.formatter) (entry : log_entry) : unit =
|
||||
Format.fprintf fmt "@<2>%a"
|
||||
(fun fmt -> function
|
||||
| VarDef _ -> Cli.format_with_style [ANSITerminal.blue] fmt "≔ "
|
||||
| BeginCall -> Cli.format_with_style [ANSITerminal.yellow] fmt "→ "
|
||||
| EndCall -> Cli.format_with_style [ANSITerminal.yellow] fmt "← "
|
||||
| PosRecordIfTrueBool ->
|
||||
Cli.format_with_style [ANSITerminal.green] fmt "☛ ")
|
||||
entry
|
||||
match entry with
|
||||
| VarDef _ -> Format.fprintf fmt "@{<blue>@<1>%s @}" "≔"
|
||||
| BeginCall -> Format.fprintf fmt "@{<yellow>@<1>%s @}" "→"
|
||||
| EndCall -> Format.fprintf fmt "@{<yellow>@<1>%s @}" "←"
|
||||
| PosRecordIfTrueBool -> Format.fprintf fmt "@{<green>@<1>%s @}" "☛"
|
||||
|
||||
let operator_to_string : type a. a Op.t -> string =
|
||||
let open Op in
|
||||
@ -299,17 +302,13 @@ let operator : type a. ?debug:bool -> Format.formatter -> a operator -> unit =
|
||||
let open Op in
|
||||
match op with
|
||||
| Log (entry, infos) ->
|
||||
Format.fprintf fmt "%a%a%a%a"
|
||||
(Cli.format_with_style [ANSITerminal.blue])
|
||||
"#{" log_entry entry
|
||||
Format.fprintf fmt "@{<blue>#{@}%a%a@{<blue>}@}"
|
||||
log_entry entry
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> punctuation fmt ".")
|
||||
(fun fmt info ->
|
||||
Cli.format_with_style [ANSITerminal.blue] fmt
|
||||
(fun fmt info -> Format.fprintf fmt "@{<blue>%s@}"
|
||||
(Uid.MarkedString.to_string info)))
|
||||
infos
|
||||
(Cli.format_with_style [ANSITerminal.blue])
|
||||
"}"
|
||||
| op ->
|
||||
op_style fmt
|
||||
(if debug then operator_to_string op else operator_to_shorter_string op)
|
||||
@ -434,7 +433,7 @@ let rec expr_aux :
|
||||
hide_function_body:bool ->
|
||||
debug:bool ->
|
||||
Bindlib.ctxt ->
|
||||
ANSITerminal.style list ->
|
||||
Ocolor_types.color4 list ->
|
||||
Format.formatter ->
|
||||
(a, 't) gexpr ->
|
||||
unit =
|
||||
@ -454,14 +453,14 @@ let rec expr_aux :
|
||||
let paren ~rhs ?(colors = colors) expr fmt e1 =
|
||||
if Precedence.needs_parens ~rhs ~context:e (skip_log e1) then (
|
||||
Format.pp_open_hvbox fmt 1;
|
||||
Cli.format_with_style [List.hd colors] fmt "(";
|
||||
pp_color_string (List.hd colors) fmt "(";
|
||||
expr (List.tl colors) fmt e1;
|
||||
Format.pp_close_box fmt ();
|
||||
Cli.format_with_style [List.hd colors] fmt ")")
|
||||
pp_color_string (List.hd colors) fmt ")")
|
||||
else expr colors fmt e1
|
||||
in
|
||||
let default_punct color fmt s =
|
||||
Format.pp_print_as fmt 1 (Cli.with_style [color] "%s" s)
|
||||
let default_punct =
|
||||
with_color (fun fmt -> Format.pp_print_as fmt 1)
|
||||
in
|
||||
let lhs ?(colors = colors) ex = paren ~colors ~rhs:false ex in
|
||||
let rhs ex = paren ~rhs:true ex in
|
||||
@ -673,12 +672,13 @@ let rec expr_aux :
|
||||
Format.pp_close_box fmt ()
|
||||
|
||||
let rec colors =
|
||||
ANSITerminal.blue
|
||||
:: ANSITerminal.cyan
|
||||
:: ANSITerminal.green
|
||||
:: ANSITerminal.yellow
|
||||
:: ANSITerminal.red
|
||||
:: ANSITerminal.magenta
|
||||
let open Ocolor_types in
|
||||
blue
|
||||
:: cyan
|
||||
:: green
|
||||
:: yellow
|
||||
:: red
|
||||
:: magenta
|
||||
:: colors
|
||||
|
||||
let typ_debug = typ None
|
||||
|
@ -177,35 +177,26 @@ let handle_type_error ctx (A.AnyExpr e) t1 t2 =
|
||||
let t2_repr = UnionFind.get (UnionFind.find t2) in
|
||||
let t1_pos = Mark.get t1_repr in
|
||||
let t2_pos = Mark.get t2_repr in
|
||||
let unformat_typ typ =
|
||||
let buf = Buffer.create 59 in
|
||||
let ppf = Format.formatter_of_buffer buf in
|
||||
(* set infinite width to disable line cuts *)
|
||||
Format.pp_set_margin ppf max_int;
|
||||
format_typ ctx ppf typ;
|
||||
Format.pp_print_flush ppf ();
|
||||
Buffer.contents buf
|
||||
in
|
||||
let t1_s fmt () =
|
||||
Cli.format_with_style [ANSITerminal.yellow] fmt (unformat_typ t1)
|
||||
in
|
||||
let t2_s fmt () =
|
||||
Cli.format_with_style [ANSITerminal.yellow] fmt (unformat_typ t2)
|
||||
in
|
||||
Messages.raise_multispanned_error
|
||||
Messages.raise_multispanned_error_full
|
||||
[
|
||||
( Some
|
||||
(Format.asprintf
|
||||
"Error coming from typechecking the following expression:"),
|
||||
(fun ppf -> Format.pp_print_string ppf
|
||||
"Error coming from typechecking the following expression:"),
|
||||
Expr.pos e );
|
||||
Some (Format.asprintf "Type %a coming from expression:" t1_s ()), t1_pos;
|
||||
Some (Format.asprintf "Type %a coming from expression:" t2_s ()), t2_pos;
|
||||
Some (fun ppf ->
|
||||
Format.fprintf ppf "Type @{<yellow>%a@} coming from expression:"
|
||||
(format_typ ctx) t1),
|
||||
t1_pos;
|
||||
Some (fun ppf ->
|
||||
Format.fprintf ppf "Type @{<yellow>%a@} coming from expression:"
|
||||
(format_typ ctx) t2),
|
||||
t2_pos;
|
||||
]
|
||||
"Error during typechecking, incompatible types:\n%a %a\n%a %a"
|
||||
(Cli.format_with_style [ANSITerminal.blue; ANSITerminal.Bold])
|
||||
"-->" t1_s ()
|
||||
(Cli.format_with_style [ANSITerminal.blue; ANSITerminal.Bold])
|
||||
"-->" t2_s ()
|
||||
"@[<v>Error during typechecking, incompatible types:@,\
|
||||
@{<bold;blue>-->@} @[<hov>%a@]@,\
|
||||
@{<bold;blue>-->@} @[<hov>%a@]@]"
|
||||
(format_typ ctx) t1
|
||||
(format_typ ctx) t2
|
||||
|
||||
let lit_type (lit : A.lit) : naked_typ =
|
||||
match lit with
|
||||
@ -470,28 +461,23 @@ and typecheck_expr_top_down :
|
||||
with Not_found ->
|
||||
Messages.raise_spanned_error
|
||||
(Expr.mark_pos context_mark)
|
||||
"Field %a does not belong to structure %a (no structure defines \
|
||||
"Field @{<yellow>\"%s\"@} does not belong to structure @{<yellow>\"%a\"@} (no structure defines \
|
||||
it)"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ field ^ "\"")
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" A.StructName.format_t name)
|
||||
field
|
||||
A.StructName.format_t name
|
||||
in
|
||||
try A.StructName.Map.find name candidate_structs
|
||||
with Not_found ->
|
||||
Messages.raise_spanned_error
|
||||
(Expr.mark_pos context_mark)
|
||||
"Field %a does not belong to structure %a, but to %a"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
("\"" ^ field ^ "\"")
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" A.StructName.format_t name)
|
||||
"@[<hov>Field @{<yellow>\"%s\"@}@ does not belong to@ structure @{<yellow>\"%a\"@},@ but to %a@]"
|
||||
field
|
||||
A.StructName.format_t name
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun ppf () -> Format.fprintf ppf "@ or@ ")
|
||||
(fun fmt s_name ->
|
||||
Format.fprintf fmt "%a"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
(Format.asprintf "\"%a\"" A.StructName.format_t s_name)))
|
||||
Format.fprintf fmt "@{<yellow>\"%a\"@}"
|
||||
A.StructName.format_t s_name))
|
||||
(List.map fst (A.StructName.Map.bindings candidate_structs))
|
||||
in
|
||||
A.StructField.Map.find field str
|
||||
|
@ -98,7 +98,7 @@ let rec law_struct_list_to_tree (f : Ast.law_structure list) :
|
||||
LawHeading (heading, gobbled) :: rest_out))
|
||||
|
||||
(** Style with which to display syntax hints in the terminal output *)
|
||||
let syntax_hints_style = [ANSITerminal.yellow]
|
||||
let pp_hint ppf s = Format.fprintf ppf "@{<yellow>\"%s\"@}" s
|
||||
|
||||
(** Usage: [raise_parser_error error_loc last_good_loc token msg]
|
||||
|
||||
@ -110,16 +110,16 @@ let raise_parser_error
|
||||
(error_loc : Pos.t)
|
||||
(last_good_loc : Pos.t option)
|
||||
(token : string)
|
||||
(msg : string) : 'a =
|
||||
Messages.raise_multispanned_error
|
||||
((Some "Error token:", error_loc)
|
||||
(msg : Format.formatter -> unit) : 'a =
|
||||
Messages.raise_multispanned_error_full
|
||||
((Some (fun ppf -> Format.pp_print_string ppf "Error token:"), error_loc)
|
||||
::
|
||||
(match last_good_loc with
|
||||
| None -> []
|
||||
| Some last_good_loc -> [Some "Last good token:", last_good_loc]))
|
||||
"Syntax error at token %a\n%s"
|
||||
(Cli.format_with_style syntax_hints_style)
|
||||
(Printf.sprintf "\"%s\"" token)
|
||||
| Some last_good_loc ->
|
||||
[Some (fun ppf -> Format.pp_print_string ppf "Last good token:"), last_good_loc]))
|
||||
"@[<v>Syntax error at token %a@,%t@]"
|
||||
pp_hint token
|
||||
msg
|
||||
|
||||
module ParserAux (LocalisedLexer : Lexer_common.LocalisedLexer) = struct
|
||||
@ -179,37 +179,36 @@ module ParserAux (LocalisedLexer : Lexer_common.LocalisedLexer) = struct
|
||||
acceptable_tokens
|
||||
in
|
||||
let similar_token_msg =
|
||||
if List.length similar_acceptable_tokens = 0 then None
|
||||
else
|
||||
Some
|
||||
(Printf.sprintf "did you mean %s?"
|
||||
(String.concat ", or maybe "
|
||||
(List.map
|
||||
(fun (ts, _) ->
|
||||
Cli.with_style syntax_hints_style "\"%s\"" ts)
|
||||
similar_acceptable_tokens)))
|
||||
match similar_acceptable_tokens with
|
||||
| [] -> None
|
||||
| tokens ->
|
||||
Some (fun ppf -> Format.fprintf ppf "did you mean %a?"
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun ppf () -> Format.fprintf ppf ",@ or@ maybe@ ")
|
||||
(fun ppf (ts, _) -> pp_hint ppf ts))
|
||||
tokens)
|
||||
in
|
||||
(* The parser has suspended itself because of a syntax error. Stop. *)
|
||||
let custom_menhir_message =
|
||||
let custom_menhir_message ppf =
|
||||
match Parser_errors.message (state env) with
|
||||
| exception Not_found ->
|
||||
"Message: " ^ Cli.with_style syntax_hints_style "%s" "unexpected token"
|
||||
Format.fprintf ppf "Message: @{<yellow>unexpected token@}"
|
||||
| msg ->
|
||||
"Message: "
|
||||
^ Cli.with_style syntax_hints_style "%s"
|
||||
(String.trim (String.uncapitalize_ascii msg))
|
||||
Format.fprintf ppf "Message: %a" pp_hint (String.trim (String.uncapitalize_ascii msg))
|
||||
in
|
||||
let msg =
|
||||
let msg ppf =
|
||||
match similar_token_msg with
|
||||
| None -> custom_menhir_message
|
||||
| None -> custom_menhir_message ppf
|
||||
| Some similar_token_msg ->
|
||||
Printf.sprintf "%s\nAutosuggestion: %s" custom_menhir_message
|
||||
Format.fprintf ppf "@[<v>%t@,@[<hov 4>Autosuggestion: %t@]@]"
|
||||
custom_menhir_message
|
||||
similar_token_msg
|
||||
in
|
||||
raise_parser_error
|
||||
(Pos.from_lpos (lexing_positions lexbuf))
|
||||
(Option.map Pos.from_lpos last_positions)
|
||||
(Utf8.lexeme lexbuf) msg
|
||||
(Utf8.lexeme lexbuf)
|
||||
msg
|
||||
|
||||
(** Main parsing loop *)
|
||||
let rec loop
|
||||
|
@ -99,18 +99,16 @@ module MakeBackendIO (B : Backend) = struct
|
||||
let var_and_pos =
|
||||
match vc.Conditions.vc_kind with
|
||||
| Conditions.NoEmptyError ->
|
||||
Format.asprintf "%s This variable might return an empty error:\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)))
|
||||
(Pos.retrieve_loc_text (Mark.get vc.vc_variable))
|
||||
Format.asprintf "@[<v>@{<yellow>[%a.%s]@} This variable might return an empty error:@,%a@]"
|
||||
ScopeName.format_t vc.vc_scope
|
||||
(Bindlib.name_of (Mark.remove vc.vc_variable))
|
||||
Pos.format_loc_text (Mark.get vc.vc_variable)
|
||||
| Conditions.NoOverlappingExceptions ->
|
||||
Format.asprintf
|
||||
"%s At least two exceptions overlap for this variable:\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)))
|
||||
(Pos.retrieve_loc_text (Mark.get vc.vc_variable))
|
||||
"@[<v>@{<yellow>[%a.%s]@} At least two exceptions overlap for this variable:@,%a@]"
|
||||
ScopeName.format_t vc.vc_scope
|
||||
(Bindlib.name_of (Mark.remove vc.vc_variable))
|
||||
Pos.format_loc_text (Mark.get vc.vc_variable)
|
||||
in
|
||||
let counterexample : string option =
|
||||
if !Cli.disable_counterexamples then
|
||||
@ -142,14 +140,13 @@ module MakeBackendIO (B : Backend) = struct
|
||||
(vc : Conditions.verification_condition * vc_encoding_result) : bool =
|
||||
let vc, z3_vc = vc in
|
||||
|
||||
Messages.emit_debug "For this variable:\n%s\n"
|
||||
(Pos.retrieve_loc_text (Expr.pos vc.Conditions.vc_guard));
|
||||
Messages.emit_debug "@[<v>For this variable:@,%a@,@]"
|
||||
Pos.format_loc_text (Expr.pos vc.Conditions.vc_guard);
|
||||
Messages.emit_debug
|
||||
"This verification condition was generated for %a:@\n\
|
||||
%a@\n\
|
||||
with assertions:@\n\
|
||||
%a"
|
||||
(Cli.format_with_style [ANSITerminal.yellow])
|
||||
"@[<v>This verification condition was generated for @{<yellow>%s@}:@,\
|
||||
%a@,\
|
||||
with assertions:@,\
|
||||
%a@]"
|
||||
(match vc.vc_kind with
|
||||
| Conditions.NoEmptyError ->
|
||||
"the variable definition never to return an empty error"
|
||||
@ -158,7 +155,7 @@ module MakeBackendIO (B : Backend) = struct
|
||||
|
||||
match z3_vc with
|
||||
| Success (encoding, backend_ctx) -> (
|
||||
Messages.emit_debug "The translation to Z3 is the following:\n%s"
|
||||
Messages.emit_debug "@[<v>The translation to Z3 is the following:@,%s@]"
|
||||
(B.print_encoding encoding);
|
||||
match B.solve_vc_encoding backend_ctx encoding with
|
||||
| ProvenTrue -> true
|
||||
@ -167,10 +164,9 @@ module MakeBackendIO (B : Backend) = struct
|
||||
false
|
||||
| Unknown -> failwith "The solver failed at proving or disproving the VC")
|
||||
| Fail msg ->
|
||||
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)))
|
||||
Messages.emit_warning "@[<v>@{<yellow>[%a.%s]@} The translation to Z3 failed:@,%s@]"
|
||||
ScopeName.format_t vc.vc_scope
|
||||
(Bindlib.name_of (Mark.remove vc.vc_variable))
|
||||
msg;
|
||||
false
|
||||
end
|
||||
|
@ -229,9 +229,8 @@ let print_model (ctx : context) (model : Model.model) : string =
|
||||
match StringMap.find_opt symbol_name ctx.ctx_z3vars with
|
||||
| None -> ()
|
||||
| Some (v, ty) ->
|
||||
Format.fprintf fmt "%s %s : %s\n"
|
||||
(Cli.with_style [ANSITerminal.blue] "%s" "-->")
|
||||
(Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v))
|
||||
Format.fprintf fmt "@{<blue>-->@} @{<yellow>%s@} : %s\n"
|
||||
(Bindlib.name_of v)
|
||||
(print_z3model_expr ctx ty e))
|
||||
else
|
||||
(* Declaration d is a function *)
|
||||
@ -244,9 +243,8 @@ let print_model (ctx : context) (model : Model.model) : string =
|
||||
| Some f ->
|
||||
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
|
||||
let v, _ = StringMap.find symbol_name ctx.ctx_z3vars in
|
||||
Format.fprintf fmt "%s %s : %s"
|
||||
(Cli.with_style [ANSITerminal.blue] "%s" "-->")
|
||||
(Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v))
|
||||
Format.fprintf fmt "@{<blue>-->@} @{<yellow>%s@} : %s\n"
|
||||
(Bindlib.name_of v)
|
||||
(* TODO: Model of a Z3 function should be pretty-printed *)
|
||||
(Model.FuncInterp.to_string f)))
|
||||
decls
|
||||
|
Loading…
Reference in New Issue
Block a user