From 1e2b0bee559e543455ff839d969c5778d5c353bd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Nov 2002 11:19:36 +0000 Subject: [PATCH] bug in hypotesis parsing solved --- helm/gTopLevel/esempi/fourier.cic | 41 +++++++++++++++- helm/gTopLevel/fourier.ml | 12 +++-- helm/gTopLevel/fourierR.ml | 82 ++++++++++++++++++++++++++----- 3 files changed, 116 insertions(+), 19 deletions(-) diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic index ba51e64ad..d2f9e4983 100644 --- a/helm/gTopLevel/esempi/fourier.cic +++ b/helm/gTopLevel/esempi/fourier.cic @@ -14,7 +14,13 @@ alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 alias not /Coq/Init/Logic/not.con alias or /Coq/Init/Logic/or.ind#1/1 -(*test real*) +//baco +!x:R. +(Rlt (Rmult(Ropp x)R1) +R0) +->(Rlt R0 x) + +// test 3x4 -> 35'' !x:R.!y:R.!z:R. (Rge (Rplus @@ -44,6 +50,39 @@ alias or /Coq/Init/Logic/or.ind#1/1 -> (Rlt z R1) +// test 6x6 -> + +!x:R.!y:R.!z:R.!t:R.!u:R.!v:R. +(Rgt +(Rplus (Ropp x) (Rplus y (Rplus z (Rplus t (Rplus u (Rplus v (Rplus R1 R1))))))) + R0) +-> +(Rgt +(Rplus x (Rplus (Ropp y) (Rplus (Ropp z) (Rplus (Ropp t) (Rplus (Ropp u) (Rplus R1 R1)))))) + R0) +-> +(Rgt +(Rplus y (Rplus (Ropp z) (Rplus t (Rplus u (Rplus R1 R1))))) + R0) +-> +(Rgt +(Rplus y (Rplus z (Rplus (Ropp t) (Rplus (Ropp (Rmult (Rplus R1 R1)v)) (Rplus R1 R1))))) + R0) +-> +(Rgt +(Rplus y (Rplus z (Rplus t (Rplus (Ropp u) (Rplus R1 R1))))) + R0) +-> +(Rlt +(Rplus (Rmult (Rplus R1 R1) x) (Rplus v y)) + R0) +-> (Rlt (Rmult (Rplus R1 R1) x) R0) + + + + + + //test base1 ok !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml index 3704bf67b..d7728c0b3 100644 --- a/helm/gTopLevel/fourier.ml +++ b/helm/gTopLevel/fourier.ml @@ -171,12 +171,14 @@ let deduce_add lneg lpos = (* élimination de la première variable à partir d'une liste d'inéquations: opération qu'on itère dans l'algorithme de Fourier. *) -let deduce1 s = +let deduce1 s i= match (partitionne s) with [lneg;lnul;lpos] -> - let lnew = deduce_add lneg lpos in - (List.map ie_tl lnul)@lnew - |_->assert false + let lnew = deduce_add lneg lpos in + (match lneg with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->(); + match lpos with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->()); + (List.map ie_tl lnul)@lnew + |_->assert false ;; (* algorithme de Fourier: on élimine successivement toutes les variables. *) @@ -184,7 +186,7 @@ let deduce lie = let n = List.length (fst (List.hd lie)) in let lie=ref (add_hist lie) in for i=1 to n-1 do - lie:= deduce1 !lie; + lie:= deduce1 !lie i; done; !lie ;; diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index d6d5fd34a..f6f44e950 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -146,11 +146,18 @@ let flin_coef f x = @param c a rational @return the new flin *) -let flin_add f x c = - let cx = flin_coef f x in - Hashtbl.remove f.fhom x; - Hashtbl.add f.fhom x (rplus cx c); - f +let flin_add f x c = + match x with + Cic.Rel(n) ->( + let cx = flin_coef f x in + Hashtbl.remove f.fhom x; + Hashtbl.add f.fhom x (rplus cx c); + f) + |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n"); + let cx = flin_coef f x in + Hashtbl.remove f.fhom x; + Hashtbl.add f.fhom x (rplus cx c); + f ;; (** Adds c to f.fcste @@ -189,7 +196,7 @@ let flin_minus f1 f2 = ;; (** - @return f times a + @return a times f *) let flin_emult a f = let f2 = flin_zero() in @@ -248,7 +255,13 @@ let rec rational_of_term t = (* coq wrapper let rational_of_const = rational_of_term;; *) - +let fails f a = + try + let tmp = (f a) in + false + with + _-> true + ;; let rec flin_of_term t = let fl_of_binop f l = @@ -276,19 +289,59 @@ let rec flin_of_term t = let arg1 = (List.hd next) and arg2 = (List.hd(List.tl next)) in - try + if fails rational_of_term arg1 + then + if fails rational_of_term arg2 + then + ( (* prodotto tra 2 incognite ????? impossibile*) + failwith "Sistemi lineari!!!!\n" + ) + else + ( + match arg1 with + Cic.Rel(n) -> (*trasformo al volo*) + (flin_add (flin_zero()) arg1 (rational_of_term arg2)) + |_-> (* test this *) + let tmp = flin_of_term arg1 in + flin_emult (rational_of_term arg2) (tmp) + ) + else + if fails rational_of_term arg2 + then + ( + match arg2 with + Cic.Rel(n) -> (*trasformo al volo*) + (flin_add (flin_zero()) arg2 (rational_of_term arg1)) + |_-> (* test this *) + let tmp = flin_of_term arg2 in + flin_emult (rational_of_term arg1) (tmp) + + ) + else + ( (*prodotto tra razionali*) + (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2))) + ) + (*try begin - let a = rational_of_term arg1 in + (*let a = rational_of_term arg1 in + debug("ho fatto rational of term di "^CicPp.ppterm arg1^ + " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*) + let a = flin_of_term arg1 try begin let b = (rational_of_term arg2) in + debug("ho fatto rational of term di "^CicPp.ppterm arg2^ + " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n"); (flin_add_cste (flin_zero()) (rmult a b)) end with - _ -> (flin_add (flin_zero()) arg2 a) + _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n"); + (flin_add (flin_zero()) arg2 a) end with - _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2)) + _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n"); + (flin_add(flin_zero()) arg1 (rational_of_term arg2)) + *) end |"cic:/Coq/Reals/Rdefinitions/Rinv.con"-> let a=(rational_of_term (List.hd next)) in @@ -316,7 +369,7 @@ let rec flin_of_term t = |_-> assert false end |_-> assert false) - with _ -> flin_add (flin_zero()) t r1 + with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1 ;; (* coq wrapper @@ -454,7 +507,10 @@ let fourier_lineq lineq1 = Hashtbl.iter (fun x c -> try (Hashtbl.find hvar x;()) with _-> nvar:=(!nvar)+1; - Hashtbl.add hvar x (!nvar)) + Hashtbl.add hvar x (!nvar); + debug("aggiungo una var "^ + string_of_int !nvar^" per "^ + CicPp.ppterm x^"\n")) f.hflin.fhom) lineq1; (*print_hash hvar;*) -- 2.39.2