X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=d3d36ca6e9cf630cfd64e93ea07e732a8df3973f;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=5a567b84aa75e6056814d845ea1a35e6d81a6120;hpb=f5b6be7239a35e1d0aba504605b5a0df5cf06726;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 5a567b84a..d3d36ca6e 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -23,8 +23,10 @@
  * http://cs.unibo.it/helm/.
  *)
 
+open ProofEngineTypes
+
 (*
-let reduction_tac ~reduction ~status:(proof,goal) =
+let reduction_tac ~reduction (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let new_ty = reduction context ty in
@@ -40,7 +42,7 @@ let reduction_tac ~reduction ~status:(proof,goal) =
 *)
 
 (* The default of term is the thesis of the goal to be prooved *)
-let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
+let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let terms =
@@ -89,41 +91,56 @@ let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
       (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 simpl_tac ~also_in_hypotheses ~terms = 
+ mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.simpl 
+  ~also_in_hypotheses ~terms);;
 
-let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let term' = reduction 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
+let reduce_tac ~also_in_hypotheses ~terms = 
+ mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.reduce
+  ~also_in_hypotheses ~terms);;
+  
+let whd_tac ~also_in_hypotheses ~terms = 
+ mk_tactic ( reduction_tac ~reduction:CicReduction.whd 
+  ~also_in_hypotheses ~terms);;
+
+let normalize_tac ~also_in_hypotheses ~terms = 
+ mk_tactic ( reduction_tac ~reduction:CicReduction.normalize 
+  ~also_in_hypotheses ~terms);;
+
+let fold_tac ~reduction ~also_in_hypotheses ~term =
+ let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+   let term' = reduction 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,None))  -> Some (n,Cic.Def ((replace t),None))
+           | None -> None
+           | Some (_,Cic.Def (_,Some _)) -> assert false
+         ) context
+       else
+        context
+      in
        List.map
         (function
-            Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
-          | Some (n,Cic.Def (t,None))  -> Some (n,Cic.Def ((replace t),None))
-          | None -> None
-          | Some (_,Cic.Def (_,Some _)) -> assert false
-        ) context
-      else
-       context
+            (n,_,_) when n = metano -> (metano,context',ty')
+          | _ as t -> t
+        ) metasenv
+      
      in
-      List.map
-       (function
-           (n,_,_) when n = metano -> (metano,context',ty')
-         | _ as t -> t
-       ) metasenv
-     
-    in
-     (curi,metasenv',pbo,pty), [metano]
+      (curi,metasenv',pbo,pty), [metano]
+ in
+  mk_tactic (fold_tac ~reduction ~also_in_hypotheses ~term)
 ;;