Skip to content

Commit

Permalink
account for new merge
Browse files Browse the repository at this point in the history
  • Loading branch information
@ionchirica
ionchirica committed Mar 25, 2024
2 parents d76965d + c198f14 commit c2fc98a
Show file tree
Hide file tree
Showing 26 changed files with 329 additions and 167 deletions.
2 changes: 2 additions & 0 deletions CHANGES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@

## Improved

- Make the type-checker save type information in a file
[\#376](https://github.com/ocaml-gospel/gospel/pull/376)
- Make the `with` necessary when declaring type invariants
[\#372](https://github.com/ocaml-gospel/gospel/pull/372) and
[\#374](https://github.com/ocaml-gospel/gospel/pull/374)
Expand Down
1 change: 0 additions & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,6 @@ well-formed, well-typed, and remain in sync with the interface they annotate!

```shell
$ gospel check max_array.mli
OK
```

Gospel also provides a ppx rewriter to allow odoc to display the contents of
Expand Down
39 changes: 22 additions & 17 deletions bin/check.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,32 +27,37 @@ let type_check load_path name sigs =
path2module name |> Utils.Sstr.singleton |> Typing.penv load_path
in
let md = List.fold_left (Typing.type_sig_item penv) md sigs in
wrap_up_muc md
md

let run_file config file =
try
let ocaml = parse_ocaml_signature file in
if config.verbose then (
pp fmt "@[@\n*******************************@]@.";
pp fmt "@[********** Parsed file ********@]@.";
pp fmt "@[*******************************@]@.";
pp fmt "@[%a@]@." Opprintast.signature ocaml);

let module_nm = path2module file in
let sigs = parse_signature_gospel ~filename:file ocaml module_nm in
if config.verbose then (
pp fmt "@[@\n*******************************@]@.";
pp fmt "@[****** GOSPEL translation *****@]@.";
pp fmt "@[*******************************@]@.";
pp fmt "@[%a@]@." Upretty_printer.s_signature sigs);
let md =
if String.equal ".gospel" (Filename.extension file) then
read_gospel_file file
else
let ocaml = parse_ocaml_signature file in
if config.verbose then (
pp fmt "@[@\n*******************************@]@.";
pp fmt "@[********** Parsed file ********@]@.";
pp fmt "@[*******************************@]@.";
pp fmt "@[%a@]@." Opprintast.signature ocaml);

let file = type_check config.load_path file sigs in
let module_nm = path2module file in
let sigs = parse_signature_gospel ~filename:file ocaml module_nm in
if config.verbose then (
pp fmt "@[@\n*******************************@]@.";
pp fmt "@[****** GOSPEL translation *****@]@.";
pp fmt "@[*******************************@]@.";
pp fmt "@[%a@]@." Upretty_printer.s_signature sigs);
type_check config.load_path file sigs
in
let file = wrap_up_muc md in
if config.verbose then (
pp fmt "@[@\n*******************************@]@.";
pp fmt "@[********* Typed GOSPEL ********@]@.";
pp fmt "@[*******************************@]@.";
pp fmt "@[%a@]@." print_file file);
pp fmt "OK\n";
write_gospel_file md;
true
with W.Error e ->
let bt = Printexc.get_backtrace () in
Expand Down
34 changes: 14 additions & 20 deletions bin/cli.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,32 +10,21 @@

open Cmdliner

type test = { pred : string -> bool; err : string }
let file s = List.mem (Filename.extension s) [ ".mli"; ".ml" ]
let intf s = List.mem (Filename.extension s) [ ".mli"; ".gospel" ]

let test_file =
{
pred = (fun s -> List.mem (Filename.extension s) [ ".mli"; ".ml" ]);
err = "file";
}

let test_intf =
{
pred = (fun s -> String.equal (Filename.extension s) ".mli");
err = "interface file";
}

let ocaml_test test =
let test test =
let parse s =
match Sys.file_exists s with
| true ->
if test.pred s then `Ok s
else `Error (Printf.sprintf "Error: `%s' is not an OCaml %s" s test.err)
if test s then `Ok s
else `Error (Printf.sprintf "don't know what to do with %s" s)
| false -> `Error (Printf.sprintf "Error: `%s' not found" s)
in
(parse, Format.pp_print_string)

let ocaml_intf = ocaml_test test_intf
let ocaml_file = ocaml_test test_file
let test_intf = test intf
let test_file = test file

let verbose =
let doc = "Print all intermediate forms." in
Expand All @@ -45,8 +34,13 @@ let load_path =
let doc = "Include directory in load path." in
Arg.(value & opt_all dir [] & info [ "L"; "load-path" ] ~doc ~docv:"DIR")

let intfs = Arg.(non_empty & pos_all ocaml_intf [] & info [] ~docv:"FILE")
let files = Arg.(non_empty & pos_all ocaml_file [] & info [] ~docv:"FILE")
let intfs =
let doc = "File to be processed, expect a .mli or a .gospel file" in
Arg.(non_empty & pos_all test_intf [] & info [] ~doc ~docv:"FILE")

let files =
let doc = "File to be processed, expect a .mli or a .ml file" in
Arg.(non_empty & pos_all test_file [] & info [] ~doc ~docv:"FILE")

let run_check verbose load_path file =
let load_path =
Expand Down
24 changes: 9 additions & 15 deletions docs/docs/dune.inc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target faq.gospel)
(action
(progn
(with-stdout-to faq.output
(chdir %{project_root}
(run gospel check %{dep:faq.mli})))
(diff? %{project_root}/test/utils/check_success faq.output))))
(chdir %{project_root}
(run gospel check %{dep:faq.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -33,12 +31,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target stdlib.gospel)
(action
(progn
(with-stdout-to stdlib.output
(chdir %{project_root}
(run gospel check %{dep:stdlib.mli})))
(diff? %{project_root}/test/utils/check_success stdlib.output))))
(chdir %{project_root}
(run gospel check %{dep:stdlib.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -54,10 +50,8 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target welcome.gospel)
(action
(progn
(with-stdout-to welcome.output
(chdir %{project_root}
(run gospel check %{dep:welcome.mli})))
(diff? %{project_root}/test/utils/check_success welcome.output))))
(chdir %{project_root}
(run gospel check %{dep:welcome.mli}))))

32 changes: 12 additions & 20 deletions docs/docs/getting-started/dune.inc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target first-spec.gospel)
(action
(progn
(with-stdout-to first-spec.output
(chdir %{project_root}
(run gospel check %{dep:first-spec.mli})))
(diff? %{project_root}/test/utils/check_success first-spec.output))))
(chdir %{project_root}
(run gospel check %{dep:first-spec.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -33,12 +31,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target going-further.gospel)
(action
(progn
(with-stdout-to going-further.output
(chdir %{project_root}
(run gospel check %{dep:going-further.mli})))
(diff? %{project_root}/test/utils/check_success going-further.output))))
(chdir %{project_root}
(run gospel check %{dep:going-further.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -54,12 +50,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target installation.gospel)
(action
(progn
(with-stdout-to installation.output
(chdir %{project_root}
(run gospel check %{dep:installation.mli})))
(diff? %{project_root}/test/utils/check_success installation.output))))
(chdir %{project_root}
(run gospel check %{dep:installation.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -75,10 +69,8 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target tools.gospel)
(action
(progn
(with-stdout-to tools.output
(chdir %{project_root}
(run gospel check %{dep:tools.mli})))
(diff? %{project_root}/test/utils/check_success tools.output))))
(chdir %{project_root}
(run gospel check %{dep:tools.mli}))))

1 change: 0 additions & 1 deletion docs/docs/getting-started/first-spec.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -185,5 +185,4 @@ type-checker:

```shell
$ gospel check ./container.mli
OK
```
80 changes: 30 additions & 50 deletions docs/docs/language/dune.inc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target attributes.gospel)
(action
(progn
(with-stdout-to attributes.output
(chdir %{project_root}
(run gospel check %{dep:attributes.mli})))
(diff? %{project_root}/test/utils/check_success attributes.output))))
(chdir %{project_root}
(run gospel check %{dep:attributes.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -33,12 +31,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target constant-specifications.gospel)
(action
(progn
(with-stdout-to constant-specifications.output
(chdir %{project_root}
(run gospel check %{dep:constant-specifications.mli})))
(diff? %{project_root}/test/utils/check_success constant-specifications.output))))
(chdir %{project_root}
(run gospel check %{dep:constant-specifications.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -54,12 +50,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target expressions.gospel)
(action
(progn
(with-stdout-to expressions.output
(chdir %{project_root}
(run gospel check %{dep:expressions.mli})))
(diff? %{project_root}/test/utils/check_success expressions.output))))
(chdir %{project_root}
(run gospel check %{dep:expressions.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -75,12 +69,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target function-contracts.gospel)
(action
(progn
(with-stdout-to function-contracts.output
(chdir %{project_root}
(run gospel check %{dep:function-contracts.mli})))
(diff? %{project_root}/test/utils/check_success function-contracts.output))))
(chdir %{project_root}
(run gospel check %{dep:function-contracts.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -96,12 +88,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target lexical-conventions.gospel)
(action
(progn
(with-stdout-to lexical-conventions.output
(chdir %{project_root}
(run gospel check %{dep:lexical-conventions.mli})))
(diff? %{project_root}/test/utils/check_success lexical-conventions.output))))
(chdir %{project_root}
(run gospel check %{dep:lexical-conventions.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -117,12 +107,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target logical.gospel)
(action
(progn
(with-stdout-to logical.output
(chdir %{project_root}
(run gospel check %{dep:logical.mli})))
(diff? %{project_root}/test/utils/check_success logical.output))))
(chdir %{project_root}
(run gospel check %{dep:logical.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -138,12 +126,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target scope.gospel)
(action
(progn
(with-stdout-to scope.output
(chdir %{project_root}
(run gospel check %{dep:scope.mli})))
(diff? %{project_root}/test/utils/check_success scope.output))))
(chdir %{project_root}
(run gospel check %{dep:scope.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -159,12 +145,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target semantics.gospel)
(action
(progn
(with-stdout-to semantics.output
(chdir %{project_root}
(run gospel check %{dep:semantics.mli})))
(diff? %{project_root}/test/utils/check_success semantics.output))))
(chdir %{project_root}
(run gospel check %{dep:semantics.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -180,12 +164,10 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target syntax.gospel)
(action
(progn
(with-stdout-to syntax.output
(chdir %{project_root}
(run gospel check %{dep:syntax.mli})))
(diff? %{project_root}/test/utils/check_success syntax.output))))
(chdir %{project_root}
(run gospel check %{dep:syntax.mli}))))

(rule
(enabled_if %{bin-available:awk})
Expand All @@ -201,10 +183,8 @@
(alias runtest)
(enabled_if %{bin-available:awk})
(deps %{bin:gospel})
(target type-specifications.gospel)
(action
(progn
(with-stdout-to type-specifications.output
(chdir %{project_root}
(run gospel check %{dep:type-specifications.mli})))
(diff? %{project_root}/test/utils/check_success type-specifications.output))))
(chdir %{project_root}
(run gospel check %{dep:type-specifications.mli}))))

Loading

0 comments on commit c2fc98a

Please sign in to comment.