Fixes in handling of implicit arguments:

- Now [ id : Class foo ] makes id an explicit argument, 
  and [ Class foo ] is equivalent to [ {someid} : Class foo ].
  This makes declarations such as "Class Ord [ eq : Eq a ]" have
  sensible implicit args.
- Better handling of {} in class and record declarations, refactorize 
  code for declaring structures and classes.  
- Fix merging of implicit arguments information on section closing.


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

6 files changed, 119 insertions, 120 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d07051b718..5599f4d665 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -110,40 +110,15 @@ let interp_fields_evars isevars env avoid l =
 
 open Topconstr
 
-let declare_implicit_proj c proj imps sub =
-  let len = List.length c.cl_context in
-  let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) (snd proj)) in
-  let expls =
-    let rec aux i expls = function
-	[] -> expls
-      | (Name n, _) :: tl -> 
-	  let impl = ExplByPos (i, Some n), (true, true) in
-	    aux (succ i) (impl :: List.remove_assoc (ExplByName n) expls) tl
-      | (Anonymous,_) :: _ -> assert(false)
-    in
-      aux 1 [] (List.rev ctx)
-  in 
-  let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in
-    if sub then 
-      declare_instance_cst true (snd proj);
-    Impargs.declare_manual_implicits false (ConstRef (snd proj)) true expls
-      
-let declare_implicits impls subs cl =
-  Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub)
-    cl.cl_projs impls subs;
-  let len = List.length cl.cl_context in
-  let indimps = 
-    list_fold_left_i 
-      (fun i acc (is, (na, b, t)) -> 
-	if len - i <= cl.cl_params then acc
-	else 
-	  match is with
-	      None | Some (_, false) -> (ExplByPos (i, Some (Nameops.out_name na)), (false, true)) :: acc
-	    | _ -> acc)
-      1 [] (List.rev cl.cl_context)
-  in
-    Impargs.declare_manual_implicits false cl.cl_impl false indimps
-      
+let implicits_of_context ctx =
+  list_map_i (fun i name ->
+    let explname = 
+      match name with 
+      | Name n -> Some n
+      | Anonymous -> None
+    in ExplByPos (i, explname), (true, true))
+    1 (List.rev (Anonymous :: (List.map pi1 ctx)))
+
 let degenerate_decl (na,b,t) =
   let id = match na with
     | Name id -> id
@@ -152,29 +127,6 @@ let degenerate_decl (na,b,t) =
     | None -> (id, Entries.LocalAssum t)
     | Some b -> (id, Entries.LocalDef b)
 
-let declare_structure env id idbuild params arity fields =
-  let nparams = List.length params and nfields = List.length fields in
-  let args = extended_rel_list nfields params in
-  let ind = applist (mkRel (1+nparams+nfields), args) in
-  let type_constructor = it_mkProd_or_LetIn ind fields in
-  let mie_ind =
-    { mind_entry_typename = id;
-      mind_entry_arity = arity;
-      mind_entry_consnames = [idbuild];
-      mind_entry_lc = [type_constructor] } in
-  let mie =
-    { mind_entry_params = List.map degenerate_decl params;
-      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 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 ~kind:Method ~name:id (List.map (fun _ -> false) fields) fields in
-  let _build = ConstructRef (rsp,1) in
-    Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
-    rsp
-
 let name_typeclass_binder avoid = function
   | LocalRawAssum ([loc, Anonymous], bk, c) ->
       let name = 
@@ -235,6 +187,12 @@ let new_class id par ar sup props =
   let ctx_props = Evarutil.nf_rel_context_evar sigma ctx_props in
   let arity = Reductionops.nf_evar sigma arity in
   let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
+  let fieldimpls = 
+    (* Make the class and all params implicits in the projections *)
+    let ctx_impls = implicits_of_context ctx_params in
+    let len = succ (List.length ctx_params) in
+      List.rev_map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls
+  in
   let impl, projs = 
     let params = ctx_params and fields = ctx_props in
       List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
@@ -267,12 +225,18 @@ let new_class id par ar sup props =
 	    let proj_cst = Declare.declare_constant proj_name
 	      (DefinitionEntry proj_entry, IsDefinition Definition) 
 	    in
-	      ConstRef cst, [proj_name, proj_cst]
+	    let cref = ConstRef cst in
+	      Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps;
+	      Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls);
+	      cref, [proj_name, proj_cst]
 	| _ ->
 	    let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
