diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-11 16:37:58 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:15:49 +0200 |
commit | e6eacd35e2822712b35723b372b167ab894d8472 (patch) | |
tree | b706f808fab5f2c1d9e84298e1b34a78bfde4d41 | |
parent | f3b186bad386f6215aa9d9ebd02ab97246ee50c1 (diff) |
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.
-rw-r--r-- | plugins/romega/ReflOmegaCore.v | 15 | ||||
-rw-r--r-- | plugins/romega/const_omega.ml | 41 | ||||
-rw-r--r-- | plugins/romega/const_omega.mli | 2 | ||||
-rw-r--r-- | plugins/romega/refl_omega.ml | 2 |
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 |] |