Module subtyping : allow many <: and module type declaration with <:

 Any place where <: was legal can now contain many <: declarations.
 Moreover we can say that the module type we are declaring is a subtype
 of an earlier module type. See DecidableType2 for examples.
 Also try to handle correctly the freeze/unfreeze summaries
 when simulating start/include/end (syntax ... := ... <+ ...)

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

2 files changed, 30 insertions, 21 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 38ab689f5..56946ef27 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -388,17 +388,16 @@ GEXTEND Gram
   gallina_ext:
     [ [ (* Interactive module declaration *)
         IDENT "Module"; export = export_token; id = identref;
-	bl = LIST0 module_binder; mty_o = OPT of_module_type;
-	o = OPT is_module_expr ->
-	  VernacDefineModule (export, id, bl, mty_o,
-			      match o with None -> [] | Some l -> l)
+	bl = LIST0 module_binder; sign = of_module_type;
+	body = is_module_expr ->
+	  VernacDefineModule (export, id, bl, sign, body)
       | IDENT "Module"; "Type"; id = identref;
-	bl = LIST0 module_binder; o = OPT is_module_type ->
-	  VernacDeclareModuleType (id, bl,
-				   match o with None -> [] | Some l -> l)
+	bl = LIST0 module_binder; sign = check_module_types;
+	body = is_module_type ->
+	  VernacDeclareModuleType (id, bl, sign, body)
       | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
 	bl = LIST0 module_binder; ":"; mty = module_type ->
-	  VernacDeclareModule (export, id, bl, (mty,true))
+	  VernacDeclareModule (export, id, bl, mty)
       (* Section beginning *)
       | IDENT "Section"; id = identref -> VernacBeginSection id
       | IDENT "Chapter"; id = identref -> VernacBeginSection id
@@ -433,15 +432,23 @@ GEXTEND Gram
   ext_module_expr:
     [ [ "<+"; mexpr = module_expr -> mexpr ] ]
   ;
+  check_module_type:
+    [ [ "<:"; mty = module_type -> mty ] ]
+  ;
+  check_module_types:
+    [ [ mtys = LIST0 check_module_type -> mtys ] ]
+  ;
   of_module_type:
-    [ [ ":"; mty = module_type -> (mty, true)
-      | "<:"; mty = module_type -> (mty, false) ] ]
+    [ [ ":"; mty = module_type -> Enforce mty
+      | mtys = check_module_types -> Check mtys ] ]
   ;
   is_module_type:
-    [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l) ] ]
+    [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l)
+      | -> [] ] ]
   ;
   is_module_expr:
-    [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l) ] ]
+    [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l)
+      | -> [] ] ]
   ;
 
   (* Module binder  *)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4407ca6aa..190271159 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -253,9 +253,10 @@ and  pr_module_expr = function
       pr_module_expr me1 ++ spc() ++
       hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
 
-let pr_of_module_type prc (mty,b) =
-  str (if b then ":" else "<:") ++
-  pr_module_type prc mty
+let pr_of_module_type prc = function
+  | Enforce mty -> str ":" ++ pr_module_type prc mty
+  | Check mtys ->
+      prlist_strict (fun m -> str "<:" ++ pr_module_type prc m) mtys
 
 let pr_require_token = function
   | Some true -> str "Export "
@@ -746,24 +747,25 @@ let rec pr_vernac = function
      hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_lident id)
 
   (* Modules and Module Types *)
-  | VernacDefineModule (export,m,bl,ty,bd) ->
+  | VernacDefineModule (export,m,bl,tys,bd) ->
       let b = pr_module_binders_list bl pr_lconstr in
       hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
                pr_lident m ++ b ++
-               pr_opt (pr_of_module_type pr_lconstr) ty ++
+               pr_of_module_type pr_lconstr tys ++
 	       (if bd = [] then mt () else str ":= ") ++
 	       prlist_with_sep (fun () -> str " <+ ") pr_module_expr bd)
   | VernacDeclareModule (export,id,bl,m1) ->
       let b = pr_module_binders_list bl pr_lconstr in
 	hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
              pr_lident id ++ b ++
-             pr_of_module_type pr_lconstr m1)
-  | VernacDeclareModuleType (id,bl,m) ->
+             pr_module_type pr_lconstr m1)
+  | VernacDeclareModuleType (id,bl,tyl,m) ->
       let b = pr_module_binders_list bl pr_lconstr in
+      let pr_mt = pr_module_type pr_lconstr in
 	hov 2 (str"Module Type " ++ pr_lident id ++ b ++
+		 prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++
 		 (if m = [] then mt () else str ":= ") ++
-		 prlist_with_sep (fun () -> str " <+ ")
-		                 (pr_module_type pr_lconstr) m)
+		 prlist_with_sep (fun () -> str " <+ ") pr_mt m)
   | VernacInclude (b,CIMTE(mty,mtys)) ->
       let pr_mty = pr_module_type pr_lconstr in
       hov 2 (str"Include " ++ str (if b then "Self " else "") ++ str "Type " ++