[coqtop] use a map form module, not module names

There is a problem using just module names: there can be several
modules with the same name (but under different paths) in a Coq
theory.

Signed-off-by: Rodolphe Lepigre <rodolphe@bedrocksystems.com>

bin/coqtop.ml

@@ -80,18 +80,17 @@ let term =
                       [ Pp.textf "cannot find file: %s" coq_file_arg ]
               in
               let stanza =
-                let name = Dune_rules.Coq_module.name coq_module in
-                Dune_rules.Coq_sources.lookup_module coq_src name
+                Dune_rules.Coq_sources.lookup_module coq_src coq_module
               in
               let* (args, boot_type) =
                 match stanza with
                 | None ->
                     User_error.raise
                       [ Pp.textf "file not part of any stanza: %s" coq_file_arg ]
-                | Some(`Theory theory) ->
+                | Some (`Theory theory) ->
                     Dune_rules.Coq_rules.coqtop_args_theory ~sctx ~dir
                       ~dir_contents:dc theory coq_module
-                | Some(`Extraction extr) ->
+                | Some (`Extraction extr) ->
                     Dune_rules.Coq_rules.coqtop_args_extraction ~sctx ~dir
                       ~dir_contents:dc extr
               in

src/dune_rules/coq_module.ml

@@ -21,15 +21,32 @@ module Name = struct
   let to_string s = s
 end
 
-module Map = Map.Make(Name)
-
-(* We keep prefix and name separated as the handling of `From Foo Require Bar.`
-   may benefit from it. *)
-type t =
-  { source : Path.Build.t
-  ; prefix : string list
-  ; name : Name.t
-  }
+module Module = struct
+  (* We keep prefix and name separated as the handling of `From Foo Require Bar.`
+     may benefit from it. *)
+  type t =
+    { source : Path.Build.t
+    ; prefix : string list
+    ; name : Name.t
+    }
+
+  let compare { source; prefix; name } t =
+    let open Ordering.O in
+    let= () = Path.Build.compare source t.source in
+    let= () = List.compare prefix t.prefix ~compare:String.compare in
+    Name.compare name t.name
+
+  let to_dyn { source; prefix; name } =
+    Dyn.record
+      [ ("source", Path.Build.to_dyn source)
+      ; ("prefix", Dyn.list Dyn.string prefix)
+      ; ("name", Name.to_dyn name)
+      ]
+end
+
+include Module
+
+module Map = Map.Make(Module)
 
 let make ~source ~prefix ~name = { source; prefix; name }
 

src/dune_rules/coq_module.mli

@@ -20,10 +20,10 @@ module Name : sig
   val to_string : t -> string
 end
 
-module Map : Map.S with type key = Name.t
-
 type t
 
+module Map : Map.S with type key = t
+
 (** A Coq module [a.b.foo] defined in file [a/b/foo.v] *)
 val make :
      source:Path.Build.t

src/dune_rules/coq_sources.ml

@@ -74,7 +74,7 @@ let of_dir (d : _ Dir_with_dune.t) ~include_subdirs ~dirs =
       in
       let rev_map =
         List.fold_left modules ~init:acc.rev_map ~f:(fun acc m ->
-          Coq_module.Map.add_exn acc (Coq_module.name m) (`Theory coq))
+          Coq_module.Map.add_exn acc m (`Theory coq))
       in
       { acc with directories; libraries; rev_map }
     | Extraction.T extr ->
@@ -90,12 +90,9 @@ let of_dir (d : _ Dir_with_dune.t) ~include_subdirs ~dirs =
             [ Pp.text "no coq source corresponding to prelude field" ]
       in
       let extract = Loc.Map.add_exn acc.extract extr.buildable.loc m in
-      let rev_map =
-        let name = Coq_module.name m in
-        Coq_module.Map.add_exn acc.rev_map name (`Extraction extr)
-      in
+      let rev_map = Coq_module.Map.add_exn acc.rev_map m (`Extraction extr) in
       { acc with extract; rev_map }
     | _ -> acc)
 
-let lookup_module t name =
-  Coq_module.Map.find t.rev_map name
+let lookup_module t m =
+  Coq_module.Map.find t.rev_map m

src/dune_rules/coq_sources.mli

@@ -30,5 +30,5 @@ val find_module :
 
 val lookup_module :
      t
-  -> Coq_module.Name.t
+  -> Coq_module.t
   -> [ `Theory of Theory.t | `Extraction of Extraction.t ] option