Skip to content

Commit 6ff6b86

Browse files
committed
Make only dolmen_bin depend on progress
1 parent ecea2c8 commit 6ff6b86

16 files changed

Lines changed: 397 additions & 319 deletions

dolmen_bin.opam

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ depends: [
1818
"fmt"
1919
"cmdliner" { >= "1.1.0" }
2020
"odoc" { with-doc }
21+
"progress"
22+
"terminal"
23+
]
24+
pin-depends: [
25+
[ "progress" "git+https://github.com/Gbury/progress.git#custom" ]
2126
]
2227
depopts: [
2328
"memtrace"

dolmen_loop.opam

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,9 @@ depends: [
1919
"progress"
2020
"terminal"
2121
]
22+
pin-depends: [
23+
[ "progress" "git+https://github.com/Gbury/progress.git#custom" ]
24+
]
2225
tags: [ "logic" "computation" "automated theorem prover" ]
2326
homepage: "https://github.com/Gbury/dolmen"
2427
dev-repo: "git+https://github.com/Gbury/dolmen.git"

src/bin/errors.ml

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,35 +14,35 @@ let exn st = function
1414
| Dolmen_loop.Pipeline.Sigint ->
1515
Format.pp_print_flush Format.std_formatter ();
1616
Format.pp_print_flush Format.err_formatter ();
17-
Loop.State.error st Dolmen_loop.Report.Error.user_interrupt ()
17+
State.error st Dolmen_loop.Report.Error.user_interrupt ()
1818

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

2424
| Dolmen_loop.Pipeline.Out_of_space ->
2525
Format.pp_print_flush Format.std_formatter ();
2626
Format.pp_print_flush Format.err_formatter ();
27-
Loop.State.error st Dolmen_loop.Report.Error.spaceout ()
27+
State.error st Dolmen_loop.Report.Error.spaceout ()
2828

2929
(* Internal Dolmen Expr errors *)
3030
| Dolmen.Std.Expr.Ty.Bad_arity (c, l) ->
3131
let pp_sep fmt () = Format.fprintf fmt ";@ " in
32-
Loop.State.error st Dolmen_loop.Report.Error.internal_error
32+
State.error st Dolmen_loop.Report.Error.internal_error
3333
(Format.dprintf
3434
"@[<hv>Internal error: Bad arity for type constant '%a',\
3535
@ which was provided arguments:@ [@[<hv>%a@]]@]"
3636
Dolmen.Std.Expr.Print.ty_cst c
3737
(Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Ty.print) l)
3838
| Dolmen.Std.Expr.Type_already_defined c ->
39-
Loop.State.error st Dolmen_loop.Report.Error.internal_error
39+
State.error st Dolmen_loop.Report.Error.internal_error
4040
(Format.dprintf
4141
"@[<hv>Internal error: Type constant '%a' was already defined earlier,\
4242
@ cannot re-define it.@]"
4343
Dolmen.Std.Expr.Print.id c)
4444
| Dolmen.Std.Expr.Term.Wrong_type (t, ty) ->
45-
Loop.State.error st Dolmen_loop.Report.Error.internal_error
45+
State.error st Dolmen_loop.Report.Error.internal_error
4646
(Format.dprintf
4747
"@[<hv>Internal error: A term of type@ %a@ was expected \
4848
but instead got a term of type@ %a@]"
@@ -52,5 +52,5 @@ let exn st = function
5252
(* Generic catch-all *)
5353
| exn ->
5454
let bt = Printexc.get_raw_backtrace () in
55-
Loop.State.error st Dolmen_loop.Report.Error.uncaught_exn (exn, bt)
55+
State.error st Dolmen_loop.Report.Error.uncaught_exn (exn, bt)
5656

src/bin/loop.ml

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,7 @@
11

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

4-
module State = Dolmen_loop.State
54
module Pipeline = Dolmen_loop.Pipeline.Make(State)
6-
7-
module Stats = Dolmen_loop.Stats.Make(State)
85
module Parser = Dolmen_loop.Parser.Make(State)(Stats)
96
module Header = Dolmen_loop.Headers.Make(State)
107
module Typer = Dolmen_loop.Typer.Typer(State)

src/bin/main.ml

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,18 @@
11

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

4-
54
(* Debug printing *)
65
(* ************** *)
76

87
let debug_parsed_pipe st c =
9-
if Loop.State.get Loop.State.debug st then
8+
if State.get State.debug st then
109
Format.eprintf "[logic][parsed][%a] @[<hov>%a@]@."
1110
Dolmen.Std.Loc.print_compact c.Dolmen.Std.Statement.loc
1211
Dolmen.Std.Statement.print c;
1312
st, c
1413

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

