Make [neg] a unary operation in reflection

It now takes a meta-level [Z] argument which is the bit width.  I
haven't modified any of the extraction directives, so I don't know if
extraction still works nicely.

1 files changed, 20 insertions, 5 deletions

diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v
index 116e3513e..ab47929b1 100644
--- a/src/Reflection/Z/Syntax.v
+++ b/src/Reflection/Z/Syntax.v
@@ -39,7 +39,7 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type :=
 | Shr : op (tZ * tZ) tZ
 | Land : op (tZ * tZ) tZ
 | Lor : op (tZ * tZ) tZ
-| Neg : op (tZ * tZ) tZ
+| Neg (int_width : Z) : op tZ tZ
 | Cmovne : op (tZ * tZ * tZ * tZ) tZ
 | Cmovle : op (tZ * tZ * tZ * tZ) tZ.
 
@@ -52,7 +52,7 @@ Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_typ
      | Shr => fun xy => fst xy >> snd xy
      | Land => fun xy => Z.land (fst xy) (snd xy)
      | Lor => fun xy => Z.lor (fst xy) (snd xy)
-     | Neg => fun xy => ModularBaseSystemListZOperations.neg (fst xy) (snd xy)
+     | Neg int_width => fun x => ModularBaseSystemListZOperations.neg int_width x
      | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w
      | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovl x y z w
      end%Z.
@@ -83,8 +83,8 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : reifi
      | Land, _ => false
      | Lor, Lor => true
      | Lor, _ => false
-     | Neg, Neg => true
-     | Neg, _ => false
+     | Neg n, Neg m => Z.eqb n m
+     | Neg _, _ => false
      | Cmovne, Cmovne => true
      | Cmovne, _ => false
      | Cmovle, Cmovle => true
@@ -112,7 +112,22 @@ Definition op_beq_hetero_eq {t1 tR t1' tR'} f g
       _ (op_beq_hetero_type_eqs f g pf)
     = g.
 Proof.
-  destruct f, g; simpl; try solve [ reflexivity | intros [] ].
+  destruct f, g; simpl; try solve [ reflexivity | intros [] ];
+    unfold op_beq_hetero; simpl;
+      repeat match goal with
+             | [ |- context[to_prop (reified_Prop_of_bool ?x)] ]
+               => destruct (Sumbool.sumbool_of_bool x) as [P|P]
+             | [ H : NatUtil.nat_beq _ _ = true |- _ ]
+               => apply NatUtil.internal_nat_dec_bl in H
+             | [ H : Z.eqb _ _ = true |- _ ]
+               => apply Z.eqb_eq in H
+             | _ => progress subst
+             | _ => reflexivity
+             | [ H : ?x = false |- context[reified_Prop_of_bool ?x] ]
+               => rewrite H
+             | _ => progress simpl @to_prop
+             | _ => tauto
+             end.
 Qed.
 
 Lemma op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y.