X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FreductionTactics.ml;h=0080e4571255062d85a4b91be1bdb8b2e701a2f4;hb=850b1a2e1b00104239484ac25aef29c0b943e1e5;hp=0e5688e02ebe5e98a82cbca5e486e8fb8ee2bf5d;hpb=3066e4dcb7270a5eb20020a91d45da9eb87e2f2e;p=helm.git

diff --git a/helm/gTopLevel/reductionTactics.ml b/helm/gTopLevel/reductionTactics.ml
index 0e5688e02..0080e4571 100644
--- a/helm/gTopLevel/reductionTactics.ml
+++ b/helm/gTopLevel/reductionTactics.ml
@@ -23,6 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(*
 let reduction_tac ~reduction ~status:(proof,goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
@@ -36,7 +37,91 @@ let reduction_tac ~reduction ~status:(proof,goal) =
    in
     (curi,new_metasenv,pbo,pty), [metano]
 ;;
+*)
+
+(* The default of term is the thesis of the goal to be prooved *)
+let reduction_tac ~also_in_hypotheses ~reduction ~term ~status:(proof,goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let term =
+   match term with None -> ty | Some t -> t
+  in
+  (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+  (* the type of one metavariable. So we replace it everywhere.   *)
+  (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
+  (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma,  *)
+  (*CSC: e' meglio prima cercare il termine e scoprirne il        *)
+  (*CSC: contesto, poi ridurre e infine rimpiazzare.              *)
+   let replace context where=
+(*CSC: Per il momento se la riduzione fallisce significa solamente che *)
+(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!!      *)
+(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
+   try
+    let term' = reduction context term in
+     ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
+      ~where:where
+   with
+    _ -> where
+   in
+    let ty' = replace context ty in
+    let context' =
+     if also_in_hypotheses then
+      List.fold_right
+       (fun entry context ->
+         match entry with
+            Some (name,Cic.Def  t) ->
+             (Some (name,Cic.Def  (replace context t)))::context
+          | Some (name,Cic.Decl t) ->
+             (Some (name,Cic.Decl (replace context t)))::context
+          | None -> None::context
+       ) context []
+     else
+      context
+    in
+     let metasenv' = 
+      List.map
+       (function
+           (n,_,_) when n = metano -> (metano,context',ty')
+         | _ as t -> t
+       ) metasenv
+     in
+      (curi,metasenv',pbo,pty), [metano]
+;;
 
 let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;;
 let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
 let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
+
+let fold_tac ~also_in_hypotheses ~term ~status:(proof,goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let term' = CicReduction.whd context term in
+   (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+   (* the type of one metavariable. So we replace it everywhere.   *)
+   (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
+   (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
+   let replace =
+    ProofEngineReduction.replace ~equality:(=) ~what:term' ~with_what:term
+   in
+    let ty' = replace ty in
+    let metasenv' =
+     let context' =
+      if also_in_hypotheses then
+       List.map
+        (function
+            Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
+          | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
+          | None -> None
+        ) context
+      else
+       context
+     in
+      List.map
+       (function
+           (n,_,_) when n = metano -> (metano,context',ty')
+         | _ as t -> t
+       ) metasenv
+     
+    in
+     (curi,metasenv',pbo,pty), [metano]
+;;