Skip to content

Commit

Permalink
Make only dolmen_bin depend on progress
Browse files Browse the repository at this point in the history
  • Loading branch information
Gbury committed Dec 2, 2022
1 parent ecea2c8 commit bc971b8
Show file tree
Hide file tree
Showing 16 changed files with 394 additions and 321 deletions.
5 changes: 5 additions & 0 deletions dolmen_bin.opam
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,11 @@ depends: [
"fmt"
"cmdliner" { >= "1.1.0" }
"odoc" { with-doc }
"progress"
"terminal"
]
pin-depends: [
[ "progress" "git+https://github.com/Gbury/progress.git#custom" ]
]
depopts: [
"memtrace"
Expand Down
2 changes: 0 additions & 2 deletions dolmen_loop.opam
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,6 @@ depends: [
"gen"
"odoc" { with-doc }
"pp_loc" { >= "2.0.0" }
"progress"
"terminal"
]
tags: [ "logic" "computation" "automated theorem prover" ]
homepage: "https://github.com/Gbury/dolmen"
Expand Down
14 changes: 7 additions & 7 deletions src/bin/errors.ml
Original file line number Diff line number Diff line change
Expand Up @@ -14,35 +14,35 @@ let exn st = function
| Dolmen_loop.Pipeline.Sigint ->
Format.pp_print_flush Format.std_formatter ();
Format.pp_print_flush Format.err_formatter ();
Loop.State.error st Dolmen_loop.Report.Error.user_interrupt ()
State.error st Dolmen_loop.Report.Error.user_interrupt ()

(* Timeout, potentially wrapped by the typechecker *)
| Dolmen_loop.Pipeline.Out_of_time ->
Format.pp_print_flush Format.std_formatter ();
Loop.State.error st Dolmen_loop.Report.Error.timeout ()
State.error st Dolmen_loop.Report.Error.timeout ()

| Dolmen_loop.Pipeline.Out_of_space ->
Format.pp_print_flush Format.std_formatter ();
Format.pp_print_flush Format.err_formatter ();
Loop.State.error st Dolmen_loop.Report.Error.spaceout ()
State.error st Dolmen_loop.Report.Error.spaceout ()

(* Internal Dolmen Expr errors *)
| Dolmen.Std.Expr.Ty.Bad_arity (c, l) ->
let pp_sep fmt () = Format.fprintf fmt ";@ " in
Loop.State.error st Dolmen_loop.Report.Error.internal_error
State.error st Dolmen_loop.Report.Error.internal_error
(Format.dprintf
"@[<hv>Internal error: Bad arity for type constant '%a',\
@ which was provided arguments:@ [@[<hv>%a@]]@]"
Dolmen.Std.Expr.Print.ty_cst c
(Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Ty.print) l)
| Dolmen.Std.Expr.Type_already_defined c ->
Loop.State.error st Dolmen_loop.Report.Error.internal_error
State.error st Dolmen_loop.Report.Error.internal_error
(Format.dprintf
"@[<hv>Internal error: Type constant '%a' was already defined earlier,\
@ cannot re-define it.@]"
Dolmen.Std.Expr.Print.id c)
| Dolmen.Std.Expr.Term.Wrong_type (t, ty) ->
Loop.State.error st Dolmen_loop.Report.Error.internal_error
State.error st Dolmen_loop.Report.Error.internal_error
(Format.dprintf
"@[<hv>Internal error: A term of type@ %a@ was expected \
but instead got a term of type@ %a@]"
Expand All @@ -52,5 +52,5 @@ let exn st = function
(* Generic catch-all *)
| exn ->
let bt = Printexc.get_raw_backtrace () in
Loop.State.error st Dolmen_loop.Report.Error.uncaught_exn (exn, bt)
State.error st Dolmen_loop.Report.Error.uncaught_exn (exn, bt)

3 changes: 0 additions & 3 deletions src/bin/loop.ml
Original file line number Diff line number Diff line change
@@ -1,10 +1,7 @@

(* This file is free software, part of dolmen. See file "LICENSE" for more information *)

module State = Dolmen_loop.State
module Pipeline = Dolmen_loop.Pipeline.Make(State)

module Stats = Dolmen_loop.Stats.Make(State)
module Parser = Dolmen_loop.Parser.Make(State)(Stats)
module Header = Dolmen_loop.Headers.Make(State)
module Typer = Dolmen_loop.Typer.Typer(State)
Expand Down
15 changes: 7 additions & 8 deletions src/bin/main.ml
Original file line number Diff line number Diff line change
@@ -1,19 +1,18 @@

(* This file is free software, part of dolmen. See file "LICENSE" for more information *)


(* Debug printing *)
(* ************** *)

let debug_parsed_pipe st c =
if Loop.State.get Loop.State.debug st then
if State.get State.debug st then
Format.eprintf "[logic][parsed][%a] @[<hov>%a@]@."
Dolmen.Std.Loc.print_compact c.Dolmen.Std.Statement.loc
Dolmen.Std.Statement.print c;
st, c

let debug_typed_pipe st stmt =
if Loop.State.get Loop.State.debug st then
if State.get State.debug st then
Format.eprintf "[logic][typed][%a] @[<hov>%a@]@\n@."
Dolmen.Std.Loc.print_compact stmt.Loop.Typer_Pipe.loc
Loop.Typer_Pipe.print stmt;
Expand All @@ -24,7 +23,7 @@ let debug_typed_pipe st stmt =
(* ************************ *)

let handle_exn st exn =
let () = Dolmen_loop.Tui.finalise_display () in
let () = Tui.finalise_display () in
let _st = Errors.exn st exn in
exit 125

Expand All @@ -38,14 +37,14 @@ let finally st e =
handle_exn st exn

let run st =
if Loop.State.get Loop.State.debug st then begin
if State.get State.debug st then begin
Dolmen.Std.Expr.Print.print_index := true;
()
end;
let st, g =
try
Loop.Parser.parse_logic [] st
(Loop.State.get Loop.State.logic_file st)
(State.get State.logic_file st)
with exn -> handle_exn st exn
in
let st =
Expand All @@ -62,9 +61,9 @@ let run st =
)
)
in
let () = Dolmen_loop.Tui.finalise_display () in
let () = Tui.finalise_display () in
let st = Loop.Header.check st in
let _st = Dolmen_loop.State.flush st () in
let _st = State.flush st () in
()

