Do a second pass on the treatment of user-given implicit arguments. Now

works in inductive type definitions and fixpoints. The semantics of
an implicit inductive parameter is maybe a bit weird: it is implicit in the
inductive definition of constructors and the contructor types but not in
the inductive type itself (ie. to model the fact that one rarely wants A
in vector A n to be implicit but in vnil yes). Example in test-suite/
Also, correct the handling of the implicit arguments across sections. 
Every definition which had no explicitely given implicit arguments was
treated as if we asked to do global automatic implicit arguments on
section closing. Hence some arguments were given implicit status for no
apparent reason.
Also correct and test the parsing rule which disambiguates between {wf
..} and {A ..}.


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

4 files changed, 57 insertions, 41 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4af59ff62..3896f02dd 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -183,7 +183,7 @@ let declare_structure env id idbuild params arity fields =
       mind_entry_record = true;
       mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
-  let kn = Command.declare_mutual_with_eliminations true mie in
+  let kn = Command.declare_mutual_with_eliminations true mie [] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
   let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 327fe904e..b5c9cb59b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -139,8 +139,7 @@ let red_constant_entry bl ce = function
 let declare_global_definition ident ce local imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
   let gr = ConstRef kn in
-    if Impargs.is_implicit_args () || imps <> [] then
-      declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
     if local = Local && Flags.is_verbose() then
       msg_warning (pr_id ident ++ str" is declared as a global definition");
     definition_message ident;
@@ -192,8 +191,7 @@ let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) =
         let kn =
           declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
 	let gr = ConstRef kn in
-	  if Impargs.is_implicit_args () || imps <> [] then
-	    declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+	  maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
         assumption_message ident;
         if local=Local & Flags.is_verbose () then
           msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -459,18 +457,18 @@ let declare_eliminations sp =
 
 (* 3b| Mutual inductive definitions *)
 
-let compute_interning_datas env l nal typl =
-  let mk_interning_data na typ =
+let compute_interning_datas env l nal typl impll =
+  let mk_interning_data na typ impls =
     let idl, impl =
