2 files changed, 52 insertions, 6 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index b5bcfe5f..e37e9d26 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -9,12 +9,6 @@ Require Import ZArith.
 Require Import Omega.
 Require Import Eqdep_dec.
 
-Module Z_eq_dec.
-Definition U := Z.
-Definition eq_dec := Z.eq_dec.
-End Z_eq_dec.
-Module ZEqdep := DecidableEqDep (Z_eq_dec).
-
 Fixpoint cast_positive (T : positive -> Type) (p q : positive) : T p -> p = q -> T q.
 refine (
 match p, q with
@@ -444,6 +438,20 @@ Definition sgteq_vec := sgteq_bv.
 
 *)
 
+Definition eq_vec_dec {n} : forall (x y : mword n), {x = y} + {x <> y}.
+refine (match n with
+| Z0 => _
+| Zpos m => _
+| Zneg m => _
+end).
+* simpl. apply Word.weq.
+* simpl. apply Word.weq.
+* simpl. destruct x.
+Defined.
+
+Instance Decidable_eq_mword {n} : forall (x y : mword n), Decidable (x = y) :=
+  Decidable_eq_from_dec eq_vec_dec.
+
 Program Fixpoint reverse_endianness_word {n} (bits : word n) : word n :=
   match n with
   | S (S (S (S (S (S (S (S m))))))) =>
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 83fe1dc7..48cfc222 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -8,10 +8,18 @@ Require Import bbv.Word.
 Require Export List.
 Require Export Sumbool.
 Require Export DecidableClass.
+Require Import Eqdep_dec.
 Import ListNotations.
 
 Open Scope Z.
 
+Module Z_eq_dec.
+Definition U := Z.
+Definition eq_dec := Z.eq_dec.
+End Z_eq_dec.
+Module ZEqdep := DecidableEqDep (Z_eq_dec).
+
+
 (* Constraint solving basics.  A HintDb which unfolding hints and lemmata
    can be added to, and a typeclass to wrap constraint arguments in to
    trigger automatic solving. *)
@@ -93,6 +101,22 @@ split.
   tauto.
 Qed.
 
+Definition generic_dec {T:Type} (x y:T) `{Decidable (x = y)} : {x = y} + {x <> y}.
+refine ((if Decidable_witness as b return (b = true <-> x = y -> _) then fun H' => _ else fun H' => _) Decidable_spec).
+* left. tauto.
+* right. intuition.
+Defined.
+
+(* Used by generated code that builds Decidable equality instances for records. *)
+Ltac cmp_record_field x y :=
+  let H := fresh "H" in
+  case (generic_dec x y);
+  intro H; [ |
+    refine (Build_Decidable _ false _);
+    split; [congruence | intros Z; destruct H; injection Z; auto]
+  ].
+
+
 
 (* Project away range constraints in comparisons *)
 Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.ltb (projT1 l) r.
@@ -1736,6 +1760,20 @@ Qed.
 
 Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v.
 
+Definition vec_eq_dec {T n} (D : forall x y : T, {x = y} + {x <> y}) (x y : vec T n) :
+  {x = y} + {x <> y}.
+refine (if List.list_eq_dec D (projT1 x) (projT1 y) then left _ else right _).
+* apply eq_sigT_hprop; auto using ZEqdep.UIP.
+* contradict n0. rewrite n0. reflexivity.
+Defined.
+
+Instance Decidable_eq_vec {T : Type} {n} `(DT : forall x y : T, Decidable (x = y)) :
+  forall x y : vec T n, Decidable (x = y) := {
+  Decidable_witness := proj1_sig (bool_of_sumbool (vec_eq_dec (fun x y => generic_dec x y) x y))
+}.
+destruct (vec_eq_dec _ x y); simpl; split; congruence.
+Defined.
+
 Program Definition vec_of_list {A} n (l : list A) : option (vec A n) :=
   if sumbool_of_bool (n =? length_list l) then Some (existT _ l _) else None.
 Next Obligation.