From 08c33d273f1ce92bf8538af3679f98ece9cf6c4a Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 2 Jul 2024 16:28:40 +0200 Subject: [PATCH] Accept `.gospel` files in addition to `.mli`s --- bin/registration.ml | 24 ++++++++++++++-------- bin/registration.mli | 4 +++- plugins/monolith/src/ortac_monolith.ml | 2 +- plugins/monolith/src/ortac_monolith.mli | 2 +- plugins/qcheck-stm/src/ortac_qcheck_stm.ml | 2 +- plugins/wrapper/src/generate.mli | 2 +- plugins/wrapper/src/ortac_wrapper.ml | 2 +- plugins/wrapper/test/suite/translation.ml | 2 +- src/core/dune | 2 +- src/core/utils.ml | 10 ++++----- src/core/utils.mli | 2 +- 11 files changed, 31 insertions(+), 23 deletions(-) diff --git a/bin/registration.ml b/bin/registration.ml index e52a7ee1..e790ffea 100644 --- a/bin/registration.ml +++ b/bin/registration.ml @@ -1,5 +1,8 @@ type plugins = unit Cmdliner.Cmd.t Queue.t +type input_file = MLI of string | GOSPEL of string +let unwrap = function MLI s | GOSPEL s -> s +let pp_input_file ppf x = Fmt.(pf ppf "%s" (unwrap x)) let plugins = Queue.create () let register cmd = Queue.add cmd plugins let fold = Queue.fold @@ -35,16 +38,19 @@ let output_file = let quiet = Arg.(value & flag & info [ "q"; "quiet" ] ~doc:"Don't print any warnings.") -let ocaml_file = +let input_file = let parse s = - match Sys.file_exists s with - | true -> - if Sys.is_directory s || Filename.extension s <> ".mli" then - `Error (Fmt.str "Error: `%s' is not an OCaml interface file" s) - else `Ok s - | false -> `Error (Fmt.str "Error: `%s' not found" s) + if not (Sys.file_exists s) then `Error (Fmt.str "Error: `%s' not found" s) + else + match Filename.extension s with + | ".mli" -> `Ok (MLI s) + | ".gospel" -> `Ok (GOSPEL s) + | _ -> `Error "Error, expecting .mli or .gospel file." in Arg.( required - & pos 0 (some (parse, Fmt.string)) None - & info [] ~docv:"FILE" ~doc:"Read Gospel specifications in FILE.") + & pos 0 (some (parse, pp_input_file)) None + & info [] ~docv:"FILE" + ~doc: + "Read Gospel specifications in FILE. FILE can be an OCaml interface \ + or a .gospel file") diff --git a/bin/registration.mli b/bin/registration.mli index fbc7e8ee..98a0ad94 100644 --- a/bin/registration.mli +++ b/bin/registration.mli @@ -1,5 +1,7 @@ type plugins +type input_file = MLI of string | GOSPEL of string +val unwrap : input_file -> string val plugins : plugins val register : unit Cmdliner.Cmd.t -> unit val fold : ('a -> unit Cmdliner.Cmd.t -> 'a) -> 'a -> plugins -> 'a @@ -7,5 +9,5 @@ val get_out_formatter : string option -> Format.formatter val setup_log : unit Cmdliner.Term.t val include_ : string option Cmdliner.Term.t val output_file : string option Cmdliner.Term.t -val ocaml_file : string Cmdliner.Term.t +val input_file : input_file Cmdliner.Term.t val quiet : bool Cmdliner.Term.t diff --git a/plugins/monolith/src/ortac_monolith.ml b/plugins/monolith/src/ortac_monolith.ml index dfee8e6b..59a021e9 100644 --- a/plugins/monolith/src/ortac_monolith.ml +++ b/plugins/monolith/src/ortac_monolith.ml @@ -156,7 +156,7 @@ end = struct Cmd.info "monolith" ~doc:"Generate Monolith test file according to Gospel specifications." - let term = Term.(const main $ ocaml_file $ output_file $ setup_log) + let term = Term.(const main $ input_file $ output_file $ setup_log) let cmd = Cmd.v info term end diff --git a/plugins/monolith/src/ortac_monolith.mli b/plugins/monolith/src/ortac_monolith.mli index 87a254ac..9ae1caac 100644 --- a/plugins/monolith/src/ortac_monolith.mli +++ b/plugins/monolith/src/ortac_monolith.mli @@ -1,4 +1,4 @@ -val generate : string -> Format.formatter -> unit +val generate : Registration.input_file -> 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 *) diff --git a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml index 991dc530..a3e2a45f 100644 --- a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml +++ b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml @@ -34,7 +34,7 @@ end = struct let term = let open Registration in - Term.(const main $ ocaml_file $ config $ output_file $ quiet $ setup_log) + Term.(const main $ input_file $ config $ output_file $ quiet $ setup_log) let cmd = Cmd.v info term end diff --git a/plugins/wrapper/src/generate.mli b/plugins/wrapper/src/generate.mli index fdbe8141..685bbc2f 100644 --- a/plugins/wrapper/src/generate.mli +++ b/plugins/wrapper/src/generate.mli @@ -5,7 +5,7 @@ val signature : Gospel.Tast.signature_item list -> Ppxlib.structure -val generate : string -> Format.formatter -> unit +val generate : Registration.input_file -> 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 *) diff --git a/plugins/wrapper/src/ortac_wrapper.ml b/plugins/wrapper/src/ortac_wrapper.ml index 78bafa04..d13dfcbc 100644 --- a/plugins/wrapper/src/ortac_wrapper.ml +++ b/plugins/wrapper/src/ortac_wrapper.ml @@ -19,7 +19,7 @@ end = struct ~doc: "Wrap module functions with assertions to check their specifications." - let term = Term.(const main $ ocaml_file $ output_file $ setup_log) + let term = Term.(const main $ input_file $ output_file $ setup_log) let cmd = Cmd.v info term end diff --git a/plugins/wrapper/test/suite/translation.ml b/plugins/wrapper/test/suite/translation.ml index 87b8899b..b91b0c26 100644 --- a/plugins/wrapper/test/suite/translation.ml +++ b/plugins/wrapper/test/suite/translation.ml @@ -3,7 +3,7 @@ module Utils = Ortac_core__Utils let translate path = let open Utils in - let { module_name; namespace; ast } = check path in + let { module_name; namespace; ast } = check (Registration.MLI path) in let context = Ortac_core.Context.init module_name namespace in Ortac_wrapper__Ir_of_gospel.signature ~context ast diff --git a/src/core/dune b/src/core/dune index 5f709714..ff9d1d42 100644 --- a/src/core/dune +++ b/src/core/dune @@ -3,7 +3,7 @@ (public_name ortac-core) (preprocess (pps ppxlib.metaquot)) - (libraries fmt gospel ppxlib.ast)) + (libraries fmt registration gospel ppxlib.ast)) (rule (enabled_if diff --git a/src/core/utils.ml b/src/core/utils.ml index 4a5e8dbf..08ee29ea 100644 --- a/src/core/utils.ml +++ b/src/core/utils.ml @@ -37,11 +37,11 @@ let read_gospel_file filename = (gfile.muc_import, sigs) let check filename = - let module_name = module_name_of_path filename + let open Registration in + let module_name = module_name_of_path (unwrap filename) and env, ast = - match Filename.extension filename with - | ".mli" -> type_check [] filename - | ".gospel" -> read_gospel_file filename - | _ -> invalid_arg "check" + match filename with + | MLI filename -> type_check [] filename + | GOSPEL filename -> read_gospel_file filename in { module_name; namespace = List.hd env; ast } diff --git a/src/core/utils.mli b/src/core/utils.mli index 31d7a5ba..7e7ebbae 100644 --- a/src/core/utils.mli +++ b/src/core/utils.mli @@ -10,7 +10,7 @@ type checked = { ast : Gospel.Tast.signature; } -val check : string -> checked +val check : Registration.input_file -> checked (** [check filename] calls the Gospel type checker on [filename] with an empty load path if it is an interface and read its content if it is a [.gospel] file *)