Fourier tactic update

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index c11947a0e8f595c33cb0e5f30f9c575009225418..1942e1821eca02547a149b3f903cebcf20fae720 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -182,24 +182,24 @@ let rec rational_of_term t =
         (match t1 with
            Cic.Const (u,boh) ->
                (match (UriManager.string_of_uri u) with
-                "cic:/Coq/Reals/Rdefinitions/Ropp" -> 
+                "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> 
                      rat_of_unop rop next 
-               |"cic:/Coq/Reals/Rdefinitions/Rinv" -> 
+               |"cic:/Coq/Reals/Rdefinitions/Rinv.con" -> 
                       rat_of_unop rinv next 
-                |"cic:/Coq/Reals/Rdefinitions/Rmult" -> 
+                |"cic:/Coq/Reals/Rdefinitions/Rmult.con" -> 
                       rat_of_binop rmult next
-                |"cic:/Coq/Reals/Rdefinitions/Rdiv" -> 
+                |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" -> 
                       rat_of_binop rdiv next
-                |"cic:/Coq/Reals/Rdefinitions/Rplus" -> 
+                |"cic:/Coq/Reals/Rdefinitions/Rplus.con" -> 
                       rat_of_binop rplus next
-                |"cic:/Coq/Reals/Rdefinitions/Rminus" -> 
+                |"cic:/Coq/Reals/Rdefinitions/Rminus.con" -> 
                       rat_of_binop rminus next
                 | _ -> failwith "not a rational")
           | _ -> failwith "not a rational")
   | Cic.Const (u,boh) ->
         (match (UriManager.string_of_uri u) with
-              "cic:/Coq/Reals/Rdefinitions/R1" -> r1
-              |"cic:/Coq/Reals/Rdefinitions/R0" -> r0
+              "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
+              |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
               |  _ -> failwith "not a rational")
   |  _ -> failwith "not a rational"
 ;;
@@ -224,13 +224,13 @@ let rec flin_of_term t =
         Cic.Const (u,boh) ->
             begin
            match (UriManager.string_of_uri u) with
-            "cic:/Coq/Reals/Rdefinitions/Ropp" -> 
+            "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> 
                   flin_emult (rop r1) (flin_of_term (List.hd next))
-           |"cic:/Coq/Reals/Rdefinitions/Rplus"-> 
+           |"cic:/Coq/Reals/Rdefinitions/Rplus.con"-> 
                   fl_of_binop flin_plus next 
-           |"cic:/Coq/Reals/Rdefinitions/Rminus"->
+           |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
                   fl_of_binop flin_minus next
-           |"cic:/Coq/Reals/Rdefinitions/Rmult"->
+           |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
                begin
                let arg1 = (List.hd next) and
                    arg2 = (List.hd(List.tl next)) 
@@ -249,10 +249,10 @@ let rec flin_of_term t =
                with 
                        _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
                end
-           |"cic:/Coq/Reals/Rdefinitions/Rinv"->
+           |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
               let a=(rational_of_term (List.hd next)) in
               flin_add_cste (flin_zero()) (rinv a)
-           |"cic:/Coq/Reals/Rdefinitions/Rdiv"->
+           |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
                begin
                let b=(rational_of_term (List.hd(List.tl next))) in
                try 
@@ -270,8 +270,8 @@ let rec flin_of_term t =
   | Cic.Const (u,boh) ->
         begin
        match (UriManager.string_of_uri u) with
-        "cic:/Coq/Reals/Rdefinitions/R1" -> flin_one ()
-        |"cic:/Coq/Reals/Rdefinitions/R0" -> flin_zero ()
+        "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
+        |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
         |_-> assert false
        end
   |_-> assert false)
@@ -282,97 +282,109 @@ let rec flin_of_term t =
 let flin_of_constr = flin_of_term;;
 *)
 
-(*
+(**
+       Translates a flin to (c,x) list
+       @param f a flin
+       @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
+*)
 let flin_to_alist f =
     let res=ref [] in
     Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
     !res
-;;*)
+;;
 
 (* Représentation des hypothèses qui sont des inéquations ou des équations.
 *)
-(*
-type hineq={hname:constr; (* le nom de l'hypothèse *)
+
+(**
+       The structure for ineq
+*)
+type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
-            hleft:constr;
-            hright:constr;
+            hleft:Cic.term;
+            hright:Cic.term;
             hflin:flin;
             hstrict:bool}
-;;*)
+;;
 
 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 *)
