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, 7 insertions, 5 deletions

diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 6885b82cd..c093d7ca0 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -420,9 +420,10 @@ Qed.
 (* Provides the cone member from the witness, i.e., ConeMember *)
 Fixpoint eval_cone (l : list NFormula) (cm : ConeMember) {struct cm} : NFormula :=
 match cm with
-| S_In n => match nth n l (PEc cO, Equal) with
-            | (_, NonEqual) => (PEc cO, Equal)
-            | f => f
+| S_In n => let f := nth n l (PEc cO, Equal) in
+            match f with
+              | (_, NonEqual) => (PEc cO, Equal)
+              | _ => f
             end
 | S_Ideal p cm' => nformula_times_0 p (eval_cone l cm')
 | S_Square p => (PEmul p p, NonStrict)
@@ -746,9 +747,10 @@ Fixpoint simpl_expr (e:PExprC) : PExprC :=
 
 Definition simpl_cone (e:ConeMember) : ConeMember :=
   match e with
-    | S_Square t => match simpl_expr t with
+    | S_Square t => let x:=simpl_expr t in
+                    match x with
                       | PEc c   => if ceqb cO c then S_Z else S_Pos (ctimes c c)
-                      |       x     => S_Square x
+                      | _ => S_Square x
                     end
     | S_Mult t1 t2 => 
       match t1 , t2 with