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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
|
From Coq Require Import Lists.List Strings.String.
From Coq Require Import
Structures.OrderedTypeEx
FSets.FMapList
Program.Basics
PeanoNat.
From CoqUp Require Import Helper Tactics Show.
Import ListNotations.
Module Verilog.
Module Map := FMapList.Make String_as_OT.
Inductive value : Type :=
| VBool (b : bool)
| VArray (l : list value).
Definition cons_value (a b : value) : value :=
match a, b with
| VBool _, VArray b' => VArray (a :: b')
| VArray a', VBool _ => VArray (List.concat [a'; [b]])
| VArray a', VArray b' => VArray (List.concat [a'; b'])
| _, _ => VArray [a; b]
end.
(** * Conversion to and from value *)
Fixpoint nat_to_value' (sz n : nat) : value :=
match sz with
| 0 => VArray []
| S sz' =>
if Nat.even n then
cons_value (VBool false) (nat_to_value' sz' (Nat.div n 2))
else
cons_value (VBool true) (nat_to_value' sz' (Nat.div n 2))
end.
Definition nat_to_value (n : nat) : value :=
nat_to_value' ((Nat.log2 n) + 1) n.
Definition state : Type := Map.t value * Map.t value.
Inductive binop : Type :=
| Plus
| Minus
| Times
| Divide
| LT
| GT
| LE
| GE
| Eq
| And
| Or
| Xor.
Inductive expr : Type :=
| Lit (n : value)
| Var (s : string)
| Neg (a : expr)
| BinOp (op : binop) (a1 a2 : expr)
| Ternary (c t f : expr).
Inductive stmnt : Type :=
| Skip
| Block (s : list stmnt)
| Cond (c : expr) (st sf : stmnt)
| Case (c : expr) (b : list (expr * stmnt))
| Blocking (a b : expr)
| Nonblocking (a b : expr).
Inductive verilog : Type := Verilog (s : list stmnt).
Coercion VBool : bool >-> value.
Coercion Lit : value >-> expr.
Coercion Var : string >-> expr.
Definition value_is_bool (v : value) : bool :=
match v with
| VBool _ => true
| VArray _ => false
end.
Definition value_is_array : value -> bool := compose negb value_is_bool.
Definition flat_value (v : value) : bool :=
match v with
| VBool _ => true
| VArray l => forallb value_is_bool l
end.
Inductive value_is_boolP : value -> Prop :=
| ValIsBool : forall b : bool, value_is_boolP (VBool b).
Inductive value_is_arrayP : value -> Prop :=
| ValIsArray : forall v : list value, value_is_arrayP (VArray v).
Inductive flat_valueP : value -> Prop :=
| FLV0 : forall b : bool, flat_valueP (VBool b)
| FLVA : forall l : list value,
Forall (value_is_boolP) l -> flat_valueP (VArray l).
Lemma value_is_bool_equiv :
forall v, value_is_boolP v <-> value_is_bool v = true.
Proof.
split; intros.
- inversion H. trivial.
- destruct v. constructor. unfold value_is_bool in H. discriminate.
Qed.
Lemma value_is_array_equiv :
forall v, value_is_arrayP v <-> value_is_array v = true.
Proof.
split; intros.
- inversion H. trivial.
- destruct v; try constructor. unfold value_is_array in H.
unfold compose, value_is_bool, negb in H. discriminate.
Qed.
Lemma flat_value_equiv :
forall v, flat_valueP v <-> flat_value v = true.
Proof.
split; intros.
- unfold flat_value. inversion H. subst. trivial.
+ rewrite Forall_forall in H0. rewrite forallb_forall. intros. subst.
apply value_is_bool_equiv. apply H0. assumption.
- destruct v. constructor. constructor. unfold flat_value in H.
rewrite Forall_forall. rewrite forallb_forall in H. intros. apply value_is_bool_equiv.
apply H. assumption.
Qed.
Fixpoint value_to_nat' (i : nat) (v : value) : option nat :=
match i, v with
| _, VBool b => Some (Nat.b2n b)
| _, VArray [VBool b] => Some (Nat.b2n b)
| S i', VArray ((VBool b) :: l) =>
Option.map (compose (Nat.add (Nat.b2n b)) (Mult.tail_mult 2)) (value_to_nat' i' (VArray l))
| _, _ => None
end.
Definition value_length (v : value) : nat :=
match v with
| VBool _ => 1
| VArray l => Datatypes.length l
end.
Definition value_to_nat (v : value) : option nat :=
value_to_nat' (value_length v) v.
Lemma empty_is_flat : flat_valueP (VArray []).
Proof.
constructor. apply Forall_forall. intros. inversion H.
Qed.
Lemma check_5_is_101 :
value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5.
Proof. reflexivity. Qed.
Lemma cons_value_flat :
forall (b : bool) (v : value),
flat_valueP v -> flat_valueP (cons_value (VBool b) v).
Proof.
intros. unfold cons_value. destruct v.
- constructor. apply Forall_forall. intros.
inversion H0; subst. constructor.
inversion H1; subst. constructor.
inversion H2.
- intros. inversion H. inversion H1; subst; constructor.
+ apply Forall_forall. intros.
inversion H0; subst. constructor.
inversion H2.
+ repeat constructor. assumption. assumption.
Qed.
Lemma nat_to_value'_is_flat :
forall (sz n : nat),
flat_valueP (nat_to_value' sz n).
Proof.
induction sz; intros.
- subst. apply empty_is_flat.
- unfold_rec nat_to_value'.
destruct (Nat.even n); apply cons_value_flat; apply IHsz.
Qed.
Lemma nat_to_value_is_flat :
forall (sz n : nat),
flat_valueP (nat_to_value n).
Proof.
intros. unfold nat_to_value. apply nat_to_value'_is_flat.
Qed.
Lemma nat_to_value_idempotent :
forall (sz n : nat),
sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n.
Proof.
induction sz; intros.
- inversion H.
- unfold_rec value_to_nat'.
assert (flat_valueP (nat_to_value' (S sz) n)).
{ apply nat_to_value'_is_flat. }
destruct (nat_to_value' (S sz) n) eqn:?.
Admitted.
Module VerilogEval.
Definition app (f : nat -> nat -> nat) (a : value) (b : value) : option value :=
Option.map nat_to_value (Option.liftA2 f (value_to_nat a) (value_to_nat b)).
Definition state_find (k : string) (s : state) : option value :=
Map.find k (fst s).
Definition eval_binop (op : binop) (a1 a2 : value) : option value :=
match op with
| Plus => app Nat.add a1 a2
| Minus => app Nat.sub a1 a2
| Times => app Mult.tail_mult a1 a2
| Divide => app Nat.div a1 a2
| _ => Some a1
end.
(* Fixpoint eval_expr (s : state) (e : expr) : option value :=
match e with
| Lit n => Some n
| Var v => state_find v s
| Neg a => 0 - (eval_expr s a)
| BinOp op a1 a2 => eval_binop op a1 a2
| Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f
end.
*)
End VerilogEval.
End Verilog.
Export Verilog.
|
