reduce with path

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 10fe24030d00c27951d49580f499fbd5c2c49754..7471e4546e7db2c5841bc1ea2d85884ea910c444 100644 (file)
--- 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