diff --git a/CHANGES.md b/CHANGES.md index 25e170d8..8ba6af4d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -7,6 +7,10 @@ ## Improved +- Check for repeated name of module and module types + [\#444](https://github.com/ocaml-gospel/gospel/pull/444) +- Fix bug in creation of fresh type variables + [\#435](https://github.com/ocaml-gospel/gospel/pull/435) - Fix typing of pattern with inlined record [\#429](https://github.com/ocaml-gospel/gospel/pull/429) - Remove support for the record update syntax @@ -46,8 +50,6 @@ ## Internals -- Fix bug in creation of fresh type variables - [\#435](https://github.com/ocaml-gospel/gospel/pull/435) - Fix premature parsing of specification keywords in the preprocessor. [\#394](https://github.com/ocaml-gospel/gospel/pull/394) - Fix `ls_name` of `unit` logical symbol to be `()` diff --git a/src/tmodule.ml b/src/tmodule.ml index c68cb8d0..032ae9b3 100644 --- a/src/tmodule.ml +++ b/src/tmodule.ml @@ -75,8 +75,6 @@ let ns_add_xs ~allow_duplicate ns s xs = in { ns with ns_xs } -(* FIXME: Adding multiple modules with the same name to the export should not be - allowed either. *) let ns_add_ns ~allow_duplicate:_ ns s new_ns = { ns with ns_ns = Mstr.add s new_ns ns.ns_ns } @@ -107,6 +105,7 @@ let ns_find_xs ns s = ns_find (fun ns -> ns.ns_xs) ns s let ns_find_ns ns s = ns_find (fun ns -> ns.ns_ns) ns s let ns_find_tns ns s = ns_find (fun ns -> ns.ns_tns) ns s let ns_exists_ns ns s = Mstr.mem s ns.ns_ns +let ns_exists_tns ns s = Mstr.mem s ns.ns_tns let rec ns_rm_ts ns = function | [] -> assert false diff --git a/src/typing.ml b/src/typing.ml index 9bfa5a18..ce508285 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -1469,6 +1469,8 @@ and process_modtype path penv muc umty = and process_mod path penv loc m muc = let nm = Option.value ~default:"_" m.mdname.txt in + (if ns_exists_ns (get_top_import muc) nm then + W.(error ~loc (Repeated_name (`Module_def, nm)))); let muc = open_module muc nm in let muc, mty = process_modtype (path @ [ nm ]) penv muc m.mdtype in let decl = @@ -1483,6 +1485,8 @@ and process_mod path penv loc m muc = and process_modtype_decl path penv loc decl muc = let nm = decl.mtdname.txt in + (if ns_exists_tns (get_top_import muc) nm then + W.(error ~loc (Repeated_name (`Module_type, nm)))); let muc = open_module muc nm in let md_mty = Option.map (process_modtype path penv muc) decl.mtdtype in let muc, mty = diff --git a/src/warnings.ml b/src/warnings.ml index a5b051a4..65a6a10f 100644 --- a/src/warnings.ml +++ b/src/warnings.ml @@ -37,6 +37,7 @@ type kind = | Pattern_redundant of string | Predicate_symbol_expected of string | Public_type_invariant of string + | Repeated_name of ([ `Module_def | `Module_type ] * string) | Return_unit_without_modifies of string | Symbol_not_found of string list | Syntax_error @@ -147,6 +148,12 @@ let pp_kind ppf = function p | Predicate_symbol_expected s -> pf ppf "Not a predicate symbol: %s" s | Public_type_invariant t -> pf ppf "Invariant on public type %s" t + | Repeated_name (k, m) -> + pf ppf + "Multiple definition of the %s name %s.@\n\ + Names must be unique in a given signature" + (match k with `Module_def -> "module" | `Module_type -> "module type") + m | Return_unit_without_modifies f -> pf ppf "The function %s returns unit@ but its specifications does not contain \ diff --git a/test/typechecker/dune.inc b/test/typechecker/dune.inc index 98a390e3..0cb0d1fc 100644 --- a/test/typechecker/dune.inc +++ b/test/typechecker/dune.inc @@ -775,6 +775,50 @@ ; Syntax sanity check (run ocamlc -c %{dep:labeled_arg8.mli})))) +(rule + (deps + %{bin:gospel} + (:checker %{project_root}/test/utils/testchecker.exe)) + (targets multiple_module_definition.gospel) + (action + (with-outputs-to multiple_module_definition.mli.output + (run %{checker} %{dep:multiple_module_definition.mli})))) + +(rule + (alias runtest) + (action + (diff multiple_module_definition.mli multiple_module_definition.mli.output))) + +(rule + (alias test-cmis) + (action + (chdir %{project_root} + ; Syntax sanity check + (with-accepted-exit-codes 2 + (run ocamlc -c %{dep:multiple_module_definition.mli}))))) + +(rule + (deps + %{bin:gospel} + (:checker %{project_root}/test/utils/testchecker.exe)) + (targets multiple_module_type.gospel) + (action + (with-outputs-to multiple_module_type.mli.output + (run %{checker} %{dep:multiple_module_type.mli})))) + +(rule + (alias runtest) + (action + (diff multiple_module_type.mli multiple_module_type.mli.output))) + +(rule + (alias test-cmis) + (action + (chdir %{project_root} + ; Syntax sanity check + (with-accepted-exit-codes 2 + (run ocamlc -c %{dep:multiple_module_type.mli}))))) + (rule (deps %{bin:gospel} diff --git a/test/typechecker/dune_gen.options b/test/typechecker/dune_gen.options index 6b703376..e7503120 100644 --- a/test/typechecker/dune_gen.options +++ b/test/typechecker/dune_gen.options @@ -7,3 +7,7 @@ type_arity3.mli 2 type_arity5.mli 2 +multiple_module_definition.mli +2 +multiple_module_type.mli +2 diff --git a/test/typechecker/multiple_module_definition.mli b/test/typechecker/multiple_module_definition.mli new file mode 100644 index 00000000..62efdbf3 --- /dev/null +++ b/test/typechecker/multiple_module_definition.mli @@ -0,0 +1,9 @@ +module M : sig end +module M : sig end +(* {gospel_expected| + [125] File "multiple_module_definition.mli", line 2, characters 0-18: + 2 | module M : sig end + ^^^^^^^^^^^^^^^^^^ + Error: Multiple definition of the module name M. + Names must be unique in a given signature. + |gospel_expected} *) diff --git a/test/typechecker/multiple_module_type.mli b/test/typechecker/multiple_module_type.mli new file mode 100644 index 00000000..c4778df4 --- /dev/null +++ b/test/typechecker/multiple_module_type.mli @@ -0,0 +1,9 @@ +module type S = sig end +module type S = sig end +(* {gospel_expected| + [125] File "multiple_module_type.mli", line 2, characters 0-23: + 2 | module type S = sig end + ^^^^^^^^^^^^^^^^^^^^^^^ + Error: Multiple definition of the module type name S. + Names must be unique in a given signature. + |gospel_expected} *)