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

5 files changed, 52 insertions, 13 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 54abacaf6..6c09e4ace 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -696,11 +696,9 @@ let intern_typeclass_binders intern_type lvar env bl =
 	(env, (na,bk,None,ty)::bl))
     env bl
 
-let intern_typeclass_binder intern_type lvar (env,bl) na b ty =
-  let ctx = (na, b, ty) in
-  let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
-  let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in
-    intern_typeclass_binders intern_type lvar (env,ifvs) bind
+let intern_typeclass_binder intern_type lvar (env,bl) cb =
+  let (ids, fvs, bind) = Implicit_quantifiers.generalize_class_binder_raw (pi1 env) cb in
+    intern_typeclass_binders intern_type lvar (env,bl) (fvs@[bind])
     
 let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function
   | LocalRawAssum(nal,bk,ty) ->
@@ -713,8 +711,8 @@ let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = fu
 		(fun ((ids,ts,sc),bl) (_,na) ->
 		  ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
 		(env,bl) nal
-	| TypeClass b ->
-	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty)
+	| TypeClass (b,b') ->
+	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal, (b,b'), ty))
   | LocalRawDef((loc,na),def) ->
       ((name_fold Idset.add na ids,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
@@ -1029,9 +1027,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
     in
       match bk with
 	| Default b -> default env b nal
-	| TypeClass b -> 
+	| TypeClass (b,b') -> 
 	    let env, ibind = intern_typeclass_binder intern_type lvar
-	      (env, []) (List.hd nal) b ty in
+	      (env, []) (List.hd nal,(b,b'),ty) in
 	    let body = intern_type env body in
 	      it_mkRProd ibind body
 					   
@@ -1045,9 +1043,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
       | [] -> intern env body
     in match bk with
       | Default b -> default env b nal
-      | TypeClass b ->	  
+      | TypeClass (b, b') ->	  
 	  let env, ibind = intern_typeclass_binder intern_type lvar
-	    (env, []) (List.hd nal) b ty in
+	    (env, []) (List.hd nal,(b,b'),ty) in
 	  let body = intern env body in
 	    it_mkRLambda ibind body
 	      
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bef2573e5..d084a3f7d 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -193,6 +193,44 @@ let resolve_class_binders env l =
   in
     fv_ctx, ctx
 
+let full_class_binder env (iid, (bk, bk'), cl as c) = 
+  let avoid = Idset.union env (ids_of_list (compute_context_vars env [c])) in
+  let c, avoid =
+    match bk' with
+    | Implicit -> 
+	let (loc, id, l) = 
+	  try destClassAppExpl cl 
+	  with Not_found -> 
+	    user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
+	in
+	let gr = Nametab.global id in
+	  (try
+	      let c = class_info gr in
+	      let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
+		(iid, bk, CAppExpl (loc, (None, id), args)), avoid
+	    with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
+    | Explicit -> ((iid,bk,cl), avoid)
+  in c
+
+let compute_constraint_freevars env (oid, _, x) =
+  let bound = match snd oid with Name n -> Idset.add n env | Anonymous -> env in
+  let ids = free_vars_of_constr_expr x ~bound [] in
+    freevars_of_ids env (List.rev ids)
+
+let resolve_class_binder env c = 
+  let cstr = full_class_binder env c in
+  let fv_ctx = 
+    let elts = compute_constraint_freevars env cstr in
+      List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
+  in fv_ctx, cstr
+    
+let generalize_class_binder_raw env c = 
+  let env = Idset.union env (Termops.vars_of_env (Global.env())) in
+  let fv_ctx, cstr = resolve_class_binder env c in
+  let ids' = List.fold_left (fun acc ((loc, id), t) -> Idset.add id acc) env fv_ctx in
+  let ctx' = List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx in
+    ids', ctx', cstr
+
 let generalize_class_binders_raw env l = 
   let env = Idset.union env (Termops.vars_of_env (Global.env())) in
   let fv_ctx, cstrs = resolve_class_binders env l in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index bd061a1ed..ac1b8c99a 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -43,6 +43,9 @@ val resolve_class_binders : Idset.t -> typeclass_context ->
   (identifier located * constr_expr) list * typeclass_context
 
 val full_class_binders : Idset.t -> typeclass_context -> typeclass_context
+
+val generalize_class_binder_raw : Idset.t -> name located * (binding_kind * binding_kind) * constr_expr -> 
+  Idset.t * typeclass_context * typeclass_constraint
   
 val generalize_class_binders_raw : Idset.t -> typeclass_context -> 
   (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cef1b9391..570eae7e5 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -590,7 +590,7 @@ type notation = string
 
 type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
 
-type binder_kind = Default of binding_kind | TypeClass of binding_kind
+type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 6790e400f..46133c27b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -95,7 +95,7 @@ type notation = string
 
 type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
   
-type binder_kind = Default of binding_kind | TypeClass of binding_kind
+type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)