From e6eacd35e2822712b35723b372b167ab894d8472 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Thu, 11 May 2017 16:37:58 +0200
Subject: 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.
---
 plugins/romega/ReflOmegaCore.v | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'plugins/romega/ReflOmegaCore.v')

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} *)
-- 
cgit v1.2.3