From c5b08eb60c8ede80fad4f44abd8439cef9b339c1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 1 Jul 2005 13:05:51 +0000 Subject: [PATCH] pattern_of function reimplemented. Now it takes a term and a list of subterms and it returns the _minimal_ pattern for the subterms in the term. --- helm/ocaml/tactics/proofEngineHelpers.ml | 303 ++++++++++++++++------ helm/ocaml/tactics/proofEngineHelpers.mli | 10 + 2 files changed, 230 insertions(+), 83 deletions(-) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index aefb1c1e6..ea797481c 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -256,88 +256,225 @@ let select_in_term ~context ~term ~pattern:(wanted,where) = in find_in_roots roots +(** create a pattern from a term and a list of subterms. +* the pattern is granted to have a ? for every subterm that has no selected +* subterms +* @param equality equality function used while walking the term. Defaults to +* physical equality (==) *) +let pattern_of ?(equality=(==)) ~term terms = + let (===) x y = equality x y in + let not_found = false, Cic.Implicit None in + let rec aux t = + match t with + | t when List.exists (fun t' -> t === t') terms -> + true,Cic.Implicit (Some `Hole) + | Cic.Var (uri, subst) -> + let b,subst = aux_subst subst in + if b then + true,Cic.Var (uri, subst) + else + not_found + | Cic.Meta (i, ctxt) -> + let b,ctxt = + List.fold_right + (fun e (b,ctxt) -> + match e with + None -> b,None::ctxt + | Some t -> let bt,t = aux t in b||bt ,Some t::ctxt + ) ctxt (false,[]) + in + if b then + true,Cic.Meta (i, ctxt) + else + not_found + | Cic.Cast (te, ty) -> + let b1,te = aux te in + let b2,ty = aux ty in + if b1||b2 then true,Cic.Cast (te, ty) + else + not_found + | Cic.Prod (name, s, t) -> + let b1,s = aux s in + let b2,t = aux t in + if b1||b2 then + true, Cic.Prod (name, s, t) + else + not_found + | Cic.Lambda (name, s, t) -> + let b1,s = aux s in + let b2,t = aux t in + if b1||b2 then + true, Cic.Lambda (name, s, t) + else + not_found + | Cic.LetIn (name, s, t) -> + let b1,s = aux s in + let b2,t = aux t in + if b1||b2 then + true, Cic.LetIn (name, s, t) + else + not_found + | Cic.Appl terms -> + let b,terms = + List.fold_right + (fun t (b,terms) -> + let bt,t = aux t in + b||bt,t::terms + ) terms (false,[]) + in + if b then + true,Cic.Appl terms + else + not_found + | Cic.Const (uri, subst) -> + let b,subst = aux_subst subst in + if b then + true, Cic.Const (uri, subst) + else + not_found + | Cic.MutInd (uri, tyno, subst) -> + let b,subst = aux_subst subst in + if b then + true, Cic.MutInd (uri, tyno, subst) + else + not_found + | Cic.MutConstruct (uri, tyno, consno, subst) -> + let b,subst = aux_subst subst in + if b then + true, Cic.MutConstruct (uri, tyno, consno, subst) + else + not_found + | Cic.MutCase (uri, tyno, outty, t, pat) -> + let b1,outty = aux outty in + let b2,t = aux t in + let b3,pat = + List.fold_right + (fun t (b,pat) -> + let bt,t = aux t in + bt||b,t::pat + ) pat (false,[]) + in + if b1 || b2 || b3 then + true, Cic.MutCase (uri, tyno, outty, t, pat) + else + not_found + | Cic.Fix (funno, funs) -> + let b,funs = + List.fold_right + (fun (name, i, ty, bo) (b,funs) -> + let b1,ty = aux ty in + let b2,bo = aux bo in + b||b1||b2, (name, i, ty, bo)::funs) funs (false,[]) + in + if b then + true, Cic.Fix (funno, funs) + else + not_found + | Cic.CoFix (funno, funs) -> + let b,funs = + List.fold_right + (fun (name, ty, bo) (b,funs) -> + let b1,ty = aux ty in + let b2,bo = aux bo in + b||b1||b2, (name, ty, bo)::funs) funs (false,[]) + in + if b then + true, Cic.CoFix (funno, funs) + else + not_found + | Cic.Rel _ + | Cic.Sort _ + | Cic.Implicit _ -> not_found + and aux_subst subst = + List.fold_right + (fun (uri, t) (b,subst) -> + let b1,t = aux t in + b||b1,(uri, t)::subst) subst (false,[]) + in + snd (aux term) + exception Fail of string -(** select metasenv conjecture pattern -* select all subterms of [conjecture] matching [pattern]. -* It returns the set of matched terms (that can be compared using physical -* equality to the subterms of [conjecture]) together with their contexts. -* The representation of the set mimics the ProofEngineTypes.pattern type: -* a list of hypothesis (names of) together with the list of its matched -* subterms (and their contexts) + the list of matched subterms of the -* with their context conclusion. Note: in the result the list of hypothesis -* has an entry for each entry in the context and in the same order. -* Of course the list of terms (with their context) associated to the -* hypothesis name may be empty. *) -let select ~metasenv ~conjecture:(_,context,ty) ~pattern:(what,hyp_patterns,goal_pattern) = - let find_pattern_for name = - try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) - with Not_found -> None in - let ty_terms = select_in_term ~context ~term:ty ~pattern:(what,goal_pattern) in - let context_len = List.length context in - let context_terms = - fst - (List.fold_right - (fun entry (res,context) -> - match entry with - None -> (None::res),(None::context) - | Some (name,Cic.Decl term) -> - (match find_pattern_for name with - | None -> ((Some (`Decl []))::res),(entry::context) - | Some pat -> - try - let what = - match what with - None -> None - | Some what -> - let what,subst',metasenv' = - CicMetaSubst.delift_rels [] metasenv - (context_len - List.length context) what - in - assert (subst' = []); - assert (metasenv' = metasenv); - Some what in - let terms = select_in_term ~context ~term ~pattern:(what,pat) in - ((Some (`Decl terms))::res),(entry::context) - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise - (Fail - ("The term the user wants to convert is not closed " ^ - "in the context of the position of the substitution."))) - | Some (name,Cic.Def (bo, ty)) -> - (match find_pattern_for name with - | None -> - let selected_ty= match ty with None -> None | Some _ -> Some [] in - ((Some (`Def ([],selected_ty)))::res),(entry::context) - | Some pat -> - try - let what = - match what with - None -> None - | Some what -> - let what,subst',metasenv' = - CicMetaSubst.delift_rels [] metasenv - (context_len - List.length context) what - in - assert (subst' = []); - assert (metasenv' = metasenv); - Some what in - let terms_bo = - select_in_term ~context ~term:bo ~pattern:(what,pat) in - let terms_ty = - match ty with - None -> None - | Some ty -> - Some (select_in_term ~context ~term:ty ~pattern:(what,pat)) - in - ((Some (`Def (terms_bo,terms_ty)))::res),(entry::context) - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise - (Fail - ("The term the user wants to convert is not closed " ^ - "in the context of the position of the substitution."))) - ) context ([],[])) - in - context_terms, ty_terms + (** select metasenv conjecture pattern + * select all subterms of [conjecture] matching [pattern]. + * It returns the set of matched terms (that can be compared using physical + * equality to the subterms of [conjecture]) together with their contexts. + * The representation of the set mimics the ProofEngineTypes.pattern type: + * a list of hypothesis (names of) together with the list of its matched + * subterms (and their contexts) + the list of matched subterms of the + * with their context conclusion. Note: in the result the list of hypothesis + * has an entry for each entry in the context and in the same order. + * Of course the list of terms (with their context) associated to the + * hypothesis name may be empty. *) + let select ~metasenv ~conjecture:(_,context,ty) ~pattern:(what,hyp_patterns,goal_pattern) = + let find_pattern_for name = + try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) + with Not_found -> None in + let ty_terms = select_in_term ~context ~term:ty ~pattern:(what,goal_pattern) in + let context_len = List.length context in + let context_terms = + fst + (List.fold_right + (fun entry (res,context) -> + match entry with + None -> (None::res),(None::context) + | Some (name,Cic.Decl term) -> + (match find_pattern_for name with + | None -> ((Some (`Decl []))::res),(entry::context) + | Some pat -> + try + let what = + match what with + None -> None + | Some what -> + let what,subst',metasenv' = + CicMetaSubst.delift_rels [] metasenv + (context_len - List.length context) what + in + assert (subst' = []); + assert (metasenv' = metasenv); + Some what in + let terms = select_in_term ~context ~term ~pattern:(what,pat) in + ((Some (`Decl terms))::res),(entry::context) + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise + (Fail + ("The term the user wants to convert is not closed " ^ + "in the context of the position of the substitution."))) + | Some (name,Cic.Def (bo, ty)) -> + (match find_pattern_for name with + | None -> + let selected_ty= match ty with None -> None | Some _ -> Some [] in + ((Some (`Def ([],selected_ty)))::res),(entry::context) + | Some pat -> + try + let what = + match what with + None -> None + | Some what -> + let what,subst',metasenv' = + CicMetaSubst.delift_rels [] metasenv + (context_len - List.length context) what + in + assert (subst' = []); + assert (metasenv' = metasenv); + Some what in + let terms_bo = + select_in_term ~context ~term:bo ~pattern:(what,pat) in + let terms_ty = + match ty with + None -> None + | Some ty -> + Some (select_in_term ~context ~term:ty ~pattern:(what,pat)) + in + ((Some (`Def (terms_bo,terms_ty)))::res),(entry::context) + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise + (Fail + ("The term the user wants to convert is not closed " ^ + "in the context of the position of the substitution."))) + ) context ([],[])) + in + context_terms, ty_terms diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 85dc61e81..219d426e4 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -48,6 +48,16 @@ val compare_metasenvs : * A pattern is a Cic term in which Cic.Implicit terms annotated with `Hole * appears *) +(** create a pattern from a term and a list of subterms. +* the pattern is granted to have a ? for every subterm that has no selected +* subterms +* @param equality equality function used while walking the term. Defaults to +* physical equality (==) *) +val pattern_of: + ?equality:(Cic.term -> Cic.term -> bool) -> term:Cic.term -> Cic.term list -> + Cic.term + + (** select metasenv conjecture pattern * select all subterms of [conjecture] matching [pattern]. * It returns the set of matched terms (that can be compared using physical -- 2.39.2