diff options
Diffstat (limited to 'mppa_k1c/Chunks.v')
| -rw-r--r-- | mppa_k1c/Chunks.v | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/mppa_k1c/Chunks.v b/mppa_k1c/Chunks.v deleted file mode 100644 index 40778877..00000000 --- a/mppa_k1c/Chunks.v +++ /dev/null @@ -1,22 +0,0 @@ -Require Import AST. -Require Import Values. -Require Import Integers. -Require Import Coq.ZArith.BinIntDef. -Require Import BinNums. - -Local Open Scope Z_scope. - -Definition zscale_of_chunk (chunk: memory_chunk) : Z := - match chunk with - | Mint8signed => 0 - | Mint8unsigned => 0 - | Mint16signed => 1 - | Mint16unsigned => 1 - | Mint32 => 2 - | Mint64 => 3 - | Mfloat32 => 2 - | Mfloat64 => 3 - | Many32 => 2 - | Many64 => 3 - end. -Definition scale_of_chunk chunk := Vint (Int.repr (zscale_of_chunk chunk)). |