Read gospel files

CHANGES.md

@@ -1,5 +1,7 @@
 # 0.3.0
 
+- Read also `.gospel` files
+  [\#196](https://github.com/ocaml-gospel/ortac/pull/196)
 - Read an optional `cleanup` function from configuration module
   [\#226](https://github.com/ocaml-gospel/ortac/pull/226)
 - Fix field access translation

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

@@ -132,12 +132,9 @@ let standalone module_name env s =
   :: specs
 
 let generate path fmt =
-  let module_name = Ortac_core.Utils.module_name_of_path path 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
+  let open Ortac_core.Utils in
+  let { module_name; namespace; ast } = check path in
+  standalone module_name namespace ast
   |> Fmt.pf fmt "%a@." Ppxlib_ast.Pprintast.structure;
   W.report ()
 
@@ -159,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/config.ml

@@ -220,11 +220,8 @@ let scan_config cfg_uc config_mod =
 let init gospel config_module =
   let open Reserr in
   try
-    let module_name = Utils.module_name_of_path gospel in
-    Parser_frontend.parse_ocaml_gospel gospel |> Utils.type_check [] gospel
-    |> fun (env, sigs) ->
-    assert (List.length env = 1);
-    let namespace = List.hd env in
+    let open Utils in
+    let { module_name; namespace; ast } = Utils.check gospel in
     let context = Context.init module_name namespace in
     let add ctx s =
       (* we add to the context the pure OCaml values and the functions and
@@ -237,10 +234,10 @@ let init gospel config_module =
           Context.add_function fun_ls fun_ls.ls_name.id_str ctx
       | _ -> ctx
     in
-    let context = List.fold_left add context sigs in
+    let context = List.fold_left add context ast in
     let* config =
       scan_config config_under_construction config_module >>= mk_config context
     in
-    ok (sigs, config)
+    ok (ast, config)
   with Gospel.Warnings.Error (l, k) ->
     error (Ortac_core.Warnings.GospelError k, l)

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