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, 19 insertions, 1 deletions

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index a5ac92db8..b4b40ca73 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -20,4 +20,22 @@ Require Import VarMap.
 Require Import RingMicromega.
 Require Import NArith.
 
-Extraction "micromega.ml"  List.map simpl_cone map_cone indexes  n_of_Z Nnat.N_of_nat ZTautoChecker QTautoChecker find.
+Extract Inductive prod => "( * )" [ "(,)" ].
+Extract Inductive List.list => list [ "[]" "(::)" ].
+Extract Inductive bool => bool [ true false ].
+Extract Inductive sumbool => bool [ true false ].
+Extract Inductive option => option [ Some None ].
+Extract Inductive sumor => option [ Some None ].
+(** Then, in a ternary alternative { }+{ }+{ },
+   -  leftmost choice (Inleft Left) is (Some true),
+   -  middle choice (Inleft Right) is (Some false),
+   -  rightmost choice (Inright) is (None) *)
+
+
+(** To preserve its laziness, andb is normally expansed.
+    Let's rather use the ocaml && *)
+Extract Inlined Constant andb => "(&&)".
+
+Extraction "micromega.ml"
+  List.map simpl_cone map_cone indexes
+  n_of_Z Nnat.N_of_nat ZTautoChecker QTautoChecker find.