Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)

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

2 files changed, 23 insertions, 7 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 20016281a..3aa075384 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -214,14 +214,29 @@ Module ZnZ.
 
  Let wB := base digits.
 
- Definition WO h :=
+ Definition WO' (eq0:t->bool) zero h :=
   if eq0 h then W0 else WW h zero.
 
- Definition OW l :=
+ Definition WO := Eval lazy beta delta [WO'] in
+   let eq0 := ZnZ.eq0 in
+   let zero := ZnZ.zero in
+   WO' eq0 zero.
+
+ Definition OW' (eq0:t->bool) zero l :=
   if eq0 l then W0 else WW zero l.
 
- Definition WW h l :=
-  if eq0 h then OW l else WW h l.
+ Definition OW := Eval lazy beta delta [OW'] in
+   let eq0 := ZnZ.eq0 in
+   let zero := ZnZ.zero in
+   OW' eq0 zero.
+
+ Definition WW'  (eq0:t->bool) zero h l :=
+  if eq0 h then OW' eq0 zero l else WW h l.
+
+ Definition WW := Eval lazy beta delta [WW' OW'] in
+   let eq0 := ZnZ.eq0 in
+   let zero := ZnZ.zero in
+   WW' eq0 zero.
 
  Lemma spec_WO : forall h,
    zn2z_to_Z wB to_Z (WO h) = (to_Z h)*wB.
@@ -247,6 +262,7 @@ Module ZnZ.
  unfold WW; simpl; intros.
  case_eq (eq0 h); intros.
  rewrite (spec_eq0 _ H); auto.
+ fold (OW l).
  rewrite spec_OW; auto.
  simpl; auto.
  Qed.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 286424974..c30d38186 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -103,9 +103,9 @@ Section Z_2nZ.
 
  Let to_Z := zn2z_to_Z wB w_to_Z.
 
- Let w_W0 (x:t) := ZnZ.WO x.
- Let w_0W (x:t) := ZnZ.OW x.
- Let w_WW (x y:t) := ZnZ.WW x y.
+ Let w_W0 := ZnZ.WO.
+ Let w_0W := ZnZ.OW.
+ Let w_WW := ZnZ.WW.
 
  Let ww_of_pos p :=
   match w_of_pos p with