Declarations.mli: reorganization of modular structures

 The earlier type [struct_expr_body] was far too broad,
 leading to code with unclear invariants, many "assert false", etc etc.
 Its replacement [module_alg_expr] has only three constructors:
   * MEident
   * MEapply : note the module_path as 2nd arg, no more constraints here
   * MEwith : no more constant_body inside, constr is just fine
 But no more SEBfunctor or SEBstruct constructor here (see below).
 This way, this datatype corresponds to algebraic expressions,
 i.e. anything that can appear in non-interactive modules.
 In fact, it even coincides now with [Entries.module_struct_entry].

 - Functor constructors are now necessarily on top of other
   structures thanks to a generic [functorize] datatype.

 - Structures are now separated from algebraic expressions by design :
   the [mod_type] and [typ_expr] fields now only contain structures
   (or functorized structures), while [mod_type_alg] and [typ_expr_alg]
   are restricted to algebraic expressions only.

 - Only the implementation field [mod_expr] could be either algebraic
   or structural. We handle this via a specialized datatype
   [module_implementation] with four constructors:

    * Abstract : no implementation (cf. for instance Declare Module)
    * Algebraic(_) : for non-interactive modules, e.g. Module M := N.
    * Struct(_) : for interactive module, e.g. Module M : T. ... End M.
    * FullStruct : for interactive module with no type restriction.

   The [FullStruct] is a particular case of [Struct] where the implementation
   need not be stored at all, since it is exactly equal to its expanded
   type present in [mod_type]. This is less fragile than hoping as earlier
   that pointer equality between [mod_type] and [mod_expr] will be
   preserved...

 - We clearly emphasize that only [mod_type] and [typ_expr] are
   relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
   are there only for a nicer extraction and shorter module printing.
   [mod_expr] is also not accessed by the kernel, but it is important
   for Print Assumptions later.

 - A few implicit invariants remain, for instance "no MEwith in mod_expr",
   see the final comment in Declarations

 - Heavy refactoring of module-related files : modops, mod_typing,
   safe_typing, declaremods, extraction/extract_env.ml ...

 - Coqchk has been adapted accordingly. The code concerning MEwith
   in Mod_checking is now gone, since we cannot have any in mod_expr.

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

1 files changed, 90 insertions, 79 deletions

diff --git a/printing/printmod.ml b/printing/printmod.ml
index ee4a2db7f..b5d1d8a18 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -114,18 +114,24 @@ let nametab_register_module_body mp struc =
     nametab_register_dir mp;
     List.iter (nametab_register_body mp DirPath.empty) struc
 
-let nametab_register_module_param mbid seb =
-  (* For algebraic seb, we use a Declaremods function that converts into mse *)
-  try Declaremods.process_module_binding mbid seb
-  with e when Errors.noncritical e ->
-    (* Otherwise, for expanded structure, we try to play with the nametab *)
-    match seb with
-      | SEBstruct struc ->
-        let mp = MPbound mbid in
-        let dir = DirPath.make [MBId.to_id mbid] in
-        nametab_register_dir mp;
-        List.iter (nametab_register_body mp dir) struc
-      | _ -> ()
+let get_typ_expr_alg mtb = match mtb.typ_expr_alg with
+  | Some (NoFunctor me) -> me
+  | _ -> raise Not_found
+
+let nametab_register_modparam mbid mtb =
+  match mtb.typ_expr with
+  | MoreFunctor _ -> () (* functorial param : nothing to register *)
+  | NoFunctor struc ->
+    (* We first try to use the algebraic type expression if any,
+       via a Declaremods function that converts back to module entries *)
+    try
+      Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
+    with e when Errors.noncritical e ->
+      (* Otherwise, we try to play with the nametab ourselves *)
+      let mp = MPbound mbid in
+      let dir = DirPath.make [MBId.to_id mbid] in
+      nametab_register_dir mp;
+      List.iter (nametab_register_body mp dir) struc
 
 let print_body is_impl env mp (l,body) =
   let name = str (Label.to_string l) in
