blob: 912d6daf7bb0e8083247b53cebb503d1ee1ad88a (
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
{-# OPTIONS --without-K --safe #-}
------------------------------------------------------------------------
-- 2.5 Modules
module Wasm.Expression.Modules where
open import Data.Maybe using (Maybe)
open import Wasm.Expression.Types
open import Wasm.Expression.Utilities using (Vec′; module Indices)
open import Wasm.Expression.Values using (Byte; Name)
open import Wasm.Expression.Instructions using (Expr)
------------------------------------------------------------------------
-- 2.5.1 Indices
-- NOTE: defined in Wasm.Expression.Utilities
------------------------------------------------------------------------
-- 2.5.2 Types
-- NOTE: no new definitions
------------------------------------------------------------------------
-- 2.5.3 Functions
record Func : Set where
field
type : Indices.TypeIdx
locals : Vec′ ValType
body : Expr
------------------------------------------------------------------------
-- 2.5.4 Tables
Table : Set
Table = TableType
------------------------------------------------------------------------
-- 2.5.5 Memories
Mem : Set
Mem = MemType
------------------------------------------------------------------------
-- 2.5.6 Globals
record Global : Set where
field
type : GlobalType
init : Expr
------------------------------------------------------------------------
-- 2.5.7 Element Segments
data ElemMode : Set where
passive : ElemMode
active : (table : Indices.TableIdx) → (offset : Expr) → ElemMode
declarative : ElemMode
record Elem : Set where
field
type : RefType
init : Vec′ Expr
mode : ElemMode
------------------------------------------------------------------------
-- 2.5.8 Data Segments
data DataMode : Set where
passive : DataMode
active : (memory : Indices.MemIdx) → (offset : Expr) → DataMode
record Data : Set where
field
init : Vec′ Byte
mode : DataMode
------------------------------------------------------------------------
-- 2.5.9 Start Function
Start : Set
Start = Indices.FuncIdx
------------------------------------------------------------------------
-- 2.5.10 Exports
data ExportDesc : Set where
func : Indices.FuncIdx → ExportDesc
table : Indices.TableIdx → ExportDesc
mem : Indices.MemIdx → ExportDesc
global : Indices.GlobalIdx → ExportDesc
record Export : Set where
field
name : Name
desc : ExportDesc
------------------------------------------------------------------------
-- 2.5.11 Imports
data ImportDesc : Set where
func : Indices.TypeIdx → ImportDesc
table : TableType → ImportDesc
mem : MemType → ImportDesc
global : GlobalType → ImportDesc
record Import : Set where
field
mod : Name
name : Name
desc : ImportDesc
------------------------------------------------------------------------
-- Module definition
record Mod : Set where
field
types : Vec′ FuncType
funcs : Vec′ Func
tables : Vec′ Table
mems : Vec′ Mem
globals : Vec′ Global
elems : Vec′ Elem
datas : Vec′ Data
start : Maybe Start
imports : Vec′ Import
exports : Vec′ Export
|
