syntax for import filters

4 files changed, 52 insertions, 14 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1f52641b82..642f504050 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -566,14 +566,18 @@ GRAMMAR EXTEND Gram
       | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token
         ; qidl = LIST1 global ->
         { VernacRequire (Some ns, export, qidl) }
-      | IDENT "Import"; qidl = LIST1 global -> { VernacImport (false,qidl) }
-      | IDENT "Export"; qidl = LIST1 global -> { VernacImport (true,qidl) }
+      | IDENT "Import"; qidl = LIST1 filtered_import -> { VernacImport (false,qidl) }
+      | IDENT "Export"; qidl = LIST1 filtered_import -> { VernacImport (true,qidl) }
       | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
           { VernacInclude(e::l) }
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
          { warn_deprecated_include_type ~loc ();
         VernacInclude(e::l) } ] ]
   ;
+  filtered_import:
+    [ [ m = global -> { (m, ImportAll) }
+      | m = global; "("; ns = LIST1 global SEP ","; ")" -> { (m, ImportNames ns) } ] ]
+  ;
   export_token:
     [ [ IDENT "Import" -> { Some false }
       | IDENT "Export" -> { Some true }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 054b60853f..be57fc37e7 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -86,7 +86,10 @@ open Pputils
 
   let pr_module = Libnames.pr_qualid
 
-  let pr_import_module = Libnames.pr_qualid
+  let pr_import_module (m,f) =
+    Libnames.pr_qualid m ++ match f with
+    | ImportAll -> mt()
+    | ImportNames ns -> surround (prlist_with_sep pr_comma Libnames.pr_qualid ns)
 
   let sep_end = function
     | VernacBullet _
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index de781109ef..cf7b43bde0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -872,12 +872,37 @@ let vernac_constraint ~poly l =
 (**********************)
 (* Modules            *)
 
+let interp_filter_in m = function
+  | ImportAll ->  Libobject.Unfiltered
+  | ImportNames ns ->
+    let module NSet = Globnames.ExtRefSet in
+    let dp_m = Nametab.dirpath_of_module m in
+    let ns =
+      List.fold_left (fun ns n ->
+          let full_n =
+            let dp_n,n = repr_qualid n in
+            make_path (append_dirpath dp_m dp_n) n
+          in
+          let n = try Nametab.extended_global_of_path full_n
+            with Not_found ->
+              CErrors.user_err
+                Pp.(str "Cannot find name " ++ pr_qualid n ++ spc() ++
+                    str "in module " ++ pr_qualid (Nametab.shortest_qualid_of_module m))
+          in
+          NSet.add n ns)
+        NSet.empty ns
+    in
+    Libobject.Names ns
+
 let vernac_import export refl =
-  let import_mod qid =
-    try Declaremods.import_module Libobject.Unfiltered ~export @@ Nametab.locate_module qid
-    with Not_found ->
-      CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
-   in
+  let import_mod (qid,f) =
+    let m = try Nametab.locate_module qid
+      with Not_found ->
+        CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
+    in
+    let f = interp_filter_in m f in
+    Declaremods.import_module f ~export m
+  in
   List.iter import_mod refl
 
 let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
@@ -893,7 +918,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   let mp = Declaremods.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in
   Dumpglob.dump_moddef ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
-  Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
+  Option.iter (fun export -> vernac_import export [qualid_of_ident id, ImportAll]) export
 
 let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
@@ -914,7 +939,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [qualid_of_ident id]) export
+             (fun export -> vernac_import export [qualid_of_ident id, ImportAll]) export
          ) argsexport
     | _::_ ->
        let binders_ast = List.map
@@ -929,14 +954,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
        Dumpglob.dump_moddef ?loc mp "mod";
        Flags.if_verbose Feedback.msg_info
          (str "Module " ++ Id.print id ++ str " is defined");
-       Option.iter (fun export -> vernac_import export [qualid_of_ident id])
+       Option.iter (fun export -> vernac_import export [qualid_of_ident id, ImportAll])
          export
 
 let vernac_end_module export {loc;v=id} =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
-  Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
+  Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id, ImportAll]) export
 
 let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
   if Global.sections_are_opened () then
@@ -957,7 +982,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
+             (fun export -> vernac_import export [qualid_of_ident ?loc id, ImportAll]) export
          ) argsexport
 
     | _ :: _ ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index d6e7a3947a..70ccfc139d 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -101,7 +101,13 @@ type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
+
 type export_flag    = bool (* true = Export;        false = Import         *)
+
+type import_filter_expr =
+  | ImportAll
+  | ImportNames of qualid list
+
 type onlyparsing_flag = { onlyparsing : bool }
  (* Some v = Parse only;  None = Print also.
     If v<>Current, it contains the name of the coq version
@@ -320,7 +326,7 @@ type nonrec vernac_expr =
   | VernacEndSegment of lident
   | VernacRequire of
       qualid option * export_flag option * qualid list
-  | VernacImport of export_flag * qualid list
+  | VernacImport of export_flag * (qualid * import_filter_expr) list
   | VernacCanonical of qualid or_by_notation
   | VernacCoercion of qualid or_by_notation *
       class_rawexpr * class_rawexpr