@@ -161,71 +167,71 @@ let print_body is_impl env mp (l,body) =
 let print_struct is_impl env mp struc =
   prlist_with_sep spc (print_body is_impl env mp) struc
 
+let print_structure is_type env mp locals struc =
+  let env' = Option.map
+    (Modops.add_structure mp struc Mod_subst.empty_delta_resolver) env in
+  nametab_register_module_body mp struc;
+  let kwd = if is_type then "Sig" else "Struct" in
+  hv 2 (str kwd ++ spc () ++ print_struct false env' mp struc ++
+	brk (1,-2) ++ str "End")
+
 let rec flatten_app mexpr l = match mexpr with
-  | SEBapply (mexpr, SEBident arg,_) -> flatten_app mexpr (arg::l)
-  | SEBident mp -> mp::l
-  | _ -> assert false
+  | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l)
+  | MEident mp -> mp::l
+  | MEwith _ -> assert false
 
-let rec print_modtype env mp locals mty =
+let rec print_typ_expr env mp locals mty =
   match mty with
-    | SEBident kn -> print_kn locals kn
-    | SEBfunctor (mbid,mtb1,mtb2) ->
-      let mp1 = MPbound mbid in
-      let env' = Option.map
-	  (Modops.add_module (Modops.module_body_of_type mp1 mtb1)) env in
-      let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
-      let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals
-      in
-      nametab_register_module_param mbid seb1;
-      hov 2 (str "Funsig" ++ spc () ++ str "(" ++
-	       pr_id (MBId.to_id mbid) ++ str ":" ++
-	       print_modtype env mp1 locals seb1 ++
-	       str ")" ++ spc() ++ print_modtype env' mp locals' mtb2)
-  | SEBstruct (sign) ->
-      let env' = Option.map
-	(Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
-      nametab_register_module_body mp sign;
-      hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
-	    brk (1,-2) ++ str "End")
-  | SEBapply _ ->
+  | MEident kn -> print_kn locals kn
+  | MEapply _ ->
       let lapp = flatten_app mty [] in
       let fapp = List.hd lapp in
       let mapp = List.tl lapp in
       hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
 		 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
-  | SEBwith(seb,With_definition_body(idl,cb))->
+  | MEwith(me,WithDef(idl,c))->
       let env' = None in (* TODO: build a proper environment if env <> None *)
