Micromega: improvement of the code obtained by extraction

  * In eval_cone and simpl_cone, default patterns were leading
    to duplicated computations. Adaptation of RingMicromega.v
    to prevent that.
  * Use the Ocaml builtin types (lists, pairs, bool, etc) and
    remove the useless conversion functions in mutils.ml and alii.
  * andb was extracted to a correctly lazy but ugly match.
    Let's rather use Ocaml's (&&).

  Remain to be done: take advantage of extraction during the build,
   - either directly if we are using plugins, (no dependency issues)
   - or if we compile statically, at least check later that the
     micromega.ml in the archive and the one auto-generated are in sync.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12034 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 33 deletions

diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index f94f091e8..948391466 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -1,22 +1,11 @@
 type __ = Obj.t
 
-type bool =
-  | True
-  | False
-
 val negb : bool -> bool
 
 type nat =
   | O
   | S of nat
 
-type 'a option =
-  | Some of 'a
-  | None
-
-type ('a, 'b) prod =
-  | Pair of 'a * 'b
-
 type comparison =
   | Eq
   | Lt
@@ -24,18 +13,6 @@ type comparison =
 
 val compOpp : comparison -> comparison
 
-type sumbool =
-  | Left
-  | Right
-
-type 'a sumor =
-  | Inleft of 'a
-  | Inright
-
-type 'a list =
-  | Nil
-  | Cons of 'a * 'a list
-
 val app : 'a1 list -> 'a1 list -> 'a1 list
 
 val nth : nat -> 'a1 list -> 'a1 -> 'a1
@@ -105,11 +82,11 @@ val zmult : z -> z -> z
 
 val zcompare : z -> z -> comparison
 
-val dcompare_inf : comparison -> sumbool sumor
+val dcompare_inf : comparison -> bool option
 
 val zcompare_rec : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 
-val z_gt_dec : z -> z -> sumbool
+val z_gt_dec : z -> z -> bool
 
 val zle_bool : z -> z -> bool
 
@@ -121,9 +98,9 @@ val zeq_bool : z -> z -> bool
 
 val n_of_nat : nat -> n
 
-val zdiv_eucl_POS : positive -> z -> (z, z) prod
+val zdiv_eucl_POS : positive -> z -> z  *  z
 
-val zdiv_eucl : z -> z -> (z, z) prod
+val zdiv_eucl : z -> z -> z  *  z
 
 type 'c pol =
   | Pc of 'c
@@ -257,7 +234,7 @@ type op1 =
   | Strict
   | NonStrict
 
-type 'c nFormula = ('c pExprC, op1) prod
+type 'c nFormula = 'c pExprC  *  op1
 
 type monoidMember = nat list
 
@@ -331,6 +308,10 @@ val qnum : q -> z
 
 val qden : q -> positive
 
+val qeq_bool : q -> q -> bool
+
+val qle_bool : q -> q -> bool
+
 val qplus : q -> q -> q
 
 val qmult : q -> q -> q
@@ -371,7 +352,7 @@ val qceiling : q -> z
 
 val makeLbCut : z pExprC -> q -> z nFormula
 
-val neg_nformula : z nFormula -> (z pExpr, op1) prod
+val neg_nformula : z nFormula -> z pExpr  *  op1
 
 val cutChecker :
   z nFormula list -> z pExpr -> q -> zWitness -> z nFormula option
@@ -386,10 +367,6 @@ val indexes : zWitness -> nat list
 
 val n_of_Z : z -> n
 
-val qeq_bool : q -> q -> bool
-
-val qle_bool : q -> q -> bool
-
 type qWitness = q coneMember
 
 val qWeakChecker : q nFormula list -> q coneMember -> bool