Modules and ppvernac, sequel of Enrico's commit 16261

 After some investigation, I see no reason to try to hack
 the nametab in ppvernac, since everything happens there
 at a lower level (constr_expr). So the offending code that
 Enrico protected with a State.with_state_protection is now gone.

 By the way, moved some types from Declaremods to Vernacexpr
 to avoid some dependencies

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

interp/topconstr.mli

@@ -7,12 +7,8 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Libnames
-open Glob_term
-open Term
-open Mod_subst
 open Misctypes
 open Decl_kinds
 open Constrexpr
@@ -22,7 +18,7 @@ open Notation_term
 
 val oldfashion_patterns : bool ref
 
-(** Utilities on constr_expr                                           *)
+(** Utilities on constr_expr *)
 
 val replace_vars_constr_expr :
   (Id.t * Id.t) list -> constr_expr -> constr_expr

intf/vernacexpr.mli

@@ -12,7 +12,6 @@ open Names
 open Tacexpr
 open Misctypes
 open Constrexpr
-open Notation_term
 open Decl_kinds
 open Libnames
 
@@ -26,6 +25,7 @@ type lreference = reference
 type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
 
 type goal_identifier = string
+type scope_name = string
 
 type goal_reference =
   | OpenSubgoals
@@ -179,9 +179,6 @@ type inductive_expr =
 type one_inductive_expr =
   lident * local_binder list * constr_expr option * constructor_expr list
 
-type module_ast_inl = module_ast Declaremods.annotated
-type module_binder = bool option * lident list * module_ast_inl
-
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
   | TacNonTerm of Loc.t * string * (Names.Id.t * string) option
@@ -203,13 +200,45 @@ type scheme =
   | CaseScheme of bool * reference or_by_notation * sort_expr
   | EqualityScheme of reference or_by_notation
 
-type inline = int option (* inlining level, none for no inlining *)
-
 type bullet =
     | Dash
     | Star
     | Plus
 
+(** {6 Types concerning the module layer} *)
+
+(** Rigid / flexible module signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Which module inline annotations should we honor,
+    either None or the ones whose level is less or equal
+    to the given integer *)
+
+type inline =
+  | NoInline
+  | DefaultInline
+  | InlineAt of int
+
+(** Should we adapt a few scopes during functor application ? *)
+
+type scope_subst = (string * string) list
+
+(** The type of annotations for functor applications *)
+
+type funct_app_annot =
+  { ann_inline : inline;
+    ann_scope_subst : scope_subst }
+
+type 'a annotated = ('a * funct_app_annot)
+
+type module_ast_inl = module_ast annotated
+type module_binder = bool option * lident list * module_ast_inl
+
+(** {6 The type of vernacular expressions} *)
+
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
@@ -277,7 +306,7 @@ type vernac_expr =
   | VernacDeclareModule of bool option * lident *
       module_binder list * module_ast_inl
   | VernacDefineModule of bool option * lident * module_binder list *
-      module_ast_inl Declaremods.module_signature * module_ast_inl list
+      module_ast_inl module_signature * module_ast_inl list
   | VernacDeclareModuleType of lident *
       module_binder list * module_ast_inl list * module_ast_inl list
   | VernacInclude of module_ast_inl list

library/declaremods.ml

@@ -16,16 +16,7 @@ open Libnames
 open Libobject
 open Lib
 open Mod_subst
-
-(** Rigid / flexible signature *)
-
-type 'a module_signature =
-  | Enforce of 'a (** ... : T *)
-  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
-
-(** Should we adapt a few scopes during functor application ? *)
-
-type scope_subst = (string * string) list
+open Vernacexpr
 
 let scope_subst = ref (String.Map.empty : string String.Map.t)
 
@@ -41,30 +32,15 @@ let subst_scope sc =
 let reset_scope_subst () =
   scope_subst := String.Map.empty
 