(* Warning/Error list *)
Expand Down
28 changes: 14 additions & 14 deletions src/bin/options.ml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ let profiling_section = "PROFILING"

type cmd =
| Run of {
state : Loop.State.t;
state : State.t;
}
| List_reports of {
conf : Dolmen_loop.Report.Conf.t;
Expand Down Expand Up @@ -244,9 +244,9 @@ let c_size = parse_size, print_size

let report_style =
Arg.enum [
"minimal", Loop.State.Minimal;
"regular", Loop.State.Regular;
"contextual", Loop.State.Contextual;
"minimal", State.Minimal;
"regular", State.Regular;
"contextual", State.Contextual;
]


Expand Down Expand Up @@ -345,11 +345,17 @@ let mk_run_state
let () = if gc then at_exit (fun () -> Gc.print_stat stdout;) in
let () = if abort_on_bug then Dolmen_loop.Code.abort Dolmen_loop.Code.bug in
(* State creation *)
Loop.State.empty
|> Loop.State.init
State.empty
|> State.init
~debug ~report_style ~reports
~max_warn ~time_limit ~size_limit
~logic_file ~response_file
|> Stats.init
~mem:progress_mem
~max_mem:(int_of_float size_limit)
~enabled:progress_enabled
~typing:type_check
~model:check_model
|> Loop.Parser.init
~syntax_error_ref
~interactive_prompt:Loop.Parser.interactive_prompt_lang
Expand All @@ -360,12 +366,6 @@ let mk_run_state
~header_check
~header_licenses
~header_lang_version
|> Loop.Stats.init
~mem:progress_mem
~max_mem:(int_of_float size_limit)
~enabled:progress_enabled
~typing:type_check
~model:check_model

(* Profiling *)
(* ************************************************************************* *)
Expand Down Expand Up @@ -633,10 +633,10 @@ let cli =
| false, None ->
`Ok (Run { state; })
| false, Some report ->
let conf = Loop.State.get Loop.State.reports state in
let conf = State.get State.reports state in
`Ok (Doc { report; conf; })
| true, None ->
let conf = Loop.State.get Loop.State.reports state in
let conf = State.get State.reports state in
`Ok (List_reports { conf; })
| true, Some _ ->
`Error (false,
Expand Down
120 changes: 120 additions & 0 deletions src/bin/state.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@

(* This file is free software, part of dolmen. See file "LICENSE" for more information *)

include Dolmen_loop.State

(* Erros, Warnings & locations *)
(* ************************************************************************* *)

let loc_input ?file st (loc : Dolmen.Std.Loc.loc) =
(* sanity check to avoid pp_loc trying to read and/or print
too much when printing the source code snippet) *)
if loc.max_line_length >= 150 ||
loc.stop_line - loc.start_line >= 100 then
None
else begin
match get report_style st, (file : _ file option) with
| _, None -> None
| _, Some { source = `Stdin; _ } -> None
| (Minimal | Regular), _ -> None
| Contextual, Some { source = `File filename; dir; _ } ->
let full_filename = Filename.concat dir filename in
let input = Pp_loc.Input.file full_filename in
Some input
| Contextual, Some { source = `Raw (_, contents); _ } ->
let input = Pp_loc.Input.string contents in
Some input
end

let pp_loc ?file st fmt o =
match o with
| None -> ()
| Some loc ->
if Dolmen.Std.Loc.is_dummy loc then ()
else begin
match loc_input ?file st loc with
| None ->
Format.fprintf fmt "%a:@ "
Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) Dolmen.Std.Loc.fmt) loc
| Some input ->
let loc_start, loc_end = Dolmen.Std.Loc.lexing_positions loc in
let locs = Pp_loc.Position.of_lexing loc_start, Pp_loc.Position.of_lexing loc_end in
Format.fprintf fmt "%a:@ %a"
Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) Dolmen.Std.Loc.fmt) loc
(Pp_loc.pp ~max_lines:5 ~input) [locs]
end

let flush st () =
let aux _ = set cur_warn 0 st in
let cur = get cur_warn st in
let max = get max_warn st in
if cur <= max then
aux ()
else
match get report_style st with
| Minimal ->
Format.kfprintf aux Format.err_formatter
"W:%d@." (cur - max)
| Regular | Contextual ->
Format.kfprintf aux Format.err_formatter
("@[<v>%a @[<hov>%s@ %d@ %swarnings@]@]@.")
Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning"
(if max = 0 then "Counted" else "Plus")
(cur - max) (if max = 0 then "" else "additional ")

let error ?file ?loc st error payload =
let () = Tui.finalise_display () in
let st = flush st () in
let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in
let aux _ = Dolmen_loop.Code.exit (Dolmen_loop.Report.Error.code error) in
match get report_style st with
| Minimal ->
Format.kfprintf aux Format.err_formatter
"E:%s@." (Dolmen_loop.Report.Error.mnemonic error)
| Regular | Contextual ->
Format.kfprintf aux Format.err_formatter
("@[<v>%a%a @[<hov>%a@]%a@]@.")
(pp_loc ?file st) loc
Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Error"
Dolmen_loop.Report.Error.print (error, payload)
Dolmen_loop.Report.Error.print_hints (error, payload)

let warn ?file ?loc st warn payload =
let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in
match Dolmen_loop.Report.Conf.status (get reports st) warn with
| Disabled -> st
| Enabled ->
let aux _ = update cur_warn ((+) 1) st in
if get cur_warn st >= get max_warn st then
aux st
else
begin match get report_style st with
| Minimal ->
Tui.kfprintf aux Format.err_formatter
"W:%s@." (Dolmen_loop.Report.Warning.mnemonic warn)
| Regular | Contextual ->
Tui.kfprintf aux Format.err_formatter
("@[<v>%a%a @[<hov>%a@]%a@]@.")
(pp_loc ?file st) loc
Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning"
Dolmen_loop.Report.Warning.print (warn, payload)
Dolmen_loop.Report.Warning.print_hints (warn, payload)
end
| Fatal ->
let () = Tui.finalise_display () in
let st = flush st () in
let aux _ = Dolmen_loop.Code.exit (Dolmen_loop.Report.Warning.code warn) in
begin match get report_style st with
| Minimal ->
Format.kfprintf aux Format.err_formatter
"F:%s@." (Dolmen_loop.Report.Warning.mnemonic warn)
| Regular | Contextual ->
Format.kfprintf aux Format.err_formatter
("@[<v>%a%a @[<hov>%a@]%a@]@.")
(pp_loc ?file st) loc
Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Fatal Warning"
Dolmen_loop.Report.Warning.print (warn, payload)
Dolmen_loop.Report.Warning.print_hints (warn, payload)
end


Loading

0 comments on commit bc971b8

Please sign in to comment.