Pretty-printing improvements.

generator/print_coq.ml

@@ -242,8 +242,34 @@ and mod_typ mt =
 let mod_binding (xs, mt) = 
   binding (separate_map space string xs) (mod_typ mt)
 
-let mod_bindings bs = 
-  separate_map space mod_binding bs
+let pmod_binding mb =
+  space ^^ parens (mod_binding mb)
+
+let pmod_bindings mbs = 
+  group (concat_map pmod_binding mbs)
+
+(* Module expressions. *)
+
+let mod_expr xs =
+  separate_map space string xs
+
+(* Module definitions. *)
+
+let mod_def = function
+  | Mod_def_inline me ->
+      block (space ^^ colonequals) (break 1 ^^ mod_expr me) dot
+  | Mod_def_declare ->
+      dot
+
+(* Module casts. *)
+
+let mod_cast = function
+  | Mod_cast_exact mt ->
+      spacecolon ^^ space ^^ mod_typ mt
+  | Mod_cast_super mt ->
+      space ^^ string "<:" ^^ space ^^ mod_typ mt
+  | Mod_cast_free ->
+      empty
 
 (* -------------------------------------------------------------------------- *)
 
@@ -386,6 +412,20 @@ let top = function
       sprintf "Set Implicit Arguments."
   | Coqtop_text s -> 
       sprintf "%s" s
+  | Coqtop_declare_module (x, mt) ->
+      string "Declare Module" ^^
+      parameter (string x) (mod_typ mt)
+  | Coqtop_module (x, bs, c, d) ->
+      string "Module" ^^ space ^^
+      string x ^^
+      pmod_bindings bs ^^
+      mod_cast c ^^
+      mod_def d
+  | Coqtop_module_type (x, bs, d) ->
+      string "Module Type" ^^ space ^^
+      string x ^^
+      pmod_bindings bs ^^
+      mod_def d
   | Coqtop_module_type_include x ->
       sprintf "Include Type %s." x
   | Coqtop_end x ->
@@ -397,15 +437,6 @@ let top t =
 let tops ts =
   concat_map (fun t -> top t ^^ hardline ^^ hardline) ts
 
-(*
-  | Coqtop_declare_module (x,mt) ->
-      sprintf "Declare Module %s : %s." x (mod_typ mt)
-  | Coqtop_module (x,bs,c,d) ->
-      sprintf "Module %s %s %s %s" x (string_of_mod_bindings bs) (string_of_mod_cast c) (string_of_mod_def x d)
-  | Coqtop_module_type (x,bs,d) ->
-      sprintf "Module Type %s %s %s" x (string_of_mod_bindings bs) (string_of_mod_def x d)
-*)
-
 (* -------------------------------------------------------------------------- *)
 
 (* The main entry point translates a list of toplevel elements to a string. *)