Extraction: get advantage of nicer, algebraic, module types

We use the mod_type_alg and typ_expr_alg field when they aren't
 empty.  As a consequences, many signatures are now simple
 abbreviations, or "with" constructions, leading to .mli that are
 _way_ shorter this way.  Various fixups concerning the "with
 Definition" syntax. In extract_seb_spec, we propagate both the alg
 and non-alg versions of the structure, for handlying nicely the
 "with" situation, and expanding situations not possible in ocaml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13249 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 66 insertions, 54 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3210f2f16..b1195b4be 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -137,14 +137,42 @@ let factor_fix env l cb msb =
     labels, recd, msb''
   end
 
-let my_type_of_mb env mb =
-  match mb.mod_type_alg with Some m -> m | None -> mb.mod_type
+(** Expanding a [struct_expr_body] into a version without abbreviations
+    or functor applications. This is done via a detour to entries
+    (hack proposed by Elie)
+*)
+
+let rec seb2mse = function
+  | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s')
+  | SEBident mp -> Entries.MSEident mp
+  | _ -> failwith "seb2mse: received a non-atomic seb"
+
+let expand_seb env mp seb =
+  let seb,_,_,_ =
+    Mod_typing.translate_struct_module_entry env mp true (seb2mse seb)
+  in seb
+
+(** When possible, we use the nicer, shorter, algebraic type structures
+    instead of the expanded ones. *)
+
+let my_type_of_mb mb =
+  let m0 = mb.mod_type in
+  match mb.mod_type_alg with Some m -> m0,m | None -> m0,m0
+
+let my_type_of_mtb mtb =
+  let m0 = mtb.typ_expr in
+  match mtb.typ_expr_alg with Some m -> m0,m | None -> m0,m0
 
 (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
     To check with Elie. *)
 
-let env_for_mtb_with env mp mtb idl =
-  let sig_b = match mtb with
+let rec msid_of_seb = function
+  | SEBident mp -> mp
+  | SEBwith (seb,_) -> msid_of_seb seb
+  | _ -> assert false
+
+let env_for_mtb_with env mp seb idl =
+  let sig_b = match seb with
     | SEBstruct(sig_b) -> sig_b
     | _ -> assert false
   in
@@ -172,49 +200,47 @@ let rec extract_sfb_spec env mp = function
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmodule mb) :: msig ->
       let specs = extract_sfb_spec env mp msig in
-      let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb env mb) in
+      let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb mb) in
       (l,Smodule spec) :: specs
   | (l,SFBmodtype mtb) :: msig ->
       let specs = extract_sfb_spec env mp msig in
-      (l,Smodtype (extract_seb_spec env mtb.typ_mp mtb.typ_expr)) :: specs
+      let spec = extract_seb_spec env mtb.typ_mp (my_type_of_mtb mtb) in
+      (l,Smodtype spec) :: specs
 
 (* From [struct_expr_body] to specifications *)
 
