From 8ef3bc0e8a65b3a0338da39aa54cd75b1c2c1bb7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Sat, 4 Feb 2017 19:55:18 +0100
Subject: Extraction: simplify the generated code for difficult name conflicts

 No more pp_alias_spec et pp_alias_decl.
 Instead, we use "include" and "module type of".
 The extracted code might hence need OCaml 3.12 (quite rarely)
---
 plugins/extraction/ocaml.ml | 33 ++-------------------------------
 1 file changed, 2 insertions(+), 31 deletions(-)

(limited to 'plugins/extraction/ocaml.ml')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 31e481d12..404939cff 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -555,24 +555,6 @@ let pp_decl = function
     | Dfix (rv,defs,typs) ->
 	pp_Dfix (rv,defs,typs)
 
-let pp_alias_decl ren = function
-  | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Dtype (r, l, _) ->
-      let name = pp_global Type r in
-      let l = rename_tvars keywords l in
-      let ids = pp_parameters l in
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
-	     str (ren^".") ++ name)
-  | Dterm (r, a, t) ->
-      let name = pp_global Term r in
-      hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
-  | Dfix (rv, _, _) ->
-      prvecti (fun i r -> if is_inline_custom r then mt () else
-		 let name = pp_global Term r in
-		 hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
-		 fnl ())
-	rv
-
 let pp_spec = function
   | Sval (r,_) when is_inline_custom r -> mt ()
   | Stype (r,_,_) when is_inline_custom r -> mt ()
@@ -597,16 +579,6 @@ let pp_spec = function
       in
       hov 2 (str "type " ++ ids ++ name ++ def)
 
-let pp_alias_spec ren = function
-  | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Stype (r,l,_) ->
-      let name = pp_global Type r in
-      let l = rename_tvars keywords l in
-      let ids = pp_parameters l in
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
-	     str (ren^".") ++ name)
-  | Sval _ -> assert false
-
 let rec pp_specif = function
   | (_,Spec (Sval _ as s)) -> pp_spec s
   | (l,Spec s) ->
@@ -615,7 +587,7 @@ let rec pp_specif = function
       | Some ren ->
 	 hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_spec ren s)
+         str ("include module type of struct include "^ren^" end"))
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
@@ -685,8 +657,7 @@ let rec pp_structure_elem = function
       | 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)
+	 fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
-- 
cgit v1.2.3