romega: use N instead of nat for Tvar

 In a coming commit, we'll normalize terms by a Coq function
 that will compare Tvar's instead of blindly applying a trace,
 so let's speed-up these comparisons.

4 files changed, 39 insertions, 21 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index b0c9cd6e5..dad9909d2 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -796,7 +796,7 @@ Inductive term : Set :=
   | Tmult : term -> term -> term
   | Tminus : term -> term -> term
   | Topp : term -> term
-  | Tvar : nat -> term.
+  | Tvar : N -> term.
 
 Delimit Scope romega_scope with term.
 Arguments Tint _%I.
@@ -980,7 +980,7 @@ Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
   | (st11 * st12), (st21 * st22) => eq_term st11 st21 && eq_term st12 st22
   | (st11 - st12), (st21 - st22) => eq_term st11 st21 && eq_term st12 st22
   | (- st1), (- st2) => eq_term st1 st2
-  | [st1], [st2] => beq_nat st1 st2
+  | [st1], [st2] => N.eqb st1 st2
   | _, _ => false
   end.
 
@@ -990,7 +990,7 @@ Theorem eq_term_iff (t t' : term) :
  eq_term t t' = true <-> t = t'.
 Proof.
  revert t'. induction t; destruct t'; simpl in *;
- rewrite ?andb_true_iff, ?beq_iff, ?Nat.eqb_eq, ?IHt, ?IHt1, ?IHt2;
+ rewrite ?andb_true_iff, ?beq_iff, ?N.eqb_eq, ?IHt, ?IHt1, ?IHt2;
   intuition congruence.
 Qed.
 
@@ -1002,6 +1002,13 @@ Qed.
 (* \subsection{Interprétations}
    \subsubsection{Interprétation des termes dans Z} *)
 
+Fixpoint Nnth {A} (n:N)(l:list A)(default:A) :=
+ match n, l with
+   | _, nil => default
+   | 0%N, x::_ => x
+   | _, _::l => Nnth (N.pred n) l default
+ end.
+
 Fixpoint interp_term (env : list int) (t : term) {struct t} : int :=
   match t with
   | Tint x => x
@@ -1009,7 +1016,7 @@ Fixpoint interp_term (env : list int) (t : term) {struct t} : int :=
   | (t1 * t2)%term => interp_term env t1 * interp_term env t2
   | (t1 - t2)%term => interp_term env t1 - interp_term env t2
   | (- t)%term => - interp_term env t
-  | [n]%term => nth n env 0
+  | [n]%term => Nnth n env 0
   end.
 
 (* \subsubsection{Interprétation des prédicats} *)
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index cf5d20aeb..f7eab17df 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -274,6 +274,30 @@ let parse_logic_rel c =
    | _ -> Rother
  with e when Logic.catchable_exception e -> Rother
 
+(* Binary numbers *)
+
+let coq_xH = lazy (bin_constant "xH")
+let coq_xO = lazy (bin_constant "xO")
+let coq_xI = lazy (bin_constant "xI")
+let coq_Z0 = lazy (bin_constant "Z0")
+let coq_Zpos = lazy (bin_constant "Zpos")
+let coq_Zneg = lazy (bin_constant "Zneg")
+let coq_N0 = lazy (bin_constant "N0")
+let coq_Npos = lazy (bin_constant "Npos")
+
+let rec mk_positive n =
+  if Bigint.equal n Bigint.one then Lazy.force coq_xH
+  else
+    let (q,r) = Bigint.euclid n Bigint.two in
+    Term.mkApp
+      ((if Bigint.equal r Bigint.zero
+        then Lazy.force coq_xO else Lazy.force coq_xI),
+       [| mk_positive q |])
+
+let mk_N = function
+  | 0 -> Lazy.force coq_N0
+  | n -> Term.mkApp (Lazy.force coq_Npos,
+                     [| mk_positive (Bigint.of_int n) |])
 
 module type Int = sig
   val typ : Term.constr Lazy.t
@@ -297,13 +321,6 @@ let mult = lazy (z_constant  "Z.mul")
 let opp = lazy (z_constant "Z.opp")
 let minus = lazy (z_constant "Z.sub")
 
-let coq_xH = lazy (bin_constant "xH")
-let coq_xO = lazy (bin_constant "xO")
-let coq_xI = lazy (bin_constant "xI")
-let coq_Z0 = lazy (bin_constant "Z0")
-let coq_Zpos = lazy (bin_constant "Zpos")
-let coq_Zneg = lazy (bin_constant "Zneg")
-
 let recognize t =
   let rec loop t =
     let f,l = dest_const_apply t in
@@ -319,16 +336,8 @@ let recognize t =
       | "Z0",[] -> Bigint.zero
       | _ -> failwith "not a number";;
 
-let rec mk_positive n =
-  if n=Bigint.one then Lazy.force coq_xH
-  else
-    let (q,r) = Bigint.euclid n Bigint.two in
-    Term.mkApp
-      ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI),
-       [| mk_positive q |])
-
 let mk_Z n =
-  if n = Bigint.zero then Lazy.force coq_Z0
+  if Bigint.equal n Bigint.zero then Lazy.force coq_Z0
   else if Bigint.is_strictly_pos n then
     Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
   else
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 1c67af806..2901cc028 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -116,6 +116,8 @@ val do_seq : Term.constr -> Term.constr -> Term.constr
 val do_list : Term.constr list -> Term.constr
 
 val mk_nat : int -> Term.constr
+val mk_N : int -> Term.constr
+
 (** Precondition: the type of the list is in Set *)
 val mk_list : Term.constr -> Term.constr list -> Term.constr
 val mk_plist : Term.types list -> Term.types
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 85f076760..a0ed68a8a 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -371,7 +371,7 @@ let rec reified_of_formula env = function
       app coq_t_mult [| reified_of_formula env t1; reified_of_formula env t2 |]
   | Oint v ->  app coq_t_int [| Z.mk v |]
   | Oufo t -> reified_of_formula env t
-  | Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |]
+  | Oatom i -> app coq_t_var [| mk_N (reified_of_atom env i) |]
   | Ominus(t1,t2) ->
       app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]