Frontend for the standard version of Coq (still bad computational behavior)

1 files changed, 35 insertions, 49 deletions

diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/versions/standard/Int63/Int63Op_standard.v
index 933a045..119e6bd 100644
--- a/src/versions/standard/Int63/Int63Op_standard.v
+++ b/src/versions/standard/Int63/Int63Op_standard.v
@@ -15,38 +15,34 @@
 (**************************************************************************)
 
 
+Require Import Int63Lib Cyclic63.
 Require Export Int63Native.
 Require Import BigNumPrelude.
 Require Import Bvector.
 
-Set Vm Optimize.
-
 
 Local Open Scope int63_scope.
 
 (** The number of digits as a int *)
-Definition digits := 63.
+Definition digits := zdigits.
 
 (** The bigger int *)
 Definition max_int := Eval vm_compute in 0 - 1.
-Register max_int as PrimInline.
 
 (** Access to the nth digits *)
 Definition get_digit x p := (0 < (x land (1 << p))).
 
 Definition set_digit x p (b:bool) :=
-  if (0 <= p) && (p < digits) then 
+  if (0 <= p) && (p < digits) then
     if b then x lor (1 << p)
     else x land (max_int lxor (1 << p))
   else x.
 
 (** Equality to 0 *)
 Definition is_zero (i:int) := i == 0.
-Register is_zero as PrimInline.
 
 (** Parity *)
 Definition is_even (i:int) := is_zero (i land 1).
-Register is_even as PrimInline.
 
 (** Bit *)
 
@@ -55,100 +51,88 @@ Definition bit i n :=  negb (is_zero ((i >> n) << (digits - 1))).
 
 (** Extra modulo operations *)
 Definition opp (i:int) := 0 - i.
-Register opp as PrimInline.
 Notation "- x" := (opp x) : int63_scope.
 
 Definition oppcarry i := max_int - i.
-Register oppcarry as PrimInline.
 
 Definition succ i := i + 1.
-Register succ as PrimInline.
 
 Definition pred i := i - 1.
-Register pred as PrimInline.
 
 Definition addcarry i j := i + j + 1.
-Register addcarry as PrimInline.
 
 Definition subcarry i j := i - j - 1.
-Register subcarry as PrimInline.
 
 (** Exact arithmetic operations *)
 
 Definition addc_def x y :=
   let r := x + y in
   if r < x then C1 r else C0 r.
-(* the same but direct implementation for effeciancy *)
-Register addc      : int -> int -> carry int as int63_addc.
+(* the same but direct implementation for efficiancy *)
+Definition addc : int -> int -> carry int := add63c.
 Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope.
 
 Definition addcarryc_def x y :=
   let r := addcarry x y in
   if r <= x then C1 r else C0 r.
-(* the same but direct implementation for effeciancy *)
-Register addcarryc : int -> int -> carry int as int63_addcarryc.
+(* the same but direct implementation for efficiancy *)
+Definition addcarryc : int -> int -> carry int := add63carryc.
 
-Definition subc_def x y := 
+Definition subc_def x y :=
   if y <= x then C0 (x - y) else C1 (x - y).
-(* the same but direct implementation for effeciancy *)
-Register subc      : int -> int -> carry int as int63_subc.
+(* the same but direct implementation for efficiancy *)
+Definition subc : int -> int -> carry int := sub63c.
 Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope.
 
 Definition subcarryc_def x y :=
   if y < x then C0 (x - y - 1) else C1 (x - y - 1).
-(* the same but direct implementation for effeciancy *)
-Register subcarryc : int -> int -> carry int as int63_subcarryc.
+(* the same but direct implementation for efficiancy *)
+Definition subcarryc : int -> int -> carry int := sub63carryc.
 
 Definition diveucl_def x y := (x/y, x\%y).
-(* the same but direct implementation for effeciancy *) 
-Register diveucl   : int -> int -> int * int as int63_diveucl.
+(* the same but direct implementation for efficiancy *)
+Definition diveucl : int -> int -> int * int := div63.
 
-Register diveucl_21    : int -> int -> int -> int * int as int63_div21.
+Definition diveucl_21 : int -> int -> int -> int * int := div6321.
 
 Definition addmuldiv_def p x y :=
   (x << p) lor (y >> (digits - p)).
