has_type_b

1 files changed, 21 insertions, 0 deletions

diff --git a/common/Values.v b/common/Values.v
index 4146dd59..5d32e54e 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -89,6 +89,27 @@ Definition has_type (v: val) (t: typ) : Prop :=
   | _, _ => False
   end.
 
+Definition has_type_b (v: val) (t: typ) :=
+  match v, t with
+  | Vundef, _ => true
+  | Vint _, Tint => true
+  | Vlong _, Tlong => true
+  | Vfloat _, Tfloat => true
+  | Vsingle _, Tsingle => true
+  | Vptr _ _, Tint => negb Archi.ptr64
+  | Vptr _ _, Tlong => Archi.ptr64
+  | (Vint _ | Vsingle _), Tany32 => true
+  | Vptr _ _, Tany32 => negb Archi.ptr64
+  | _, Tany64 => true
+  | _, _ => false
+  end.
+
+Lemma has_type_b_correct: forall v t,
+    has_type_b v t = true <-> has_type v t.
+Proof.
+  destruct v; destruct t; cbn; destruct Archi.ptr64; cbn; split; intros; auto; discriminate.
+Qed.
+
 Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop :=
   match vl, tl with
   | nil, nil => True