diff options
Diffstat (limited to 'plugins/micromega/csdpcert.ml')
| -rw-r--r-- | plugins/micromega/csdpcert.ml | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index b5c08300..b41f29c9 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,13 +12,11 @@ (* *) (************************************************************************) -open Big_int open Num open Sos open Sos_types open Sos_lib - module Mc = Micromega module Ml2C = Mutils.CamlToCoq module C2Ml = Mutils.CoqToCaml @@ -55,13 +53,12 @@ struct end open M -open List open Mutils -let rec canonical_sum_to_string = function s -> failwith "not implemented" +let canonical_sum_to_string = function s -> failwith "not implemented" let print_canonical_sum m = Format.print_string (canonical_sum_to_string m) @@ -122,7 +119,7 @@ let real_nonlinear_prover d l = match kd with | Axiom_lt i -> poly_mul p y | Axiom_eq i -> poly_mul (poly_pow p 2) y - | _ -> failwith "monoids") m (poly_const (Int 1)) , map snd m)) + | _ -> failwith "monoids") m (poly_const (Int 1)) , List.map snd m)) (sets_of_list neq) in let (cert_ideal, cert_cone,monoid) = deepen_until d (fun d -> @@ -130,10 +127,10 @@ let real_nonlinear_prover d l = real_positivnullstellensatz_general false d peq pge (poly_neg (fst m) ) in (ci,cc,snd m)) monoids) 0 in - let proofs_ideal = map2 (fun q i -> Eqmul(term_of_poly q,Axiom_eq i)) + let proofs_ideal = List.map2 (fun q i -> Eqmul(term_of_poly q,Axiom_eq i)) cert_ideal (List.map snd eq) in - let proofs_cone = map term_of_sos cert_cone in + let proofs_cone = List.map term_of_sos cert_cone in let proof_ne = let (neq , lt) = List.partition @@ -150,7 +147,7 @@ let real_nonlinear_prover d l = S (Some proof) with | Sos_lib.TooDeep -> S None - | x when x <> Sys.Break -> F (Printexc.to_string x) + | any -> F (Printexc.to_string any) (* This is somewhat buggy, over Z, strict inequality vanish... *) let pure_sos l = @@ -159,8 +156,8 @@ let pure_sos l = (* If there is no strict inequality, I should nonetheless be able to try something - over Z > is equivalent to -1 >= *) try - let l = List.combine l (interval 0 (length l -1)) in - let (lt,i) = try (List.find (fun (x,_) -> snd x = Mc.Strict) l) + let l = List.combine l (interval 0 (List.length l -1)) in + let (lt,i) = try (List.find (fun (x,_) -> Pervasives.(=) (snd x) Mc.Strict) l) with Not_found -> List.hd l in let plt = poly_neg (poly_of_term (expr_to_term (fst lt))) in let (n,polys) = sumofsquares plt in (* n * (ci * pi^2) *) @@ -174,7 +171,7 @@ let pure_sos l = S (Some proof) with (* | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *) - | x when x <> Sys.Break -> (* May be that could be refined *) S None + | any -> (* May be that could be refined *) S None |