From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/certificate.ml | 358 +++++++++++++++++++-------------------- 1 file changed, 179 insertions(+), 179 deletions(-) (limited to 'plugins/micromega/certificate.ml') diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 2a1c2fe22..c5760229c 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -47,28 +47,28 @@ struct (* A monomial is represented by a multiset of variables *) module Map = Map.Make(struct type t = var let compare = Pervasives.compare end) open Map - + type t = int Map.t (* The monomial that corresponds to a constant *) let const = Map.empty - + (* The monomial 'x' *) let var x = Map.add x 1 Map.empty (* Get the degre of a variable in a monomial *) let find x m = try find x m with Not_found -> 0 - + (* Multiply a monomial by a variable *) let mult x m = add x ( (find x m) + 1) m - + (* Product of monomials *) let prod m1 m2 = Map.fold (fun k d m -> add k ((find k m) + d) m) m1 m2 - + (* Total ordering of monomials *) let compare m1 m2 = Map.compare Pervasives.compare m1 m2 - let pp o m = Map.iter (fun k v -> + let pp o m = Map.iter (fun k v -> if v = 1 then Printf.fprintf o "x%i." (C2Ml.index k) else Printf.fprintf o "x%i^%i." (C2Ml.index k) v) m @@ -79,8 +79,8 @@ end module Poly : (* A polynomial is a map of monomials *) - (* - This is probably a naive implementation + (* + This is probably a naive implementation (expected to be fast enough - Coq is probably the bottleneck) *The new ring contribution is using a sparse Horner representation. *) @@ -106,22 +106,22 @@ struct type t = num P.t - let pp o p = P.iter (fun k v -> + let pp o p = P.iter (fun k v -> if compare_num v (Int 0) <> 0 - then + then if Monomial.compare Monomial.const k = 0 then Printf.fprintf o "%s " (string_of_num v) - else Printf.fprintf o "%s*%a " (string_of_num v) Monomial.pp k) p + else Printf.fprintf o "%s*%a " (string_of_num v) Monomial.pp k) p (* Get the coefficient of monomial mn *) - let get : Monomial.t -> t -> num = + let get : Monomial.t -> t -> num = fun mn p -> try find mn p with Not_found -> (Int 0) (* The polynomial 1.x *) let variable : var -> t = fun x -> add (Monomial.var x) (Int 1) empty - + (*The constant polynomial *) let constant : num -> t = fun c -> add (Monomial.const) c empty @@ -129,27 +129,27 @@ struct (* The addition of a monomial *) let add : Monomial.t -> num -> t -> t = - fun mn v p -> + fun mn v p -> let vl = (get mn p) <+> v in add mn vl p - (** Design choice: empty is not a polynomial - I do not remember why .... + (** Design choice: empty is not a polynomial + I do not remember why .... **) (* The product by a monomial *) let mult : Monomial.t -> num -> t -> t = - fun mn v p -> + fun mn v p -> fold (fun mn' v' res -> P.add (Monomial.prod mn mn') (v<*>v') res) p empty let addition : t -> t -> t = fun p1 p2 -> fold (fun mn v p -> add mn v p) p1 p2 - + let product : t -> t -> t = - fun p1 p2 -> + fun p1 p2 -> fold (fun mn v res -> addition (mult mn v p2) res ) p1 empty @@ -181,7 +181,7 @@ let z_spec = { mult = Mc.zmult; eqb = Mc.zeq_bool } - + let q_spec = { bigint_to_number = (fun x -> {Mc.qnum = Ml2C.bigint x; Mc.qden = Mc.XH}); @@ -198,53 +198,53 @@ let r_spec = z_spec let dev_form n_spec p = - let rec dev_form p = + let rec dev_form p = match p with | Mc.PEc z -> Poly.constant (n_spec.number_to_num z) | Mc.PEX v -> Poly.variable v - | Mc.PEmul(p1,p2) -> + | Mc.PEmul(p1,p2) -> let p1 = dev_form p1 in let p2 = dev_form p2 in - Poly.product p1 p2 + Poly.product p1 p2 | Mc.PEadd(p1,p2) -> Poly.addition (dev_form p1) (dev_form p2) | Mc.PEopp p -> Poly.uminus (dev_form p) | Mc.PEsub(p1,p2) -> Poly.addition (dev_form p1) (Poly.uminus (dev_form p2)) - | Mc.PEpow(p,n) -> + | Mc.PEpow(p,n) -> let p = dev_form p in let n = C2Ml.n n in - let rec pow n = - if n = 0 + let rec pow n = + if n = 0 then Poly.constant (n_spec.number_to_num n_spec.unit) else Poly.product p (pow (n-1)) in pow n in dev_form p -let monomial_to_polynomial mn = - Monomial.fold - (fun v i acc -> +let monomial_to_polynomial mn = + Monomial.fold + (fun v i acc -> let mn = if i = 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in if acc = Mc.PEc (Mc.Zpos Mc.XH) - then mn + then mn else Mc.PEmul(mn,acc)) - mn + mn (Mc.PEc (Mc.Zpos Mc.XH)) - -let list_to_polynomial vars l = + +let list_to_polynomial vars l = assert (List.for_all (fun x -> ceiling_num x =/ x) l); - let var x = monomial_to_polynomial (List.nth vars x) in + let var x = monomial_to_polynomial (List.nth vars x) in let rec xtopoly p i = function | [] -> p - | c::l -> if c =/ (Int 0) then xtopoly p (i+1) l + | c::l -> if c =/ (Int 0) then xtopoly p (i+1) l else let c = Mc.PEc (Ml2C.bigint (numerator c)) in - let mn = + let mn = if c = Mc.PEc (Mc.Zpos Mc.XH) then var i else Mc.PEmul (c,var i) in let p' = if p = Mc.PEc Mc.Z0 then mn else Mc.PEadd (mn, p) in xtopoly p' (i+1) l in - + xtopoly (Mc.PEc Mc.Z0) 0 l let rec fixpoint f x = @@ -259,54 +259,54 @@ let rec fixpoint f x = -let rec_simpl_cone n_spec e = - let simpl_cone = +let rec_simpl_cone n_spec e = + let simpl_cone = Mc.simpl_cone n_spec.zero n_spec.unit n_spec.mult n_spec.eqb in let rec rec_simpl_cone = function - | Mc.PsatzMulE(t1, t2) -> + | Mc.PsatzMulE(t1, t2) -> simpl_cone (Mc.PsatzMulE (rec_simpl_cone t1, rec_simpl_cone t2)) - | Mc.PsatzAdd(t1,t2) -> + | Mc.PsatzAdd(t1,t2) -> simpl_cone (Mc.PsatzAdd (rec_simpl_cone t1, rec_simpl_cone t2)) | x -> simpl_cone x in rec_simpl_cone e - - + + let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c - -type cone_prod = - Const of cone - | Ideal of cone *cone - | Mult of cone * cone + +type cone_prod = + Const of cone + | Ideal of cone *cone + | Mult of cone * cone | Other of cone and cone = Mc.zWitness let factorise_linear_cone c = - - let rec cone_list c l = + + let rec cone_list c l = match c with | Mc.PsatzAdd (x,r) -> cone_list r (x::l) | _ -> c :: l in - + let factorise c1 c2 = match c1 , c2 with - | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> + | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> if x = x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None - | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> + | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> if x = x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None | _ -> None in - + let rec rebuild_cone l pending = match l with | [] -> (match pending with | None -> Mc.PsatzZ | Some p -> p ) - | e::l -> + | e::l -> (match pending with - | None -> rebuild_cone l (Some e) + | None -> rebuild_cone l (Some e) | Some p -> (match factorise p e with | None -> Mc.PsatzAdd(p, rebuild_cone l (Some e)) | Some f -> rebuild_cone l (Some f) ) @@ -316,15 +316,15 @@ let factorise_linear_cone c = -(* The binding with Fourier might be a bit obsolete +(* The binding with Fourier might be a bit obsolete -- how does it handle equalities ? *) (* Certificates are elements of the cone such that P = 0 *) (* To begin with, we search for certificates of the form: - a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0 + a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0 where pi >= 0 qi > 0 - ai >= 0 + ai >= 0 bi >= 0 Sum bi + c >= 1 This is a linear problem: each monomial is considered as a variable. @@ -343,96 +343,96 @@ open Mfourier (* fold_left followed by a rev ! *) -let constrain_monomial mn l = +let constrain_monomial mn l = let coeffs = List.fold_left (fun acc p -> (Poly.get mn p)::acc) [] l in if mn = Monomial.const - then - { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; - op = Eq ; + then + { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; + op = Eq ; cst = Big_int zero_big_int } else - { coeffs = Vect.from_list ((Big_int zero_big_int):: (List.rev coeffs)) ; - op = Eq ; + { coeffs = Vect.from_list ((Big_int zero_big_int):: (List.rev coeffs)) ; + op = Eq ; cst = Big_int zero_big_int } - -let positivity l = - let rec xpositivity i l = + +let positivity l = + let rec xpositivity i l = match l with | [] -> [] | (_,Mc.Equal)::l -> xpositivity (i+1) l - | (_,_)::l -> - {coeffs = Vect.update (i+1) (fun _ -> Int 1) Vect.null ; - op = Ge ; + | (_,_)::l -> + {coeffs = Vect.update (i+1) (fun _ -> Int 1) Vect.null ; + op = Ge ; cst = Int 0 } :: (xpositivity (i+1) l) in xpositivity 0 l let string_of_op = function - | Mc.Strict -> "> 0" - | Mc.NonStrict -> ">= 0" + | Mc.Strict -> "> 0" + | Mc.NonStrict -> ">= 0" | Mc.Equal -> "= 0" | Mc.NonEqual -> "<> 0" -(* If the certificate includes at least one strict inequality, +(* If the certificate includes at least one strict inequality, the obtained polynomial can also be 0 *) let build_linear_system l = (* Gather the monomials: HINT add up of the polynomials *) let l' = List.map fst l in - let monomials = + let monomials = List.fold_left (fun acc p -> Poly.addition p acc) (Poly.constant (Int 0)) l' in (* For each monomial, compute a constraint *) - let s0 = + let s0 = Poly.fold (fun mn _ res -> (constrain_monomial mn l')::res) monomials [] in (* I need at least something strictly positive *) let strict = { coeffs = Vect.from_list ((Big_int unit_big_int):: - (List.map (fun (x,y) -> - match y with Mc.Strict -> - Big_int unit_big_int + (List.map (fun (x,y) -> + match y with Mc.Strict -> + Big_int unit_big_int | _ -> Big_int zero_big_int) l)); op = Ge ; cst = Big_int unit_big_int } in (* Add the positivity constraint *) - {coeffs = Vect.from_list ([Big_int unit_big_int]) ; - op = Ge ; + {coeffs = Vect.from_list ([Big_int unit_big_int]) ; + op = Ge ; cst = Big_int zero_big_int}::(strict::(positivity l)@s0) let big_int_to_z = Ml2C.bigint - -(* For Q, this is a pity that the certificate has been scaled + +(* For Q, this is a pity that the certificate has been scaled -- at a lower layer, certificates are using nums... *) -let make_certificate n_spec (cert,li) = +let make_certificate n_spec (cert,li) = let bint_to_cst = n_spec.bigint_to_number in match cert with | [] -> failwith "empty_certificate" - | e::cert' -> + | e::cert' -> let cst = match compare_big_int e zero_big_int with | 0 -> Mc.PsatzZ - | 1 -> Mc.PsatzC (bint_to_cst e) - | _ -> failwith "positivity error" + | 1 -> Mc.PsatzC (bint_to_cst e) + | _ -> failwith "positivity error" in let rec scalar_product cert l = match cert with | [] -> Mc.PsatzZ | c::cert -> match l with | [] -> failwith "make_certificate(1)" - | i::l -> + | i::l -> let r = scalar_product cert l in match compare_big_int c zero_big_int with | -1 -> Mc.PsatzAdd ( - Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), + Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), r) | 0 -> r | _ -> Mc.PsatzAdd ( Mc.PsatzMulE (Mc.PsatzC (bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), r) in - - ((factorise_linear_cone + + ((factorise_linear_cone (simplify_cone n_spec (Mc.PsatzAdd (cst, scalar_product cert' li))))) @@ -440,59 +440,59 @@ exception Found of Monomial.t exception Strict -let primal l = +let primal l = let vr = ref 0 in let module Mmn = Map.Make(Monomial) in let vect_of_poly map p = - Poly.fold (fun mn vl (map,vect) -> - if mn = Monomial.const + Poly.fold (fun mn vl (map,vect) -> + if mn = Monomial.const then (map,vect) - else + else let (mn,m) = try (Mmn.find mn map,map) with Not_found -> let res = (!vr, Mmn.add mn !vr map) in incr vr ; res in (m,if sign_num vl = 0 then vect else (mn,vl)::vect)) p (map,[]) in - + let op_op = function Mc.NonStrict -> Ge |Mc.Equal -> Eq | _ -> raise Strict in let cmp x y = Pervasives.compare (fst x) (fst y) in snd (List.fold_right (fun (p,op) (map,l) -> - let (mp,vect) = vect_of_poly map p in + let (mp,vect) = vect_of_poly map p in let cstr = {coeffs = List.sort cmp vect; op = op_op op ; cst = minus_num (Poly.get Monomial.const p)} in (mp,cstr::l)) l (Mmn.empty,[])) -let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = +let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = (* List.iter (fun (p,op) -> Printf.fprintf stdout "%a %s 0\n" Poly.pp p (string_of_op op) ) l ; *) - - + + let sys = build_linear_system l in - try + try match Fourier.find_point sys with | Inr _ -> None - | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) + | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) (* should not use rats_to_ints *) - with x -> - if debug - then (Printf.printf "raw certificate %s" (Printexc.to_string x); + with x -> + if debug + then (Printf.printf "raw certificate %s" (Printexc.to_string x); flush stdout) ; None -let raw_certificate l = - try +let raw_certificate l = + try let p = primal l in match Fourier.find_point p with - | Inr prf -> - if debug then Printf.printf "AProof : %a\n" pp_proof prf ; + | Inr prf -> + if debug then Printf.printf "AProof : %a\n" pp_proof prf ; let cert = List.map (fun (x,n) -> x+1,n) (fst (List.hd (Proof.mk_proof p prf))) in - if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; + if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; Some (rats_to_ints (Vect.to_list cert)) | Inl _ -> None - with Strict -> + with Strict -> (* Fourier elimination should handle > *) - dual_raw_certificate l + dual_raw_certificate l let simple_linear_prover (*to_constant*) l = @@ -500,26 +500,26 @@ let simple_linear_prover (*to_constant*) l = match raw_certificate lc with | None -> None (* No certificate *) | Some cert -> (* make_certificate to_constant*)Some (cert,li) - - + + let linear_prover n_spec l = let li = List.combine l (interval 0 (List.length l -1)) in - let (l1,l') = List.partition + let (l1,l') = List.partition (fun (x,_) -> if snd x = Mc.NonEqual then true else false) li in - let l' = List.map + let l' = List.map (fun ((x,y),i) -> match y with Mc.NonEqual -> failwith "cannot happen" | y -> ((dev_form n_spec x, y),i)) l' in - - simple_linear_prover (*n_spec*) l' + + simple_linear_prover (*n_spec*) l' let linear_prover n_spec l = try linear_prover n_spec l with x -> (print_string (Printexc.to_string x); None) -let linear_prover_with_cert spec l = +let linear_prover_with_cert spec l = match linear_prover spec l with | None -> None | Some cert -> Some (make_certificate spec cert) @@ -529,21 +529,21 @@ let linear_prover_with_cert spec l = (* zprover.... *) (* I need to gather the set of variables ---> - Then go for fold + Then go for fold Once I have an interval, I need a certificate : 2 other fourier elims. - (I could probably get the certificate directly + (I could probably get the certificate directly as it is done in the fourier contrib.) *) let make_linear_system l = let l' = List.map fst l in - let monomials = List.fold_left (fun acc p -> Poly.addition p acc) + let monomials = List.fold_left (fun acc p -> Poly.addition p acc) (Poly.constant (Int 0)) l' in - let monomials = Poly.fold + let monomials = Poly.fold (fun mn _ l -> if mn = Monomial.const then l else mn::l) monomials [] in - (List.map (fun (c,op) -> - {coeffs = Vect.from_list (List.map (fun mn -> (Poly.get mn c)) monomials) ; - op = op ; + (List.map (fun (c,op) -> + {coeffs = Vect.from_list (List.map (fun mn -> (Poly.get mn c)) monomials) ; + op = op ; cst = minus_num ( (Poly.get Monomial.const c))}) l ,monomials) @@ -552,106 +552,106 @@ let pplus x y = Mc.PEadd(x,y) let pmult x y = Mc.PEmul(x,y) let pconst x = Mc.PEc x let popp x = Mc.PEopp x - + let debug = false - + (* keep track of enumerated vectors *) -let rec mem p x l = +let rec mem p x l = match l with [] -> false | e::l -> if p x e then true else mem p x l -let rec remove_assoc p x l = +let rec remove_assoc p x l = match l with [] -> [] | e::l -> if p x (fst e) then - remove_assoc p x l else e::(remove_assoc p x l) + remove_assoc p x l else e::(remove_assoc p x l) let eq x y = Vect.compare x y = 0 let remove e l = List.fold_left (fun l x -> if eq x e then l else x::l) [] l -(* The prover is (probably) incomplete -- +(* The prover is (probably) incomplete -- only searching for naive cutting planes *) -let candidates sys = +let candidates sys = let ll = List.fold_right ( fun (e,k) r -> - match k with + match k with | Mc.NonStrict -> (dev_form z_spec e , Ge)::r - | Mc.Equal -> (dev_form z_spec e , Eq)::r + | Mc.Equal -> (dev_form z_spec e , Eq)::r (* we already know the bound -- don't compute it again *) | _ -> failwith "Cannot happen candidates") sys [] in let (sys,var_mn) = make_linear_system ll in let vars = mapi (fun _ i -> Vect.set i (Int 1) Vect.null) var_mn in - (List.fold_left (fun l cstr -> + (List.fold_left (fun l cstr -> let gcd = Big_int (Vect.gcd cstr.coeffs) in - if gcd =/ (Int 1) && cstr.op = Eq - then l + if gcd =/ (Int 1) && cstr.op = Eq + then l else (Vect.mul (Int 1 // gcd) cstr.coeffs)::l) [] sys) @ vars -let rec xzlinear_prover planes sys = +let rec xzlinear_prover planes sys = match linear_prover z_spec sys with | Some prf -> Some (Mc.RatProof (make_certificate z_spec prf,Mc.DoneProof)) | None -> (* find the candidate with the smallest range *) (* Grrr - linear_prover is also calling 'make_linear_system' *) let ll = List.fold_right (fun (e,k) r -> match k with - Mc.NonEqual -> r - | k -> (dev_form z_spec e , + Mc.NonEqual -> r + | k -> (dev_form z_spec e , match k with - Mc.NonStrict -> Ge + Mc.NonStrict -> Ge | Mc.Equal -> Eq | Mc.Strict | Mc.NonEqual -> failwith "Cannot happen") :: r) sys [] in let (ll,var) = make_linear_system ll in - let candidates = List.fold_left (fun acc vect -> + let candidates = List.fold_left (fun acc vect -> match Fourier.optimise vect ll with | None -> acc - | Some i -> + | Some i -> (* Printf.printf "%s in %s\n" (Vect.string vect) (string_of_intrvl i) ; *) - flush stdout ; + flush stdout ; (vect,i) ::acc) [] planes in - let smallest_interval = - match List.fold_left (fun (x1,i1) (x2,i2) -> - if Itv.smaller_itv i1 i2 - then (x1,i1) else (x2,i2)) (Vect.null,(None,None)) candidates + let smallest_interval = + match List.fold_left (fun (x1,i1) (x2,i2) -> + if Itv.smaller_itv i1 i2 + then (x1,i1) else (x2,i2)) (Vect.null,(None,None)) candidates with | (x,(Some i, Some j)) -> Some(i,x,j) | x -> None (* This might be a cutting plane *) in match smallest_interval with - | Some (lb,e,ub) -> - let (lbn,lbd) = + | Some (lb,e,ub) -> + let (lbn,lbd) = (Ml2C.bigint (sub_big_int (numerator lb) unit_big_int), Ml2C.bigint (denominator lb)) in - let (ubn,ubd) = - (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) , + let (ubn,ubd) = + (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) , Ml2C.bigint (denominator ub)) in let expr = list_to_polynomial var (Vect.to_list e) in - (match + (match (*x <= ub -> x > ub *) - linear_prover z_spec + linear_prover z_spec ((pplus (pmult (pconst ubd) expr) (popp (pconst ubn)), Mc.NonStrict) :: sys), (* lb <= x -> lb > x *) - linear_prover z_spec + linear_prover z_spec ((pplus (popp (pmult (pconst lbd) expr)) (pconst lbn), - Mc.NonStrict)::sys) + Mc.NonStrict)::sys) with - | Some cub , Some clb -> - (match zlinear_enum (remove e planes) expr - (ceiling_num lb) (floor_num ub) sys + | Some cub , Some clb -> + (match zlinear_enum (remove e planes) expr + (ceiling_num lb) (floor_num ub) sys with | None -> None - | Some prf -> - let bound_proof (c,l) = make_certificate z_spec (List.tl c , List.tl (List.map (fun x -> x -1) l)) in - + | Some prf -> + let bound_proof (c,l) = make_certificate z_spec (List.tl c , List.tl (List.map (fun x -> x -1) l)) in + Some (Mc.EnumProof((*Ml2C.q lb,expr,Ml2C.q ub,*) bound_proof clb, bound_proof cub,prf))) | _ -> None ) | _ -> None -and zlinear_enum planes expr clb cub l = +and zlinear_enum planes expr clb cub l = if clb >/ cub then Some [] else @@ -665,9 +665,9 @@ and zlinear_enum planes expr clb cub l = | None -> None | Some prfl -> Some (prf :: prfl) -let zlinear_prover sys = +let zlinear_prover sys = let candidates = candidates sys in - (* Printf.printf "candidates %d" (List.length candidates) ; *) + (* Printf.printf "candidates %d" (List.length candidates) ; *) (*let t0 = Sys.time () in*) let res = xzlinear_prover candidates sys in (*Printf.printf "Time prover : %f" (Sys.time () -. t0) ;*) res @@ -675,7 +675,7 @@ let zlinear_prover sys = open Sos_types open Mutils -let rec scale_term t = +let rec scale_term t = match t with | Zero -> unit_big_int , Zero | Const n -> (denominator n) , Const (Big_int (numerator n)) @@ -708,7 +708,7 @@ let get_index_of_ith_match f i l = match l with | [] -> failwith "bad index" | e::l -> if f e - then + then (if j = i then res else get (j+1) (res+1) l ) else get j (res+1) l in get 0 0 l @@ -722,19 +722,19 @@ let rec scale_certificate pos = match pos with | Rational_eq n -> (denominator n) , Rational_eq (Big_int (numerator n)) | Rational_le n -> (denominator n) , Rational_le (Big_int (numerator n)) | Rational_lt n -> (denominator n) , Rational_lt (Big_int (numerator n)) - | Square t -> let s,t' = scale_term t in + | Square t -> let s,t' = scale_term t in mult_big_int s s , Square t' | Eqmul (t, y) -> let s1,y1 = scale_term t and s2,y2 = scale_certificate y in mult_big_int s1 s2 , Eqmul (y1,y2) - | Sum (y, z) -> let s1,y1 = scale_certificate y + | Sum (y, z) -> let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in let g = gcd_big_int s1 s2 in let s1' = div_big_int s1 g in let s2' = div_big_int s2 g in - mult_big_int g (mult_big_int s1' s2'), + mult_big_int g (mult_big_int s1' s2'), Sum (Product(Rational_le (Big_int s2'), y1), Product (Rational_le (Big_int s1'), y2)) - | Product (y, z) -> + | Product (y, z) -> let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in mult_big_int s1 s2 , Product (y1,y2) @@ -743,7 +743,7 @@ open Micromega let rec term_to_q_expr = function | Const n -> PEc (Ml2C.q n) | Zero -> PEc ( Ml2C.q (Int 0)) - | Var s -> PEX (Ml2C.index + | Var s -> PEX (Ml2C.index (int_of_string (String.sub s 1 (String.length s - 1)))) | Mul(p1,p2) -> PEmul(term_to_q_expr p1, term_to_q_expr p2) | Add(p1,p2) -> PEadd(term_to_q_expr p1, term_to_q_expr p2) @@ -755,20 +755,20 @@ open Micromega let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e) - let rec product l = + let rec product l = match l with | [] -> Mc.PsatzZ | [i] -> Mc.PsatzIn (Ml2C.nat i) | i ::l -> Mc.PsatzMulE(Mc.PsatzIn (Ml2C.nat i), product l) -let q_cert_of_pos pos = +let q_cert_of_pos pos = let rec _cert_of_pos = function Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_le i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l - | Rational_eq n | Rational_le n | Rational_lt n -> + | Rational_eq n | Rational_le n | Rational_lt n -> if compare_num n (Int 0) = 0 then Mc.PsatzZ else Mc.PsatzC (Ml2C.q n) | Square t -> Mc.PsatzSquare (term_to_q_pol t) @@ -781,7 +781,7 @@ let q_cert_of_pos pos = let rec term_to_z_expr = function | Const n -> PEc (Ml2C.bigint (big_int_of_num n)) | Zero -> PEc ( Z0) - | Var s -> PEX (Ml2C.index + | Var s -> PEX (Ml2C.index (int_of_string (String.sub s 1 (String.length s - 1)))) | Mul(p1,p2) -> PEmul(term_to_z_expr p1, term_to_z_expr p2) | Add(p1,p2) -> PEadd(term_to_z_expr p1, term_to_z_expr p2) @@ -792,14 +792,14 @@ let q_cert_of_pos pos = let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.zplus Mc.zmult Mc.zminus Mc.zopp Mc.zeq_bool (term_to_z_expr e) -let z_cert_of_pos pos = +let z_cert_of_pos pos = let s,pos = (scale_certificate pos) in let rec _cert_of_pos = function Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_le i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l - | Rational_eq n | Rational_le n | Rational_lt n -> + | Rational_eq n | Rational_le n | Rational_lt n -> if compare_num n (Int 0) = 0 then Mc.PsatzZ else Mc.PsatzC (Ml2C.bigint (big_int_of_num n)) | Square t -> Mc.PsatzSquare (term_to_z_pol t) -- cgit v1.2.3