From e72cb7cb39f69af02097e06d525031c9bb5cbd88 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 29 Aug 2007 18:42:33 +0000 Subject: Prise en compte des redéfinitions de variables (définitions locales triviales en provenance de l'algo de compilation du filtrage) lors du calcul de la projection des variables dans real_clean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10103 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarutil.ml | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 5729d6c71..72f5fbf45 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -397,6 +397,23 @@ and clear_hyps_in_evi evd evi ids = let need_restriction k args = not (array_for_all (closedn k) args) +(* A utility to circumvent the introduction of aliases to rel by the + pattern-matching compilation algorithm *) + +let rec expand_var env x = match kind_of_term x with + | Rel n -> + begin try match pi2 (lookup_rel n env) with + | Some t when isRel t -> expand_var env (lift n t) + | _ -> x + with Not_found -> x + end + | Var id -> + begin match pi2 (lookup_named id env) with + | Some t when isVar t -> expand_var env t + | _ -> x + end + | _ -> x + (* We try to instantiate the evar assuming the body won't depend * on arguments that are not Rels or Vars, or appearing several times * (i.e. we tackle only Miller-Pfenning patterns unification) @@ -424,14 +441,15 @@ exception NotClean of constr let rec real_clean env isevars ev subst rhs = let evd = ref isevars in - let subst' = List.map (fun (x,y) -> (y,mkVar x)) subst in + let invert_binding (x,y) = (expand_var env y,mkVar x) in + let subst' = List.map invert_binding subst in let rec subs rigid k t = match kind_of_term t with | Rel i -> if i<=k then t else (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *) - (try List.assoc (mkRel (i-k)) subst' + (try List.assoc (expand_var env (mkRel (i-k))) subst' with Not_found -> if rigid then try unique_projection env evd (mkRel (i-k)) subst -- cgit v1.2.3