Extraction : get_duplicates (via option) instead of check_duplicates (via Not_found)

 This clarifies the execution flow

3 files changed, 31 insertions, 32 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9446cf667..de97ba97c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -308,15 +308,16 @@ end
 
 module DupMap = Map.Make(DupOrd)
 
-let add_duplicate, check_duplicate =
+let add_duplicate, get_duplicate =
   let index = ref 0 and dups = ref DupMap.empty in
   register_cleanup (fun () -> index := 0; dups := DupMap.empty);
   let add mp l =
      incr index;
      let ren = "Coq__" ^ string_of_int !index in
      dups := DupMap.add (mp,l) ren !dups
-  and check mp l = DupMap.find (mp, l) !dups
-  in (add,check)
+  and get mp l =
+    try Some (DupMap.find (mp, l) !dups) with Not_found -> None
+  in (add,get)
 
 type reset_kind = AllButExternal | Everything
 
@@ -510,10 +511,11 @@ let pp_duplicate k' prefix mp rls olab =
       (* Here rls=s::rls', we search the label for s inside mp *)
       List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp
   in
-  try dottify (check_duplicate prefix lbl :: rls')
-  with Not_found ->
-    assert (get_phase () == Pre); (* otherwise it's too late *)
-    add_duplicate prefix lbl; dottify rls
+  match get_duplicate prefix lbl with
+  | Some ren -> dottify (ren :: rls')
+  | None ->
+     assert (get_phase () == Pre); (* otherwise it's too late *)
+     add_duplicate prefix lbl; dottify rls
 
 let fstlev_ks k = function
   | [] -> assert false
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 2f5601964..b8e95afb3 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -62,7 +62,7 @@ val top_visible_mp : unit -> module_path
 val push_visible : module_path -> module_path list -> unit
 val pop_visible : unit -> unit
 
-val check_duplicate : module_path -> Label.t -> string
+val get_duplicate : module_path -> Label.t -> string option
 
 type reset_kind = AllButExternal | Everything
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 5d10cb939..31e481d12 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -610,30 +610,29 @@ let pp_alias_spec ren = function
 let rec pp_specif = function
   | (_,Spec (Sval _ as s)) -> pp_spec s
   | (l,Spec s) ->
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+     (match Common.get_duplicate (top_visible_mp ()) l with
+      | None -> pp_spec s
+      | Some ren ->
 	 hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_spec ren s
-       with Not_found -> pp_spec s)
+	 pp_alias_spec ren s)
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> Pp.mt ()
+       | Some ren ->
          fnl () ++
          hov 1 (str ("module "^ren^" :") ++ spc () ++
-                str "module type of struct include " ++ name ++ str " end")
-       with Not_found -> Pp.mt ())
+                str "module type of struct include " ++ name ++ str " end"))
   | (l,Smodtype mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> Pp.mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> Pp.mt ()
+       | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
 
 and pp_module_type params = function
   | MTident kn ->
@@ -682,12 +681,12 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) ->
-       (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+     (match Common.get_duplicate (top_visible_mp ()) l with
+      | None -> pp_decl d
+      | Some ren ->
 	 hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_decl ren d
-	with Not_found -> pp_decl d)
+	 pp_alias_decl ren d)
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
@@ -700,18 +699,16 @@ let rec pp_structure_elem = function
       hov 1
 	(str "module " ++ name ++ typ ++ str " =" ++
 	 (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ str ("module "^ren^" = ") ++ name
-       with Not_found -> mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
+       | None -> mt ())
   | (l,SEmodtype m) ->
       let def = pp_module_type [] m in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-         fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> mt ()
+       | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
 
 and pp_module_expr params = function
   | MEident mp -> pp_modname mp