Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 110 insertions, 104 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a83071d1..d6e207f3 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: implicit_quantifiers.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: implicit_quantifiers.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -58,7 +58,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
   in
   let rec aux bdvars l c = match c with
     | CRef (Ident (_,id)) -> found id bdvars l
-    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) ->
 	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
     | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
   in aux bound l c
@@ -81,17 +81,84 @@ let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
     | [] -> bdvars, l
   in aux bound l binders
 
+let add_name_to_ids set na = 
+  match na with 
+  | Anonymous -> set 
+  | Name id -> Idset.add id set 
+	
+let free_vars_of_rawconstr ?(bound=Idset.empty) =
+  let rec vars bound vs = function
+    | RVar (loc,id) -> 
+	if is_freevar bound (Global.env ()) id then
+	  if List.mem_assoc id vs then vs 
+	  else (id, loc) :: vs
+	else vs
+    | RApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
+    | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> 
+	let vs' = vars bound vs ty in 
+	let bound' = add_name_to_ids bound na in 
+	vars bound' vs' c
+    | RCases (loc,sty,rtntypopt,tml,pl) ->
+	let vs1 = vars_option bound vs rtntypopt in 
+	let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in 
+	List.fold_left (vars_pattern bound) vs2 pl
+    | RLetTuple (loc,nal,rtntyp,b,c) ->
+	let vs1 = vars_return_type bound vs rtntyp in 
+	let vs2 = vars bound vs1 b in 
+	let bound' = List.fold_left add_name_to_ids bound nal in
+	vars bound' vs2 c
+    | RIf (loc,c,rtntyp,b1,b2) -> 
+	let vs1 = vars_return_type bound vs rtntyp in 
+	let vs2 = vars bound vs1 c in 
+	let vs3 = vars bound vs2 b1 in 
+	vars bound vs3 b2
+    | RRec (loc,fk,idl,bl,tyl,bv) ->
+	let bound' = Array.fold_right Idset.add idl bound in 
+	let vars_fix i vs fid = 
+	  let vs1,bound1 = 
+	    List.fold_left 
+	      (fun (vs,bound) (na,k,bbd,bty) -> 
+		 let vs' = vars_option bound vs bbd in 
+		 let vs'' = vars bound vs' bty in
+		 let bound' = add_name_to_ids bound na in 
+		 (vs'',bound')
+	      )
+	      (vs,bound')
+	      bl.(i)
+	  in
+	  let vs2 = vars bound1 vs1 tyl.(i) in 
+	  vars bound1 vs2 bv.(i)
+	in
+	array_fold_left_i vars_fix vs idl
+    | RCast (loc,c,k) -> let v = vars bound vs c in 
+	(match k with CastConv (_,t) -> vars bound v t | _ -> v)
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
+
+  and vars_pattern bound vs (loc,idl,p,c) = 
+    let bound' = List.fold_right Idset.add idl bound  in 
+    vars bound' vs c
+
+  and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
+
+  and vars_return_type bound vs (na,tyopt) = 
+    let bound' = add_name_to_ids bound na in 
+    vars_option bound' vs tyopt
+  in 
+  fun rt -> List.rev (vars bound [] rt)
+      
 let rec make_fresh ids env x =
   if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
 
 let freevars_of_ids env ids = 
   List.filter (is_freevar env (Global.env())) ids
-
-let binder_list_of_ids ids =
-  List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids
       
 let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-    
+
+let next_name_away_from na avoid = 
+  match na with
+  | Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon")
+  | Name id -> make_fresh avoid (Global.env ()) id
+
 let combine_params avoid fn applied needed =
   let named, applied = 
     List.partition 
@@ -116,7 +183,7 @@ let combine_params avoid fn applied needed =
       | (x, None) :: app, (None, (Name id, _, _)) :: need ->
 	  aux (x :: ids) avoid app need
 	    
-      | _, (Some cl, (Name id, _, _) as d) :: need -> 
+      | _, (Some cl, (_, _, _) as d) :: need -> 
 	  let t', avoid' = fn avoid d in
 	    aux (t' :: ids) avoid' app need
 
@@ -126,26 +193,19 @@ let combine_params avoid fn applied needed =
 	  let t', avoid' = fn avoid decl in
 	    aux (t' :: ids) avoid' app need
 
-      | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
-
-      | _, _ -> raise (Invalid_argument "combine_params")
+      | (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 (_, (id, _, _)) -> 
-      let id' = next_ident_away_from (Nameops.out_name 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))
-    [] l
-
+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
+    | CAppExpl (loc, (None, ref), l) -> loc, ref, l
     | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
       
@@ -155,88 +215,34 @@ let destClassAppExpl cl =
     | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
 
-let full_class_binders env l = 
-  let avoid = Idset.union env (ids_of_list (compute_context_vars env l)) in
-  let l', avoid =
-    List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
-      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)) :: l', avoid
-		with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
-	| Explicit -> (x :: l', avoid))
-      ([], avoid) l
-  in List.rev l'
-
-let compute_context_freevars env ctx =
-  let bound, ids = 
-    List.fold_left 
-      (fun (bound, acc) (oid, id, x) -> 
-	let bound = match snd oid with Name n -> Idset.add n bound | Anonymous -> bound in
-	  bound, free_vars_of_constr_expr x ~bound acc)
-      (env,[]) ctx
-  in freevars_of_ids env (List.rev ids)
-
-let resolve_class_binders env l = 
-  let ctx = full_class_binders env l in
-  let fv_ctx = 
-    let elts = compute_context_freevars env ctx in
-      List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
-  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
-    List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx,
-  List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs
-	
+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