-      let s = (String.concat "." (List.map Id.to_string idl)) in
-      hov 2 (print_modtype env' mp locals seb ++ spc() ++ str "with" ++ spc() ++
-	       str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
-  | SEBwith(seb,With_module_body(idl,mp))->
-      let s =(String.concat "." (List.map Id.to_string idl)) in
-      hov 2 (print_modtype env mp locals seb ++ spc() ++ str "with" ++ spc() ++
-	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
-
-let rec print_modexpr env mp locals mexpr = match mexpr with
-  | SEBident mp -> print_modpath locals mp
-  | SEBfunctor (mbid,mty,mexpr) ->
-      let mp' = MPbound mbid in
-      let env' = Option.map
-	(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
-      let typ = Option.default mty.typ_expr mty.typ_expr_alg in
+      let s = String.concat "." (List.map Id.to_string idl) in
+      hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
+             ++ str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
+  | MEwith(me,WithMod(idl,mp))->
+      let s = String.concat "." (List.map Id.to_string idl) in
+      hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++
+             str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
+
+let print_mod_expr env mp locals = function
+  | MEident mp -> print_modpath locals mp
+  | MEapply _ as me ->
+      let lapp = flatten_app me [] in
+      hov 3
+        (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
+  | MEwith _ -> assert false (* No 'with' syntax for modules *)
+
+let rec print_functor fty fatom is_type env mp locals = function
+  |NoFunctor me -> fatom is_type env mp locals me
+  |MoreFunctor (mbid,mtb1,me2) ->
+      nametab_register_modparam mbid mtb1;
+      let mp1 = MPbound mbid in
+      let pr_mtb1 = fty env mp1 locals mtb1 in
+      let env' = Option.map (Modops.add_module_type mp1 mtb1) env in
       let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in
-      nametab_register_module_param mbid typ;
-      hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(MBId.to_id mbid) ++
-	     str ":" ++ print_modtype env mp' locals typ ++
-      str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
-  | SEBstruct struc ->
-      let env' = Option.map
-	(Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
-      nametab_register_module_body mp struc;
-      hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
-	    brk (1,-2) ++ str "End")
-  | SEBapply _ ->
-      let lapp = flatten_app mexpr [] in
-      hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
-  | SEBwith (_,_)-> anomaly (Pp.str "Not available yet")
+      let kwd = if is_type then "Funsig" else "Functor" in
+      hov 2
+        (str kwd ++ spc () ++
+	 str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++
+	 spc() ++ print_functor fty fatom is_type env' mp locals' me2)
+
+let rec print_expression x =
+  print_functor
+    print_modtype
+    (function true -> print_typ_expr | false -> print_mod_expr) x
+
+and print_signature x =
+  print_functor print_modtype print_structure x
 
+and print_modtype env mp locals mtb = match mtb.typ_expr_alg with
+  | Some me -> print_expression true env mp locals me
+  | None -> print_signature true env mp locals mtb.typ_expr
 
 let rec printable_body dir =
   let dir = pop_dirpath dir in
@@ -241,23 +247,28 @@ let rec printable_body dir =
 (** Since we might play with nametab above, we should reset to prior
     state after the printing *)
 
-let print_modexpr' env mp mexpr =
+let print_expression' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_modexpr env mp [] e)) mexpr
+    (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me
 
-let print_modtype' env mp mty =
+let print_signature' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_modtype env mp [] e)) mty
+    (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me
 
-let print_module' env mp with_body mb =
+let unsafe_print_module env mp with_body mb =
   let name = print_modpath [] mp in
+  let pr_equals = spc () ++ str ":= " in
   let body = match with_body, mb.mod_expr with
     | false, _
-    | true, None -> mt()
-    | true, Some mexpr ->
-	spc () ++ str ":= " ++ print_modexpr' env mp mexpr
+    | true, Abstract -> mt()
+    | _, Algebraic me -> pr_equals ++ print_expression' false env mp me
+    | _, Struct sign -> pr_equals ++ print_signature' false env mp sign
+    | _, FullStruct -> pr_equals ++ print_signature' false env mp mb.mod_type
   in
-  let modtype = brk (1,1) ++ str": " ++ print_modtype' env mp mb.mod_type
+  let modtype = match mb.mod_expr, mb.mod_type_alg with
+    | FullStruct, _ -> mt ()
+    | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true env mp ty
+    | _, _ -> brk (1,1) ++ str": " ++ print_signature' true env mp mb.mod_type
   in
   hv 0 (str "Module " ++ name ++ modtype ++ body)
 
@@ -267,9 +278,9 @@ let print_module with_body mp =
   let me = Global.lookup_module mp in
   try
     if !short then raise ShortPrinting;
-    print_module' (Some (Global.env ())) mp with_body me ++ fnl ()
+    unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl ()
   with e when Errors.noncritical e ->
-    print_module' None mp with_body me ++ fnl ()
+    unsafe_print_module None mp with_body me ++ fnl ()
 
 let print_modtype kn =
   let mtb = Global.lookup_modtype kn in
@@ -278,6 +289,6 @@ let print_modtype kn =
     (str "Module Type " ++ name ++ str " =" ++ spc () ++
      (try
 	if !short then raise ShortPrinting;
-	print_modtype' (Some (Global.env ())) kn mtb.typ_expr
+	print_signature' true (Some (Global.env ())) kn mtb.typ_expr
       with e when Errors.noncritical e ->
-	print_modtype' None kn mtb.typ_expr))
+	print_signature' true None kn mtb.typ_expr))