From 3e25c8d9f6e7802a2fc28697795b9128af731494 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Aug 2007 08:14:21 +0000 Subject: [PATCH] select now works correctly even if multiple hypotheses with the same name are present in the context. --- .../components/tactics/proofEngineHelpers.ml | 26 +++++++++++++++---- 1 file changed, 21 insertions(+), 5 deletions(-) diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index ec2e1919c..fa5c77d71 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -486,17 +486,33 @@ exception Fail of string Lazy.t let find_pattern_for name = try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) with Not_found -> None in + (* Multiple hypotheses with the same name can be in the context. + In this case we need to pick the last one, but we will perform + a fold_right on the context. Thus we pre-process hyp_patterns. *) + let full_hyp_pattern = + let rec aux blacklist = + function + [] -> [] + | None::tl -> None::aux blacklist tl + | Some (name,_)::tl -> + if List.mem name blacklist then + None::aux blacklist tl + else + find_pattern_for name::aux (name::blacklist) tl + in + aux [] context + in let subst,metasenv,ugraph,ty_terms = select_in_term ~metasenv ~context ~ugraph ~term:ty ~pattern:(what,goal_pattern) in let subst,metasenv,ugraph,context_terms = let subst,metasenv,ugraph,res,_ = (List.fold_right - (fun entry (subst,metasenv,ugraph,res,context) -> + (fun (pattern,entry) (subst,metasenv,ugraph,res,context) -> match entry with - None -> subst,metasenv,ugraph,(None::res),(None::context) + None -> subst,metasenv,ugraph,None::res,None::context | Some (name,Cic.Decl term) -> - (match find_pattern_for name with + (match pattern with | None -> subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context) | Some pat -> @@ -507,7 +523,7 @@ exception Fail of string Lazy.t subst,metasenv,ugraph,((Some (`Decl terms))::res), (entry::context)) | Some (name,Cic.Def (bo, ty)) -> - (match find_pattern_for name with + (match pattern with | None -> let selected_ty=match ty with None -> None | Some _ -> Some [] in subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res), @@ -528,7 +544,7 @@ exception Fail of string Lazy.t in subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res), (entry::context)) - ) context (subst,metasenv,ugraph,[],[])) + ) (List.combine full_hyp_pattern context) (subst,metasenv,ugraph,[],[])) in subst,metasenv,ugraph,res in -- 2.39.2