-Register addmuldiv   : int -> int -> int -> int as int63_addmuldiv.
+(* the same but direct implementation for efficiancy *)
+Definition addmuldiv : int -> int -> int -> int := addmuldiv63.
 
 Definition oppc (i:int) := 0 -c i.
-Register oppc as PrimInline.
 
 Definition succc i := i +c 1.
-Register succc as PrimInline.
 
 Definition predc i := i -c 1.
-Register predc as PrimInline.
 
 (** Comparison *)
 Definition compare_def x y :=
-  if x < y then Lt 
+  if x < y then Lt
   else if (x == y) then Eq else Gt.
 
-Register compare : int -> int -> comparison as int63_compare.
+Definition compare : int -> int -> comparison := compare63.
 Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope.
 
 (** Exotic operations *)
 
 (** I should add the definition (like for compare) *)
-Register head0 : int -> int as int63_head0.
-Register tail0 : int -> int as int63_tail0.
+Definition head0 : int -> int := head063.
+Definition tail0 : int -> int := tail063.
 
 (** Iterators *)
 
 Definition foldi {A} (f:int -> A -> A) from to :=
   foldi_cont (fun i cont a => cont (f i a)) from to (fun a => a).
-Register foldi as PrimInline.
 
 Definition fold {A} (f: A -> A) from to :=
   foldi_cont (fun i cont a => cont (f a)) from to (fun a => a).
-Register fold as PrimInline.
 
 Definition foldi_down {A} (f:int -> A -> A) from downto :=
   foldi_down_cont (fun i cont a => cont (f i a)) from downto (fun a => a).
-Register foldi_down as PrimInline.
 
 Definition fold_down {A} (f:A -> A) from downto :=
   foldi_down_cont (fun i cont a => cont (f a)) from downto (fun a => a).
-Register fold_down as PrimInline.
 
 Definition forallb (f:int -> bool) from to :=
   foldi_cont (fun i cont _ => if f i then cont tt else false) from to (fun _ => true) tt.
@@ -158,17 +142,19 @@ Definition existsb (f:int -> bool) from to :=
 
 (** Translation to Z *)
 
-Fixpoint to_Z_rec (n:nat) (i:int) :=
-  match n with 
-  | O => 0%Z 
-  | S n => 
-    (if is_even i then Zdouble else Zdouble_plus_one) (to_Z_rec n (i >> 1))
-  end.
+(* Fixpoint to_Z_rec (n:nat) (i:int) := *)
+(*   match n with *)
+(*   | O => 0%Z *)
+(*   | S n => *)
+(*     (if is_even i then Zdouble else Zdouble_plus_one) (to_Z_rec n (i >> 1)) *)
+(*   end. *)
 
-Definition to_Z := to_Z_rec size.
+(* Definition to_Z := to_Z_rec size. *)
+
+Definition to_Z := phi.
 
 Fixpoint of_pos_rec (n:nat) (p:positive) :=
-  match n, p with 
+  match n, p with
   | O, _ => 0
   | S n, xH => 1
   | S n, xO p => (of_pos_rec n p) << 1
@@ -177,7 +163,7 @@ Fixpoint of_pos_rec (n:nat) (p:positive) :=
 
 Definition of_pos := of_pos_rec size.
 
-Definition of_Z z := 
+Definition of_Z z :=
   match z with
   | Zpos p => of_pos p
   | Z0 => 0
@@ -227,7 +213,7 @@ Definition sqrt2_step (rec: int -> int -> int -> int)
       match j +c quo with
       | C0 m1 => rec ih il (m1 >> 1)
       | C1 m1 => rec ih il ((m1 >> 1) + high_bit)
-      end 
+      end
     else j
   else j.
 
@@ -237,7 +223,7 @@ Definition iter2_sqrt :=
           (rec: int  -> int -> int -> int)
           (ih il j: int) {struct n} : int :=
   sqrt2_step
-   (fun ih il j => 
+   (fun ih il j =>
      match n with
      | O =>  rec ih il j
      | S n => (iter2_sqrt n (iter2_sqrt n rec)) ih il j
@@ -254,7 +240,7 @@ Definition sqrt2 ih il :=
   end.
 
 (* Extra function on equality *)
- 
+
 Definition cast i j :=
      (if i == j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j))
       then fun Heq : true = true -> i = j =>