diff options
Diffstat (limited to 'src/verilog/Value.v')
-rw-r--r-- | src/verilog/Value.v | 44 |
1 files changed, 36 insertions, 8 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 1d31110..21e59be 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -60,13 +60,6 @@ Definition valueToN (v : value) : N := Definition NToValue sz (n : N) : value := mkvalue sz (NToWord sz n). -Definition posToValue sz (p : positive) : value := - mkvalue sz (posToWord sz p). - -Definition posToValueAuto (p : positive) : value := - let size := Z.to_nat (Z.succ (log_inf p)) in - mkvalue size (Word.posToWord size p). - Definition ZToValue (s : nat) (z : Z) : value := mkvalue s (ZToWord s z). @@ -76,6 +69,19 @@ Definition valueToZ (v : value) : Z := Definition uvalueToZ (v : value) : Z := uwordToZ (vword v). +Definition posToValue sz (p : positive) : value := + mkvalue sz (posToWord sz p). + +Definition posToValueAuto (p : positive) : value := + let size := Z.to_nat (Z.succ (log_inf p)) in + mkvalue size (Word.posToWord size p). + +Definition valueToPos (v : value) : positive := + match valueToZ v with + | Zpos p => p + | _ => 1 + end. + Definition intToValue (i : Integers.int) : value := ZToValue Int.wordsize (Int.unsigned i). @@ -95,8 +101,10 @@ Definition boolToValue (sz : nat) (b : bool) : value := (** ** Arithmetic operations *) +Definition EQ_trivial : forall x, vsize x = vsize x. trivial. Defined. + Lemma unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. -Proof. intros; subst; assumption. Qed. +Proof. intros; subst; assumption. Defined. Definition value_eq_size: forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. @@ -141,6 +149,26 @@ Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value) | _ => None end. +Lemma eqvalue {sz : nat} (x y : word sz) : x = y -> (mkvalue sz x = mkvalue sz y). +Proof. intros. subst. reflexivity. Qed. + +Lemma nevalue {sz : nat} (x y : word sz) : x <> y -> (mkvalue sz x <> mkvalue sz y). +Proof. Admitted. + +Definition valueEqCheck (sz : nat) (x y : word sz) : + {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} := + match weq x y with + | left eq => left (eqvalue x y eq) + | right ne => right (nevalue x y ne) + end. + +Definition valueEq (x y : value) (EQ : vsize x = vsize y): {x = y} + {x <> y} := + let unif_y := unify_word (vsize x) (vsize y) (vword y) EQ in + match weq (vword x) unif_y with + | left _ => left _ + | right _ => right _ + end. + (** Arithmetic operations over [value], interpreting them as signed or unsigned depending on the operation. |