From de86de8c74dd6714517d27712d6397efd4599814 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sun, 29 Mar 2009 15:40:31 +0000 Subject: 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 --- plugins/micromega/mutils.ml | 17 ----------------- 1 file changed, 17 deletions(-) (limited to 'plugins/micromega/mutils.ml') diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 03e3999fd..23db2928a 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -14,9 +14,6 @@ let debug = false -let fst' (Micromega.Pair(x,y)) = x -let snd' (Micromega.Pair(x,y)) = y - let map_option f x = match x with | None -> None @@ -225,11 +222,6 @@ struct let num x = Num.Big_int (z_big_int x) - let rec list elt l = - match l with - | Nil -> [] - | Cons(e,l) -> (elt e)::(list elt l) - let q_to_num {qnum = x ; qden = y} = Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y))) @@ -256,10 +248,6 @@ struct else if 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)) @@ -279,8 +267,6 @@ struct (List.rev (digits_of_int n)) (XH) - - let z x = match compare x 0 with | 0 -> Z0 @@ -311,9 +297,6 @@ struct {Micromega.qnum = bigint (numerator n) ; Micromega.qden = positive_big_int (denominator n)} - - let list elt l = List.fold_right (fun x l -> Cons(elt x, l)) l Nil - end module Cmp = -- cgit v1.2.3