From fa2c122dc2d20e0d8b473bef9128464c3477d419 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 08:44:39 +0000 Subject: [PATCH] This commit makes ProofEngineHelpers.select reach its full potentials. Its arguments are now a conjecture and a pattern and its output is a conjecture-like structure made of physical pointers to matching subterms (together with their contexts). --- helm/ocaml/tactics/proofEngineHelpers.ml | 125 +++++++++++++++------- helm/ocaml/tactics/proofEngineHelpers.mli | 30 +++--- helm/ocaml/tactics/reductionTactics.ml | 117 ++++++-------------- helm/ocaml/tactics/variousTactics.ml | 11 +- 4 files changed, 138 insertions(+), 145 deletions(-) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 4adcb8416..eb92f1351 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -166,7 +166,7 @@ let find_subterms ~wanted ~context t = in find context wanted t -let select ~context ~term ~pattern:(wanted,where) = +let select_in_term ~context ~term ~pattern:(wanted,where) = let add_ctx context name entry = (Some (name, entry)) :: context in @@ -252,43 +252,88 @@ let select ~context ~term ~pattern:(wanted,where) = in find_in_roots roots -let pattern_of ?(equality=(==)) ~term terms = - let (===) x y = equality x y in - let rec aux t = - match t with - | t when List.exists (fun t' -> t === t') terms -> Cic.Implicit (Some `Hole) - | Cic.Var (uri, subst) -> Cic.Var (uri, aux_subst subst) - | Cic.Meta (i, ctxt) -> - let ctxt = - List.map (function None -> None | Some t -> Some (aux t)) ctxt - in - Cic.Meta (i, ctxt) - | Cic.Cast (t, ty) -> Cic.Cast (aux t, aux ty) - | Cic.Prod (name, s, t) -> Cic.Prod (name, aux s, aux t) - | Cic.Lambda (name, s, t) -> Cic.Lambda (name, aux s, aux t) - | Cic.LetIn (name, s, t) -> Cic.LetIn (name, aux s, aux t) - | Cic.Appl terms -> Cic.Appl (List.map aux terms) - | Cic.Const (uri, subst) -> Cic.Const (uri, aux_subst subst) - | Cic.MutInd (uri, tyno, subst) -> Cic.MutInd (uri, tyno, aux_subst subst) - | Cic.MutConstruct (uri, tyno, consno, subst) -> - Cic.MutConstruct (uri, tyno, consno, aux_subst subst) - | Cic.MutCase (uri, tyno, outty, t, pat) -> - Cic.MutCase (uri, tyno, aux outty, aux t, List.map aux pat) - | Cic.Fix (funno, funs) -> - let funs = - List.map (fun (name, i, ty, bo) -> (name, i, aux ty, aux bo)) funs - in - Cic.Fix (funno, funs) - | Cic.CoFix (funno, funs) -> - let funs = - List.map (fun (name, ty, bo) -> (name, aux ty, aux bo)) funs - in - Cic.CoFix (funno, funs) - | Cic.Rel _ - | Cic.Sort _ - | Cic.Implicit _ -> t - and aux_subst subst = - List.map (fun (uri, t) -> (uri, aux t)) subst - in - 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 diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index c11ad6eca..85dc61e81 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -48,18 +48,22 @@ 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 subterm. -* @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 context term (what,where) -* select all subterms of [term] matching [what] in positions rooted at the holes -* of the pattern [where]. [context] is the context of [term]. It returns -* the list of the matched terms (that can be compared using physical equality) -* together with their contexts. *) +(** 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 conjecture type (but for the id): +* a list of (possibly removed) hypothesis (without their names) together with +* the list of its matched subterms (and their contexts) + the list of matched +* subterms of the conclusion with their context. Note: in the result the list +* of hypotheses * 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 one +* hypothesis may be empty. *) val select: - context:Cic.context -> term:Cic.term -> pattern:(Cic.term option * Cic.term) -> + metasenv:Cic.metasenv -> + conjecture:Cic.conjecture -> + pattern:ProofEngineTypes.pattern -> + [ `Decl of (Cic.context * Cic.term) list + | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option + ] option list * (Cic.context * Cic.term) list diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 65dc19912..af5edd160 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -26,98 +26,41 @@ open ProofEngineTypes (* The default of term is the thesis of the goal to be prooved *) -let reduction_tac ~reduction ~pattern:(what,hyp_patterns,goal_pattern) +let reduction_tac ~reduction ~pattern (proof,goal) = let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let replace where terms = - let terms, terms' = - List.split (List.map (fun (context, t) -> t, reduction context t) terms) - in - ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' - ~where:where in - 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' = - let terms = - ProofEngineHelpers.select ~context ~term:ty ~pattern:(what,goal_pattern) - in - replace ty terms in - let context_len = List.length context in - let context' = - if hyp_patterns <> [] then - List.fold_right - (fun entry context -> - match entry with - None -> None::context - | Some (name,Cic.Decl term) -> - (match find_pattern_for name with - | None -> 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 = - ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in - let term' = replace term terms in - Some (name,Cic.Decl term') :: context - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise - (ProofEngineTypes.Fail - ("The term the user wants to convert is not closed " ^ - "in the context of the position of the substitution."))) - | Some (name,Cic.Def (term, ty)) -> - (match find_pattern_for name with - | None -> 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 = - ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in - let term' = replace term terms in - let ty' = - match ty with - None -> None - | Some ty -> - let terms = - ProofEngineHelpers.select - ~context ~term:ty ~pattern:(what,pat) - in - Some (replace ty terms) - in - Some (name,Cic.Def (term',ty')) :: context - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise - (ProofEngineTypes.Fail - ("The term the user wants to convert is not closed " ^ - "in the context of the position of the substitution."))) - ) context [] + if terms = [] then where else - context - in + let terms, terms' = + List.split (List.map (fun (context, t) -> t, reduction context t) terms) + in + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' + ~where:where in + let (selected_context,selected_ty) = + ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in + let ty' = replace ty selected_ty in + let context' = + List.fold_right2 + (fun entry selected_entry context' -> + match entry,selected_entry with + None,None -> None::context' + | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> + let ty' = replace ty selected_ty in + Some (name,Cic.Decl ty')::context' + | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> + let bo' = replace bo selected_bo in + let ty' = + match ty,selected_ty with + None,None -> None + | Some ty,Some selected_ty -> Some (replace ty selected_ty) + | _,_ -> assert false + in + Some (name,Cic.Def (bo',ty'))::context' + | _,_ -> assert false + ) context selected_context [] in let metasenv' = List.map (function | (n,_,_) when n = metano -> (metano,context',ty') diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 2e6810387..73309c43e 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -66,7 +66,7 @@ let assumption_tac = exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;; exception TheSelectedTermsMustLiveInTheGoalContext exception AllSelectedTermsMustBeConvertible;; -exception CannotGeneralizeInHypotheses;; +exception GeneralizationInHypothesesNotImplementedYet;; (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda e li aggiunga nel context, poi si conta la lunghezza di questo nuovo @@ -80,15 +80,16 @@ let generalize_tac let generalize_tac mk_fresh_name_callback ~pattern:(term,hyps_pat,concl_pat) status = - if hyps_pat <> [] then raise CannotGeneralizeInHypotheses ; + if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet; let (proof, goal) = status in let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let terms_with_context = - ProofEngineHelpers.select ~context ~term:ty ~pattern:(term,concl_pat) in + let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in + let selected_hyps,terms_with_context = + ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in + assert (selected_hyps = []); let typ,term = match terms_with_context, term with [], None -> -- 2.39.2