-(* Invariant: the [seb] given to [extract_seb_spec] should either come:
-   - from a [mod_type] or [type_expr] field
-   - from the output of [Modops.eval_struct].
+(* Invariant: the [seb] given to [extract_seb_spec] should either come
+   from a [mod_type] or [type_expr] field, or their [_alg] counterparts.
    This way, any encountered [SEBident] should be a true module type.
-   For instance, [my_type_of_mb] ensures this invariant.
 *)
 
-and extract_seb_spec env mp1 = function
+and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
   | SEBident mp -> Visit.add_mp mp; MTident mp
-  | SEBwith(mtb',With_definition_body(idl,cb))->
-      let env' = env_for_mtb_with env  mp1 mtb' idl in
-      let mtb''= extract_seb_spec env mp1 mtb' in
+  | SEBwith(seb',With_definition_body(idl,cb))->
+      let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in
+      let mt = extract_seb_spec env mp1 (seb,seb') in
       (match extract_with_type env' cb with (* cb peut contenir des kn  *)
-	 | None ->  mtb''
-	 | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ)))
-  | SEBwith(mtb',With_module_body(idl,mp))->
+	 | None -> mt
+	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
+  | SEBwith(seb',With_module_body(idl,mp))->
       Visit.add_mp mp;
-      MTwith(extract_seb_spec env mp1 mtb',
+      MTwith(extract_seb_spec env mp1 (seb,seb'),
 	     ML_With_module(idl,mp))
-(* TODO: On pourrait peut-etre oter certaines eta-expansion, du genre:
-   | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_))
-     when mbid = mbid2 -> extract_seb_spec env m
-   (* faudrait alors ajouter un test de non-apparition de mbid dans mb *)
-*)
- | SEBfunctor (mbid, mtb, mtb') ->
+  | SEBfunctor (mbid, mtb, seb_alg') ->
+      let seb' = match seb with
+	| SEBfunctor (mbid',_,seb') when mbid' = mbid -> seb'
+	| _ -> assert false
+      in
       let mp = MPbound mbid in
-      let env' = Modops.add_module (Modops.module_body_of_type mp mtb) 
-	env in
-      MTfunsig (mbid, extract_seb_spec env mp mtb.typ_expr,
-		extract_seb_spec env' mp1 mtb')
+      let env' = Modops.add_module (Modops.module_body_of_type mp mtb) env in
+      MTfunsig (mbid, extract_seb_spec env mp (my_type_of_mtb mtb),
+		extract_seb_spec env' mp1 (seb',seb_alg'))
   | SEBstruct (msig) ->
       let env' = Modops.add_signature mp1 msig empty_delta_resolver env in
-	MTsig (mp1, extract_sfb_spec env' mp1 msig)
+      MTsig (mp1, extract_sfb_spec env' mp1 msig)
   | SEBapply _ ->
-      assert false
+      if seb <> seb_alg then extract_seb_spec env mp1 (seb,seb)
+      else assert false
 
 
 
@@ -267,23 +293,15 @@ let rec extract_sfb env mp all = function
       let ms = extract_sfb env mp all msb in
       let mp = MPdot (mp,l) in
        if all || Visit.needed_mp mp then
-	(l,SEmodtype (extract_seb_spec env mp mtb.typ_expr)) :: ms
+	(l,SEmodtype (extract_seb_spec env mp (my_type_of_mtb mtb))) :: ms
       else ms
 
 (* From [struct_expr_body] to implementations *)
 
 and extract_seb env mp all = function
   | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml ->
-      (* in Haskell/Scheme, we expanse everything *)
-      let rec seb2mse = function
-	| SEBident mp -> Entries.MSEident mp
-	| SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s')
-	| _ -> assert false
-      in
-      let seb,_,_,_ =
-	Mod_typing.translate_struct_module_entry env mp true (seb2mse seb)
-      in
-      extract_seb env mp all seb
+      (* in Haskell/Scheme, we expand everything *)
+      extract_seb env mp all (expand_seb env mp seb)
   | SEBident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
       Visit.add_mp mp; MEident mp
@@ -294,7 +312,7 @@ and extract_seb env mp all = function
       let mp1 = MPbound mbid in
       let env' = Modops.add_module (Modops.module_body_of_type  mp1 mtb)
 	env  in
-      MEfunctor (mbid, extract_seb_spec env mp1 mtb.typ_expr,
+      MEfunctor (mbid, extract_seb_spec env mp1 (my_type_of_mtb mtb),
 		 extract_seb env' mp true meb)
   | SEBstruct (msb) ->
       let env' = Modops.add_signature mp msb empty_delta_resolver env in
@@ -305,7 +323,7 @@ and extract_module env mp all mb =
   (* [mb.mod_expr <> None ], since we look at modules from outside. *)
   (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
   { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr);
-    ml_mod_type = extract_seb_spec env mp (my_type_of_mb env mb) }
+    ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
 
 
 let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index ceb2246ad..baec2eae4 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -646,26 +646,20 @@ and pp_module_type params = function
       let mp_w =
 	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
       in
-      let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l))
-      in
+      let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in
       push_visible mp_mt [];
-      let s =
-	pp_module_type [] mt ++ str " with type " ++
-	  pp_global Type r ++ ids
-      in
+      let pp_w = str " with type " ++ ids ++ pp_global Type r in
       pop_visible();
-      s ++ str "=" ++ spc () ++ pp_type false vl typ
+      pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_type false vl typ
   | MTwith(mt,ML_With_module(idl,mp)) ->
       let mp_mt = msid_of_mt mt in
       let mp_w =
 	List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
       in
       push_visible mp_mt [];
-      let s =
-	pp_module_type [] mt ++ str " with module " ++ pp_modname mp_w
-      in
+      let pp_w = str " with module " ++ pp_modname mp_w in
       pop_visible ();
-      s ++ str " = " ++ pp_modname mp
+      pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_modname mp
 
 let is_short = function MEident _ | MEapply _ -> true | _ -> false