-(*let ineq1_of_constr (h,t) =
-    match (kind_of_term t) with
-       App (f,args) ->
-         let t1= args.(0) in
-         let t2= args.(1) in
-         (match kind_of_term f with
-           Const c ->
-            (match (string_of_path c) with
-                "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h;
+
+let ineq1_of_term (h,t) =
+    match t with
+       Cic.Appl (t1::next) ->
+         let arg1= List.hd next in
+         let arg2= List.hd(List.tl next) in
+         (match t1 with
+           Cic.Const (u,boh) ->
+            (match UriManager.string_of_uri u with
+                "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
                            htype="Rlt";
-                          hleft=t1;
-                          hright=t2;
-                          hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
+                          hleft=arg1;
+                          hright=arg2;
+                          hflin= flin_minus (flin_of_term arg1)
+                                             (flin_of_term arg2);
                           hstrict=true}]
-               |"Coq.Reals.Rdefinitions.Rgt" -> [{hname=h;
+               |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h;
                            htype="Rgt";
-                          hleft=t2;
-                          hright=t1;
-                          hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
+                          hleft=arg2;
+                          hright=arg1;
+                          hflin= flin_minus (flin_of_term arg2)
+                                             (flin_of_term arg1);
                           hstrict=true}]
-               |"Coq.Reals.Rdefinitions.Rle" -> [{hname=h;
+               |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h;
                            htype="Rle";
-                          hleft=t1;
-                          hright=t2;
-                          hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
+                          hleft=arg1;
+                          hright=arg2;
+                          hflin= flin_minus (flin_of_term arg1)
+                                             (flin_of_term arg2);
                           hstrict=false}]
-               |"Coq.Reals.Rdefinitions.Rge" -> [{hname=h;
+               |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h;
                            htype="Rge";
-                          hleft=t2;
-                          hright=t1;
-                          hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
+                          hleft=arg2;
+                          hright=arg1;
+                          hflin= flin_minus (flin_of_term arg2)
+                                             (flin_of_term arg1);
                           hstrict=false}]
                 |_->assert false)
-          | Ind (sp,i) ->
-              (match (string_of_path sp) with 
-                "Coq.Init.Logic_Type.eqT" ->  let t0= args.(0) in
-                           let t1= args.(1) in
-                           let t2= args.(2) in
-                   (match (kind_of_term t0) with
-                         Const c ->
-                          (match (string_of_path c) with
-                             "Coq.Reals.Rdefinitions.R"->
+          | Cic.MutInd (u,i,o) ->
+              (match UriManager.string_of_uri u with 
+                "cic:/Coq/Init/Logic_Type/eqT.con" ->  
+                          let t0= arg1 in
+                           let arg1= arg2 in
+                           let arg2= List.hd(List.tl (List.tl next)) in
+                   (match t0 with
+                         Cic.Const (u,boh) ->
+                          (match UriManager.string_of_uri u with
+                             "cic:/Coq/Reals/Rdefinitions/R.con"->
                          [{hname=h;
                            htype="eqTLR";
-                          hleft=t1;
-                          hright=t2;
-                          hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
+                          hleft=arg1;
+                          hright=arg2;
+                          hflin= flin_minus (flin_of_term arg1)
+                                             (flin_of_term arg2);
                           hstrict=false};
                           {hname=h;
                            htype="eqTRL";
-                          hleft=t2;
-                          hright=t1;
-                          hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
+                          hleft=arg2;
+                          hright=arg1;
+                          hflin= flin_minus (flin_of_term arg2)
+                                             (flin_of_term arg1);
                           hstrict=false}]
                            |_-> assert false)
                          |_-> assert false)
                    |_-> assert false)
           |_-> assert false)
         |_-> assert false
-;;*)
+;;
+(* coq wrapper 
+let ineq1_of_constr = ineq1_of_term;;
+*)
 
 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 *)
 
-(*let fourier_lineq lineq1 = 
+let fourier_lineq lineq1 = 
    let nvar=ref (-1) in
    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
    List.iter (fun f ->
@@ -389,23 +401,23 @@ type hineq={hname:constr; (* le nom de l'hypoth
                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
              lineq1 in
    unsolvable sys
-;;*)
+;;
 
 (******************************************************************************
 Construction de la preuve en cas de succès de la méthode de Fourier,
 i.e. on obtient une contradiction.
 *)
 
-(*let is_int x = (x.den)=1
-;;*)
+let is_int x = (x.den)=1
+;;
 
 (* fraction = couple (num,den) *)
-(*let rec rational_to_fraction x= (x.num,x.den)
-;;*)
+let rec rational_to_fraction x= (x.num,x.den)
+;;
     
 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 *)
-(*let int_to_real n =
+let int_to_real n =
    let nn=abs n in
    let s=ref "" in
    if nn=0
@@ -414,13 +426,14 @@ i.e. on obtient une contradiction.
         for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
    if n<0 then s:="(Ropp "^(!s)^")";
    !s
-;;*)
+;;
+
 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 *)
-(*let rational_to_real x =
+let rational_to_real x =
    let (n,d)=rational_to_fraction x in
    ("(Rmult "^(int_to_real n)^" (Rinv "^(int_to_real d)^"))")
-;;*)
+;;
 
 (* preuve que 0<n*1/d
 *)