blob: 4edd2e3d914923275947d99d3890235c0346e47b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Floats.
Definition bits_of_float x :=
match x with
| Vfloat f => Vlong (Float.to_bits f)
| _ => Vundef
end.
Definition bits_of_single x :=
match x with
| Vsingle f => Vint (Float32.to_bits f)
| _ => Vundef
end.
Definition bitwise_select_int b vtrue vfalse :=
Val.or (Val.and (Val.neg b) vtrue)
(Val.and (Val.sub b Vone) vfalse).
Lemma bitwise_select_int_true :
forall vtrue vfalse,
bitwise_select_int (Val.of_optbool (Some true)) (Vint vtrue) (Vint vfalse)
= Vint vtrue.
Proof.
intros. cbn. f_equal.
change (Int.neg Int.one) with Int.mone.
rewrite Int.and_commut.
rewrite Int.and_mone.
rewrite Int.sub_idem.
rewrite Int.and_commut.
rewrite Int.and_zero.
apply Int.or_zero.
Qed.
Lemma bitwise_select_int_false :
forall vtrue vfalse,
bitwise_select_int (Val.of_optbool (Some false)) (Vint vtrue) (Vint vfalse)
= Vint vfalse.
Proof.
intros. cbn. f_equal.
rewrite Int.neg_zero.
rewrite Int.and_commut.
rewrite Int.and_zero.
rewrite Int.sub_zero_r.
change (Int.neg Int.one) with Int.mone.
rewrite Int.and_commut.
rewrite Int.and_mone.
rewrite Int.or_commut.
apply Int.or_zero.
Qed.
Definition bitwise_select_long b vtrue vfalse :=
let b' := Val.longofint b in
Val.orl (Val.andl (Val.negl b') vtrue)
(Val.andl (Val.subl b' (Vlong Int64.one)) vfalse).
Lemma bitwise_select_long_true :
forall vtrue vfalse,
bitwise_select_long (Val.of_optbool (Some true)) (Vlong vtrue) (Vlong vfalse)
= Vlong vtrue.
Proof.
intros. cbn. f_equal.
change (Int64.neg Int64.one) with Int64.mone.
rewrite Int64.and_commut.
rewrite Int64.and_mone.
rewrite Int64.sub_idem.
rewrite Int64.and_commut.
rewrite Int64.and_zero.
apply Int64.or_zero.
Qed.
Lemma bitwise_select_long_false :
forall vtrue vfalse,
bitwise_select_long (Val.of_optbool (Some false)) (Vlong vtrue) (Vlong vfalse)
= Vlong vfalse.
Proof.
intros. cbn. f_equal.
change (Int64.repr (Int.signed Int.zero)) with Int64.zero.
rewrite Int64.neg_zero.
rewrite Int64.and_commut.
rewrite Int64.and_zero.
rewrite Int64.sub_zero_r.
change (Int64.neg Int64.one) with Int64.mone.
rewrite Int64.and_commut.
rewrite Int64.and_mone.
rewrite Int64.or_commut.
apply Int64.or_zero.
Qed.
(*
Compute (Int.unsigned (Float32.to_bits (Float32.of_int (Int.repr 4200)))).
Compute (Int64.unsigned (Float.to_bits (Float.of_int (Int.repr 4233)))).
*)
|
