diff options
Diffstat (limited to 'plugins/micromega')
29 files changed, 585 insertions, 640 deletions
diff --git a/plugins/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v deleted file mode 100644 index 04336747..00000000 --- a/plugins/micromega/CheckerMaker.v +++ /dev/null @@ -1,132 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* *) -(* Micromega: A reflexive tactic using the Positivstellensatz *) -(* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) -(* *) -(************************************************************************) - -(* FK: scheduled for deletion *) -(* -Require Import Setoid. -Require Import Decidable. -Require Import List. -Require Import Refl. - -Set Implicit Arguments. - -Section CheckerMaker. - -(* 'Formula' is a syntactic representation of a certain kind of propositions. *) -Variable Formula : Type. - -Variable Env : Type. - -Variable eval : Env -> Formula -> Prop. - -Variable Formula' : Type. - -Variable eval' : Env -> Formula' -> Prop. - -Variable normalise : Formula -> Formula'. - -Variable negate : Formula -> Formula'. - -Hypothesis normalise_sound : - forall (env : Env) (t : Formula), eval env t -> eval' env (normalise t). - -Hypothesis negate_correct : - forall (env : Env) (t : Formula), eval env t <-> ~ (eval' env (negate t)). - -Variable Witness : Type. - -Variable check_formulas' : list Formula' -> Witness -> bool. - -Hypothesis check_formulas'_sound : - forall (l : list Formula') (w : Witness), - check_formulas' l w = true -> - forall env : Env, make_impl (eval' env) l False. - -Definition normalise_list : list Formula -> list Formula' := map normalise. -Definition negate_list : list Formula -> list Formula' := map negate. - -Definition check_formulas (l : list Formula) (w : Witness) : bool := - check_formulas' (map normalise l) w. - -(* Contraposition of normalise_sound for lists *) -Lemma normalise_sound_contr : forall (env : Env) (l : list Formula), - make_impl (eval' env) (map normalise l) False -> make_impl (eval env) l False. -Proof. -intros env l; induction l as [| t l IH]; simpl in *. -trivial. -intros H1 H2. apply IH. apply H1. now apply normalise_sound. -Qed. - -Theorem check_formulas_sound : - forall (l : list Formula) (w : Witness), - check_formulas l w = true -> forall env : Env, make_impl (eval env) l False. -Proof. -unfold check_formulas; intros l w H env. destruct l as [| t l]; simpl in *. -pose proof (check_formulas'_sound H env) as H1; now simpl in H1. -intro H1. apply normalise_sound in H1. -pose proof (check_formulas'_sound H env) as H2; simpl in H2. -apply H2 in H1. now apply normalise_sound_contr. -Qed. - -(* In check_conj_formulas', t2 is supposed to be a list of negations of -formulas. If, for example, t1 = [A1, A2] and t2 = [~ B1, ~ B2], then -check_conj_formulas' checks that each of [~ B1, A1, A2] and [~ B2, A1, A2] is -inconsistent. This means that A1 /\ A2 -> B1 and A1 /\ A2 -> B1, i.e., that -A1 /\ A2 -> B1 /\ B2. *) - -Fixpoint check_conj_formulas' - (t1 : list Formula') (wits : list Witness) (t2 : list Formula') {struct wits} : bool := -match t2 with -| nil => true -| t':: rt2 => - match wits with - | nil => false - | w :: rwits => - match check_formulas' (t':: t1) w with - | true => check_conj_formulas' t1 rwits rt2 - | false => false - end - end -end. - -(* checks whether the conjunction of t1 implies the conjunction of t2 *) - -Definition check_conj_formulas - (t1 : list Formula) (wits : list Witness) (t2 : list Formula) : bool := - check_conj_formulas' (normalise_list t1) wits (negate_list t2). - -Theorem check_conj_formulas_sound : - forall (t1 : list Formula) (t2 : list Formula) (wits : list Witness), - check_conj_formulas t1 wits t2 = true -> - forall env : Env, make_impl (eval env) t1 (make_conj (eval env) t2). -Proof. -intro t1; induction t2 as [| a2 t2' IH]. -intros; apply make_impl_true. -intros wits H env. -unfold check_conj_formulas in H; simpl in H. -destruct wits as [| w ws]; simpl in H. discriminate. -case_eq (check_formulas' (negate a2 :: normalise_list t1) w); -intro H1; rewrite H1 in H; [| discriminate]. -assert (H2 : make_impl (eval' env) (negate a2 :: normalise_list t1) False) by -now apply check_formulas'_sound with (w := w). clear H1. -pose proof (IH ws H env) as H1. simpl in H2. -assert (H3 : eval' env (negate a2) -> make_impl (eval env) t1 False) -by auto using normalise_sound_contr. clear H2. -rewrite <- make_conj_impl in *. -rewrite make_conj_cons. intro H2. split. -apply <- negate_correct. intro; now elim H3. exact (H1 H2). -Qed. - -End CheckerMaker. -*)
\ No newline at end of file diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v index 31c4a565..dd4d596f 100644 --- a/plugins/micromega/Env.v +++ b/plugins/micromega/Env.v @@ -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 *) diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 424f9f37..62a7333d 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -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 *) diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v new file mode 100644 index 00000000..72425585 --- /dev/null +++ b/plugins/micromega/Lia.v @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2013 *) +(* *) +(************************************************************************) + +Require Import ZMicromega. +Require Import ZArith. +Require Import RingMicromega. +Require Import VarMap. +Require Tauto. +Declare ML Module "micromega_plugin". + +Ltac preprocess := + zify ; unfold Z.succ in * ; unfold Z.pred in *. + +Ltac lia := + preprocess; + xlia ; + abstract ( + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). + +Ltac nia := + preprocess; + xnlia ; + abstract ( + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). + + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 607eb2b6..22ddd549 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -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 *) diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v index 2469f644..34b8bbdd 100644 --- a/plugins/micromega/OrderedRing.v +++ b/plugins/micromega/OrderedRing.v @@ -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 *) @@ -85,9 +85,9 @@ Notation "x < y" := (rlt x y). Add Relation R req - reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ ) - symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ ) - transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ ) + reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _) + symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _) + transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _) as sor_setoid. diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 42c65b5a..675321d9 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -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 *) @@ -16,35 +16,55 @@ Require Import ZMicromega. Require Import QMicromega. Require Import RMicromega. Require Import QArith. -Require Export Ring_normalize. Require Import ZArith. Require Import Rdefinitions. -Require Export RingMicromega. +Require Import RingMicromega. Require Import VarMap. Require Tauto. Declare ML Module "micromega_plugin". +Ltac preprocess := + zify ; unfold Z.succ in * ; unfold Z.pred in *. + +Ltac lia := + preprocess; + xlia ; + abstract ( + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). + +Ltac nia := + preprocess; + xnlia ; + abstract ( + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). + + Ltac xpsatz dom d := let tac := lazymatch dom with | Z => (sos_Z || psatz_Z d) ; + abstract( intros __wit __varmap __ff ; change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity + apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)) | R => (sos_R || psatz_R d) ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (intros __wit __varmap __ff ; + try (abstract(intros __wit __varmap __ff ; change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity) + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) | Q => (sos_Q || psatz_Q d) ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (intros __wit __varmap __ff ; + try (abstract(intros __wit __varmap __ff ; change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity) + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) | _ => fail "Unsupported domain" end in tac. @@ -53,26 +73,22 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1. Ltac psatzl dom := let tac := lazymatch dom with - | Z => - psatzl_Z ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity + | Z => lia | Q => psatzl_Q ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (intros __wit __varmap __ff ; + try (abstract(intros __wit __varmap __ff ; change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity) + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) | R => unfold Rdiv in * ; psatzl_R ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (intros __wit __varmap __ff ; + try abstract((intros __wit __varmap __ff ; change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity) + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) | _ => fail "Unsupported domain" end in tac. @@ -80,19 +96,6 @@ Ltac psatzl dom := Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac lia := - zify ; unfold Z.succ in * ; - (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. - -Ltac nia := - zify ; unfold Z.succ in * ; - xnlia ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. (* Local Variables: *) diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index cbd7e334..6c157def 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -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 *) @@ -66,7 +66,7 @@ Require Import EnvRing. Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := match e with | PEc c => c - | PEX j => env j + | PEX _ j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) @@ -78,7 +78,7 @@ Lemma Qeval_expr_simpl : forall env e, Qeval_expr env e = match e with | PEc c => c - | PEX j => env j + | PEX _ j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 65911a72..e9ab6962 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -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 *) @@ -243,7 +243,6 @@ Proof. unfold IQR ; intros. simpl. repeat rewrite mult_IZR. - simpl. rewrite Pos2Nat.inj_mul. rewrite mult_INR. repeat INR_nat_of_P. @@ -260,8 +259,8 @@ Proof. simpl. intros. unfold Qinv. - destruct x ; simpl in *. - destruct Qnum ; simpl. + destruct x. + destruct Qnum ; simpl in *. exfalso. auto with zarith. clear H. repeat INR_nat_of_P. diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v index 6072e582..499a8c4c 100644 --- a/plugins/micromega/Refl.v +++ b/plugins/micromega/Refl.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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 *) diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index a2136506..a0545637 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -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 *) @@ -57,7 +57,7 @@ Variables ceqb cleb : C -> C -> bool. Variable phi : C -> R. (* Power coefficients *) -Variable E : Set. (* the type of exponents *) +Variable E : Type. (* the type of exponents *) Variable pow_phi : N -> E. Variable rpow : R -> E -> R. @@ -78,9 +78,9 @@ Record SORaddon := mk_SOR_addon { Variable addon : SORaddon. Add Relation R req - reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ ) - symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ ) - transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ ) + reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _) + symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _) + transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _) as micomega_sor_setoid. Add Morphism rplus with signature req ==> req ==> req as rplus_morph. @@ -141,8 +141,8 @@ Qed. Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *) Definition PolEnv := Env R. (* For interpreting PolC *) -Definition eval_pol (env : PolEnv) (p:PolC) : R := - Pphi rplus rtimes phi env p. +Definition eval_pol : PolEnv -> PolC -> R := + Pphi rplus rtimes phi. Inductive Op1 : Set := (* relations with 0 *) | Equal (* == 0 *) @@ -412,12 +412,12 @@ Proof. induction e. (* PsatzIn *) simpl ; intros. - destruct (nth_in_or_default n l (Pc cO, Equal)). + destruct (nth_in_or_default n l (Pc cO, Equal)) as [Hin|Heq]. (* index is in bounds *) - apply H ; congruence. + apply H. congruence. (* index is out-of-bounds *) inversion H0. - rewrite e. simpl. + rewrite Heq. simpl. now apply addon.(SORrm).(morph0). (* PsatzSquare *) simpl. intros. inversion H0. @@ -679,7 +679,8 @@ match o with | OpGt => fun x y : R => y < x end. -Definition eval_pexpr (l : PolEnv) (pe : PExpr C) : R := PEeval rplus rtimes rminus ropp phi pow_phi rpow l pe. +Definition eval_pexpr : PolEnv -> PExpr C -> R := + PEeval rplus rtimes rminus ropp phi pow_phi rpow. Record Formula (T:Type) : Type := { Flhs : PExpr T; @@ -910,7 +911,7 @@ Proof. unfold pow_N. ring. Qed. -Definition denorm (p : Pol C) := xdenorm xH p. +Definition denorm := xdenorm xH. Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p). Proof. @@ -947,7 +948,7 @@ Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c). Fixpoint map_PExpr (e : PExpr S) : PExpr C := match e with | PEc c => PEc (C_of_S c) - | PEX p => PEX _ p + | PEX _ p => PEX _ p | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2) | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2) | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2) @@ -960,8 +961,8 @@ Definition map_Formula (f : Formula S) : Formula C := Build_Formula (map_PExpr l) o (map_PExpr r). -Definition eval_sexpr (env : PolEnv) (e : PExpr S) : R := - PEeval rplus rtimes rminus ropp phiS pow_phi rpow env e. +Definition eval_sexpr : PolEnv -> PExpr S -> R := + PEeval rplus rtimes rminus ropp phiS pow_phi rpow. Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop := let (lhs, op, rhs) := f in diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index a1d200ea..39d0c6b1 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -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 *) @@ -31,10 +31,10 @@ Set Implicit Arguments. Fixpoint eval_f (A:Type) (ev:A -> Prop ) (f:BFormula A) {struct f}: Prop := match f with - | TT => True - | FF => False + | TT _ => True + | FF _ => False | A a => ev a - | X p => p + | X _ p => p | Cj e1 e2 => (eval_f ev e1) /\ (eval_f ev e2) | D e1 e2 => (eval_f ev e1) \/ (eval_f ev e2) | N e => ~ (eval_f ev e) @@ -54,9 +54,9 @@ Set Implicit Arguments. Fixpoint map_bformula (T U : Type) (fct : T -> U) (f : BFormula T) : BFormula U := match f with - | TT => TT _ - | FF => FF _ - | X p => X _ p + | TT _ => TT _ + | FF _ => FF _ + | X _ p => X _ p | A a => A (fct a) | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2) | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2) @@ -172,9 +172,9 @@ Set Implicit Arguments. Fixpoint xcnf (pol : bool) (f : BFormula Term) {struct f}: cnf := match f with - | TT => if pol then tt else ff - | FF => if pol then ff else tt - | X p => if pol then ff else ff (* This is not complete - cannot negate any proposition *) + | TT _ => if pol then tt else ff + | FF _ => if pol then ff else tt + | X _ p => if pol then ff else ff (* This is not complete - cannot negate any proposition *) | A x => if pol then normalise x else negate x | N e => xcnf (negb pol) e | Cj e1 e2 => diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 4391a01b..6e1fe222 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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 *) diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index 7f748a0b..4c4b81a0 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -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 *) @@ -41,19 +41,19 @@ Notation "x < y" := (rlt x y). Lemma req_refl : forall x, req x x. Proof. - destruct sor.(SORsetoid). + destruct sor.(SORsetoid) as (Equivalence_Reflexive,_,_). apply Equivalence_Reflexive. Qed. Lemma req_sym : forall x y, req x y -> req y x. Proof. - destruct sor.(SORsetoid). + destruct sor.(SORsetoid) as (_,Equivalence_Symmetric,_). apply Equivalence_Symmetric. Qed. Lemma req_trans : forall x y z, req x y -> req y z -> req x z. Proof. - destruct sor.(SORsetoid). + destruct sor.(SORsetoid) as (_,_,Equivalence_Transitive). apply Equivalence_Transitive. Qed. @@ -93,6 +93,7 @@ Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption. Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption. Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp. +Declare Equivalent Keys gen_order_phi_Z gen_phiZ. Notation phi_pos := (gen_phiPOS 1 rplus rtimes). Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes). diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 4aecb39a..84a8d13c 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -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 *) @@ -62,7 +62,7 @@ Qed. Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := match e with | PEc c => c - | PEX x => env x + | PEX _ x => env x | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2 | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2 | PEpow e1 n => Z.pow (Zeval_expr env e1) (Z.of_N n) @@ -155,12 +155,16 @@ Proof. Qed. Definition psub := psub Z0 Z.add Z.sub Z.opp Zeq_bool. +Declare Equivalent Keys psub RingMicromega.psub. Definition padd := padd Z0 Z.add Zeq_bool. +Declare Equivalent Keys padd RingMicromega.padd. Definition norm := norm 0 1 Z.add Z.mul Z.sub Z.opp Zeq_bool. +Declare Equivalent Keys norm RingMicromega.norm. Definition eval_pol := eval_pol Z.add Z.mul (fun x => x). +Declare Equivalent Keys eval_pol RingMicromega.eval_pol. Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) = eval_pol env lhs - eval_pol env rhs. Proof. @@ -202,11 +206,10 @@ Definition normalise (t:Formula Z) : cnf (NFormula Z) := Lemma normalise_correct : forall env t, eval_cnf eval_nformula env (normalise t) <-> Zeval_formula env t. Proof. - Opaque padd. - unfold normalise, xnormalise ; simpl; intros env t. + unfold normalise, xnormalise; cbn -[padd]; intros env t. rewrite Zeval_formula_compat. unfold eval_cnf, eval_clause. - destruct t as [lhs o rhs]; case_eq o; simpl; + destruct t as [lhs o rhs]; case_eq o; cbn -[padd]; repeat rewrite eval_pol_sub; repeat rewrite eval_pol_add; repeat rewrite <- eval_pol_norm ; simpl in *; @@ -216,7 +219,6 @@ Proof. generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst; intuition (auto with zarith). - Transparent padd. Qed. Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) := @@ -317,7 +319,7 @@ Qed. Require Import QArith. -Inductive ZArithProof : Type := +Inductive ZArithProof := | DoneProof | RatProof : ZWitness -> ZArithProof -> ZArithProof | CutProof : ZWitness -> ZArithProof -> ZArithProof diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 32aeb993..b4f305dd 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.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 *) @@ -76,7 +76,7 @@ let dev_form n_spec p = let p = dev_form p in let n = C2Ml.n n in let rec pow n = - if n = 0 + if Int.equal n 0 then Poly.constant (n_spec.number_to_num n_spec.unit) else Poly.product p (pow (n-1)) in pow n in @@ -87,8 +87,8 @@ let monomial_to_polynomial mn = Monomial.fold (fun v i acc -> let v = Ml2C.positive v in - 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) + let mn = if Int.equal i 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in + if Pervasives.(=) acc (Mc.PEc (Mc.Zpos Mc.XH)) (** FIXME *) then mn else Mc.PEmul(mn,acc)) mn @@ -105,10 +105,10 @@ let list_to_polynomial vars 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 = - if c = Mc.PEc (Mc.Zpos Mc.XH) + if Pervasives.(=) 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 + let p' = if Pervasives.(=) p (Mc.PEc Mc.Z0) then mn else Mc.PEadd (mn, p) in xtopoly p' (i+1) l in @@ -116,7 +116,7 @@ let list_to_polynomial vars l = let rec fixpoint f x = let y' = f x in - if y' = x then y' + if Pervasives.(=) y' x then y' else fixpoint f y' let rec_simpl_cone n_spec e = @@ -153,9 +153,9 @@ let factorise_linear_cone c = let factorise c1 c2 = match c1 , c2 with | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> - if x = x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None + if Pervasives.(=) x x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> - if x = x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None + if Pervasives.(=) x x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None | _ -> None in let rec rebuild_cone l pending = @@ -199,7 +199,7 @@ open Mfourier let constrain_monomial mn l = let coeffs = List.fold_left (fun acc p -> (Poly.get mn p)::acc) [] l in - if mn = Monomial.const + if Pervasives.(=) mn Monomial.const then { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; op = Eq ; @@ -230,6 +230,7 @@ let string_of_op = function | Mc.NonEqual -> "<> 0" +module MonSet = Set.Make(Monomial) (* If the certificate includes at least one strict inequality, the obtained polynomial can also be 0 *) @@ -238,8 +239,6 @@ let build_linear_system l = (* Gather the monomials: HINT add up of the polynomials ==> This does not work anymore *) let l' = List.map fst l in - let module MonSet = Set.Make(Monomial) in - let monomials = List.fold_left (fun acc p -> Poly.fold (fun m _ acc -> MonSet.add m acc) p acc) @@ -299,27 +298,28 @@ exception Found of Monomial.t exception Strict +module MonMap = Map.Make(Monomial) + 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 + if Pervasives.(=) mn Monomial.const then (map,vect) 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 (mn,m) = try (MonMap.find mn map,map) with Not_found -> let res = (!vr, MonMap.add mn !vr map) in incr vr ; res in + (m,if Int.equal (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 + let cmp x y = Int.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 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,[])) + (mp,cstr::l)) l (MonMap.empty,[])) 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 ; *) @@ -332,8 +332,8 @@ let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) (* should not use rats_to_ints *) with x when Errors.noncritical x -> - if debug - then (Printf.printf "raw certificate %s" (Printexc.to_string x); + if debug + then (Printf.printf "raw certificate %s" (Printexc.to_string x); flush stdout) ; None @@ -367,7 +367,7 @@ let linear_prover n_spec l = let build_system n_spec l = let li = List.combine l (interval 0 (List.length l -1)) in let (l1,l') = List.partition - (fun (x,_) -> if snd x = Mc.NonEqual then true else false) li in + (fun (x,_) -> if Pervasives.(=) (snd x) Mc.NonEqual then true else false) li in List.map (fun ((x,y),i) -> match y with Mc.NonEqual -> failwith "cannot happen" @@ -378,7 +378,7 @@ let linear_prover n_spec l = let linear_prover n_spec l = try linear_prover n_spec l - with x when x <> Sys.Break -> + with x when Errors.noncritical x -> (print_string (Printexc.to_string x); None) let linear_prover_with_cert spec l = @@ -394,7 +394,7 @@ let make_linear_system l = let monomials = List.fold_left (fun acc p -> Poly.addition p acc) (Poly.constant (Int 0)) l' in let monomials = Poly.fold - (fun mn _ l -> if mn = Monomial.const then l else mn::l) monomials [] in + (fun mn _ l -> if Pervasives.(=) 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 ; @@ -406,9 +406,7 @@ 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 = match l with [] -> false | e::l -> if p x e then true else mem p x l @@ -417,7 +415,7 @@ 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) -let eq x y = Vect.compare x y = 0 +let eq x y = Int.equal (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 @@ -477,7 +475,7 @@ let rec scale_term t = let s1' = div_big_int s1 g in let s2' = div_big_int s2 g in let e = mult_big_int g (mult_big_int s1' s2') in - if (compare_big_int e unit_big_int) = 0 + if Int.equal (compare_big_int e unit_big_int) 0 then (unit_big_int, Add (y1,y2)) else e, Add (Mul(Const (Big_int s2'), y1), Mul (Const (Big_int s1'), y2)) @@ -499,7 +497,7 @@ let get_index_of_ith_match f i l = | [] -> failwith "bad index" | e::l -> if f e then - (if j = i then res else get (j+1) (res+1) l ) + (if Int.equal j i then res else get (j+1) (res+1) l ) else get j (res+1) l in get 0 0 l @@ -559,7 +557,7 @@ let q_cert_of_pos pos = | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l | Rational_eq n | Rational_le n | Rational_lt n -> - if compare_num n (Int 0) = 0 then Mc.PsatzZ else + if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else Mc.PsatzC (Ml2C.q n) | Square t -> Mc.PsatzSquare (term_to_q_pol t) | Eqmul (t, y) -> Mc.PsatzMulC(term_to_q_pol t, _cert_of_pos y) @@ -590,7 +588,7 @@ let z_cert_of_pos pos = | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l | Rational_eq n | Rational_le n | Rational_lt n -> - if compare_num n (Int 0) = 0 then Mc.PsatzZ else + if Int.equal (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) | Eqmul (t, y) -> @@ -631,7 +629,7 @@ struct let rec xid_of_hyp i l = match l with | [] -> failwith "id_of_hyp" - | hyp'::l -> if hyp = hyp' then i else xid_of_hyp (i+1) l in + | hyp'::l -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l in xid_of_hyp 0 l end @@ -757,7 +755,7 @@ let check_sat (cstr,prf) = if eq_num gcd (Int 1) then Normalise(cstr,prf) else - if sign_num (mod_num cst gcd) = 0 + if Int.equal (sign_num (mod_num cst gcd)) 0 then (* We can really normalise *) begin assert (sign_num gcd >=1 ) ; @@ -797,18 +795,18 @@ let pivot v (c1,p1) (c2,p2) = match Vect.get v v1 , Vect.get v v2 with | None , _ | _ , None -> None | Some a , Some b -> - if (sign_num a) * (sign_num b) = -1 + if Int.equal ((sign_num a) * (sign_num b)) (-1) then let cv1 = abs_num b and cv2 = abs_num a in Some (xpivot cv1 cv2) else - if op1 = Eq + if op1 == Eq then let cv1 = minus_num (b */ (Int (sign_num a))) and cv2 = abs_num a in Some (xpivot cv1 cv2) - else if op2 = Eq + else if op2 == Eq then let cv1 = abs_num b and cv2 = minus_num (a */ (Int (sign_num b))) in @@ -817,7 +815,7 @@ let pivot v (c1,p1) (c2,p2) = exception FoundProof of prf_rule -let rec simpl_sys sys = +let simpl_sys sys = List.fold_left (fun acc (c,p) -> match check_sat (c,p) with | Tauto -> acc @@ -831,7 +829,7 @@ let rec simpl_sys sys = Source: http://en.wikipedia.org/wiki/Extended_Euclidean_algorithm *) let rec ext_gcd a b = - if sign_big_int b = 0 + if Int.equal (sign_big_int b) 0 then (unit_big_int,zero_big_int) else let (q,r) = quomod_big_int a b in @@ -852,7 +850,7 @@ let pp_ext_gcd a b = exception Result of (int * (proof * cstr_compat)) let split_equations psys = - List.partition (fun (c,p) -> c.op = Eq) + List.partition (fun (c,p) -> c.op == Eq) let extract_coprime (c1,p1) (c2,p2) = @@ -860,9 +858,9 @@ let extract_coprime (c1,p1) (c2,p2) = match vect1 , vect2 with | _ , [] | [], _ -> None | (v1,n1)::vect1' , (v2, n2) :: vect2' -> - if v1 = v2 + if Pervasives.(=) v1 v2 then - if compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int = 0 + if Int.equal (compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int) 0 then Some (v1,n1,n2) else exist2 vect1' vect2' @@ -871,7 +869,7 @@ let extract_coprime (c1,p1) (c2,p2) = then exist2 vect1' vect2 else exist2 vect1 vect2' in - if c1.op = Eq && c2.op = Eq + if c1.op == Eq && c2.op == Eq then exist2 c1.coeffs c2.coeffs else None @@ -928,7 +926,7 @@ let reduce_coprime psys = (** If there is an equation [eq] of the form 1.x + e = c, do a pivot over x with equation [eq] *) let reduce_unary psys = let is_unary_equation (cstr,prf) = - if cstr.op = Eq + if cstr.op == Eq then try Some (fst (List.find (fun (_,n) -> n =/ (Int 1) || n=/ (Int (-1))) cstr.coeffs)) @@ -944,12 +942,12 @@ let reduce_unary psys = let reduce_non_lin_unary psys = let is_unary_equation (cstr,prf) = - if cstr.op = Eq + if cstr.op == Eq then try let x = fst (List.find (fun (x,n) -> (n =/ (Int 1) || n=/ (Int (-1))) && Monomial.is_var (LinPoly.MonT.retrieve x) ) cstr.coeffs) in let x' = LinPoly.MonT.retrieve x in - if List.for_all (fun (y,_) -> y = x || snd (Monomial.div (LinPoly.MonT.retrieve y) x') = 0) cstr.coeffs + if List.for_all (fun (y,_) -> Pervasives.(=) y x || Int.equal (snd (Monomial.div (LinPoly.MonT.retrieve y) x')) 0) cstr.coeffs then Some x else None with Not_found -> None @@ -976,7 +974,7 @@ let reduce_var_change psys = Some ((x,v),(x',numerator v')) with Not_found -> rel_prime vect in - let rel_prime (cstr,prf) = if cstr.op = Eq then rel_prime cstr.coeffs else None in + let rel_prime (cstr,prf) = if cstr.op == Eq then rel_prime cstr.coeffs else None in let (oeq,sys) = extract rel_prime psys in @@ -1007,7 +1005,7 @@ let reduce_var_change psys = let reduce_pivot psys = let is_equation (cstr,prf) = - if cstr.op = Eq + if cstr.op == Eq then try Some (fst (List.hd cstr.coeffs)) @@ -1067,7 +1065,7 @@ let reduce_var_change psys = (* For lia, there are no equations => these precautions are not needed *) (* For nlia, there are equations => do not enumerate over equations! *) let all_planes sys = - let (eq,ineq) = List.partition (fun c -> c.op = Eq) sys in + let (eq,ineq) = List.partition (fun c -> c.op == Eq) sys in match eq with | [] -> List.rev_map (fun c -> c.coeffs) ineq | _ -> @@ -1197,8 +1195,6 @@ let reduce_var_change psys = let is_linear = List.for_all (fun ((p,_),_) -> Poly.is_linear p) sys in - let module MonMap = Map.Make(Monomial) in - let collect_square = List.fold_left (fun acc ((p,_),_) -> Poly.fold (fun m _ acc -> diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7e10464a..2812e36e 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.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 *) @@ -16,6 +16,7 @@ (* *) (************************************************************************) +open Pp open Mutils (** @@ -44,7 +45,7 @@ type tag = Tag.t (** * An atom is of the form: - * pExpr1 {<,>,=,<>,<=,>=} pExpr2 + * pExpr1 \{<,>,=,<>,<=,>=\} pExpr2 * where pExpr1, pExpr2 are polynomial expressions (see Micromega). pExprs are * parametrized by 'cst, which is used as the type of constants. *) @@ -65,7 +66,7 @@ type 'cst formula = | C of 'cst formula * 'cst formula | D of 'cst formula * 'cst formula | N of 'cst formula - | I of 'cst formula * Names.identifier option * 'cst formula + | I of 'cst formula * Names.Id.t option * 'cst formula (** * Formula pretty-printer. @@ -82,7 +83,7 @@ let rec pp_formula o f = | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)" pp_formula f1 (match n with - | Some id -> Names.string_of_id id + | Some id -> Names.Id.to_string id | None -> "") pp_formula f2 | N(f) -> Printf.fprintf o "N(%a)" pp_formula f @@ -111,7 +112,7 @@ let rec ids_of_formula f = (** * A clause is a list of (tagged) nFormulas. * nFormulas are normalized formulas, i.e., of the form: - * cPol {=,<>,>,>=} 0 + * cPol \{=,<>,>,>=\} 0 * with cPol compact polynomials (see the Pol inductive type in EnvRing.v). *) @@ -242,10 +243,10 @@ let rec add_term t0 = function * MODULE: Ordered set of integers. *) -module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) +module ISet = Set.Make(Int) (** - * Given a set of integers s={i0,...,iN} and a list m, return the list of + * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of * elements of m that are at position i0,...,iN. *) @@ -535,10 +536,10 @@ struct let get_left_construct term = match Term.kind_of_term term with - | Term.Construct(_,i) -> (i,[| |]) + | Term.Construct((_,i),_) -> (i,[| |]) | Term.App(l,rst) -> (match Term.kind_of_term l with - | Term.Construct(_,i) -> (i,rst) + | Term.Construct((_,i),_) -> (i,rst) | _ -> raise ParseError ) | _ -> raise ParseError @@ -577,7 +578,7 @@ struct let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) - let rec dump_n x = + let dump_n x = match x with | Mc.N0 -> Lazy.force coq_N0 | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) @@ -590,12 +591,12 @@ struct let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x) - let rec pp_n o x = output_string o (string_of_int (CoqToCaml.n x)) + let pp_n o x = output_string o (string_of_int (CoqToCaml.n x)) let dump_pair t1 t2 dump_t1 dump_t2 (x,y) = Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|]) - let rec parse_z term = + let parse_z term = let (i,c) = get_left_construct term in match i with | 1 -> Mc.Z0 @@ -622,7 +623,7 @@ struct let parse_q term = match Term.kind_of_term term with - | Term.App(c, args) -> if c = Lazy.force coq_Qmake then + | Term.App(c, args) -> if Constr.equal c (Lazy.force coq_Qmake) then {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) } else raise ParseError | _ -> raise ParseError @@ -780,7 +781,7 @@ struct Printf.fprintf o "0" in pp_cone o e - let rec dump_op = function + let dump_op = function | Mc.OpEq-> Lazy.force coq_OpEq | Mc.OpNEq-> Lazy.force coq_OpNEq | Mc.OpLe -> Lazy.force coq_OpLe @@ -808,7 +809,7 @@ struct let assoc_const x l = try - snd (List.find (fun (x',y) -> x = Lazy.force x') l) + snd (List.find (fun (x',y) -> Constr.equal x (Lazy.force x')) l) with Not_found -> raise ParseError @@ -830,25 +831,33 @@ struct coq_Qeq, Mc.OpEq ] - let parse_zop (op,args) = + let has_typ gl t1 typ = + let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in + Constr.equal ty typ + + + let is_convertible gl t1 t2 = + Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2 + + let parse_zop gl (op,args) = match kind_of_term op with - | Const x -> (assoc_const op zop_table, args.(0) , args.(1)) - | Ind(n,0) -> - if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_Z + | Const (x,_) -> (assoc_const op zop_table, args.(0) , args.(1)) + | Ind((n,0),_) -> + if Constr.equal op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError | _ -> failwith "parse_zop" - let parse_rop (op,args) = + let parse_rop gl (op,args) = match kind_of_term op with - | Const x -> (assoc_const op rop_table, args.(0) , args.(1)) - | Ind(n,0) -> - if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_R + | Const (x,_) -> (assoc_const op rop_table, args.(0) , args.(1)) + | Ind((n,0),_) -> + if Constr.equal op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError | _ -> failwith "parse_zop" - let parse_qop (op,args) = + let parse_qop gl (op,args) = (assoc_const op qop_table, args.(0) , args.(1)) let is_constant t = (* This is an approx *) @@ -864,7 +873,7 @@ struct let assoc_ops x l = try - snd (List.find (fun (x',y) -> x = Lazy.force x') l) + snd (List.find (fun (x',y) -> Constr.equal x (Lazy.force x')) l) with Not_found -> Ukn "Oups" @@ -901,10 +910,7 @@ struct let parse_expr parse_constant parse_exp ops_spec env term = if debug - then (Pp.pp (Pp.str "parse_expr: "); - Pp.pp (Printer.prterm term); - Pp.pp (Pp.str "\n"); - Pp.pp_flush ()); + then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term); (* let constant_or_variable env term = @@ -941,7 +947,7 @@ struct let (expr,env) = parse_expr env args.(0) in let power = (parse_exp expr args.(1)) in (power , env) - with e when e <> Sys.Break -> + with e when Errors.noncritical e -> (* if the exponent is a variable *) let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) end @@ -994,9 +1000,9 @@ struct let rec rconstant term = match Term.kind_of_term term with | Const x -> - if term = Lazy.force coq_R0 + if Constr.equal term (Lazy.force coq_R0) then Mc.C0 - else if term = Lazy.force coq_R1 + else if Constr.equal term (Lazy.force coq_R1) then Mc.C1 else raise ParseError | App(op,args) -> @@ -1010,8 +1016,8 @@ struct with ParseError -> match op with - | op when op = Lazy.force coq_Rinv -> Mc.CInv(rconstant args.(0)) - | op when op = Lazy.force coq_IQR -> Mc.CQ (parse_q args.(0)) + | op when Constr.equal op (Lazy.force coq_Rinv) -> Mc.CInv(rconstant args.(0)) + | op when Constr.equal op (Lazy.force coq_IQR) -> Mc.CQ (parse_q args.(0)) (* | op when op = Lazy.force coq_IZR -> Mc.CZ (parse_z args.(0))*) | _ -> raise ParseError end @@ -1021,11 +1027,7 @@ struct let rconstant term = if debug - then (Pp.pp_flush (); - Pp.pp (Pp.str "rconstant: "); - Pp.pp (Printer.prterm term); - Pp.pp (Pp.str "\n"); - Pp.pp_flush ()); + then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ()); let res = rconstant term in if debug then (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; @@ -1063,26 +1065,22 @@ struct Mc.PEpow(expr,exp)) rop_spec - let parse_arith parse_op parse_expr env cstr = + let parse_arith parse_op parse_expr env cstr gl = if debug - then (Pp.pp_flush (); - Pp.pp (Pp.str "parse_arith: "); - Pp.pp (Printer.prterm cstr); - Pp.pp (Pp.str "\n"); - Pp.pp_flush ()); + then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ()); match kind_of_term cstr with | App(op,args) -> - let (op,lhs,rhs) = parse_op (op,args) in + let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr env lhs in let (e2,env) = parse_expr env rhs in ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env) | _ -> failwith "error : parse_arith(2)" - let parse_zarith = parse_arith parse_zop parse_zexpr + let parse_zarith = parse_arith parse_zop parse_zexpr - let parse_qarith = parse_arith parse_qop parse_qexpr + let parse_qarith = parse_arith parse_qop parse_qexpr - let parse_rarith = parse_arith parse_rop parse_rexpr + let parse_rarith = parse_arith parse_rop parse_rexpr (* generic parsing of arithmetic expressions *) @@ -1115,14 +1113,13 @@ struct * This is the big generic function for formula parsers. *) - let parse_formula parse_atom env tg term = + let parse_formula gl parse_atom env tg term = let parse_atom env tg t = try - let (at,env) = parse_atom env t in + let (at,env) = parse_atom env t gl in (A(at,tg,t), env,Tag.next tg) - with e when e <> Sys.Break -> (X(t),env,tg) - in + with e when Errors.noncritical e -> (X(t),env,tg) in let rec xparse_formula env tg term = match kind_of_term term with @@ -1177,7 +1174,7 @@ struct | (e::l) -> let (name,expr,typ) = e in xset (Term.mkNamedLetIn - (Names.id_of_string name) + (Names.Id.of_string name) expr typ acc) l in xset concl l @@ -1199,13 +1196,13 @@ let same_proof sg cl1 cl2 = match sg with | [] -> true | n::sg -> - (try List.nth cl1 n = List.nth cl2 n with e when e <> Sys.Break -> false) + (try Int.equal (List.nth cl1 n) (List.nth cl2 n) with Invalid_argument _ -> false) && (xsame_proof sg ) in xsame_proof sg let tags_of_clause tgs wit clause = let rec xtags tgs = function - | Mc.PsatzIn n -> Names.Idset.union tgs + | Mc.PsatzIn n -> Names.Id.Set.union tgs (snd (List.nth clause (CoqToCaml.nat n) )) | Mc.PsatzMulC(e,w) -> xtags tgs w | Mc.PsatzMulE (w1,w2) | Mc.PsatzAdd(w1,w2) -> xtags (xtags tgs w1) w2 @@ -1214,7 +1211,7 @@ let tags_of_clause tgs wit clause = (*let tags_of_cnf wits cnf = List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl) - Names.Idset.empty wits cnf *) + Names.Id.Set.empty wits cnf *) let find_witness prover polys1 = try_any prover polys1 @@ -1263,7 +1260,7 @@ let btree_of_array typ a = let btree_of_array typ a = try btree_of_array typ a - with x when x <> Sys.Break -> + with x when Errors.noncritical x -> failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x)) let dump_varmap typ env = @@ -1324,24 +1321,24 @@ let rec pp_proof_term o = function (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 (pp_list "[" "]" pp_proof_term) rst -let rec parse_hyps parse_arith env tg hyps = +let rec parse_hyps gl parse_arith env tg hyps = match hyps with | [] -> ([],env,tg) | (i,t)::l -> - let (lhyps,env,tg) = parse_hyps parse_arith env tg l in + let (lhyps,env,tg) = parse_hyps gl parse_arith env tg l in try - let (c,env,tg) = parse_formula parse_arith env tg t in + let (c,env,tg) = parse_formula gl parse_arith env tg t in ((i,c)::lhyps, env,tg) - with e when e <> Sys.Break -> (lhyps,env,tg) + with e when Errors.noncritical e -> (lhyps,env,tg) (*(if debug then Printf.printf "parse_arith : %s\n" x);*) (*exception ParseError*) -let parse_goal parse_arith env hyps term = +let parse_goal gl parse_arith env hyps term = (* try*) - let (f,env,tg) = parse_formula parse_arith env (Tag.from 0) term in - let (lhyps,env,tg) = parse_hyps parse_arith env tg hyps in + let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in + let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in (lhyps,f,env) (* with Failure x -> raise ParseError*) @@ -1385,22 +1382,31 @@ let rcst_domain_spec = lazy { * witness. *) -let micromega_order_change spec cert cert_typ env ff gl = + + +let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic = + let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in - let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in + let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) env in - Tactics.change_in_concl None + (* todo : directly generate the proof term - or generalize befor conversion? *) + Tacticals.tclTHENSEQ [ + (fun gl -> + Proofview.V82.of_tactic (Tactics.change_concl (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); ("__varmap", vm, Term.mkApp (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.pf_concl gl) - ) - gl + (Tacmach.pf_concl gl))) gl); + Tactics.generalize env ; + Tacticals.tclTHENSEQ (List.map (fun id -> Proofview.V82.of_tactic (Tactics.introduction id)) ids) ; + ] + + (** * The datastructures that aggregate prover attributes. @@ -1476,7 +1482,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = (pp_ml_list prover.pp_f) (List.map fst new_cl) ; flush stdout end ; *) - let res = try prover.compact prf remap with x when x <> Sys.Break -> + let res = try prover.compact prf remap with x when Errors.noncritical x -> if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; (* This should not happen -- this is the recovery plan... *) match prover.prover (List.map fst new_cl) with @@ -1494,7 +1500,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = let hyps_idx = prover.hyps prf in let hyps = selecti hyps_idx old_cl in - is_sublist hyps new_cl in + is_sublist Pervasives.(=) hyps new_cl in let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *) @@ -1644,7 +1650,7 @@ let micromega_gen let concl = Tacmach.pf_concl gl in let hyps = Tacmach.pf_hyps_types gl in try - let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in + let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in let env = Env.elements env in let spec = Lazy.force spec in @@ -1658,8 +1664,6 @@ let micromega_gen (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff' ]) gl with -(* | Failure x -> flush stdout ; Pp.pp_flush () ; - Tacticals.tclFAIL 0 (Pp.str x) gl *) | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; Tacticals.tclFAIL 0 (Pp.str @@ -1679,7 +1683,7 @@ let micromega_order_changer cert env ff gl = let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) env in - Tactics.change_in_concl None + Proofview.V82.of_tactic (Tactics.change_concl (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); @@ -1689,7 +1693,7 @@ let micromega_order_changer cert env ff gl = ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl) - ) + )) gl @@ -1710,7 +1714,7 @@ let micromega_genr prover gl = let concl = Tacmach.pf_concl gl in let hyps = Tacmach.pf_hyps_types gl in try - let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in + let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in let env = Env.elements env in let spec = Lazy.force spec in @@ -1729,8 +1733,6 @@ let micromega_genr prover gl = micromega_order_changer res' env (abstract_wrt_formula ff' ff) ]) gl with -(* | Failure x -> flush stdout ; Pp.pp_flush () ; - Tacticals.tclFAIL 0 (Pp.str x) gl *) | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; Tacticals.tclFAIL 0 (Pp.str @@ -1760,7 +1762,7 @@ open Persistent_cache module Cache = PHashtable(struct type t = (provername * micromega_polys) - let equal = (=) + let equal = Pervasives.(=) let hash = Hashtbl.hash end) @@ -1954,7 +1956,7 @@ let non_linear_prover_Z str o = { module CacheZ = PHashtable(struct type t = (Mc.z Mc.pol * Mc.op1) list - let equal = (=) + let equal = Pervasives.(=) let hash = Hashtbl.hash end) 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 diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 4270d5bb..1ac44a42 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -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 *) @@ -14,65 +14,65 @@ (* *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) -open Quote -open Ring -open Mutils -open Glob_term -open Util +open Errors +open Misctypes + +DECLARE PLUGIN "micromega_plugin" let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) ] -> [ Coq_micromega.psatz_Z (out_arg i) ] -| [ "psatz_Z" ] -> [ Coq_micromega.psatz_Z (-1) ] +| [ "psatz_Z" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (out_arg i)) ] +| [ "psatz_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (-1)) ] END -TACTIC EXTEND ZOmicron -[ "xlia" ] -> [ Coq_micromega.xlia] +TACTIC EXTEND Lia +[ "xlia" ] -> [ Proofview.V82.tactic (Coq_micromega.xlia) ] END -TACTIC EXTEND Nlia -[ "xnlia" ] -> [ Coq_micromega.xnlia] +TACTIC EXTEND Nia +[ "xnlia" ] -> [ Proofview.V82.tactic (Coq_micromega.xnlia) ] END TACTIC EXTEND Sos_Z -| [ "sos_Z" ] -> [ Coq_micromega.sos_Z] +| [ "sos_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_Z) ] END TACTIC EXTEND Sos_Q -| [ "sos_Q" ] -> [ Coq_micromega.sos_Q] +| [ "sos_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_Q) ] END TACTIC EXTEND Sos_R -| [ "sos_R" ] -> [ Coq_micromega.sos_R] +| [ "sos_R" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_R) ] END - +(* TACTIC EXTEND Omicron -[ "psatzl_Z" ] -> [ Coq_micromega.psatzl_Z] +[ "psatzl_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_Z) ] END +*) -TACTIC EXTEND QOmicron -[ "psatzl_Q" ] -> [ Coq_micromega.psatzl_Q] +TACTIC EXTEND LRA_Q +[ "psatzl_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_Q) ] END -TACTIC EXTEND ROmicron -[ "psatzl_R" ] -> [ Coq_micromega.psatzl_R] +TACTIC EXTEND LRA_R +[ "psatzl_R" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_R) ] END -TACTIC EXTEND RMicromega -| [ "psatz_R" int_or_var(i) ] -> [ Coq_micromega.psatz_R (out_arg i) ] -| [ "psatz_R" ] -> [ Coq_micromega.psatz_R (-1) ] +TACTIC EXTEND PsatzR +| [ "psatz_R" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_R (out_arg i)) ] +| [ "psatz_R" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_R (-1)) ] END -TACTIC EXTEND QMicromega -| [ "psatz_Q" int_or_var(i) ] -> [ Coq_micromega.psatz_Q (out_arg i) ] -| [ "psatz_Q" ] -> [ Coq_micromega.psatz_Q (-1) ] +TACTIC EXTEND PsatzQ +| [ "psatz_Q" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (out_arg i)) ] +| [ "psatz_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (-1)) ] END diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 6effa4c4..88c1a783 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -3,13 +3,14 @@ module Utils = Mutils open Polynomial open Vect - let map_option = Utils.map_option let from_option = Utils.from_option let debug = false type ('a,'b) lr = Inl of 'a | Inr of 'b +let compare_float (p : float) q = Pervasives.compare p q + (** Implementation of intervals *) module Itv = struct @@ -18,10 +19,10 @@ struct type interval = num option * num option (** None models the absence of bound i.e. infinity *) (** As a result, - - None , None -> ]-oo,+oo[ - - None , Some v -> ]-oo,v] - - Some v, None -> [v,+oo[ - - Some v, Some v' -> [v,v'] + - None , None -> \]-oo,+oo\[ + - None , Some v -> \]-oo,v\] + - Some v, None -> \[v,+oo\[ + - Some v, Some v' -> \[v,v'\] Intervals needs to be explicitely normalised. *) @@ -89,7 +90,7 @@ type vector = Vect.t {coeffs = v ; bound = (l,r) } models the constraints l <= v <= r **) -module ISet = Set.Make(struct type t = int let compare = Pervasives.compare end) +module ISet = Set.Make(Int) module PSet = ISet @@ -116,7 +117,7 @@ and cstr_info = { } -(** A system of constraints has the form [{sys = s ; vars = v}]. +(** A system of constraints has the form [\{sys = s ; vars = v\}]. [s] is a hashtable mapping a normalised vector to a [cstr_info] record where - [bound] is an interval - [prf_idx] is the set of hypothese indexes (i.e. constraints in the initial system) used to obtain the current constraint. @@ -195,7 +196,7 @@ let pp_split_cstr o (vl,v,c,_) = let merge_cstr_info i1 i2 = let { pos = p1 ; neg = n1 ; bound = i1 ; prf = prf1 } = i1 and { pos = p2 ; neg = n2 ; bound = i2 ; prf = prf2 } = i2 in - assert (p1 = p2 && n1 = n2) ; + assert (Int.equal p1 p2 && Int.equal n1 n2) ; match inter i1 i2 with | None -> None (* Could directly raise a system contradiction exception *) | Some bnd -> @@ -207,7 +208,7 @@ let merge_cstr_info i1 i2 = *) let xadd_cstr vect cstr_info sys = - if debug && System.length sys mod 1000 = 0 then (print_string "*" ; flush stdout) ; + if debug && Int.equal (System.length sys mod 1000) 0 then (print_string "*" ; flush stdout) ; try let info = System.find sys vect in match merge_cstr_info cstr_info !info with @@ -235,7 +236,7 @@ let normalise_cstr vect cinfo = | (_,n)::_ -> Cstr( (if n <>/ Int 1 then List.map (fun (x,nx) -> (x,nx // n)) vect else vect), let divn x = x // n in - if sign_num n = 1 + if Int.equal (sign_num n) 1 then{cinfo with bound = (map_option divn l , map_option divn r) } else {cinfo with pos = cinfo.neg ; neg = cinfo.pos ; bound = (map_option divn r , map_option divn l)}) @@ -252,7 +253,7 @@ let count v = | [] -> (n,p) | (_,vl)::v -> let sg = sign_num vl in assert (sg <> 0) ; - if sg = 1 then count n (p+1) v else count (n+1) p v in + if Int.equal sg 1 then count n (p+1) v else count (n+1) p v in count 0 0 v @@ -304,7 +305,7 @@ let add (v1,c1) (v2,c2) = let rec xadd v1 v2 = match v1 , v2 with | (x1,n1)::v1' , (x2,n2)::v2' -> - if x1 = x2 + if Int.equal x1 x2 then let n' = (n1 // c1) +/ (n2 // c2) in if n' =/ Int 0 then xadd v1' v2' @@ -352,7 +353,7 @@ let split x (vect: vector) info (l,m,r) = | Some bnd -> (vl,vect,{info with bound = Some bnd,None})::lst in let lb,rb = info.bound in - if sign_num vl = 1 + if Int.equal (sign_num vl) 1 then (cons_bound l lb,m,cons_bound r rb) else (* sign_num vl = -1 *) (cons_bound l rb,m,cons_bound r lb) @@ -437,7 +438,7 @@ let elim_var_using_eq vr vect cst prf sys = (** [size sys] computes the number of entries in the system of constraints *) let size sys = System.fold (fun v iref s -> s + (!iref).neg + (!iref).pos) sys 0 -module IMap = Map.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) +module IMap = Map.Make(Int) let pp_map o map = IMap.fold (fun k elt () -> Printf.fprintf o "%i -> %s\n" k (string_of_num elt)) map () @@ -498,7 +499,7 @@ let pick_small_value bnd = then ceiling_num i (* why not *) else i -(** [solution s1 sys_l = Some(sn,[(vn-1,sn-1);...; (v1,s1)]@sys_l)] +(** [solution s1 sys_l = Some(sn,\[(vn-1,sn-1);...; (v1,s1)\]\@sys_l)] then [sn] is a system which contains only [black_v] -- if it existed in [s1] and [sn+1] is obtained by projecting [vn] out of [sn] @raise SystemContradiction if system [s] has no solution @@ -556,7 +557,7 @@ struct match l1 with | [] -> xpart rl (([],info)::ltl) n (info.neg+info.pos+z) p | (vr,vl)::rl1 -> - if v = vr + if Int.equal v vr then let cons_bound lst bd = match bd with @@ -564,7 +565,7 @@ struct | Some bnd -> info.neg+info.pos::lst in let lb,rb = info.bound in - if sign_num vl = 1 + if Int.equal (sign_num vl) 1 then xpart rl ((rl1,info)::ltl) (cons_bound n lb) z (cons_bound p rb) else xpart rl ((rl1,info)::ltl) (cons_bound n rb) z (cons_bound p lb) else @@ -590,7 +591,7 @@ struct (ISet.fold (fun v (eval,s) -> let ts,vl = abstract_partition v s in ((v,vl)::eval, ts)) v ([],sl)) in - List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) evals + List.sort (fun x y -> compare_float (snd x) (snd y) ) evals end @@ -615,7 +616,7 @@ struct let rec unroll_until v l = match l with | [] -> (false,[]) - | (i,_)::rl -> if i = v + | (i,_)::rl -> if Int.equal i v then (true,rl) else if i < v then unroll_until v rl else (false,l) @@ -632,7 +633,7 @@ struct let choose_primal_equation eqs sys_l = - (* Counts the number of equations refering to variable [v] -- + (* Counts the number of equations referring to variable [v] -- It looks like nb_cst is dead... *) let is_primal_equation_var v = @@ -646,7 +647,7 @@ struct | [] -> None | (i,_)::vect -> let nb_eq = is_primal_equation_var i in - if nb_eq = 2 + if Int.equal nb_eq 2 then Some i else find_var vect in let rec find_eq_var eqs = @@ -704,7 +705,7 @@ struct (* pp_list (fun o ((v,eq,_,_),cst) -> Printf.fprintf o "((%i,%a),%i)\n" v pp_vect eq cst) stdout all_costs ; *) - List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) all_costs + List.sort (fun x y -> Int.compare (snd x) (snd y) ) all_costs | Some (v,vect, const,prf,_) -> [(v,vect,const,prf),0] @@ -727,9 +728,9 @@ struct | Inl (s,_) -> try Some (bound_of_variable IMap.empty fresh s.sys) - with - x when x <> Sys.Break -> - Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None + with x when Errors.noncritical x -> + Printf.printf "optimise Exception : %s" (Printexc.to_string x); + None let find_point cstrs = @@ -793,18 +794,18 @@ struct match Vect.get v v1 , Vect.get v v2 with | None , _ | _ , None -> None | Some a , Some b -> - if (sign_num a) * (sign_num b) = -1 + if Int.equal ((sign_num a) * (sign_num b)) (-1) then Some (add (p1,abs_num a) (p2,abs_num b) , {coeffs = add (v1,abs_num a) (v2,abs_num b) ; op = add_op op1 op2 ; cst = n1 // (abs_num a) +/ n2 // (abs_num b) }) - else if op1 = Eq + else if op1 == Eq then Some (add (p1,minus_num (a // b)) (p2,Int 1), {coeffs = add (v1,minus_num (a// b)) (v2 ,Int 1) ; op = add_op op1 op2; cst = n1 // (minus_num (a// b)) +/ n2 // (Int 1)}) - else if op2 = Eq + else if op2 == Eq then Some (add (p2,minus_num (b // a)) (p1,Int 1), {coeffs = add (v2,minus_num (b// a)) (v1 ,Int 1) ; diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 564126d2..0537cdbe 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -1499,7 +1499,7 @@ module N = (** val eqb : n -> n -> bool **) - let rec eqb n0 m = + let eqb n0 m = match n0 with | N0 -> (match m with @@ -1693,7 +1693,7 @@ module N = (** val ldiff : n -> n -> n **) - let rec ldiff n0 m = + let ldiff n0 m = match n0 with | N0 -> N0 | Npos p -> @@ -2205,7 +2205,7 @@ module Z = (** val eqb : z -> z -> bool **) - let rec eqb x y = + let eqb x y = match x with | Z0 -> (match y with diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 7f0dce04..a07cbec6 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.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 *) @@ -31,7 +31,7 @@ let finally f rst = rst () ; res with reraise -> (try rst () - with any -> raise reraise + with any -> raise reraise ); raise reraise let map_option f x = @@ -72,15 +72,15 @@ let rec map3 f l1 l2 l3 = match l1 , l2 ,l3 with | [] , [] , [] -> [] | e1::l1 , e2::l2 , e3::l3 -> (f e1 e2 e3)::(map3 f l1 l2 l3) - | _ -> raise (Invalid_argument "map3") + | _ -> invalid_arg "map3" -let rec is_sublist l1 l2 = +let rec is_sublist f l1 l2 = match l1 ,l2 with | [] ,_ -> true | e::l1', [] -> false | e::l1' , e'::l2' -> - if e = e' then is_sublist l1' l2' - else is_sublist l1 l2' + if f e e' then is_sublist f l1' l2' + else is_sublist f l1 l2' let list_try_find f = let rec try_find_f = function @@ -89,7 +89,7 @@ let list_try_find f = in try_find_f -let rec list_fold_right_elements f l = +let list_fold_right_elements f l = let rec aux = function | [] -> invalid_arg "list_fold_right_elements" | [x] -> x @@ -142,9 +142,9 @@ let rec rec_gcd_list c l = | [] -> c | e::l -> rec_gcd_list (gcd_big_int c (numerator e)) l -let rec gcd_list l = +let gcd_list l = let res = rec_gcd_list zero_big_int l in - if compare_big_int res zero_big_int = 0 + if Int.equal (compare_big_int res zero_big_int) 0 then unit_big_int else res let rats_to_ints l = @@ -192,7 +192,7 @@ let select_pos lpos l = match l with | [] -> failwith "select_pos" | e::l -> - if i = j + if Int.equal i j then e:: (xselect (i+1) rpos l) else xselect (i+1) lpos l in xselect 0 lpos l @@ -269,19 +269,19 @@ struct let rec positive n = - if n=1 then XH - else if n land 1 = 1 then XI (positive (n lsr 1)) + if Int.equal n 1 then XH + else if Int.equal (n land 1) 1 then XI (positive (n lsr 1)) else XO (positive (n lsr 1)) let n nt = if nt < 0 then assert false - else if nt = 0 then N0 + else if Int.equal nt 0 then N0 else Npos (positive nt) let rec index n = - if n=1 then XH - else if n land 1 = 1 then XI (index (n lsr 1)) + if Int.equal n 1 then XH + else if Int.equal (n land 1) 1 then XI (index (n lsr 1)) else XO (index (n lsr 1)) @@ -289,8 +289,8 @@ struct (*a.k.a path_of_int *) (* returns the list of digits of n in reverse order with initial 1 removed *) let rec digits_of_int n = - if n=1 then [] - else (n mod 2 = 1)::(digits_of_int (n lsr 1)) + if Int.equal n 1 then [] + else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1)) in List.fold_right (fun b c -> (if b then XI c else XO c)) @@ -342,7 +342,7 @@ struct | [] -> 0 (* Equal *) | f::l -> let cmp = f () in - if cmp = 0 then compare_lexical l else cmp + if Int.equal cmp 0 then compare_lexical l else cmp let rec compare_list cmp l1 l2 = match l1 , l2 with @@ -351,7 +351,7 @@ struct | _ , [] -> 1 | e1::l1 , e2::l2 -> let c = cmp e1 e2 in - if c = 0 then compare_list cmp l1 l2 else c + if Int.equal c 0 then compare_list cmp l1 l2 else c (** * hash_list takes a hash function and a list, and computes an integer which @@ -393,7 +393,7 @@ struct let from i = i let next i = i + 1 let pp o i = output_string o (string_of_int i) - let compare : int -> int -> int = Pervasives.compare + let compare : int -> int -> int = Int.compare end @@ -403,6 +403,12 @@ end module TagSet = Set.Make(Tag) +(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *) + +let rec waitpid_non_intr pid = + try snd (Unix.waitpid [] pid) + with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid + (** * Forking routine, plumbing the appropriate pipes where needed. *) @@ -422,25 +428,33 @@ let command exe_path args vl = flush outch ; (* Wait for its completion *) - let _pid,status = Unix.waitpid [] pid in + let status = waitpid_non_intr pid in finally (* Recover the result *) (fun () -> match status with | Unix.WEXITED 0 -> - let inch = Unix.in_channel_of_descr stdout_read in - begin try Marshal.from_channel inch - with x when x <> Sys.Break -> - failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) - end - | Unix.WEXITED i -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) - | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) - | Unix.WSTOPPED i -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) + let inch = Unix.in_channel_of_descr stdout_read in + begin + try Marshal.from_channel inch + with any -> + failwith + (Printf.sprintf "command \"%s\" exited %s" exe_path + (Printexc.to_string any)) + end + | Unix.WEXITED i -> + failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) + | Unix.WSIGNALED i -> + failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) + | Unix.WSTOPPED i -> + failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) (* Cleanup *) (fun () -> - List.iter (fun x -> try Unix.close x with e when e <> Sys.Break -> ()) - [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write]) + List.iter (fun x -> try Unix.close x with any -> ()) + [stdin_read; stdin_write; + stdout_read; stdout_write; + stderr_read; stderr_write]) (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 2465617a..2dc0d003 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.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 *) @@ -8,11 +8,10 @@ (* *) (* A persistent hashtable *) (* *) -(* Frédéric Besson (Inria Rennes) 2009-2011 *) +(* Frédéric Besson (Inria Rennes) 2009-2014 *) (* *) (************************************************************************) - module type PHashtable = sig type 'a t @@ -84,7 +83,7 @@ let finally f rst = rst () ; res with reraise -> (try rst () - with any -> raise reraise + with any -> raise reraise ); raise reraise @@ -93,26 +92,52 @@ let read_key_elem inch = Some (Marshal.from_channel inch) with | End_of_file -> None - | e when e <> Sys.Break -> raise InvalidTableFormat - -(** In win32, it seems that we should unlock the exact zone - that has been locked, and not the whole file *) + | e when Errors.noncritical e -> raise InvalidTableFormat + +(** + We used to only lock/unlock regions. + Is-it more robust/portable to lock/unlock a fixed region e.g. [0;1]? + In case of locking failure, the cache is not used. +**) + +type lock_kind = Read | Write + +let lock kd fd = + let pos = lseek fd 0 SEEK_CUR in + let success = + try + ignore (lseek fd 0 SEEK_SET); + let lk = match kd with + | Read -> F_RLOCK + | Write -> F_LOCK in + lockf fd lk 1; true + with Unix.Unix_error(_,_,_) -> false in + ignore (lseek fd pos SEEK_SET) ; + success + +let unlock fd = + let pos = lseek fd 0 SEEK_CUR in + try + ignore (lseek fd 0 SEEK_SET) ; + lockf fd F_ULOCK 1 + with + Unix.Unix_error(_,_,_) -> () + (* Here, this is really bad news -- + there is a pending lock which could cause a deadlock. + Should it be an anomaly or produce a warning ? + *); + ignore (lseek fd pos SEEK_SET) -let locked_start = ref 0 -let lock fd = - locked_start := lseek fd 0 SEEK_CUR; - lockf fd F_LOCK 0 +(* We make the assumption that an acquired lock can always be released *) -let rlock fd = - locked_start := lseek fd 0 SEEK_CUR; - lockf fd F_RLOCK 0 +let do_under_lock kd fd f = + if lock kd fd + then + finally f (fun () -> unlock fd) + else f () + -let unlock fd = - let pos = lseek fd 0 SEEK_CUR in - ignore (lseek fd !locked_start SEEK_SET); - lockf fd F_ULOCK 0; - ignore (lseek fd pos SEEK_SET) let open_in f = let flags = [O_RDONLY ; O_CREAT] in @@ -128,37 +153,30 @@ let open_in f = xload () in try (* Locking of the (whole) file while reading *) - rlock finch; - finally - (fun () -> xload () ) - (fun () -> - unlock finch ; - close_in_noerr inch ; - ) ; + do_under_lock Read finch xload ; + close_in_noerr inch ; { - outch = out_channel_of_descr (openfile f [O_WRONLY;O_APPEND;O_CREAT] 0o666) ; - status = Open ; - htbl = htbl + outch = out_channel_of_descr (openfile f [O_WRONLY;O_APPEND;O_CREAT] 0o666) ; + status = Open ; + htbl = htbl } with InvalidTableFormat -> - (* Try to keep as many entries as possible *) - begin - let flags = [O_WRONLY; O_TRUNC;O_CREAT] in - let out = (openfile f flags 0o666) in - let outch = out_channel_of_descr out in - lock out; - (try - Table.iter - (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl; - flush outch ; - with e when e <> Sys.Break -> () ) - ; - unlock out ; - { outch = outch ; - status = Open ; - htbl = htbl - } - end + (* The file is corrupted *) + begin + close_in_noerr inch ; + let flags = [O_WRONLY; O_TRUNC;O_CREAT] in + let out = (openfile f flags 0o666) in + let outch = out_channel_of_descr out in + do_under_lock Write out + (fun () -> + Table.iter + (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl; + flush outch) ; + { outch = outch ; + status = Open ; + htbl = htbl + } + end let close t = @@ -172,22 +190,22 @@ let close t = let add t k e = let {outch = outch ; status = status ; htbl = tbl} = t in - if status = Closed + if status == Closed then raise UnboundTable else let fd = descr_of_out_channel outch in begin - Table.add tbl k e ; - lock fd; - ignore (lseek fd 0 SEEK_END); - Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; - flush outch ; - unlock fd + Table.add tbl k e ; + do_under_lock Write fd + (fun _ -> + Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; + flush outch + ) end let find t k = let {outch = outch ; status = status ; htbl = tbl} = t in - if status = Closed + if status == Closed then raise UnboundTable else let res = Table.find tbl k in diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index 9372cb66..b8b42a3f 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.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 *) @@ -44,7 +44,7 @@ end = struct (* A monomial is represented by a multiset of variables *) - module Map = Map.Make(struct type t = var let compare = Pervasives.compare end) + module Map = Map.Make(Int) open Map type t = int Map.t @@ -65,8 +65,8 @@ struct fun m1 m2 -> let s1 = sum_degree m1 and s2 = sum_degree m2 in - if s1 = s2 then Map.compare Pervasives.compare m1 m2 - else Pervasives.compare s1 s2 + if Int.equal s1 s2 then Map.compare Int.compare m1 m2 + else Int.compare s1 s2 let is_const m = (m = Map.empty) @@ -218,7 +218,7 @@ struct let fold = P.fold - let is_null p = fold (fun mn vl b -> b & sign_num vl = 0) p true + let is_null p = fold (fun mn vl b -> b && sign_num vl = 0) p true let compare = compare compare_num @@ -241,8 +241,7 @@ module Vect = type var = int type t = (var * num) list -(** [equal v1 v2 = true] if the vectors are syntactically equal. - ([num] is not handled by [Pervasives.equal] *) +(** [equal v1 v2 = true] if the vectors are syntactically equal. *) let rec equal v1 v2 = match v1 , v2 with @@ -250,7 +249,7 @@ module Vect = | [] , _ -> false | _::_ , [] -> false | (i1,n1)::v1 , (i2,n2)::v2 -> - (i1 = i2) && n1 =/ n2 && equal v1 v2 + (Int.equal i1 i2) && n1 =/ n2 && equal v1 v2 let hash v = let rec hash i = function @@ -294,7 +293,7 @@ module Vect = match t with | [] -> cons i (f zero_num) [] | (k,v)::l -> - match Pervasives.compare i k with + match Int.compare i k with | 0 -> cons k (f v) l | -1 -> cons i (f zero_num) t | 1 -> (k,v) ::(update i f l) @@ -304,7 +303,7 @@ module Vect = match t with | [] -> cons i n [] | (k,v)::l -> - match Pervasives.compare i k with + match Int.compare i k with | 0 -> cons k n l | -1 -> cons i n t | 1 -> (k,v) :: (set i n l) @@ -315,7 +314,7 @@ module Vect = if Big_int.compare_big_int res Big_int.zero_big_int = 0 then Big_int.unit_big_int else res - let rec mul z t = + let mul z t = match z with | Int 0 -> [] | Int 1 -> t @@ -346,7 +345,7 @@ module Vect = let compare : t -> t -> int = Utils.Cmp.compare_list (fun x y -> Utils.Cmp.compare_lexical [ - (fun () -> Pervasives.compare (fst x) (fst y)); + (fun () -> Int.compare (fst x) (fst y)); (fun () -> compare_num (snd x) (snd y))]) (** [tail v vect] returns @@ -359,7 +358,7 @@ module Vect = match vect with | [] -> None | (v',vl)::vect' -> - match Pervasives.compare v' v with + match Int.compare v' v with | 0 -> Some (vl,vect) (* Ok, found *) | -1 -> tail v vect' (* Might be in the tail *) | _ -> None (* Hopeless *) @@ -585,7 +584,7 @@ struct module MonT = struct module MonoMap = Map.Make(Monomial) - module IntMap = Map.Make(struct type t = int let compare = Pervasives.compare end) + module IntMap = Map.Make(Int) (** A hash table might be preferable but requires a hash function. *) let (index_of_monomial : int MonoMap.t ref) = ref (MonoMap.empty) @@ -615,7 +614,7 @@ struct end let normalise (v,c) = - (List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) v , c) + (List.sort (fun x y -> Int.compare (fst x) (fst y)) v , c) let output_mon o (x,v) = diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index 6ddc48e7..cc89e2b9 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -1,16 +1,15 @@ (* ========================================================================= *) (* - This code originates from John Harrison's HOL LIGHT 2.30 *) (* (see file LICENSE.sos for license, copyright and disclaimer) *) -(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) +(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) (* independent bits *) -(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) +(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) (* ========================================================================= *) (* ========================================================================= *) (* Nonlinear universal reals procedure using SOS decomposition. *) (* ========================================================================= *) open Num;; -open List;; open Sos_types;; open Sos_lib;; @@ -40,7 +39,7 @@ let decimalize = let z = pow10(-e) */ y +/ Int 1 in let k = round_num(pow10 d */ z) in (if x </ Int 0 then "-0." else "0.") ^ - implode(tl(explode(string_of_num k))) ^ + implode(List.tl(explode(string_of_num k))) ^ (if e = 0 then "" else "e"^string_of_int e);; (* ------------------------------------------------------------------------- *) @@ -123,7 +122,7 @@ let vector_dot (v1:vector) (v2:vector) = (combine ( */ ) (fun x -> x =/ Int 0) (snd v1) (snd v2));; let vector_of_list l = - let n = length l in + let n = List.length l in (n,itlist2 (|->) (1--n) l undefined :vector);; (* ------------------------------------------------------------------------- *) @@ -176,9 +175,9 @@ let diagonal (v:vector) = ((n,n),foldl (fun a i c -> ((i,i) |-> c) a) undefined (snd v) : matrix);; let matrix_of_list l = - let m = length l in + let m = List.length l in if m = 0 then matrix_0 (0,0) else - let n = length (hd l) in + let n = List.length (List.hd l) in (m,n),itern 1 l (fun v i -> itern 1 v (fun c j -> (i,j) |-> c)) undefined;; (* ------------------------------------------------------------------------- *) @@ -201,11 +200,11 @@ let monomial_pow (m:monomial) k = else mapf (fun x -> k * x) m;; let monomial_divides (m1:monomial) (m2:monomial) = - foldl (fun a x k -> tryapplyd m2 x 0 >= k & a) true m1;; + foldl (fun a x k -> tryapplyd m2 x 0 >= k && a) true m1;; let monomial_div (m1:monomial) (m2:monomial) = let m = combine (+) (fun x -> x = 0) m1 (mapf (fun x -> -x) m2) in - if foldl (fun a x k -> k >= 0 & a) true m then m + if foldl (fun a x k -> k >= 0 && a) true m then m else failwith "monomial_div: non-divisible";; let monomial_degree x (m:monomial) = tryapplyd m x 0;; @@ -227,7 +226,7 @@ let eval assig (p:poly) = let poly_0 = (undefined:poly);; -let poly_isconst (p:poly) = foldl (fun a m c -> m = monomial_1 & a) true p;; +let poly_isconst (p:poly) = foldl (fun a m c -> m = monomial_1 && a) true p;; let poly_var x = ((monomial_var x) |=> Int 1 :poly);; @@ -283,13 +282,13 @@ let poly_variables (p:poly) = (* Order monomials for human presentation. *) (* ------------------------------------------------------------------------- *) -let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 or x1 = x2 & k1 > k2;; +let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 or x1 = x2 && k1 > k2;; let humanorder_monomial = let rec ord l1 l2 = match (l1,l2) with _,[] -> true | [],_ -> false - | h1::t1,h2::t2 -> humanorder_varpow h1 h2 or h1 = h2 & ord t1 t2 in + | h1::t1,h2::t2 -> humanorder_varpow h1 h2 or h1 = h2 && ord t1 t2 in fun m1 m2 -> m1 = m2 or ord (sort humanorder_varpow (graph m1)) (sort humanorder_varpow (graph m2));; @@ -302,14 +301,14 @@ let string_of_vector min_size max_size (v:vector) = let n_raw = dim v in if n_raw = 0 then "[]" else let n = max min_size (min n_raw max_size) in - let xs = map ((o) string_of_num (element v)) (1--n) in + let xs = List.map ((o) string_of_num (element v)) (1--n) in "[" ^ end_itlist (fun s t -> s ^ ", " ^ t) xs ^ (if n_raw > max_size then ", ...]" else "]");; let string_of_matrix max_size (m:matrix) = let i_raw,j_raw = dimensions m in let i = min max_size i_raw and j = min max_size j_raw in - let rstr = map (fun k -> string_of_vector j j (row k m)) (1--i) in + let rstr = List.map (fun k -> string_of_vector j j (row k m)) (1--i) in "["^end_itlist(fun s t -> s^";\n "^t) rstr ^ (if j > max_size then "\n ...]" else "]");; @@ -408,7 +407,7 @@ let rec poly_of_term t = match t with let sdpa_of_vector (v:vector) = let n = dim v in - let strs = map (o (decimalize 20) (element v)) (1--n) in + let strs = List.map (o (decimalize 20) (element v)) (1--n) in end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";; (* ------------------------------------------------------------------------- *) @@ -445,15 +444,15 @@ let sdpa_of_matrix k (m:matrix) = (* ------------------------------------------------------------------------- *) let sdpa_of_problem comment obj mats = - let m = length mats - 1 - and n,_ = dimensions (hd mats) in + let m = List.length mats - 1 + and n,_ = dimensions (List.hd mats) in "\"" ^ comment ^ "\"\n" ^ string_of_int m ^ "\n" ^ "1\n" ^ string_of_int n ^ "\n" ^ sdpa_of_vector obj ^ itlist2 (fun k m a -> sdpa_of_matrix (k - 1) m ^ a) - (1--length mats) mats "";; + (1--List.length mats) mats "";; (* ------------------------------------------------------------------------- *) (* More parser basics. *) @@ -461,7 +460,7 @@ let sdpa_of_problem comment obj mats = let word s = end_itlist (fun p1 p2 -> (p1 ++ p2) >> (fun (s,t) -> s^t)) - (map a (explode s));; + (List.map a (explode s));; let token s = many (some isspace) ++ word s ++ many (some isspace) >> (fun ((_,t),_) -> t);; @@ -470,7 +469,7 @@ let decimal = let numeral = some isnum in let decimalint = atleast 1 numeral >> ((o) Num.num_of_string implode) in let decimalfrac = atleast 1 numeral - >> (fun s -> Num.num_of_string(implode s) // pow10 (length s)) in + >> (fun s -> Num.num_of_string(implode s) // pow10 (List.length s)) in let decimalsig = decimalint ++ possibly (a "." ++ decimalfrac >> snd) >> (function (h,[x]) -> h +/ x | (h,_) -> h) in @@ -626,13 +625,13 @@ let scale_then = fun solver obj mats -> let cd1 = itlist common_denominator mats (Int 1) and cd2 = common_denominator (snd obj) (Int 1) in - let mats' = map (mapf (fun x -> cd1 */ x)) mats + let mats' = List.map (mapf (fun x -> cd1 */ x)) mats and obj' = vector_cmul cd2 obj in let max1 = itlist maximal_element mats' (Int 0) and max2 = maximal_element (snd obj') (Int 0) in let scal1 = pow2 (20-int_of_float(log(float_of_num max1) /. log 2.0)) and scal2 = pow2 (20-int_of_float(log(float_of_num max2) /. log 2.0)) in - let mats'' = map (mapf (fun x -> x */ scal1)) mats' + let mats'' = List.map (mapf (fun x -> x */ scal1)) mats' and obj'' = vector_cmul scal2 obj' in solver obj'' mats'';; @@ -651,7 +650,7 @@ let nice_vector n = mapa (nice_rational n);; let linear_program_basic a = let m,n = dimensions a in - let mats = map (fun j -> diagonal (column j a)) (1--n) + let mats = List.map (fun j -> diagonal (column j a)) (1--n) and obj = vector_const (Int 1) m in let rv,res = run_csdp false obj mats in if rv = 1 or rv = 2 then false @@ -665,7 +664,7 @@ let linear_program_basic a = let linear_program a b = let m,n = dimensions a in if dim b <> m then failwith "linear_program: incompatible dimensions" else - let mats = diagonal b :: map (fun j -> diagonal (column j a)) (1--n) + let mats = diagonal b :: List.map (fun j -> diagonal (column j a)) (1--n) and obj = vector_const (Int 1) m in let rv,res = run_csdp false obj mats in if rv = 1 or rv = 2 then false @@ -679,10 +678,10 @@ let linear_program a b = (* ------------------------------------------------------------------------- *) let in_convex_hull pts pt = - let pts1 = (1::pt) :: map (fun x -> 1::x) pts in - let pts2 = map (fun p -> map (fun x -> -x) p @ p) pts1 in - let n = length pts + 1 - and v = 2 * (length pt + 1) in + let pts1 = (1::pt) :: List.map (fun x -> 1::x) pts in + let pts2 = List.map (fun p -> List.map (fun x -> -x) p @ p) pts1 in + let n = List.length pts + 1 + and v = 2 * (List.length pt + 1) in let m = v + n - 1 in let mat = (m,n), @@ -700,8 +699,8 @@ let minimal_convex_hull = | (m::ms) -> if in_convex_hull ms m then ms else ms@[m] in let augment m ms = funpow 3 augment1 (m::ms) in fun mons -> - let mons' = itlist augment (tl mons) [hd mons] in - funpow (length mons') augment1 mons';; + let mons' = itlist augment (List.tl mons) [List.hd mons] in + funpow (List.length mons') augment1 mons';; (* ------------------------------------------------------------------------- *) (* Stuff for "equations" (generic A->num functions). *) @@ -743,7 +742,7 @@ let eliminate_equations = let b = tryapplyd e v (Int 0) in if b =/ Int 0 then e else equation_add e (equation_cmul (minus_num b // a) eq) in - eliminate vs ((v |-> eq') (mapf elim dun)) (map elim oeqs) + eliminate vs ((v |-> eq') (mapf elim dun)) (List.map elim oeqs) with Failure _ -> eliminate vs dun eqs in fun one vars eqs -> let assig = eliminate vars undefined eqs in @@ -774,7 +773,7 @@ let eliminate_all_equations one = let b = tryapplyd e v (Int 0) in if b =/ Int 0 then e else equation_add e (equation_cmul (minus_num b // a) eq) in - eliminate ((v |-> eq') (mapf elim dun)) (map elim oeqs) in + eliminate ((v |-> eq') (mapf elim dun)) (List.map elim oeqs) in fun eqs -> let assig = eliminate undefined eqs in let vs = foldl (fun a x f -> subtract (dom f) [one] @ a) [] assig in @@ -805,14 +804,14 @@ let solve_equations one eqs = let newton_polytope pol = let vars = poly_variables pol in - let mons = map (fun m -> map (fun x -> monomial_degree x m) vars) (dom pol) - and ds = map (fun x -> (degree x pol + 1) / 2) vars in + let mons = List.map (fun m -> List.map (fun x -> monomial_degree x m) vars) (dom pol) + and ds = List.map (fun x -> (degree x pol + 1) / 2) vars in let all = itlist (fun n -> allpairs (fun h t -> h::t) (0--n)) ds [[]] and mons' = minimal_convex_hull mons in let all' = - filter (fun m -> in_convex_hull mons' (map (fun x -> 2 * x) m)) all in - map (fun m -> itlist2 (fun v i a -> if i = 0 then a else (v |-> i) a) - vars m monomial_1) (rev all');; + List.filter (fun m -> in_convex_hull mons' (List.map (fun x -> 2 * x) m)) all in + List.map (fun m -> itlist2 (fun v i a -> if i = 0 then a else (v |-> i) a) + vars m monomial_1) (List.rev all');; (* ------------------------------------------------------------------------- *) (* Diagonalize (Cholesky/LDU) the matrix corresponding to a quadratic form. *) @@ -851,10 +850,10 @@ let deration d = let a = foldl (fun a i c -> lcm_num a (denominator c)) (Int 1) (snd l) // foldl (fun a i c -> gcd_num a (numerator c)) (Int 0) (snd l) in (c // (a */ a)),mapa (fun x -> a */ x) l in - let d' = map adj d in + let d' = List.map adj d in let a = itlist ((o) lcm_num ( (o) denominator fst)) d' (Int 1) // itlist ((o) gcd_num ( (o) numerator fst)) d' (Int 0) in - (Int 1 // a),map (fun (c,l) -> (a */ c,l)) d';; + (Int 1 // a),List.map (fun (c,l) -> (a */ c,l)) d';; (* ------------------------------------------------------------------------- *) (* Enumeration of monomials with given multidegree bound. *) @@ -865,8 +864,8 @@ let rec enumerate_monomials d vars = else if d = 0 then [undefined] else if vars = [] then [monomial_1] else let alts = - map (fun k -> let oths = enumerate_monomials (d - k) (tl vars) in - map (fun ks -> if k = 0 then ks else (hd vars |-> k) ks) oths) + List.map (fun k -> let oths = enumerate_monomials (d - k) (List.tl vars) in + List.map (fun ks -> if k = 0 then ks else (List.hd vars |-> k) ks) oths) (0--d) in end_itlist (@) alts;; @@ -883,7 +882,7 @@ let rec enumerate_products d pols = | (p,b)::ps -> let e = multidegree p in if e = 0 then enumerate_products d ps else enumerate_products d ps @ - map (fun (q,c) -> poly_mul p q,Product(b,c)) + List.map (fun (q,c) -> poly_mul p q,Product(b,c)) (enumerate_products (d - e) ps);; (* ------------------------------------------------------------------------- *) @@ -936,15 +935,15 @@ let sdpa_of_blockdiagonal k m = (* ------------------------------------------------------------------------- *) let sdpa_of_blockproblem comment nblocks blocksizes obj mats = - let m = length mats - 1 in + let m = List.length mats - 1 in "\"" ^ comment ^ "\"\n" ^ string_of_int m ^ "\n" ^ string_of_int nblocks ^ "\n" ^ - (end_itlist (fun s t -> s^" "^t) (map string_of_int blocksizes)) ^ + (end_itlist (fun s t -> s^" "^t) (List.map string_of_int blocksizes)) ^ "\n" ^ sdpa_of_vector obj ^ itlist2 (fun k m a -> sdpa_of_blockdiagonal (k - 1) m ^ a) - (1--length mats) mats "";; + (1--List.length mats) mats "";; (* ------------------------------------------------------------------------- *) (* Hence run CSDP on a problem in block diagonal form. *) @@ -996,35 +995,35 @@ let bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);; (* ------------------------------------------------------------------------- *) let blocks blocksizes bm = - map (fun (bs,b0) -> + List.map (fun (bs,b0) -> let m = foldl (fun a (b,i,j) c -> if b = b0 then ((i,j) |-> c) a else a) undefined bm in (((bs,bs),m):matrix)) - (zip blocksizes (1--length blocksizes));; + (zip blocksizes (1--List.length blocksizes));; (* ------------------------------------------------------------------------- *) (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *) (* ------------------------------------------------------------------------- *) let real_positivnullstellensatz_general linf d eqs leqs pol = - let vars = itlist ((o) union poly_variables) (pol::eqs @ map fst leqs) [] in + let vars = itlist ((o) union poly_variables) (pol::eqs @ List.map fst leqs) [] in let monoid = if linf then (poly_const num_1,Rational_lt num_1):: - (filter (fun (p,c) -> multidegree p <= d) leqs) + (List.filter (fun (p,c) -> multidegree p <= d) leqs) else enumerate_products d leqs in - let nblocks = length monoid in + let nblocks = List.length monoid in let mk_idmultiplier k p = let e = d - multidegree p in let mons = enumerate_monomials e vars in - let nons = zip mons (1--length mons) in + let nons = zip mons (1--List.length mons) in mons, itlist (fun (m,n) -> (m |-> ((-k,-n,n) |=> Int 1))) nons undefined in let mk_sqmultiplier k (p,c) = let e = (d - multidegree p) / 2 in let mons = enumerate_monomials e vars in - let nons = zip mons (1--length mons) in + let nons = zip mons (1--List.length mons) in mons, itlist (fun (m1,n1) -> itlist (fun (m2,n2) a -> @@ -1035,9 +1034,9 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = (m |-> equation_add ((k,n1,n2) |=> c) e) a) nons) nons undefined in - let sqmonlist,sqs = unzip(map2 mk_sqmultiplier (1--length monoid) monoid) - and idmonlist,ids = unzip(map2 mk_idmultiplier (1--length eqs) eqs) in - let blocksizes = map length sqmonlist in + let sqmonlist,sqs = unzip(List.map2 mk_sqmultiplier (1--List.length monoid) monoid) + and idmonlist,ids = unzip(List.map2 mk_idmultiplier (1--List.length eqs) eqs) in + let blocksizes = List.map List.length sqmonlist in let bigsum = itlist2 (fun p q a -> epoly_pmul p q a) eqs ids (itlist2 (fun (p,c) s a -> epoly_pmul p s a) monoid sqs @@ -1053,10 +1052,10 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = ((b,j,i) |-> c) (((b,i,j) |-> c) m)) undefined allassig in let diagents = foldl - (fun a (b,i,j) e -> if b > 0 & i = j then equation_add e a else a) + (fun a (b,i,j) e -> if b > 0 && i = j then equation_add e a else a) undefined allassig in - let mats = map mk_matrix qvars - and obj = length pvs, + let mats = List.map mk_matrix qvars + and obj = List.length pvs, itern 1 pvs (fun v i -> (i |--> tryapplyd diagents v (Int 0))) undefined in let raw_vec = if pvs = [] then vector_0 0 @@ -1071,11 +1070,11 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = (fun i a -> bmatrix_add (bmatrix_cmul (element vec i) (el i mats)) a) (bmatrix_neg (el 0 mats)) in let allmats = blocks blocksizes blockmat in - vec,map diag allmats in + vec,List.map diag allmats in let vec,ratdias = if pvs = [] then find_rounding num_1 - else tryfind find_rounding (map Num.num_of_int (1--31) @ - map pow2 (5--66)) in + else tryfind find_rounding (List.map Num.num_of_int (1--31) @ + List.map pow2 (5--66)) in let newassigs = itlist (fun k -> el (k - 1) pvs |-> element vec k) (1--dim vec) ((0,0,0) |=> Int(-1)) in @@ -1088,11 +1087,11 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = let mk_sos mons = let mk_sq (c,m) = c,itlist (fun k a -> (el (k - 1) mons |--> element m k) a) - (1--length mons) undefined in - map mk_sq in - let sqs = map2 mk_sos sqmonlist ratdias - and cfs = map poly_of_epoly ids in - let msq = filter (fun (a,b) -> b <> []) (map2 (fun a b -> a,b) monoid sqs) in + (1--List.length mons) undefined in + List.map mk_sq in + let sqs = List.map2 mk_sos sqmonlist ratdias + and cfs = List.map poly_of_epoly ids in + let msq = List.filter (fun (a,b) -> b <> []) (List.map2 (fun a b -> a,b) monoid sqs) in let eval_sq sqs = itlist (fun (c,q) -> poly_add (poly_cmul c (poly_mul q q))) sqs poly_0 in let sanity = @@ -1100,7 +1099,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = (itlist2 (fun p q -> poly_add (poly_mul p q)) cfs eqs (poly_neg pol)) in if not(is_undefined sanity) then raise Sanity else - cfs,map (fun (a,b) -> snd a,b) msq;; + cfs,List.map (fun (a,b) -> snd a,b) msq;; (* ------------------------------------------------------------------------- *) (* Iterative deepening. *) @@ -1138,7 +1137,7 @@ let monomial_order = else lexorder mon1 mon2;; let dest_poly p = - map (fun (m,c) -> c,dest_monomial m) + List.map (fun (m,c) -> c,dest_monomial m) (sort (fun (m1,_) (m2,_) -> monomial_order m1 m2) (graph p));; (* ------------------------------------------------------------------------- *) @@ -1164,7 +1163,7 @@ let term_of_cmonomial = let term_of_poly = fun p -> if p = poly_0 then Zero else - let cms = map term_of_cmonomial + let cms = List.map term_of_cmonomial (sort (fun (m1,_) (m2,_) -> monomial_order m1 m2) (graph p)) in end_itlist (fun t1 t2 -> Add (t1,t2)) cms;; @@ -1173,7 +1172,7 @@ let term_of_sqterm (c,p) = let term_of_sos (pr,sqs) = if sqs = [] then pr - else Product(pr,end_itlist (fun a b -> Sum(a,b)) (map term_of_sqterm sqs));; + else Product(pr,end_itlist (fun a b -> Sum(a,b)) (List.map term_of_sqterm sqs));; (* ------------------------------------------------------------------------- *) (* Interface to HOL. *) @@ -1236,7 +1235,7 @@ let REAL_NONLINEAR_SUBST_PROVER = match tm with Var(_,Tyapp("real",[])) when not (mem tm fvs) -> Int 1,tm | Comb(Comb(Const("real_mul",_),c),(Var(_,_) as t)) - when is_ratconst c & not (mem t fvs) + when is_ratconst c && not (mem t fvs) -> rat_of_term c,t | Comb(Comb(Const("real_add",_),s),t) -> (try substitutable_monomial (union (frees t) fvs) s @@ -1292,10 +1291,10 @@ let REAL_SOSFIELD = with Failure _ -> REAL_SOS t and is_inv = let is_div = is_binop `(/):real->real->real` in - fun tm -> (is_div tm or (is_comb tm & rator tm = inv_tm)) & + fun tm -> (is_div tm or (is_comb tm && rator tm = inv_tm)) && not(is_ratconst(rand tm)) in let BASIC_REAL_FIELD tm = - let is_freeinv t = is_inv t & free_in t tm in + let is_freeinv t = is_inv t && free_in t tm in let itms = setify(map rand (find_terms is_freeinv tm)) in let hyps = map (fun t -> SPEC t REAL_MUL_RINV) itms in let tm' = itlist (fun th t -> mk_imp(concl th,t)) hyps tm in @@ -1371,14 +1370,14 @@ let SOS_RULE tm = let rec allpermutations l = if l = [] then [[]] else - itlist (fun h acc -> map (fun t -> h::t) + itlist (fun h acc -> List.map (fun t -> h::t) (allpermutations (subtract l [h])) @ acc) l [];; let allvarorders l = - map (fun vlis x -> index x vlis) (allpermutations l);; + List.map (fun vlis x -> index x vlis) (allpermutations l);; let changevariables_monomial zoln (m:monomial) = - foldl (fun a x k -> (assoc x zoln |-> k) a) monomial_1 m;; + foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;; let changevariables zoln pol = foldl (fun a m c -> (changevariables_monomial zoln m |-> c) a) @@ -1390,7 +1389,7 @@ let changevariables zoln pol = let sdpa_of_vector (v:vector) = let n = dim v in - let strs = map (o (decimalize 20) (element v)) (1--n) in + let strs = List.map (o (decimalize 20) (element v)) (1--n) in end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";; let sdpa_of_blockdiagonal k m = @@ -1412,15 +1411,15 @@ let sdpa_of_matrix k (m:matrix) = " " ^ decimalize 20 c ^ "\n" ^ a) mss "";; let sdpa_of_problem comment obj mats = - let m = length mats - 1 - and n,_ = dimensions (hd mats) in + let m = List.length mats - 1 + and n,_ = dimensions (List.hd mats) in "\"" ^ comment ^ "\"\n" ^ string_of_int m ^ "\n" ^ "1\n" ^ string_of_int n ^ "\n" ^ sdpa_of_vector obj ^ itlist2 (fun k m a -> sdpa_of_matrix (k - 1) m ^ a) - (1--length mats) mats "";; + (1--List.length mats) mats "";; let run_csdp dbg obj mats = let input_file = Filename.temp_file "sos" ".dat-s" in @@ -1455,33 +1454,33 @@ let csdp obj mats = let sumofsquares_general_symmetry tool pol = let vars = poly_variables pol and lpps = newton_polytope pol in - let n = length lpps in + let n = List.length lpps in let sym_eqs = - let invariants = filter + let invariants = List.filter (fun vars' -> is_undefined(poly_sub pol (changevariables (zip vars vars') pol))) (allpermutations vars) in - let lpns = zip lpps (1--length lpps) in + let lpns = zip lpps (1--List.length lpps) in let lppcs = - filter (fun (m,(n1,n2)) -> n1 <= n2) + List.filter (fun (m,(n1,n2)) -> n1 <= n2) (allpairs (fun (m1,n1) (m2,n2) -> (m1,m2),(n1,n2)) lpns lpns) in let clppcs = end_itlist (@) - (map (fun ((m1,m2),(n1,n2)) -> - map (fun vars' -> + (List.map (fun ((m1,m2),(n1,n2)) -> + List.map (fun vars' -> (changevariables_monomial (zip vars vars') m1, changevariables_monomial (zip vars vars') m2),(n1,n2)) invariants) lppcs) in - let clppcs_dom = setify(map fst clppcs) in - let clppcs_cls = map (fun d -> filter (fun (e,_) -> e = d) clppcs) + let clppcs_dom = setify(List.map fst clppcs) in + let clppcs_cls = List.map (fun d -> List.filter (fun (e,_) -> e = d) clppcs) clppcs_dom in - let eqvcls = map (o setify (map snd)) clppcs_cls in + let eqvcls = List.map (o setify (List.map snd)) clppcs_cls in let mk_eq cls acc = match cls with [] -> raise Sanity | [h] -> acc - | h::t -> map (fun k -> (k |-> Int(-1)) (h |=> Int 1)) t @ acc in + | h::t -> List.map (fun k -> (k |-> Int(-1)) (h |=> Int 1)) t @ acc in itlist mk_eq eqvcls [] in let eqs = foldl (fun a x y -> y::a) [] (itern 1 lpps (fun m1 n1 -> @@ -1497,15 +1496,15 @@ let sumofsquares_general_symmetry tool pol = let allassig = itlist (fun v -> (v |-> (v |=> Int 1))) pvs assig in let qvars = (0,0)::pvs in let diagents = - end_itlist equation_add (map (fun i -> apply allassig (i,i)) (1--n)) in + end_itlist equation_add (List.map (fun i -> apply allassig (i,i)) (1--n)) in let mk_matrix v = ((n,n), foldl (fun m (i,j) ass -> let c = tryapplyd ass v (Int 0) in if c =/ Int 0 then m else ((j,i) |-> c) (((i,j) |-> c) m)) undefined allassig :matrix) in - let mats = map mk_matrix qvars - and obj = length pvs, + let mats = List.map mk_matrix qvars + and obj = List.length pvs, itern 1 pvs (fun v i -> (i |--> tryapplyd diagents v (Int 0))) undefined in let raw_vec = if pvs = [] then vector_0 0 else tool obj mats in @@ -1524,12 +1523,12 @@ let sumofsquares_general_symmetry tool pol = let mat = matrix_neg (el 0 mats) in deration(diag mat) else - tryfind find_rounding (map Num.num_of_int (1--31) @ - map pow2 (5--66)) in + tryfind find_rounding (List.map Num.num_of_int (1--31) @ + List.map pow2 (5--66)) in let poly_of_lin(d,v) = d,foldl(fun a i c -> (el (i - 1) lpps |-> c) a) undefined (snd v) in - let lins = map poly_of_lin dia in - let sqs = map (fun (d,l) -> poly_mul (poly_const d) (poly_pow l 2)) lins in + let lins = List.map poly_of_lin dia in + let sqs = List.map (fun (d,l) -> poly_mul (poly_const d) (poly_pow l 2)) lins in let sos = poly_cmul rat (end_itlist poly_add sqs) in if is_undefined(poly_sub sos pol) then rat,lins else raise Sanity;; diff --git a/plugins/micromega/sos.mli b/plugins/micromega/sos.mli index d7314ccb..fc0b2fd4 100644 --- a/plugins/micromega/sos.mli +++ b/plugins/micromega/sos.mli @@ -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 *) diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index baf90d4d..f54914f2 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -2,13 +2,12 @@ (* - This code originates from John Harrison's HOL LIGHT 2.30 *) (* (see file LICENSE.sos for license, copyright and disclaimer) *) (* This code is the HOL LIGHT library code used by sos.ml *) -(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) +(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) (* independent bits *) -(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) +(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) (* ========================================================================= *) -open Sos_types + open Num -open List let debugging = ref false;; @@ -16,11 +15,13 @@ let debugging = ref false;; (* Comparisons that are reflexive on NaN and also short-circuiting. *) (* ------------------------------------------------------------------------- *) -let (=?) = fun x y -> Pervasives.compare x y = 0;; -let (<?) = fun x y -> Pervasives.compare x y < 0;; -let (<=?) = fun x y -> Pervasives.compare x y <= 0;; -let (>?) = fun x y -> Pervasives.compare x y > 0;; -let (>=?) = fun x y -> Pervasives.compare x y >= 0;; +let cmp = Pervasives.compare (** FIXME *) + +let (=?) = fun x y -> cmp x y = 0;; +let (<?) = fun x y -> cmp x y < 0;; +let (<=?) = fun x y -> cmp x y <= 0;; +let (>?) = fun x y -> cmp x y > 0;; +let (>=?) = fun x y -> cmp x y >= 0;; (* ------------------------------------------------------------------------- *) (* Combinators. *) @@ -53,7 +54,7 @@ let gcd_num n1 n2 = num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));; let lcm_num x y = - if x =/ num_0 & y =/ num_0 then num_0 + if x =/ num_0 && y =/ num_0 then num_0 else abs_num((x */ y) // gcd_num x y);; @@ -62,7 +63,7 @@ let lcm_num x y = (* ------------------------------------------------------------------------- *) let rec el n l = - if n = 0 then hd l else el (n - 1) (tl l);; + if n = 0 then List.hd l else el (n - 1) (List.tl l);; (* ------------------------------------------------------------------------- *) @@ -141,7 +142,7 @@ let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);; let rec forall p l = match l with [] -> true - | h::t -> p(h) & forall p t;; + | h::t -> p(h) && forall p t;; let rec tryfind f l = match l with @@ -162,14 +163,14 @@ let index x = let rec mem x lis = match lis with [] -> false - | (h::t) -> x =? h or mem x t;; + | (h::t) -> x =? h || mem x t;; let insert x l = if mem x l then l else x::l;; let union l1 l2 = itlist insert l1 l2;; -let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1;; +let subtract l1 l2 = List.filter (fun x -> not (mem x l2)) l1;; (* ------------------------------------------------------------------------- *) (* Merging and bottom-up mergesort. *) @@ -224,7 +225,7 @@ let rec sort cmp lis = match lis with [] -> [] | piv::rest -> - let r,l = partition (cmp piv) rest in + let r,l = List.partition (cmp piv) rest in (sort cmp l) @ (piv::(sort cmp r));; (* ------------------------------------------------------------------------- *) @@ -416,7 +417,7 @@ let (|=>) = fun x y -> (x |-> y) undefined;; let rec choose t = match t with Empty -> failwith "choose: completely undefined function" - | Leaf(h,l) -> hd l + | Leaf(h,l) -> List.hd l | Branch(b,p,t1,t2) -> choose t1;; (* ------------------------------------------------------------------------- *) @@ -547,7 +548,7 @@ let fix err prs input = try prs input with Noparse -> failwith (err ^ " expected");; -let rec listof prs sep err = +let listof prs sep err = prs ++ many (sep ++ fix err prs >> snd) >> (fun (h,t) -> h::t);; let possibly prs input = @@ -583,7 +584,7 @@ let strings_of_file filename = let rec suck_lines acc = try let l = Pervasives.input_line fd in suck_lines (l::acc) - with End_of_file -> rev acc in + with End_of_file -> List.rev acc in let data = suck_lines [] in (Pervasives.close_in fd; data);; diff --git a/plugins/micromega/sos_types.ml b/plugins/micromega/sos_types.ml index 351a3133..e9543714 100644 --- a/plugins/micromega/sos_types.ml +++ b/plugins/micromega/sos_types.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 *) diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget index 30201308..bf6a1a7d 100644 --- a/plugins/micromega/vo.itarget +++ b/plugins/micromega/vo.itarget @@ -1,4 +1,3 @@ -CheckerMaker.vo EnvRing.vo Env.vo OrderedRing.vo @@ -11,3 +10,4 @@ Tauto.vo VarMap.vo ZCoeff.vo ZMicromega.vo +Lia.vo
\ No newline at end of file |