-(** Which inline annotations should we honor, either None or the ones
-    whose level is less or equal to the given integer *)
-
-type inline =
-  | NoInline
-  | DefaultInline
-  | InlineAt of int
-
 let default_inline () = Some (Flags.get_inline_level ())
 
 let inl2intopt = function
   | NoInline -> None
   | InlineAt i -> Some i
   | DefaultInline -> default_inline ()
 
-type funct_app_annot =
-  { ann_inline : inline;
-    ann_scope_subst : scope_subst }
-
 let inline_annot a = inl2intopt a.ann_inline
 
-type 'a annotated = ('a * funct_app_annot)
-
-
 (* modules and components *)
 
 (* OBSOLETE This type is a functional closure of substitutive lib_objects.

library/declaremods.mli

@@ -14,38 +14,13 @@ open Environ
 open Libnames
 open Libobject
 open Lib
+open Vernacexpr
 
 (** This modules provides official functions to declare modules and
   module types *)
 
-(** Rigid / flexible signature *)
-
-type 'a module_signature =
-  | Enforce of 'a (** ... : T *)
-  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
-
-(** Should we adapt a few scopes during functor application ? *)
-
-type scope_subst = (string * string) list
-
 val subst_scope : string -> string
 
-(** Which inline annotations should we honor, either None or the ones
-   whose level is less or equal to the given integer *)
-
-type inline =
-  | NoInline
-  | DefaultInline
-  | InlineAt of int
-
-(** The type of annotations for functor applications *)
-
-type funct_app_annot =
-  { ann_inline : inline;
-    ann_scope_subst : scope_subst }
-
-type 'a annotated = ('a * funct_app_annot)
-
 (** {6 Modules } *)
 
 (** [declare_module interp_modtype interp_modexpr id fargs typ expr]

parsing/g_vernac.ml4

@@ -222,9 +222,9 @@ GEXTEND Gram
       | IDENT "Parameters" -> (use_locality_exp (), Definitional) ] ]
   ;
   inline:
-    [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i)
-      | IDENT "Inline" -> Some (Flags.get_inline_level())
-      | -> None] ]
+    [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
+      | IDENT "Inline" -> DefaultInline
+      | -> NoInline] ]
   ;
   finite_token:
     [ [ "Inductive" -> (Inductive_kw,Finite)

printing/ppconstr.ml

@@ -17,7 +17,6 @@ open Pputils
 open Ppextend
 open Constrexpr
 open Constrexpr_ops
-open Topconstr
 open Decl_kinds
 open Misctypes
 open Locus
@@ -309,7 +308,8 @@ let split_lambda = function
 
 let rename na na' t c =
   match (na,na') with
-    | (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c)
+    | (_,Name id), (_,Name id') ->
+      (na',t,Topconstr.replace_vars_constr_expr [id,id'] c)
     | (_,Name id), (_,Anonymous) -> (na,t,c)
     | _ -> (na',t,c)
 

printing/ppvernac.ml

@@ -21,7 +21,6 @@ open Libnames
 open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
-open Declaremods
 
 let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 
@@ -256,26 +255,12 @@ let pr_require_token = function
 
 let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
   let m = pr_module_ast pr_c mty in
-  (* Update the Nametab for interpreting the body of module/modtype *)
-  States.with_state_protection (fun () ->
-    let lib_dir = Lib.library_dp() in
-    List.iter (fun (_,id) ->
-      Declaremods.process_module_bindings [id]
-        [MBId.make lib_dir id,
-         (Modintern.interp_modtype (Global.env()) mty, inl)]) idl;
-    (* Builds the stream *)
-    spc() ++
-    hov 1 (str"(" ++ pr_require_token export ++
-     prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")) ()
+  spc() ++
+  hov 1 (str"(" ++ pr_require_token export ++
+  prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
 
 let pr_module_binders l pr_c =
-  (* Effet de bord complexe pour garantir la declaration des noms des
-  modules parametres dans la Nametab des l'appel de pr_module_binders
-  malgre l'aspect paresseux des streams *)
-  let ml = List.map (pr_module_vardecls pr_c) l in
-  prlist (fun id -> id) ml
-
-let pr_module_binders_list l pr_c = pr_module_binders l pr_c
+  prlist_strict (pr_module_vardecls pr_c) l
 
 let pr_type_option pr_c = function
   | CHole (loc, k) -> mt()
@@ -740,9 +725,9 @@ let rec pr_vernac = function
 	Anonymous -> mt ()) ++
        pr_and_type_binders_arg sup ++
        str":" ++ spc () ++
-       pr_constr_expr cl ++ spc () ++
+       pr_constr cl ++ spc () ++
 	 (match props with
-	  | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr_expr p
+	  | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr p
 	  | None -> mt()))
 
  | VernacContext l ->
@@ -760,20 +745,20 @@ let rec pr_vernac = function
 
   (* Modules and Module Types *)
   | VernacDefineModule (export,m,bl,tys,bd) ->
-      let b = pr_module_binders_list bl pr_lconstr in
+      let b = pr_module_binders bl pr_lconstr in
       hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
                pr_lident m ++ b ++
                pr_of_module_type pr_lconstr tys ++
 	       (if List.is_empty bd then mt () else str ":= ") ++
 	       prlist_with_sep (fun () -> str " <+ ")
 	        (pr_module_ast_inl pr_lconstr) bd)
   | VernacDeclareModule (export,id,bl,m1) ->
-      let b = pr_module_binders_list bl pr_lconstr in
+      let b = pr_module_binders bl pr_lconstr in
 	hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
              pr_lident id ++ b ++
              pr_module_ast_inl pr_lconstr m1)
   | VernacDeclareModuleType (id,bl,tyl,m) ->
-      let b = pr_module_binders_list bl pr_lconstr in
+      let b = pr_module_binders bl pr_lconstr in
       let pr_mt = pr_module_ast_inl pr_lconstr in
 	hov 2 (str"Module Type " ++ pr_lident id ++ b ++
 		 prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++

toplevel/classes.ml

@@ -343,6 +343,9 @@ let context l =
       in
       let impl = List.exists test impls in
       let decl = (Discharge, Definitional) in
-      let nstatus = Command.declare_assumption false decl t [] impl None (Loc.ghost, id) in
+      let nstatus =
+        Command.declare_assumption false decl t [] impl
+          Vernacexpr.NoInline (Loc.ghost, id)
+      in
       status && nstatus
   in List.fold_left fn true (List.rev ctx)

toplevel/command.ml

@@ -34,6 +34,7 @@ open Evarutil
 open Evarconv
 open Indschemes
 open Misctypes
+open Vernacexpr
 
 let rec under_binders env f n c =
   if Int.equal n 0 then f env Evd.empty c else
@@ -188,7 +189,12 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match loca
   true
 | Global | Local | Discharge ->
   let local = get_locality ident local in
-  let decl = (ParameterEntry (None,c,nl), IsAssumption kind) in
+  let inl = match nl with
+    | NoInline -> None
+    | DefaultInline -> Some (Flags.get_inline_level())
+    | InlineAt i -> Some i
+  in
+  let decl = (ParameterEntry (None,c,inl), IsAssumption kind) in
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
@@ -386,8 +392,6 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
   declare_default_schemes mind;
   mind
 
-open Vernacexpr
-
 type one_inductive_impls =
   Impargs.manual_explicitation list (* for inds *)*
   Impargs.manual_explicitation list list (* for constrs *)

toplevel/command.mli

@@ -51,11 +51,11 @@ val interp_assumption :
     nor in a module type and meant to be instantiated. *)
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   Impargs.manual_implicits ->
-  bool (** implicit *) -> Entries.inline -> variable Loc.located -> bool
+  bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> bool
 
 val declare_assumptions : variable Loc.located list ->
   coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits ->
-  bool -> Entries.inline -> bool
+  bool -> Vernacexpr.inline -> bool
 
 (** {6 Inductive and coinductive types} *)