-	    let kn = declare_structure env0 (snd id) idb params arity fields in
-	      IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
-			     fields (Recordops.lookup_projections kn))
+	    let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
+	    let kn = Record.declare_structure (snd id) idb arity_imps
+	      params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
+	    in
+	      IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
+			     fields (Recordops.lookup_projections (kn,0)))
   in
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
@@ -283,12 +247,12 @@ let new_class id par ar sup props =
   in
   let k =
     { cl_impl = impl;
-      cl_params = List.length par;
       cl_context = ctx_context;
       cl_props = ctx_props;
       cl_projs = projs }
   in
-    declare_implicits (List.rev prop_impls) subs k;
+    List.iter2 (fun p sub -> if sub then declare_instance_cst true (snd p))
+      k.cl_projs subs;
     add_class k
     
 type binder_def_list = (identifier located * identifier located list * constr_expr) list
@@ -489,12 +453,17 @@ let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let avoid = Termops.ids_of_context env in
-  let ctx, l = Implicit_quantifiers.resolve_class_binders (vars_of_env env) l in
-  let env', avoid, ctx = interp_binders_evars isevars env avoid ctx in
-  let env', avoid, l = interp_typeclass_context_evars isevars env' avoid l in
+  let ctx, l = 
+    List.fold_left 
+      (fun (ids, acc) x ->
+	let ids, ctx, cstr = Implicit_quantifiers.generalize_class_binder_raw ids x in
+	  (ids, (cstr :: ctx) @ acc))
+      (vars_of_env env, []) l
+  in
+  let env', avoid, l = interp_typeclass_context_evars isevars env avoid (List.rev l) in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
-  let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in
+  let fullctx = Evarutil.nf_named_context_evar sigma l in
     List.iter (function (id,_,t) -> 
       if Lib.is_modtype () then 
 	let cst = Declare.declare_internal_constant id
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 3bc5d03266..c10ee4c97d 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -38,8 +38,8 @@ val name_typeclass_binders : Idset.t ->
     Topconstr.local_binder list ->
     Topconstr.local_binder list * Idset.t
 
-val declare_implicit_proj : typeclass -> (identifier * constant) -> 
-  Impargs.manual_explicitation list -> bool -> unit
+(* val declare_implicit_proj : typeclass -> (identifier * constant) ->  *)
+(*   Impargs.manual_explicitation list -> bool -> unit *)
 
 val new_class : identifier located ->
   local_binder list ->
@@ -85,7 +85,9 @@ val id_of_class : typeclass -> identifier
 
 (* Context command *)    
 
-val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit
+val context : ?hook:(Libnames.global_reference -> unit) -> 
+  (Names.name Util.located * (Rawterm.binding_kind * Rawterm.binding_kind) *
+  Topconstr.constr_expr) list -> unit
 
 (* Forward ref for refine *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index df133e7693..14e64ead46 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -613,13 +613,6 @@ let _ =
       optread  = (fun () -> !elim_flag) ;
       optwrite = (fun b -> elim_flag := b) }
 
-
-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 params = List.length mie.mind_entry_params in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 83332e8233..ab06673e43 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -31,29 +31,41 @@ open Topconstr
 
 (********** definition d'un record (structure) **************)
 
-let interp_decl sigma env = function
-  | Vernacexpr.AssumExpr((_,id),t) -> (id,None,interp_type Evd.empty env t)
-  | Vernacexpr.DefExpr((_,id),c,t) ->
-      let c = match t with
-	| None -> c
-	| Some t -> mkCastC (c, Rawterm.CastConv (DEFAULTcast,t))
-      in
-      let j = interp_constr_judgment Evd.empty env c in
-      (id,Some j.uj_val, refresh_universes j.uj_type)
+let interp_evars evdref env ?(impls=([],[])) k typ =
+  let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
+  let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
+    imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
+
+let mk_interning_data env na impls typ =
+  let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
+  in (out_name na, ([], impl, Notation.compute_arguments_scope typ))
+    
+let interp_fields_evars isevars env l =
+  List.fold_left
+    (fun (env, uimpls, params, impls) ((loc, i), b, t) ->
+      let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in
+      let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in
+      let data = mk_interning_data env i impl t' in
+      let d = (i,b',t') in
+	(push_rel d env, impl :: uimpls, d::params, ([], data :: snd impls)))
+    (env, [], [], ([], [])) l    
+
+let binder_of_decl = function
+  | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
+  | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None))
+
+let binders_of_decls = List.map binder_of_decl
 
 let typecheck_params_and_fields id t ps fs =
   let env0 = Global.env () in
-  let (env1,newps), _ = interp_context Evd.empty env0 ps in
+  let (env1,newps), imps = interp_context Evd.empty env0 ps in
   let fullarity = it_mkProd_or_LetIn t newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
