X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=bb1c2febf583893ed8c81fe387908782c39b0d3f;hb=23886971f037b00a358d9b422aa0b3b40a75dc10;hp=d6d5fd34add30ad755bb73963fdb47689a504925;hpb=c6b222d016300d3b123a4d1863c048b950292844;p=helm.git diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index d6d5fd34a..bb1c2febf 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -25,6 +25,7 @@ (******************** OTHER USEFUL TACTICS **********************) +(* Galla: moved in variousTactics.ml let rewrite_tac ~term:equality ~status:(proof,goal) = let module C = Cic in @@ -85,6 +86,7 @@ let rewrite_simpl_tac ~term ~status = (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) ~status ;; +*) (******************** THE FOURIER TACTIC ***********************) @@ -146,11 +148,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 +198,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 +257,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 +291,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 +371,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 +509,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;*) @@ -717,7 +775,8 @@ let r = (*CSC: Patch to undo the over-simplification of RewriteSimpl *) Tacticals.then_ ~start: - (ReductionTactics.fold_tac ~also_in_hypotheses:false + (ReductionTactics.fold_tac ~reduction:CicReduction.whd + ~also_in_hypotheses:false ~term: (Cic.Appl [_Rle ; _R0 ; @@ -910,7 +969,7 @@ debug("inizio EQ\n"); 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) = - rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) + VariousTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ~status:((curi,metasenv',pbo,pty),goal) in let new_goals = fresh_meta::goals in @@ -944,9 +1003,10 @@ let assumption_tac ~status:(proof,goal)= (* !!!!! fix !!!!!!!!!! *) let contradiction_tac ~status:(proof,goal)= Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*) + (*inutile sia questo che quello prima della chiamata*) + ~start:PrimitiveTactics.intros_tac ~continuation:(Tacticals.then_ - ~start:(Ring.elim_type_tac ~term:_False) + ~start:(VariousTactics.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) ~status:(proof,goal) ;; @@ -984,10 +1044,11 @@ theoreme,so let's parse our thesis *) (* now let's change our thesis applying the th and put it with hp *) - let proof,gl = Tacticals.then_ - ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) - ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp) - ~status:(s_proof,s_goal) in + let proof,gl = + Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) + ~continuation:PrimitiveTactics.intros_tac + ~status:(s_proof,s_goal) in let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in