Cleaner quantifiers for type classes, breaks clrewrite for the moment but implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it.

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

2 files changed, 39 insertions, 13 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4799eb7b39..162591872b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -94,19 +94,36 @@ let ids_of_named_context_avoiding avoid l =
     let id' = next_ident_away_from id avoid in id' :: ids, Idset.add id' avoid) 
     ([], avoid) (Termops.ids_of_named_context l)
     
-let combine_params avoid applied needed =
+let combine_params avoid fn applied needed =
   let rec aux ids avoid app need =
     match app, need with
 	[], need -> 
-	  let need', avoid = ids_of_named_context_avoiding avoid (List.map snd need) in
-	    List.rev ids @ (List.rev_map mkIdentC need'), avoid
-      | _, (true, (id, _, _)) :: need -> 
-	  let id' = next_ident_away_from id avoid in
-	    aux (CRef (Ident (dummy_loc, id')) :: ids) (Idset.add id' avoid) app need
-      | x :: app, (false, _) :: need -> aux (x :: ids) avoid app need    
+	  let need', avoid = 
+	    List.fold_left (fun (terms, avoid) decl -> 
+	      let t', avoid = fn avoid decl in
+		(t' :: terms, avoid))
+	      ([], avoid) need
+	  in List.rev ids @ (List.rev need'), avoid
+
+      | (x, Some (loc, ExplByName id')) :: app, (Some _, (id, _, _)) :: need when id' = id -> 
+	  aux (x :: ids) avoid app need
+
+      | _, (Some cl, (id, _, _) as d) :: need -> 
+	  let t', avoid' = fn avoid d in
+	    aux (t' :: ids) avoid' app need
+
+      | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need    
+
       | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
   in aux [] avoid applied needed
 
+let combine_params_freevar avoid applied needed =
+  combine_params avoid
+    (fun avoid (_, (id, _, _)) -> 
+      let id' = next_ident_away_from id avoid in
+	(CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
+    applied needed
+
 let compute_context_vars env l =
   List.fold_left (fun avoid (iid, _, c) -> 
     (match snd iid with Name i -> [i] | Anonymous -> []) @ (free_vars_of_constr_expr c ~bound:env avoid))
@@ -117,6 +134,11 @@ let destClassApp cl =
     | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
     | _ -> raise Not_found
 
+let destClassAppExpl cl =
+  match cl with
+    | CApp (loc, (None,CRef (Ident f)), l) -> f, l
+    | _ -> raise Not_found
+
 let ids_of_list l = 
   List.fold_right Idset.add l Idset.empty
 
@@ -126,14 +148,10 @@ let full_class_binders env l =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
 	  Explicit -> 
-	    let (id, l) = destClassApp cl in
+	    let (id, l) = destClassAppExpl cl in
 	      (try
 		  let c = class_info (snd id) in
-		  let args, avoid = combine_params avoid l 
-		    (List.rev_map (fun x -> false, x) c.cl_context @ 
-			List.rev_map (fun x -> true, x) c.cl_super @ 
-			List.rev_map (fun x -> false, x) c.cl_params) 
-		  in
+		  let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
 		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
 		with Not_found -> unbound_class (Global.env ()) id)
 	| Implicit -> (x :: l', avoid))
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d687fe6400..3e26b6c72a 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -24,6 +24,7 @@ open Typeclasses
 (*i*)
 
 val destClassApp : constr_expr -> identifier located * constr_expr list
+val destClassAppExpl : constr_expr -> identifier located * (constr_expr * explicitation located option) list
 
 val free_vars_of_constr_expr :     Topconstr.constr_expr ->
     ?bound:Idset.t ->
@@ -49,6 +50,13 @@ val nf_named_context : evar_map -> named_context -> named_context
 val nf_rel_context : evar_map -> rel_context -> rel_context
 val nf_env : evar_map -> env -> env
 
+val combine_params : Names.Idset.t ->
+  (Names.Idset.t -> Names.identifier option * (Names.identifier * Term.constr option * Term.types) ->
+    Topconstr.constr_expr * Names.Idset.t) ->
+  (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
+  (Names.identifier option * Term.named_declaration) list ->
+  Topconstr.constr_expr list * Names.Idset.t
+
 
 val ids_of_named_context_avoiding :     Names.Idset.t ->
     Sign.named_context -> Names.Idset.elt list * Names.Idset.t