Generalized implementation of generalization.

- New constr_expr construct [CGeneralization of loc * binding_kind *
abstraction_kind option * constr_expr] to generalize the free vars of
the [constr_expr], binding these using [binding_kind] and making
a lambda or a pi (or deciding from the scope) using [abstraction_kind
option] (abstraction_kind = AbsLambda | AbsPi)
- Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{
... }" for implicit bindings (both "..(" and "_(" seem much more
difficult to implement). Subject to discussion! A few examples added
in a test-suite file.
- Also add missing syntax for implicit/explicit combinations for
_binders_: "{( )}" means implicit for the generalized (outer) vars,
explicit for the (inner) variable itself. Subject to discussion as well :)
- Factor much typeclass instance declaration code. We now just have to
force generalization of the term after the : in instance declarations.
One more step to using Instance for records.


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

1 files changed, 33 insertions, 20 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4daf219551..876af8f54b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -200,14 +200,12 @@ let combine_params avoid fn applied needed =
       | (x,_) :: _, [] -> 
 	  user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments")
   in aux [] avoid applied needed
-    
-let combine_params_freevar avoid applied needed =
-  combine_params avoid
-    (fun avoid (_, (na, _, _)) -> 
-      let id' = next_name_away_from na avoid in
-	(CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
-    applied needed
 
+let combine_params_freevar =
+  fun avoid (_, (na, _, _)) -> 
+    let id' = next_name_away_from na avoid in
+      (CRef (Ident (dummy_loc, id')), Idset.add id' avoid)
+	
 let destClassApp cl =
   match cl with
     | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
@@ -221,19 +219,34 @@ let destClassAppExpl cl =
     | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
 
-let full_class_binder env (loc, id, l) gr = 
-  let avoid = 
-    Idset.union env (ids_of_list 
-			(free_vars_of_constr_expr (CApp (loc, (None, mkRefC id), l)) ~bound:env []))
-  in
-  let c, avoid =
-    let c = class_info gr in
-    let (ci, rd) = c.cl_context in
-    let pars = List.rev (List.combine ci rd) in
-    let args, avoid = combine_params_freevar avoid l pars in
-      CAppExpl (loc, (None, id), args), avoid
-  in c
-
+let implicit_application env ?(allow_partial=true) f ty = 
+  let is_class =
+    try
+      let (loc, r, _ as clapp) = destClassAppExpl ty in
+      let (loc, qid) = qualid_of_reference r in
+      let gr = Nametab.locate qid in
+	if Typeclasses.is_class gr then Some (clapp, gr) else None
+    with Not_found -> None
+  in 
+    match is_class with
+    | None -> ty
+    | Some ((loc, id, par), gr) -> 
+	let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+	let c, avoid =
+	  let c = class_info gr in
+	  let (ci, rd) = c.cl_context in
+	  if not allow_partial then
+	    begin 
+	      let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
+	      let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 ci in
+		if needlen <> applen then 
+		  Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
+	    end;
+	  let pars = List.rev (List.combine ci rd) in
+	  let args, avoid = combine_params avoid f par pars in
+	    CAppExpl (loc, (None, id), args), avoid
+	in c
+	  
 let implicits_of_rawterm l = 
   let rec aux i c = 
     match c with