From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- interp/implicit_quantifiers.ml | 214 +++++++++++++++++++++-------------------- 1 file changed, 110 insertions(+), 104 deletions(-) (limited to 'interp/implicit_quantifiers.ml') 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 -- cgit v1.2.3