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