blob: 0d213222476d112b02fd62a20e41a3ee2283d089 (
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
38
39
|
{-# OPTIONS --safe --without-K #-}
module Helium.Instructions where
open import Data.Fin
open import Data.Nat
open import Data.Sum
open import Relation.Binary.PropositionalEquality
GenReg : Set
GenReg = Fin 16
VecReg : Set
VecReg = Fin 8
module VAdd
where
record VAdd : Set where
field
size : Fin 3
dest : VecReg
src₁ : VecReg
src₂ : GenReg ⊎ VecReg
esize : VAdd → Fin 33
esize record { size = zero } = # 8
esize record { size = (suc zero) } = # 16
esize record { size = (suc (suc zero)) } = # 32
elements : VAdd → Fin 5
elements record { size = zero } = # 4
elements record { size = (suc zero) } = # 2
elements record { size = (suc (suc zero)) } = # 1
elem*esize≡32 : ∀ d → toℕ (elements d) * toℕ (esize d) ≡ 32
elem*esize≡32 record { size = zero } = refl
elem*esize≡32 record { size = (suc zero) } = refl
elem*esize≡32 record { size = (suc (suc zero)) } = refl
|
