Accept .gospel files in addition to .mlis

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")

bin/registration.mli

@@ -1,11 +1,13 @@
 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
 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

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
 

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 *)

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

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 *)

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
 

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
 

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

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 }

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 *)