-      if is_implicit_args() then
-	let impl = compute_implicits env typ in
-	let sub_impl,_ = list_chop (List.length l) impl in
-	let sub_impl' = List.filter is_status_implicit sub_impl in
+      let impl = 
+	compute_implicits_with_manual env typ (is_implicit_args ()) impls
+      in 
+      let sub_impl,_ = list_chop (List.length l) impl in
+      let sub_impl' = List.filter is_status_implicit sub_impl in
 	(List.map name_of_implicit sub_impl', impl)
-      else 
-	([],[]) in
-    (na, (idl, impl, compute_arguments_scope typ)) in
-  (l, List.map2 mk_interning_data nal typl)
+    in
+      (na, (idl, impl, compute_arguments_scope typ)) in
+  (l, list_map3 mk_interning_data nal typl impll)
 
 let declare_interning_data (_,impls) (df,c,scope) =
   silently (Metasyntax.add_notation_interpretation df impls c) scope
@@ -521,13 +519,14 @@ let interp_cstrs evdref env impls mldata arity ind =
   (* Complete conclusions of constructor types if given in ML-style syntax *)
   let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
   (* Interpret the constructor types *)
-  let ctyps'' = List.map (interp_type_evars evdref env ~impls) ctyps' in
-  (cnames, ctyps'')
+  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
+    (cnames, ctyps'', cimpls)
 
 let interp_mutual paramsl indl notations finite = 
   check_all_names_different indl;
   let env0 = Global.env() in
   let evdref = ref (Evd.create_evar_defs Evd.empty) in
+  let userimpls = Implicit_quantifiers.implicits_of_binders paramsl in
   let env_params, ctx_params = interp_context_evars evdref env0 paramsl in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
@@ -542,7 +541,8 @@ let interp_mutual paramsl indl notations finite =
   let env_ar_params = push_rel_context ctx_params env_ar in
 
   (* Compute interpretation metadatas *)
-  let impls = compute_interning_datas env0 params indnames fullarities in
+  let indimpls = List.map (fun _ -> userimpls) fullarities in
+  let impls = compute_interning_datas env0 params indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
@@ -556,17 +556,17 @@ let interp_mutual paramsl indl notations finite =
   (* Instantiate evars and check all are resolved *)
   let evd,_ = consider_remaining_unif_problems env_params !evdref in
   let sigma = evars_of evd in
-  let constructors = List.map (fun (idl,cl) -> (idl,List.map (nf_evar sigma) cl)) constructors in
+  let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
   List.iter (check_evars env_params Evd.empty evd) arities;
   Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
-  List.iter (fun (_,ctyps) ->
+  List.iter (fun (_,ctyps,_) ->
     List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
     constructors;
   
   (* Build the inductive entries *)
-  let entries = list_map3 (fun ind arity (cnames,ctypes) -> {
+  let entries = list_map3 (fun ind arity (cnames,ctypes,cimpls) -> {
     mind_entry_typename = ind.ind_name;
     mind_entry_arity = arity;
     mind_entry_consnames = cnames;
@@ -577,7 +577,7 @@ let interp_mutual paramsl indl notations finite =
   { mind_entry_params = List.map prepare_param ctx_params;
     mind_entry_record = false; 
     mind_entry_finite = finite; 
-    mind_entry_inds = entries }
+    mind_entry_inds = entries }, (List.map (fun (_,_,impls) -> userimpls, impls) constructors)
 
 let eq_constr_expr c1 c2 =
   try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
@@ -630,21 +630,36 @@ let _ =
       optwrite = (fun b -> elim_flag := b) }
 
 
-let declare_mutual_with_eliminations isrecord mie =
+let lift_implicits n = 
+  List.map (fun x -> 
+    match fst x with 
+	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
+      | _ -> x)
+
+let declare_mutual_with_eliminations isrecord mie impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
-  let (_,kn) = declare_mind isrecord mie in
-  if_verbose ppnl (minductive_message names);
-  if !elim_flag then declare_eliminations kn;
-  kn
+  let params = List.length mie.mind_entry_params in
+  let (_,kn) = declare_mind isrecord mie in    
+    list_iter_i (fun i (indimpls, constrimpls) -> 
+      let ind = (kn,i) in
+	list_iter_i
+	  (fun j impls -> 
+	    maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
+	      (is_implicit_args()) (indimpls @ (lift_implicits params impls)))
+	  constrimpls)
+      impls;
+    if_verbose ppnl (minductive_message names);
+    if !elim_flag then declare_eliminations kn;
+    kn
 
 let build_mutual l finite =
   let indl,ntnl = List.split l in
   let paramsl = extract_params indl in
   let coes = extract_coercions indl in
   let notations,indl = prepare_inductive ntnl indl in
-  let mie = interp_mutual paramsl indl notations finite in
+  let mie,impls = interp_mutual paramsl indl notations finite in
   (* Declare the mutual inductive block with its eliminations *)
-  ignore (declare_mutual_with_eliminations false mie);
+  ignore (declare_mutual_with_eliminations false mie impls);
   (* Declare the possible notations of inductive types *)
   List.iter (declare_interning_data ([],[])) notations;
   (* Declare the coercions *)
@@ -785,11 +800,9 @@ let declare_fix boxed kind f def t imps =
   } in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
   let gr = ConstRef kn in
-    if Impargs.is_implicit_args () || imps <> [] then
-      declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
     gr
-
-
+      
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
   let names = List.map (fun id -> Name id) fixnames in
@@ -828,7 +841,7 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
-  let impls = compute_interning_datas env [] fixnames fixtypes in
+  let impls = compute_interning_datas env [] fixnames fixtypes fiximps in
   let notations = List.fold_right Option.List.cons ntnl [] in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
@@ -1043,8 +1056,7 @@ let start_proof_com sopt kind (bl,t) hook =
   let j = Default.understand_judgment sigma env ib in
     start_proof id kind j.uj_val
       (fun str cst -> 
-	if Impargs.is_implicit_args () || imps <> [] then
-	  declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
+	maybe_declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
 	hook str cst)
 
 let check_anonymity id save_ident =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d67daa83a..a6a403c03 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -57,16 +57,20 @@ val compute_interning_datas :  Environ.env ->
     'a list ->
     'b list ->
     Term.types list ->
-    'a list *
+    Impargs.manual_explicitation list list ->
+  'a list *
     ('b *
-     (Names.identifier list * Impargs.implicits_list *
-      Topconstr.scope_name option list))
+	(Names.identifier list * Impargs.implicits_list *
+	    Topconstr.scope_name option list))
     list
 
 val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
 
 val declare_mutual_with_eliminations :
-  bool -> Entries.mutual_inductive_entry -> mutual_inductive
+  bool -> Entries.mutual_inductive_entry -> 
+  (Impargs.manual_explicitation list *
+      Impargs.manual_explicitation list list) list ->
+  mutual_inductive
 
 type fixpoint_kind =
   | IsFixpoint of (int option * recursion_order_expr) list
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b04557304..57a7e63b3 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -223,7 +223,7 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
       mind_entry_record = true;
       mind_entry_finite = not declare_as_coind;
       mind_entry_inds = [mie_ind] } in
-  let kn = declare_mutual_with_eliminations true mie in
+  let kn = declare_mutual_with_eliminations true mie [] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let kinds,sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)