bugfix: demodulate_tac is in module Saturation

[helm.git] / helm / ocaml / tactics / fourierR.ml

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index c51d3bf0cf77e611690355ead5841272bbdd9960..8b910bded8ebabe6c5695016930b4ef4325c721b 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 
 (******************** THE FOURIER TACTIC ***********************)
 
@@ -194,8 +196,8 @@ let rational_of_const = rational_of_term;;
 *)
 let fails f a =
  try
-   let tmp = (f a) in
-   false
+  ignore (f a);
+  false
  with 
    _-> true
  ;;
@@ -660,11 +662,7 @@ let tac_zero_inf_false gl (n,d) =
     apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status
    else
     apply_tactic (Tacticals.then_ 
-     ~start:( mk_tactic (fun status -> 
-       let (proof, goal) = status in
-       let curi,metasenv,pbo,pty = proof in
-       let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-        apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status))
+     ~start:(mk_tactic (apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt)))
      ~continuation:(tac_zero_infeq_pos gl (-n,d))) 
     status
  in
@@ -692,20 +690,19 @@ let tac_zero_infeq_false gl (n,d) =
   apply_tactic 
    (Tacticals.then_
     ~start:
-      (ReductionTactics.fold_tac ~reduction:CicReduction.whd
-        ~pattern:([],None)
+      (ReductionTactics.fold_tac
+        ~reduction:(const_lazy_reduction CicReduction.whd)
+        ~pattern:(ProofEngineTypes.conclusion_pattern None)
         ~term:
-          (Cic.Appl
+          (const_lazy_term
+            (Cic.Appl
             [_Rle ; _R0 ;
-             Cic.Appl
-              [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
-            ]
-          )
-      )
+              Cic.Appl
+               [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])))
     ~continuation:
       (Tacticals.then_ 
         ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
-        ~continuation:(tac_zero_inf_pos (-n,d)))) 
+        ~continuation:(tac_zero_inf_pos (-n,d))))
    status 
  in
   mk_tactic (tac_zero_infeq_false gl (n,d))
@@ -885,7 +882,10 @@ let equality_replace a b =
     let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
  debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
     let (proof,goals) = apply_tactic 
-     (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ())
+     (EqualityTactics.rewrite_simpl_tac
+       ~direction:`LeftToRight
+       ~pattern:(ProofEngineTypes.conclusion_pattern None)
+       (C.Meta (fresh_meta,irl)))
      ((curi,metasenv',pbo,pty),goal)
     in
     let new_goals = fresh_meta::goals in
@@ -898,7 +898,7 @@ let equality_replace a b =
 
 let tcl_fail a (proof,goal) =
   match a with
-    1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+    1 -> raise (ProofEngineTypes.Fail (lazy "fail-tactical"))
   | _ -> (proof,[goal])
 ;;
 
@@ -915,7 +915,7 @@ let assumption_tac (proof,goal)=
         )  
           context 
   in
-  Tacticals.try_tactics ~tactics:tac_list (proof,goal)
+  Tacticals.first ~tactics:tac_list (proof,goal)
 ;;
 *)
 (* Galla: moved in negationTactics.ml
@@ -939,8 +939,6 @@ let rec fourier (s_proof,s_goal)=
   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
   debug_pcontext s_context;
 
-  let fhyp = String.copy "new_hyp_for_fourier" in 
-   
 (* here we need to negate the thesis, but to do this we need to apply the 
    right theoreme,so let's parse our thesis *)
   
@@ -1133,8 +1131,9 @@ let rec fourier (s_proof,s_goal)=
              let curi,metasenv,pbo,pty = proof in
              let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              apply_tactic 
-              (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
-                ~with_what:(Cic.Appl [ _not; ineq])) 
+              (ReductionTactics.change_tac
+                ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
+                (const_lazy_term (Cic.Appl [ _not; ineq])))
               status))
            ~continuation:(Tacticals.then_ 
              ~start:(PrimitiveTactics.apply_tac ~term:
@@ -1161,7 +1160,7 @@ let rec fourier (s_proof,s_goal)=
                    r))
                  ~continuations:
                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
-                   Tacticals.try_tactics 
+                   Tacticals.first 
                      ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] 
                    ])
                ;(*Tacticals.id_tac*)
@@ -1178,8 +1177,10 @@ let rec fourier (s_proof,s_goal)=
                      |_ -> assert false)
                    in
                    let r = apply_tactic 
-                   (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
-                      ~with_what:w1) status in
+                   (ReductionTactics.change_tac
+                      ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
+                      (const_lazy_term w1)) status
+                   in
                    debug("fine MY_CHNGE\n");
                    r)) 
                  ~continuation:(*PORTINGTacticals.id_tac*)tac2]))