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/RingMicromega.v | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'plugins/micromega/RingMicromega.v') 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 -- cgit v1.2.3