Enhance handling of parameters in typeclass constraints: permit to specify any typeclass parameter by name anywhere in a

typeclass constraint. This allows to share implementations easily and to
give any subset of the parameters in any order in the constraints,
whereas we are still restricted to a prefix of the typeclass parameters
context when using "positional" specifications.


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

1 files changed, 26 insertions, 11 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index c86a2428c..0a0e144bd 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -23,6 +23,7 @@ open Topconstr
 open Libnames
 open Typeclasses
 open Typeclasses_errors
+open Pp
 (*i*)
 
 let ids_of_list l = 
@@ -120,24 +121,38 @@ let ids_of_named_context_avoiding avoid l =
     ([], avoid) (Termops.ids_of_named_context l)
     
 let combine_params avoid fn applied needed =
+  let named, applied = 
+    List.partition 
+      (function
+	  (t, Some (loc, ExplByName id)) -> 
+	    if not (List.exists (fun (_, (id', _, _)) -> id = id') needed) then
+	      user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id);
+	    true
+	| _ -> false) applied
+  in
+  let named = List.map
+    (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
+    named
+  in
   let rec aux ids avoid app need =
     match app, need with
-	[], 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
+	[], [] -> List.rev ids, avoid
 
+      | app, (_, (id, _, _)) :: need when List.mem_assoc id named ->
+	  aux (List.assoc id named :: ids) avoid app need
+	    
+      | (x, None) :: app, (None, (id, _, _)) :: need ->
+	  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    
+      | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
+
+      | [], (None, _ as decl) :: need -> 
+	  let t', avoid' = fn avoid decl in
+	    aux (t' :: ids) avoid' app need
 
       | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
   in aux [] avoid applied needed