From 2d87a9eee93e86d9866120c6ae6dfe7539ee914d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Jun 2005 14:34:55 +0000 Subject: [PATCH] reduce with path --- helm/matita/matita.txt | 4 ++-- helm/matita/matitaEngine.ml | 44 +++++++++++++++++++++++++++++++++++++ helm/matita/tests/match.ma | 13 +++++++++++ 3 files changed, 59 insertions(+), 2 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 454a13029..adf0e1cf1 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -9,10 +9,10 @@ TODO - controllo per script modificato o meno prima di uscire -> - riattaccare hbugs (brrr...) -> Zack - tattica clear ? -> Gares -- intro = intros 1 -> Gares -- timetravel -> gares DONE +- intro = intros 1 -> Gares +- timetravel (urimanager) -> Gares - implementare macro in matitaScript.ml -> Gares - history deve aggiornare anche la whelp bar -> Gares - commenti exeguibili (forse devono essere una lista e non diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 10fe24030..7471e4546 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -62,6 +62,46 @@ let tactic_of_ast = function | TacticAst.LetIn of 'term * 'ident | TacticAst.Replace_pattern of 'term pattern * 'term *) + | TacticAst.ReduceAt (_,reduction_kind,ident,path) -> + ProofEngineTypes.mk_tactic + (fun (((_,metasenv,_,_),goal) as status) -> + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let where, also_in_hypotheses = + if ident = "goal" then + ty, false + else + let hyp = + try + List.find (function + | Some (Cic.Name name,entry) when name = ident -> true + | _ -> false) + context + with + Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis")) + in + (match hyp with + | Some (_, Cic.Decl term) -> term + | Some (_, Cic.Def (term,ty)) -> term + | None -> assert false),true + in + let pointers = CicUtil.select ~term:where ~context:path in + (match reduction_kind with + | `Normalize -> + ProofEngineTypes.apply_tactic + (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers)) + status + | `Reduce -> + ProofEngineTypes.apply_tactic + (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers)) + status + | `Simpl -> + ProofEngineTypes.apply_tactic + (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers)) + status + | `Whd -> + ProofEngineTypes.apply_tactic + (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers)) + status)) | TacticAst.Reduce (_,reduction_kind,opts) -> let terms, also_in_hypotheses = match opts with @@ -70,6 +110,7 @@ let tactic_of_ast = function | None -> None, false in (match reduction_kind with + | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms | `Whd -> Tactics.whd ~also_in_hypotheses ~terms) @@ -366,6 +407,9 @@ let disambiguate_tactic status = function | TacticAst.LetIn of 'term * 'ident | TacticAst.Replace_pattern of 'term pattern * 'term *) + | TacticAst.ReduceAt (loc, reduction_kind, ident, path) -> + let path = Disambiguate.interpretate [] status.aliases path in + status, TacticAst.ReduceAt(loc, reduction_kind, ident, path) | TacticAst.Reduce (loc, reduction_kind, opts) -> let status, opts = match opts with diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma index 732e96fa0..21bad46a9 100644 --- a/helm/matita/tests/match.ma +++ b/helm/matita/tests/match.ma @@ -290,3 +290,16 @@ intros 2.simplify.elim (leb n1 m1). simplify.apply le_n_S.apply H. simplify.intros.apply H.apply le_S_n.assumption. qed. + +theorem prova : +let three \def (S (S (S O))) in +let nine \def (times three three) in +let eightyone \def (times nine nine) in +let square \def (times eightyone eightyone) in +(eq nat square O). +intro. +intro. +intro.intro. +normalize goal at (? ? % ?). + + -- 2.39.2