2625
let handle_exn st exn =
27-
let () = Dolmen_loop.Tui.finalise_display () in
26+
let () = Tui.finalise_display () in
2827
let _st = Errors.exn st exn in
2928
exit 125
3029

@@ -38,14 +37,14 @@ let finally st e =
3837
handle_exn st exn
3938

4039
let run st =
41-
if Loop.State.get Loop.State.debug st then begin
40+
if State.get State.debug st then begin
4241
Dolmen.Std.Expr.Print.print_index := true;
4342
()
4443
end;
4544
let st, g =
4645
try
4746
Loop.Parser.parse_logic [] st
48-
(Loop.State.get Loop.State.logic_file st)
47+
(State.get State.logic_file st)
4948
with exn -> handle_exn st exn
5049
in
5150
let st =
@@ -62,9 +61,9 @@ let run st =
6261
)
6362
)
6463
in
65-
let () = Dolmen_loop.Tui.finalise_display () in
64+
let () = Tui.finalise_display () in
6665
let st = Loop.Header.check st in
67-
let _st = Dolmen_loop.State.flush st () in
66+
let _st = State.flush st () in
6867
()
6968

7069
(* Warning/Error list *)

src/bin/options.ml

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ let profiling_section = "PROFILING"
1818

1919
type cmd =
2020
| Run of {
21-
state : Loop.State.t;
21+
state : State.t;
2222
}
2323
| List_reports of {
2424
conf : Dolmen_loop.Report.Conf.t;
@@ -244,9 +244,9 @@ let c_size = parse_size, print_size
244244

245245
let report_style =
246246
Arg.enum [
247-
"minimal", Loop.State.Minimal;
248-
"regular", Loop.State.Regular;
249-
"contextual", Loop.State.Contextual;
247+
"minimal", State.Minimal;
248+
"regular", State.Regular;
249+
"contextual", State.Contextual;
250250
]
251251

252252

@@ -345,11 +345,17 @@ let mk_run_state
345345
let () = if gc then at_exit (fun () -> Gc.print_stat stdout;) in
346346
let () = if abort_on_bug then Dolmen_loop.Code.abort Dolmen_loop.Code.bug in
347347
(* State creation *)
348-
Loop.State.empty
349-
|> Loop.State.init
348+
State.empty
349+
|> State.init
350350
~debug ~report_style ~reports
351351
~max_warn ~time_limit ~size_limit
352352
~logic_file ~response_file
353+
|> Stats.init
354+
~mem:progress_mem
355+
~max_mem:(int_of_float size_limit)
356+
~enabled:progress_enabled
357+
~typing:type_check
358+
~model:check_model
353359
|> Loop.Parser.init
354360
~syntax_error_ref
355361
~interactive_prompt:Loop.Parser.interactive_prompt_lang
@@ -360,12 +366,6 @@ let mk_run_state
360366
~header_check
361367
~header_licenses
362368
~header_lang_version
363-
|> Loop.Stats.init
364-
~mem:progress_mem
365-
~max_mem:(int_of_float size_limit)
366-
~enabled:progress_enabled
367-
~typing:type_check
368-
~model:check_model
369369

370370
(* Profiling *)
371371
(* ************************************************************************* *)
@@ -633,10 +633,10 @@ let cli =
633633
| false, None ->
634634
`Ok (Run { state; })
635635
| false, Some report ->
636-
let conf = Loop.State.get Loop.State.reports state in
636+
let conf = State.get State.reports state in
637637
`Ok (Doc { report; conf; })
638638
| true, None ->
639-
let conf = Loop.State.get Loop.State.reports state in
639+
let conf = State.get State.reports state in
640640
`Ok (List_reports { conf; })
641641
| true, Some _ ->
642642
`Error (false,

src/bin/state.ml

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
2+
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
3+
4+
include Dolmen_loop.State
5+
6+
(* Erros, Warnings & locations *)
7+
(* ************************************************************************* *)
8+
9+
let loc_input ?file st (loc : Dolmen.Std.Loc.loc) =
10+
(* sanity check to avoid pp_loc trying to read and/or print
11+
too much when printing the source code snippet) *)
12+
if loc.max_line_length >= 150 ||
13+
loc.stop_line - loc.start_line >= 100 then
14+
None
15+
else begin
16+
match get report_style st, (file : _ file option) with
17+
| _, None -> None
18+
| _, Some { source = `Stdin; _ } -> None
19+
| (Minimal | Regular), _ -> None
20+
| Contextual, Some { source = `File filename; dir; _ } ->
21+
let full_filename = Filename.concat dir filename in
22+
let input = Pp_loc.Input.file full_filename in
23+
Some input
24+
| Contextual, Some { source = `Raw (_, contents); _ } ->
25+
let input = Pp_loc.Input.string contents in
26+
Some input
27+
end
28+
29+
let pp_loc ?file st fmt o =
30+
match o with
31+
| None -> ()
32+
| Some loc ->
33+
if Dolmen.Std.Loc.is_dummy loc then ()
34+
else begin
35+
match loc_input ?file st loc with
36+
| None ->
37+
Format.fprintf fmt "%a:@ "
38+
Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) Dolmen.Std.Loc.fmt) loc
39+
| Some input ->
40+
let loc_start, loc_end = Dolmen.Std.Loc.lexing_positions loc in
41+
let locs = Pp_loc.Position.of_lexing loc_start, Pp_loc.Position.of_lexing loc_end in
42+
Format.fprintf fmt "%a:@ %a"
43+
Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) Dolmen.Std.Loc.fmt) loc
44+
(Pp_loc.pp ~max_lines:5 ~input) [locs]
45+
end
46+
47+
let flush st () =
48+
let aux _ = set cur_warn 0 st in
49+
let cur = get cur_warn st in
50+
let max = get max_warn st in
51+
if cur <= max then
52+
aux ()
53+
else
54+
match get report_style st with
55+
| Minimal ->
56+
Format.kfprintf aux Format.err_formatter
57+
"W:%d@." (cur - max)
58+
| Regular | Contextual ->
59+
Format.kfprintf aux Format.err_formatter
60+
("@[<v>%a @[<hov>%s@ %d@ %swarnings@]@]@.")
61+
Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning"
62+
(if max = 0 then "Counted" else "Plus")
63+
(cur - max) (if max = 0 then "" else "additional ")
64+
65+
let error ?file ?loc st error payload =
66+
let () = Tui.finalise_display () in
67+
let st = flush st () in
68+
let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in
69+
let aux _ = Dolmen_loop.Code.exit (Dolmen_loop.Report.Error.code error) in
70+
match get report_style st with
71+
| Minimal ->
72+
Format.kfprintf aux Format.err_formatter
73+
"E:%s@." (Dolmen_loop.Report.Error.mnemonic error)
74+
| Regular | Contextual ->
75+
Format.kfprintf aux Format.err_formatter
76+
("@[<v>%a%a @[<hov>%a@]%a@]@.")
77+
(pp_loc ?file st) loc
78+
Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Error"
79+
Dolmen_loop.Report.Error.print (error, payload)
80+
Dolmen_loop.Report.Error.print_hints (error, payload)
81+
82+
let warn ?file ?loc st warn payload =
83+
let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in
84+
match Dolmen_loop.Report.Conf.status (get reports st) warn with
85+
| Disabled -> st
86+
| Enabled ->
87+
let aux _ = update cur_warn ((+) 1) st in
88+
if get cur_warn st >= get max_warn st then
89+
aux st
90+
else
91+
begin match get report_style st with
92+
| Minimal ->
93+
Tui.kfprintf aux Format.err_formatter
94+
"W:%s@." (Dolmen_loop.Report.Warning.mnemonic warn)
95+
| Regular | Contextual ->
96+
Tui.kfprintf aux Format.err_formatter
97+
("@[<v>%a%a @[<hov>%a@]%a@]@.")
98+
(pp_loc ?file st) loc
99+
Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning"
100+
Dolmen_loop.Report.Warning.print (warn, payload)
101+
Dolmen_loop.Report.Warning.print_hints (warn, payload)
102+
end
103+
| Fatal ->
104+
let () = Tui.finalise_display () in
105+
let st = flush st () in
106+
let aux _ = Dolmen_loop.Code.exit (Dolmen_loop.Report.Warning.code warn) in
107+
begin match get report_style st with
108+
| Minimal ->
109+
Format.kfprintf aux Format.err_formatter
110+
"F:%s@." (Dolmen_loop.Report.Warning.mnemonic warn)
111+
| Regular | Contextual ->
112+
Format.kfprintf aux Format.err_formatter
113+
("@[<v>%a%a @[<hov>%a@]%a@]@.")
114+
(pp_loc ?file st) loc
115+
Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Fatal Warning"
116+
Dolmen_loop.Report.Warning.print (warn, payload)
117+
Dolmen_loop.Report.Warning.print_hints (warn, payload)
118+
end
119+
120+

0 commit comments

Comments
 (0)