blob: f7c25647168d6e7355672bea611e5265b4ecedc4 (
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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
{-# OPTIONS --without-K --safe #-}
------------------------------------------------------------------------
-- Type Context
module Wasm.Validation.Context where
open import Data.Fin using (Fin; toℕ; fromℕ<)
open import Data.List using (List; length; lookup)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (_<?_; _^_)
open import Data.Unit using (⊤)
open import Relation.Nullary using (yes; no)
open import Wasm.Constants
open import Wasm.Expression.Types
open import Wasm.Expression.Utilities using (module Indices)
record Context : Set where
field
types : List FuncType
funcs : List FuncType
tables : List TableType
mems : List MemType
globals : List GlobalType
elems : List RefType
datas : List ⊤
locals : List ValType
labels : List ResultType
return : Maybe ResultType
refs : List Indices.FuncIdx
private
get : ∀ {A} → List A → Fin 2^32 → Maybe A
get xs idx with toℕ idx <? length xs
... | yes idx<∣xs∣ = just (lookup xs (fromℕ< idx<∣xs∣))
... | no _ = nothing
getType : Indices.TypeIdx → Maybe FuncType
getType = get types
getFunc : Indices.FuncIdx → Maybe FuncType
getFunc = get funcs
getTable : Indices.TableIdx → Maybe TableType
getTable = get tables
getMem : Indices.MemIdx → Maybe MemType
getMem = get mems
getGlobal : Indices.GlobalIdx → Maybe GlobalType
getGlobal = get globals
getElem : Indices.ElemIdx → Maybe RefType
getElem = get elems
getData : Indices.DataIdx → Maybe ⊤
getData = get datas
getLocal : Indices.LocalIdx → Maybe ValType
getLocal = get locals
getLabel : Indices.LabelIdx → Maybe ResultType
getLabel = get labels
|
