does not yet work, arity mismatch

1 files changed, 1 insertions, 15 deletions

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 629d1449..e460727c 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -35,6 +35,7 @@ Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
 Require Import Sorting.Permutation.
+Require Import Chunks.
 
 (** * Abstract syntax *)
 
@@ -1119,21 +1120,6 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
   | Some v => Next (rsw#d <- v) mw
   end.
 
-Definition zscale_of_chunk (chunk: memory_chunk) :=
-  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)).
-
 Definition parexec_load_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
   match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with
   | None => Stuck