{-# 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