From 2d87a9eee93e86d9866120c6ae6dfe7539ee914d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
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