Skip to content

Commit

Permalink
Merge pull request #137 from n-osborne/stm-output-option
Browse files Browse the repository at this point in the history
Add an output option to qcheck-stm plugin cli
  • Loading branch information
shym authored Sep 19, 2023
2 parents 61cc4db + 8b5804d commit 310d048
Show file tree
Hide file tree
Showing 9 changed files with 34 additions and 33 deletions.
1 change: 1 addition & 0 deletions bin/registration.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ let plugins = Queue.create ()
let register cmd = Queue.add cmd plugins
let fold = Queue.fold
let get_channel = function None -> stdout | Some path -> open_out path
let get_out_formatter s = get_channel s |> Format.formatter_of_out_channel

open Cmdliner

Expand Down
2 changes: 1 addition & 1 deletion bin/registration.mli
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ type plugins
val plugins : plugins
val register : unit Cmdliner.Cmd.t -> unit
val fold : ('a -> unit Cmdliner.Cmd.t -> 'a) -> 'a -> plugins -> 'a
val get_channel : string option -> out_channel
val get_out_formatter : string option -> Format.formatter
val setup_log : unit Cmdliner.Term.t
val output_file : string option Cmdliner.Term.t
val ocaml_file : string Cmdliner.Term.t
9 changes: 4 additions & 5 deletions plugins/monolith/src/ortac_monolith.ml
Original file line number Diff line number Diff line change
Expand Up @@ -131,15 +131,14 @@ let standalone module_name env s =
:: module_s
:: specs

let generate path output =
let generate path fmt =
let module_name = Ortac_core.Utils.module_name_of_path path in
let output = Format.formatter_of_out_channel output in
Gospel.Parser_frontend.parse_ocaml_gospel path
|> Ortac_core.Utils.type_check [] path
|> fun (env, sigs) ->
assert (List.length env = 1);
standalone module_name (List.hd env) sigs
|> Fmt.pf output "%a@." Ppxlib_ast.Pprintast.structure;
|> Fmt.pf fmt "%a@." Ppxlib_ast.Pprintast.structure;
W.report ()

open Cmdliner
Expand All @@ -150,8 +149,8 @@ end = struct
open Registration

let main input output () =
let channel = get_channel output in
try generate input channel
let fmt = get_out_formatter output in
try generate input fmt
with Gospel.Warnings.Error e ->
Fmt.epr "%a@." Gospel.Warnings.pp e;
exit 1
Expand Down
2 changes: 1 addition & 1 deletion plugins/monolith/src/ortac_monolith.mli
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
val generate : string -> out_channel -> unit
val generate : string -> Format.formatter -> unit
(** [generate path output] generate the code of the tests corresponding to the
specifications present in [path] in the monolith configuration and print it
on the [output] channel *)
7 changes: 4 additions & 3 deletions plugins/qcheck-stm/src/ortac_qcheck_stm.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,10 @@ module Ir_of_gospel = Ir_of_gospel
module Reserr = Reserr
module Stm_of_ir = Stm_of_ir

let main path init sut () =
let main path init sut output () =
let open Reserr in
let pp = Fmt.((pp Ppxlib_ast.Pprintast.structure) stdout) in
let fmt = Registration.get_out_formatter output in
let pp = pp Ppxlib_ast.Pprintast.structure fmt in
pp
(let* sigs, config = Config.init path init sut in
let* ir = Ir_of_gospel.run sigs config in
Expand Down Expand Up @@ -39,7 +40,7 @@ end = struct

let term =
let open Registration in
Term.(const main $ ocaml_file $ init $ sut $ setup_log)
Term.(const main $ ocaml_file $ init $ sut $ output_file $ setup_log)

let cmd = Cmd.v info term
end
Expand Down
35 changes: 18 additions & 17 deletions plugins/qcheck-stm/test/dune
Original file line number Diff line number Diff line change
Expand Up @@ -62,9 +62,14 @@
qcheck-stm
(with-stderr-to
array_errors
(with-stdout-to
%{target}
(run ortac qcheck-stm %{dep:array.mli} "make 16 'a'" "char t"))))))
(run
ortac
qcheck-stm
%{dep:array.mli}
"make 16 'a'"
"char t"
-o
%{target})))))

(rule
(alias runtest)
Expand Down Expand Up @@ -108,14 +113,14 @@
qcheck-stm
(with-stderr-to
hashtbl_errors
(with-stdout-to
%{target}
(run
ortac
qcheck-stm
%{dep:hashtbl.mli}
"create ~random:false 16"
"(char, int) t"))))))
(run
ortac
qcheck-stm
%{dep:hashtbl.mli}
"create ~random:false 16"
"(char, int) t"
-o
%{target})))))

(rule
(alias runtest)
Expand Down Expand Up @@ -163,9 +168,7 @@
qcheck-stm
(with-stderr-to
record_errors
(with-stdout-to
%{target}
(run ortac qcheck-stm %{dep:record.mli} "make 42" "t"))))))
(run ortac qcheck-stm %{dep:record.mli} "make 42" "t" -o %{target})))))

(rule
(alias runtest)
Expand Down Expand Up @@ -213,9 +216,7 @@
qcheck-stm
(with-stderr-to
ref_errors
(with-stdout-to
%{target}
(run ortac qcheck-stm %{dep:ref.mli} "make 42" "t"))))))
(run ortac qcheck-stm %{dep:ref.mli} "make 42" "t" -o %{target})))))

(rule
(alias runtest)
Expand Down
5 changes: 2 additions & 3 deletions plugins/wrapper/src/generate.ml
Original file line number Diff line number Diff line change
Expand Up @@ -235,12 +235,11 @@ let signature ~runtime ~module_name namespace s =
Report.emit_warnings Fmt.stderr ir;
structure runtime (Context.module_name context) ir

let generate path output =
let generate path fmt =
let module_name = Ortac_core.Utils.module_name_of_path path in
let output = Format.formatter_of_out_channel output in
Gospel.Parser_frontend.parse_ocaml_gospel path
|> Ortac_core.Utils.type_check [] path
|> fun (env, sigs) ->
assert (List.length env = 1);
signature ~runtime:"Ortac_runtime" ~module_name (List.hd env) sigs
|> Fmt.pf output "%a@." Ppxlib_ast.Pprintast.structure
|> Fmt.pf fmt "%a@." Ppxlib_ast.Pprintast.structure
2 changes: 1 addition & 1 deletion plugins/wrapper/src/generate.mli
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ val signature :
Gospel.Tast.signature_item list ->
Ppxlib.structure

val generate : string -> out_channel -> unit
val generate : string -> Format.formatter -> unit
(** [generate path out] generate the code of the tests corresponding to the
specifications present in [path] in the default configuration and print it
on the [out] channel *)
4 changes: 2 additions & 2 deletions plugins/wrapper/src/ortac_wrapper.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ module Plugin : sig
val cmd : unit Cmd.t
end = struct
let main input output () =
let channel = get_channel output in
try Generate.generate input channel
let fmt = get_out_formatter output in
try Generate.generate input fmt
with Gospel.Warnings.Error e ->
Fmt.epr "%a@." Gospel.Warnings.pp e;
exit 1
Expand Down

0 comments on commit 310d048

Please sign in to comment.