blob: 66ffbf227858d799ae4a7c9db6d6c7f7c0d99b13 (
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
|
From Coq
Require Import Int63.
Import ZArith.
Declare Scope uint_scope.
Declare Scope sint_scope.
Delimit Scope uint_scope with uint.
Delimit Scope sint_scope with sint.
Record uint := wrapu { unwrapu : int }.
Record sint := wraps { unwraps : int }.
Definition uof_Z (v : Z) := wrapu (of_Z v).
Definition uto_Z (v : uint) := to_Z (unwrapu v).
Definition sof_Z (v : Z) := wraps (of_Z (v mod (2 ^ 31))).
Definition as_signed (bw : Z) (v : Z) :=
(((2 ^ (bw - 1) + v) mod (2 ^ bw)) - 2 ^ (bw - 1))%Z.
Definition sto_Z (v : sint) := as_signed 31 (to_Z (unwraps v)).
Number Notation uint uof_Z uto_Z : uint_scope.
Number Notation sint sof_Z sto_Z : sint_scope.
Open Scope uint_scope.
Compute uof_Z 0.
Compute uof_Z 1.
Compute uof_Z (-1).
Check let v := 0 in v : uint.
Check let v := 1 in v : uint.
Check let v := -1 in v : uint.
Close Scope uint_scope.
Open Scope sint_scope.
Compute sof_Z 0.
Compute sof_Z 1.
Compute sof_Z (-1).
Check let v := 0 in v : sint.
Check let v := 1 in v : sint.
Check let v := -1 in v : sint.
|
