diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /interp/implicit_quantifiers.ml | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/implicit_quantifiers.ml')
-rw-r--r-- | interp/implicit_quantifiers.ml | 136 |
1 files changed, 68 insertions, 68 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a550111a3..7b1a1ff4c 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -26,7 +26,7 @@ open Typeclasses_errors open Pp (*i*) -let ids_of_list l = +let ids_of_list l = List.fold_right Idset.add l Idset.empty let locate_reference qid = @@ -35,9 +35,9 @@ let locate_reference qid = | SynDef kn -> true let is_global id = - try + try locate_reference (qualid_of_ident id) - with Not_found -> + with Not_found -> false let is_freevar ids env x = @@ -48,13 +48,13 @@ let is_freevar ids env x = with _ -> not (is_global x) with _ -> true -(* Auxilliary functions for the inference of implicitly quantified variables. *) +(* Auxilliary functions for the inference of implicitly quantified variables. *) -let free_vars_of_constr_expr c ?(bound=Idset.empty) l = - let found id bdvars l = - if List.mem id l then l +let free_vars_of_constr_expr c ?(bound=Idset.empty) l = + let found id bdvars l = + if List.mem id l then l else if not (is_freevar bdvars (Global.env ()) id) - then l else id :: l + then l else id :: l in let rec aux bdvars l c = match c with | CRef (Ident (_,id)) -> found id bdvars l @@ -63,107 +63,107 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l = | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c in aux bound l c -let ids_of_names l = +let ids_of_names l = List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l -let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = +let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = let rec aux bdvars l c = match c with ((LocalRawAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Idset.union (ids_of_list bound) bdvars) l' tl - | ((LocalRawDef (n, c)) :: tl) -> + | ((LocalRawDef (n, c)) :: tl) -> let bound = match snd n with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Idset.union (ids_of_list bound) bdvars) l' tl - + | [] -> 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 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) -> + | RVar (loc,id) -> if is_freevar bound (Global.env ()) id then - if List.mem_assoc id vs then vs + 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 + | 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 + 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 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 + | 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 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 + let bound' = add_name_to_ids bound na in (vs'',bound') ) (vs,bound') bl.(i) in - let vs2 = vars bound1 vs1 tyl.(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 + | 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 + 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 + and vars_return_type bound vs (na,tyopt) = + let bound' = add_name_to_ids bound na in vars_option bound' vs tyopt - in + 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 fre_ids env ids = +let fre_ids env ids = List.filter (is_freevar env (Global.env())) ids - + let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id -let next_name_away_from na avoid = +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 + let named, applied = + List.partition (function - (t, Some (loc, ExplByName id)) -> + (t, Some (loc, ExplByName id)) -> if not (List.exists (fun (_, (id', _, _)) -> Name id = id') needed) then user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id); true @@ -179,43 +179,43 @@ let combine_params avoid fn applied needed = | app, (_, (Name id, _, _)) :: need when List.mem_assoc id named -> aux (List.assoc id named :: ids) avoid app need - + | (x, None) :: app, (None, (Name id, _, _)) :: need -> aux (x :: ids) avoid app need - - | _, (Some cl, (_, _, _) as d) :: need -> + + | _, (Some cl, (_, _, _) 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 - | [], (None, _ as decl) :: need -> + | [], (None, _ as decl) :: need -> let t', avoid' = fn avoid decl in aux (t' :: ids) avoid' app need - | (x,_) :: _, [] -> + | (x,_) :: _, [] -> user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments") in aux [] avoid applied needed let combine_params_freevar = - fun avoid (_, (na, _, _)) -> + 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 - + let destClassAppExpl cl = match cl with | CApp (loc, (None,CRef ref), l) -> loc, ref, l | CRef ref -> loc_of_reference ref, ref, [] | _ -> raise Not_found -let implicit_application env ?(allow_partial=true) f ty = +let implicit_application env ?(allow_partial=true) f ty = let is_class = try let (loc, r, _ as clapp) = destClassAppExpl ty in @@ -223,30 +223,30 @@ let implicit_application env ?(allow_partial=true) f ty = let gr = Nametab.locate qid in if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None - in + in match is_class with | None -> ty - | Some ((loc, id, par), gr) -> + | 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 + 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 + 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 = + +let implicits_of_rawterm l = + let rec aux i c = match c with - RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> + RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> let rest = aux (succ i) b in if bk = Implicit then let name = |