X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=f6f44e950fe961ce3c7b4f6bb8dd771447b1c1a9;hb=1e2b0bee559e543455ff839d969c5778d5c353bd;hp=17ff3f8fe732a37a923a6a3b2a91346ba7f98ccc;hpb=44fca010f5f7c9585c9530c4b6b30cd774b7cd1c;p=helm.git diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 17ff3f8fe..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,14 +507,17 @@ 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;*) debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n"); let sys= List.map (fun h-> let v=Array.create ((!nvar)+1) r0 in - Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c) + Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c) h.hflin.fhom; ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) lineq1 in @@ -847,7 +903,7 @@ let rec strip_outer_cast c = match c with | _ -> c ;; -let find_in_context id context = +(*let find_in_context id context = let rec find_in_context_aux c n = match c with [] -> failwith (id^" not found in context") @@ -865,10 +921,26 @@ let rec filter_real_hyp context cont = [] -> [] | Some(Cic.Name(h),Cic.Decl(t))::next -> ( let n = find_in_context h cont in + debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n"); [(Cic.Rel(n),t)] @ filter_real_hyp next cont) | a::next -> debug(" no\n"); filter_real_hyp next cont +;;*) +let filter_real_hyp context _ = + let rec filter_aux context num = + match context with + [] -> [] + | Some(Cic.Name(h),Cic.Decl(t))::next -> + ( + (*let n = find_in_context h cont in*) + debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n"); + [(Cic.Rel(num),t)] @ filter_aux next (num+1) + ) + | a::next -> filter_aux next (num+1) + in + filter_aux context 1 ;; + (* lifts everithing at the conclusion level *) let rec superlift c n= match c with @@ -1192,7 +1264,6 @@ theoreme,so let's parse our thesis *) let w1 = debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); (match ty with - (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*) Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) |_ -> assert false) in @@ -1203,14 +1274,6 @@ theoreme,so let's parse our thesis *) ) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) - (*tac:=(Tacticals.thens - ~start:(PrimitiveTactics.cut_tac ~term:_False) - ~continuations:[Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ~name:"??") - ~continuation:contradiction_tac - ;!tac]) FIXED - this was useless*) - (* tac:=!tac*) - |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*)