From 0929a78f9a663ac2bcdf1294de93797b9fdfefad Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 4 Feb 2017 01:50:58 +0100
Subject: Extraction: fix complexity issue #5310

  A double call to pp_module_type inside Ocaml.pp_specif was
  causing an complexity blowup when pretty-printing heavily modular
  extracted code.

  I wasn't able to figure out why this double call is there. It could
  be the leftover of some intermediate work in 2007 before commit 350398eae
  (which introduced global printing phases Pre/Impl/Intf).

  Anyway I'm reasonably sure that today these two pp_module_type calls produce
  the exact same pretty-printed signature (even if there's a large bunch of
  imperative states around). Moreover, this duplicated signature is actually
  slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
  the type of Coq__123 should not be an exact copy of the type of M, but rather
  a "strengthened" version of it (with equality between inductive types).
  So the best solution is now to use this funny feature of OCaml introduced in 3.12 :

  module Coq__123 : module type of struct include M end

  This "module type of struct include" is slightly awkward, but short, correct,
  and trivial to produce :-). And I doubt anybody will object to the (rare) use
  of some 3.12 features in extracted code of 2017...
---
 plugins/extraction/ocaml.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 1c29a9bc24..5d10cb939d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -618,12 +618,13 @@ let rec pp_specif = function
        with Not_found -> pp_spec s)
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
-      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
-	 fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
+         fnl () ++
+         hov 1 (str ("module "^ren^" :") ++ spc () ++
+                str "module type of struct include " ++ name ++ str " end")
        with Not_found -> Pp.mt ())
   | (l,Smodtype mt) ->
       let def = pp_module_type [] mt in
-- 
cgit v1.2.3