-  let env2,newfs =
-    List.fold_left
-      (fun (env,newfs) d ->
-         let decl = interp_decl Evd.empty env d in
-         (push_rel decl env, decl::newfs))
-      (env_ar,[]) fs
+  let evars = ref (Evd.create_evar_defs Evd.empty) in
+  let env2,impls,newfs,data =
+    interp_fields_evars evars env_ar (binders_of_decls fs)
   in
-  newps, newfs
+    imps, newps, impls, newfs
 
 let degenerate_decl (na,b,t) =
   let id = match na with
@@ -131,7 +143,7 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
   substl_rel_context (subst@[mkInd indsp]) fields
 
 (* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
+let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let paramdecls = mib.mind_params_ctxt in
@@ -142,8 +154,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
   let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
   let lifted_fields = lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
-    List.fold_left2
-      (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) ->
+    list_fold_left3
+      (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
 	let (sp_projs,subst) =
 	  match fi with
 	  | Anonymous ->
@@ -180,6 +192,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
 	      let refi = ConstRef kn in
 	      let constr_fi = mkConst kn in
+	      Impargs.maybe_declare_manual_implicits 
+		false refi (Impargs.is_implicit_args()) impls;
 	      if coe then begin
 	        let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi Global cl
@@ -191,28 +205,18 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,NoProjection fi::subst) in
       (nfi-1,(optci=None)::kinds,sp_projs,subst))
-      (List.length fields,[],[],[]) coers (List.rev fields)
+      (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
-(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
-   list telling if the corresponding fields must me declared as coercion *)
-let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
-  let coers,fs = List.split cfs in
-  let extract_name acc = function
-      Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
-    | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
-    | _ -> acc in
-  let allnames =  idstruc::(List.fold_left extract_name [] fs) in
-  if not (list_distinct allnames) then error "Two objects have the same name";
-  (* Now, younger decl in params and fields is on top *)
-  let params,fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
+let declare_structure id idbuild paramimpls params arity fieldimpls fields
+    ?(kind=StructureComponent) ?name is_coe coers =
   let nparams = List.length params and nfields = List.length fields in
   let args = extended_rel_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let mie_ind =
-    { mind_entry_typename = idstruc;
-      mind_entry_arity = mkSort s;
+    { mind_entry_typename = id;
+      mind_entry_arity = arity;
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] } in
   let declare_as_coind =
@@ -223,10 +227,27 @@ 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 = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] 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 *)
-  if is_coe then Class.try_add_new_coercion build Global;
-  Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
-  kn
+  let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
+  let build = ConstructRef (rsp,1) in
+    if is_coe then Class.try_add_new_coercion build Global;
+    Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
+    kn
+
+(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
+   list telling if the corresponding fields must me declared as coercion *)
+let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
+  let coers,fs = List.split cfs in
+  let extract_name acc = function
+      Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
+    | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
+    | _ -> acc in
+  let allnames =  idstruc::(List.fold_left extract_name [] fs) in
+  if not (list_distinct allnames) then error "Two objects have the same name";
+  (* Now, younger decl in params and fields is on top *)
+  let implpars, params, implfs, fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
+  let implfs = List.map 
+    (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
+    declare_structure idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers
+  
diff --git a/toplevel/record.mli b/toplevel/record.mli
index c2c6b72ee7..7799162dfd 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -14,6 +14,7 @@ open Term
 open Sign
 open Vernacexpr
 open Topconstr
+open Impargs
 (*i*)
 
 (* [declare_projections ref name coers params fields] declare projections of
@@ -21,7 +22,18 @@ open Topconstr
    as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
+  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+  bool list -> manual_explicitation list list -> rel_context -> 
+  bool list * constant option list
+
+val declare_structure : identifier -> identifier -> 
+  manual_explicitation list -> rel_context -> (* params *)
+  Term.constr -> (* arity *)
+  Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *)
+  ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+  bool -> (* coercion? *)
+  bool list -> (* field coercions *)
+  mutual_inductive
 
 val definition_structure :
   lident with_coercion * local_binder list *
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8f54e699eb..2c646f6bc2 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -239,7 +239,9 @@ type vernac_expr =
 	(lident * lident list * constr_expr) list * (* props *)
 	int option (* Priority *)
 
-  | VernacContext of typeclass_context
+  | VernacContext of 
+      (Names.name Util.located * (Rawterm.binding_kind * Rawterm.binding_kind) *
+	  Topconstr.constr_expr) list
 	
   | VernacDeclareInstance of
       lident (* instance name *)