Fourier tactic update

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 1942e1821eca02547a149b3f903cebcf20fae720..b8d88ae193b14902bfafa43b2f74a14000645fda 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -132,16 +132,6 @@ let flin_emult a f =
    
 (*****************************************************************************)
 
-(*
-
-       no idea about helm parser ??????????????????????????????
-
-let parse_ast   = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
-let pf_parse_constr gl s =
-   Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
-*)
-
 
 (**
        @param t a term
@@ -417,36 +407,79 @@ let rec rational_to_fraction x= (x.num,x.den)
     
 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 *)
-let int_to_real n =
+(*et int_to_real n =
    let nn=abs n in
-   let s=ref "" in
+   let s=ref Cic.term
    if nn=0
    then s:="R0"
    else (s:="R1";
         for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
    if n<0 then s:="(Ropp "^(!s)^")";
    !s
+;;*)
+let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
+
+let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
+let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
+let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
+
+
+let rec int_to_real_aux n =
+  match n with
+    0 -> _R0 (* o forse R0 + R0 ????? *)
+  | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
+;;     
+       
+
+let int_to_real n =
+   let x = int_to_real_aux (abs n) in
+   if n < 0 then
+       Cic.Appl [ _Ropp ; x ] 
+   else
+       x
 ;;
 
+
 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 *)
+let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
+let _Rinv  = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
+       
+
 let rational_to_real x =
-   let (n,d)=rational_to_fraction x in
-   ("(Rmult "^(int_to_real n)^" (Rinv "^(int_to_real d)^"))")
+   let (n,d)=rational_to_fraction x in 
+   Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ]  ]
 ;;
 
 (* preuve que 0<n*1/d
 *)
-(*let tac_zero_inf_pos gl (n,d) =
-   let cste = pf_parse_constr gl in
-   let tacn=ref (apply (cste "Rlt_zero_1")) in
-   let tacd=ref (apply (cste "Rlt_zero_1")) in
+
+let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
+
+let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
+
+let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
+
+
+let tcl_then ~start ~continuation ~status = 
+   let tcl_then_aux (proof,goals) goal =
+      let (newproof,newgoals) = continuation ~status:(proof,goal) in
+      (newproof, goals @ newgoals)
+   in
+   let (proof,new_goals) = start ~status in
+   List.fold_left tcl_then_aux (proof,[]) new_goals
+;;
+
+let tac_zero_inf_pos gl (n,d) =
+   (*let cste = pf_parse_constr gl in*)
+   let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
+   let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
    for i=1 to n-1 do 
-       tacn:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacn); done;
+       tacn:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
    for i=1 to d-1 do
-       tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
-   (tclTHENS (apply (cste "Rlt_mult_inv_pos")) [!tacn;!tacd])
-;;*)
+       tacd:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
+   (Ring.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
+;;
 
 (* preuve que 0<=n*1/d
 *)