From 71a463426a9cf552ba78b28708ea860adc59e553 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 23 Oct 2013 15:15:21 +0000 Subject: Optimizing Vars.replace_vars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16916 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/vars.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'kernel/vars.ml') diff --git a/kernel/vars.ml b/kernel/vars.ml index c7ec69c87..123c96d6d 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -155,20 +155,25 @@ let subst1_named_decl lam = substl_named_decl [lam] let rec thin_val = function | [] -> [] - | s :: tl -> - let id, { sit = c } = s in + | (id, c) :: tl -> match Constr.kind c with - | Constr.Var v -> if Id.equal id v then thin_val tl else s::(thin_val tl) - | _ -> s :: (thin_val tl) + | Constr.Var v -> + if Id.equal id v then thin_val tl + else (id, make_substituend c) :: (thin_val tl) + | _ -> (id, make_substituend c) :: (thin_val tl) + +let rec find_var id = function +| [] -> raise Not_found +| (idc, c) :: subst -> + if Id.equal id idc then c + else find_var id subst (* (replace_vars sigma M) applies substitution sigma to term M *) let replace_vars var_alist = - let var_alist = - List.map (fun (str,c) -> (str,make_substituend c)) var_alist in let var_alist = thin_val var_alist in let rec substrec n c = match Constr.kind c with | Constr.Var x -> - (try lift_substituend n (List.assoc x var_alist) + (try lift_substituend n (find_var x var_alist) with Not_found -> c) | _ -> Constr.map_with_binders succ substrec n c in -- cgit v1.2.3