From 6531c263da005e25ea2f58f9ee960acba7857ff6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 15:41:15 +0000 Subject: [PATCH] 1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture generalized to return the list of matched terms 2. unfold generalized to unfold several occurrences at once --- helm/matita/matitaEngine.ml | 2 +- helm/matita/matitaMathView.ml | 4 ++ helm/matita/tests/unfold.ma | 5 +- helm/ocaml/tactics/proofEngineHelpers.ml | 66 ++++++++-------------- helm/ocaml/tactics/proofEngineHelpers.mli | 16 ++---- helm/ocaml/tactics/proofEngineReduction.ml | 24 ++++---- helm/ocaml/tactics/reductionTactics.ml | 2 +- helm/ocaml/tactics/reductionTactics.mli | 2 +- helm/ocaml/tactics/tactics.mli | 2 +- 9 files changed, 52 insertions(+), 71 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index da3a730fb..f32978063 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -126,7 +126,7 @@ let tactic_of_ast = function | `Normalize -> Tactics.normalize ~pattern | `Reduce -> Tactics.reduce ~pattern | `Simpl -> Tactics.simpl ~pattern - | `Unfold what -> Tactics.unfold ~pattern ?what + | `Unfold what -> Tactics.unfold ~pattern what | `Whd -> Tactics.whd ~pattern) | GrafiteAst.Reflexivity _ -> Tactics.reflexivity | GrafiteAst.Replace (_, pattern, with_what) -> diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index efda8cd76..3cb9c8c0b 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -254,8 +254,12 @@ object (self) match term with | `Term t -> let context' = + match ProofEngineHelpers.locate_in_conjecture t (dummy_goal, context, conclusion) + with + [context,_] -> context + | _ -> assert false (* since it uses physical equality *) in dummy_goal, context', t | `Hyp context -> dummy_goal, context, Cic.Rel 1 diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma index ff68d5fd1..c91ff1863 100644 --- a/helm/matita/tests/unfold.ma +++ b/helm/matita/tests/unfold.ma @@ -21,9 +21,10 @@ lemma lem: \forall n. S (n + n) = (S n) + n. intro; reflexivity. qed. -theorem trivial: \forall n. S (myplus n n) = (S n) + n. - unfold myplus. +theorem trivial: \forall n. S (myplus n n) = myplus (S n) n. + unfold myplus in \vdash \forall _.(? ? ? %). intro. + unfold myplus. rewrite > lem. reflexivity. qed. \ No newline at end of file diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index b9ee8bb8f..22b6c8487 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -554,23 +554,17 @@ exception Fail of string in subst,metasenv,ugraph,context_terms, ty_terms -exception TermNotFound -exception TermFoundMultipleTimes - (** locate_in_term equality what where context * [what] must match a subterm of [where] according to [equality] -* It returns the matched term together with its context in [where] +* It returns the matched terms together with their contexts in [where] * [equality] defaults to physical equality * [context] must be the context of [where] -* It may raise TermNotFound or TermFoundMultipleTimes *) let locate_in_term ?(equality=(==))what ~where context = - let (@@) (l1,l2) (l1',l2') = l1 @ l1', l2 @ l2' in - let list_concat l = List.fold_right (@@) l ([],[]) in let add_ctx context name entry = (Some (name, entry)) :: context in let rec aux context where = - if equality what where then context,[where] + if equality what where then [context,where] else match where with | Cic.Implicit _ @@ -580,83 +574,67 @@ let locate_in_term ?(equality=(==))what ~where context = | Cic.Var _ | Cic.Const _ | Cic.MutInd _ - | Cic.MutConstruct _ -> [],[] - | Cic.Cast (te, ty) -> aux context te @@ aux context ty + | Cic.MutConstruct _ -> [] + | Cic.Cast (te, ty) -> aux context te @ aux context ty | Cic.Prod (name, s, t) | Cic.Lambda (name, s, t) -> - aux context s @@ aux (add_ctx context name (Cic.Decl s)) t + aux context s @ aux (add_ctx context name (Cic.Decl s)) t | Cic.LetIn (name, s, t) -> - aux context s @@ aux (add_ctx context name (Cic.Def (s,None))) t + aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t | Cic.Appl tl -> auxs context tl | Cic.MutCase (_, _, out, t, pat) -> - aux context out @@ aux context t @@ auxs context pat + aux context out @ aux context t @ auxs context pat | Cic.Fix (_, funs) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs in - list_concat + List.concat (List.map (fun (_, _, ty, bo) -> - aux context ty @@ aux (tys @ context) bo) + aux context ty @ aux (tys @ context) bo) funs) | Cic.CoFix (_, funs) -> let tys = List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs in - list_concat + List.concat (List.map (fun (_, ty, bo) -> - aux context ty @@ aux (tys @ context) bo) + aux context ty @ aux (tys @ context) bo) funs) and auxs context tl = (* as aux for list of terms *) - list_concat (List.map (fun t -> aux context t) tl) + List.concat (List.map (fun t -> aux context t) tl) in - match aux context where with - context,[] -> raise TermNotFound - | context,[t] -> context,t - | context,_ -> raise TermFoundMultipleTimes + aux context where -(** locate_in_term equality what where -* [what] must be a subterm of [where] according to [equality] -* It returns the context of [what] in [where] +(** locate_in_term equality what where context +* [what] must match a subterm of [where] according to [equality] +* It returns the matched terms together with their contexts in [where] * [equality] defaults to physical equality -* It may raise TermNotFound or TermFoundMultipleTimes +* [context] must be the context of [where] *) let locate_in_conjecture ?(equality=(==)) what (_,context,ty) = - let (@@) (l1,l2) = - function - None -> l1,l2 - | Some (l1',t) -> l1 @ l1', l2 @ [t] in - let locate_in_term what ~where context = - try - Some (locate_in_term ~equality what ~where context) - with - TermNotFound -> None in let context,res = List.fold_right (fun entry (context,res) -> match entry with None -> entry::context, res | Some (_, Cic.Decl ty) -> - let res = res @@ locate_in_term what ~where:ty context in + let res = res @ locate_in_term what ~where:ty context in let context' = entry::context in context',res | Some (_, Cic.Def (bo,ty)) -> - let res = res @@ locate_in_term what ~where:bo context in + let res = res @ locate_in_term what ~where:bo context in let res = match ty with None -> res | Some ty -> - res @@ locate_in_term what ~where:ty context in + res @ locate_in_term what ~where:ty context in let context' = entry::context in context',res - ) context ([],([],[])) + ) context ([],[]) in - let res = res @@ locate_in_term what ~where:ty context in - match res with - context,[] -> raise TermNotFound - | context,[_] -> context - | context,_ -> raise TermFoundMultipleTimes + res @ locate_in_term what ~where:ty context (* saturate_term newmeta metasenv context ty *) (* Given a type [ty] (a backbone), it returns its head and a new metasenv in *) diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 574a94413..859f1f4ba 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -80,29 +80,25 @@ val select: ] option list * (Cic.context * Cic.term) list -exception TermNotFound -exception TermFoundMultipleTimes - (** locate_in_term equality what where context * [what] must match a subterm of [where] according to [equality] -* It returns the matched term together with its context in [where] +* It returns the matched terms together with their contexts in [where] * [equality] defaults to physical equality * [context] must be the context of [where] -* It may raise TermNotFound or TermFoundMultipleTimes *) val locate_in_term: ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> where:Cic.term -> - Cic.context -> Cic.context * Cic.term + Cic.context -> (Cic.context * Cic.term) list -(** locate_in_conjecture equality what where +(** locate_in_term equality what where context * [what] must match a subterm of [where] according to [equality] -* It returns the context of [what] in [where] +* It returns the matched terms together with their contexts in [where] * [equality] defaults to physical equality -* It may raise TermNotFound or TermFoundMultipleTimes +* [context] must be the context of [where] *) val locate_in_conjecture: ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture -> - Cic.context + (Cic.context * Cic.term) list (* saturate_term newmeta metasenv context ty *) (* Given a type [ty] (a backbone), it returns its head and a new metasenv in *) diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index 8d4245068..d04acd181 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -933,24 +933,26 @@ let unfold ?what context where = | Cic.Appl (he::tl) -> hd_delta_beta context tl he | t -> cannot_delta_expand t in - let context, where' = + let context_and_matched_term_list = match what with - None -> context, where + None -> [context, where] | Some what -> - try + let res = ProofEngineHelpers.locate_in_term ~equality:first_is_the_expandable_head_of_second what ~where context - with - ProofEngineHelpers.TermNotFound -> + in + if res = [] then raise (ProofEngineTypes.Fail ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)) + else + res in - let reduced_term = hd_delta_beta context [] where' in - match what with - None -> reduced_term - | Some what -> - replace ~equality:first_is_the_expandable_head_of_second - ~what:[what] ~with_what:[reduced_term] ~where + let reduced_terms = + List.map + (function (context,where) -> hd_delta_beta context [] where) + context_and_matched_term_list in + let whats = List.map snd context_and_matched_term_list in + replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where ;; diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 492b265cb..f5c82a9fe 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -79,7 +79,7 @@ let simpl_tac ~pattern = let reduce_tac ~pattern = mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);; -let unfold_tac ?what ~pattern = +let unfold_tac what ~pattern = mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what) ~pattern);; diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index 6ef80512b..56b80c06a 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -29,7 +29,7 @@ val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val unfold_tac: - ?what:Cic.term -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic + Cic.term option -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val change_tac: pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 4780a82fb..77e3f8ac5 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -79,6 +79,6 @@ val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic val unfold : - ?what:Cic.term -> + Cic.term option -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic -- 2.39.2