From 9b6517c0c933fb1d66c7feb53fa57e1697d8124a Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 7 Jan 2010 15:32:49 +0000 Subject: Include can accept both Module and Module Type Syntax Include Type is still active, but deprecated, and triggers a warning. The syntax M <+ M' <+ M'', which performs internally an Include, also benefits from this: M, M', M'' can be independantly modules or module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_vernac.ml4 | 15 ++++++++------- parsing/pcoq.mli | 2 +- parsing/ppvernac.ml | 48 +++++++++++++++++++----------------------------- 3 files changed, 28 insertions(+), 37 deletions(-) (limited to 'parsing') diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4672a732a..f4d588b57 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -397,9 +397,10 @@ GEXTEND Gram | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr -> - VernacInclude(CIME(e::l)) + VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type -> - VernacInclude(CIMTE(e::l)) ] ] + warning "Include Type is deprecated; use Include instead"; + VernacInclude(e::l) ] ] ; export_token: [ [ IDENT "Import" -> Some false @@ -440,11 +441,11 @@ GEXTEND Gram (* Module expressions *) module_expr: [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> CMEapply (me1,me2) + | me1 = module_expr; me2 = module_expr_atom -> CMapply (me1,me2) ] ] ; module_expr_atom: - [ [ qid = qualid -> CMEident qid | "("; me = module_expr; ")" -> me ] ] + [ [ qid = qualid -> CMident qid | "("; me = module_expr; ")" -> me ] ] ; with_declaration: [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> @@ -454,10 +455,10 @@ GEXTEND Gram ] ] ; module_type: - [ [ qid = qualid -> CMTEident qid + [ [ qid = qualid -> CMident qid | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) - | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl) + | mty = module_type; me = module_expr_atom -> CMapply (mty,me) + | mty = module_type; "with"; decl = with_declaration -> CMwith (mty,decl) ] ] ; END diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d724e2e73..6d5455b1b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -214,7 +214,7 @@ module Constr : module Module : sig val module_expr : module_ast Gram.Entry.e - val module_type : module_type_ast Gram.Entry.e + val module_type : module_ast Gram.Entry.e end module Tactic : diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 4b1162dbd..92a455abc 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -234,29 +234,22 @@ let pr_with_declaration pr_c = function str"Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid -let rec pr_module_type pr_c = function - | CMTEident qid -> spc () ++ pr_located pr_qualid qid - | CMTEwith (mty,decl) -> - let m = pr_module_type pr_c mty in +let rec pr_module_ast pr_c = function + | CMident qid -> spc () ++ pr_located pr_qualid qid + | CMwith (mty,decl) -> + let m = pr_module_ast pr_c mty in let p = pr_with_declaration pr_c decl in m ++ spc() ++ str"with" ++ spc() ++ p - | CMTEapply (fexpr,mexpr)-> - let f = pr_module_type pr_c fexpr in - let m = pr_module_expr mexpr in - f ++ spc () ++ m - -and pr_module_expr = function - | CMEident qid -> pr_located pr_qualid qid - | CMEapply (me1,(CMEident _ as me2)) -> - pr_module_expr me1 ++ spc() ++ pr_module_expr me2 - | CMEapply (me1,me2) -> - pr_module_expr me1 ++ spc() ++ - hov 1 (str"(" ++ pr_module_expr me2 ++ str")") + | CMapply (me1,(CMident _ as me2)) -> + pr_module_ast pr_c me1 ++ spc() ++ pr_module_ast pr_c me2 + | CMapply (me1,me2) -> + pr_module_ast pr_c me1 ++ spc() ++ + hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")") let pr_of_module_type prc = function - | Enforce mty -> str ":" ++ pr_module_type prc mty + | Enforce mty -> str ":" ++ pr_module_ast prc mty | Check mtys -> - prlist_strict (fun m -> str "<:" ++ pr_module_type prc m) mtys + prlist_strict (fun m -> str "<:" ++ pr_module_ast prc m) mtys let pr_require_token = function | Some true -> str "Export " @@ -264,7 +257,7 @@ let pr_require_token = function | None -> mt() let pr_module_vardecls pr_c (export,idl,mty) = - let m = pr_module_type pr_c mty in + let m = pr_module_ast pr_c mty in (* Update the Nametab for interpreting the body of module/modtype *) let lib_dir = Lib.library_dp() in List.iter (fun (_,id) -> @@ -751,27 +744,24 @@ let rec pr_vernac = function pr_lident m ++ b ++ pr_of_module_type pr_lconstr tys ++ (if bd = [] then mt () else str ":= ") ++ - prlist_with_sep (fun () -> str " <+ ") pr_module_expr bd) + prlist_with_sep (fun () -> str " <+ ") + (pr_module_ast pr_lconstr) 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_module_type pr_lconstr m1) + pr_module_ast 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 + let pr_mt = pr_module_ast 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_mt m) - | VernacInclude (CIMTE(mtys)) -> - let pr_mty = pr_module_type pr_lconstr in - hov 2 (str"Include Type " ++ - prlist_with_sep (fun () -> str " <+ ") pr_mty mtys) - | VernacInclude (CIME(mexprs)) -> - let pr_me = pr_module_expr in + | VernacInclude (mexprs) -> + let pr_m = pr_module_ast pr_lconstr in hov 2 (str"Include " ++ - prlist_with_sep (fun () -> str " <+ ") pr_me mexprs) + prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) (* Solving *) | VernacSolve (i,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ -- cgit v1.2.3