@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
;;
(**
- @return f times a
+ @return a times f
*)
let flin_emult a f =
let f2 = flin_zero() in
(* 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 =
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
|_-> 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
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
| _ -> 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")
[] -> []
| 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
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
)
~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*)
projects / helm.git / blobdiff