{-# OPTIONS --without-K --safe #-}

------------------------------------------------------------------------
-- 3.4 Modules

module Wasm.Validation.Modules where

open import Data.List using (List; []; _∷_; _++_; map; mapMaybe; allFin; replicate)
open import Data.List.Relation.Unary.All using (All)
open import Data.List.Relation.Unary.AllPairs using (AllPairs)
open import Data.List.Relation.Binary.Pointwise using (Pointwise)
open import Data.Maybe using (just; nothing; maybe)
open import Data.Nat using (_≤_; z≤n; s≤s; _^_)
open import Data.Product using (_×_; ∃; _,_; proj₁; proj₂)
open import Data.Sum using (inj₁)
open import Data.Unit using (⊤)
open import Data.Vec using ([]; _∷_)
open import Data.Vec.Bounded using (Vec≤; _,_; toList)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Wasm.Constants
open import Wasm.Expression.Modules
open import Wasm.Expression.Types
open import Wasm.Expression.Utilities using (module Indices)
open import Wasm.Expression.Values using (toString)
open import Wasm.Validation.Context
open import Wasm.Validation.Instructions hiding (_≤_)
open import Wasm.Validation.Types

------------------------------------------------------------------------
-- 3.4.1 Functions

record FuncOk (C : Context) (F : Func) (τ : FuncType) : Set where
  private
    module C = Context C
    module F = Func F
    module τ = FuncType τ

  field
    typeEq : C.getType F.type ≡ just τ
    exprOk : record C
      { locals = toList F.locals ++ toList τ.from
      ; labels = τ.to ∷ []
      ; return = just τ.to
      } ⊢ᵉ F.body ∶ τ.to

------------------------------------------------------------------------
-- 3.4.2 Tables

TableOk : Context → Table → TableType → Set
TableOk C tbl τ = tbl ≡ τ × TableTypeOk τ

------------------------------------------------------------------------
-- 3.4.3 Memories

MemOk : Context → Mem → MemType → Set
MemOk C mry τ = mry ≡ τ × MemTypeOk τ

------------------------------------------------------------------------
-- 3.4.4 Globals

record GlobalOk (C : Context) (G : Global) (τ : GlobalType) : Set where
  private
    module C = Context C
    module G = Global G
    mut = proj₁ τ
    t = proj₂ τ

  field
    typeEq    : G.type ≡ τ
    typeOk    : GlobalTypeOk τ
    initOk    : C ⊢ᵉ G.init ∶ t ∷ [] , s≤s z≤n
    initConst : C ⊢* G.init const

------------------------------------------------------------------------
-- 3.4.5 Element Segments

data ElemModeOk : Context → ElemMode → RefType → Set where
  passive : ∀ {C τ} → ElemModeOk C passive τ
  active : ∀ {C x lim off t} → Context.getTable C x ≡ just (lim , t) → C ⊢ᵉ off ∶ inj₁ i32 ∷ [] , s≤s z≤n → C ⊢* off const → ElemModeOk C (active x off) t
  declarative : ∀ {C τ} → ElemModeOk C declarative τ

record ElemOk (C : Context) (E : Elem) (τ : RefType) : Set where
  private
    module C = Context C
    module E = Elem E

  field
    typeEq     : E.type ≡ τ
    initsOk    : All (λ e → ∃ (C ⊢ᵉ e ∶_)) (toList E.init)
    initsConst : All (C ⊢*_const) (toList E.init)
    modeOk     : ElemModeOk C E.mode E.type

------------------------------------------------------------------------
-- 3.4.6 Data Segments

data DataModeOk : Context → DataMode → Set where
  passive : ∀ {C} → DataModeOk C passive
  active : ∀ {C x lim off} → Context.getMem C x ≡ just lim → C ⊢ᵉ off ∶ inj₁ i32 ∷ [] , s≤s z≤n → C ⊢* off const → DataModeOk C (active x off)

DataOk : Context → Data → Set
DataOk C D = DataModeOk C (Data.mode D)

------------------------------------------------------------------------
-- 3.4.7 Start Function

StartOk : Context → Start → Set
StartOk C x = Context.getFunc C x ≡ just (([] , z≤n) ⟶ ([] , z≤n))

------------------------------------------------------------------------
-- 3.4.8 Exports

data ExportDescOk : Context → ExportDesc → ExternType → Set where
  func   : ∀ {C x t} → Context.getFunc C x ≡ just t → ExportDescOk C (func x) (func t)
  table  : ∀ {C x t} → Context.getTable C x ≡ just t → ExportDescOk C (table x) (table t)
  mem    : ∀ {C x t} → Context.getMem C x ≡ just t → ExportDescOk C (mem x) (mem t)
  global : ∀ {C x t} → Context.getGlobal C x ≡ just t → ExportDescOk C (global x) (global t)

ExportOk : Context → Export → ExternType → Set
ExportOk C exp t = ExportDescOk C (Export.desc exp) t

------------------------------------------------------------------------
-- 3.4.9 Imports

data ImportDescOk : Context → ImportDesc → ExternType → Set where
  func   : ∀ {C x t} → Context.getType C x ≡ just t → ImportDescOk C (func x) (func t)
  table  : ∀ {C t} → TableTypeOk t → ImportDescOk C (table t) (table t)
  mem    : ∀ {C t} → MemTypeOk t → ImportDescOk C (mem t) (mem t)
  global : ∀ {C t} → GlobalTypeOk t → ImportDescOk C (global t) (global t)

ImportOk : Context → Import → ExternType → Set
ImportOk C imp t = ImportDescOk C (Import.desc imp) t

------------------------------------------------------------------------
-- 3.4.10 Modules

record _⊢ᴹ_∶_⟶_ (M : Mod) (it : List ExternType) (et : List ExternType) : Set where
  field
    {ft} : List FuncType
    {tt} : List TableType
    {mt} : List MemType
    {gt} : List GlobalType
    {rt} : List RefType

  private
    module M = Mod M
    ift = mapMaybe func? it
    itt = mapMaybe table? it
    imt = mapMaybe mem? it
    igt = mapMaybe global? it
    -- FIXME: find real references
    x = []
    C = record
      { types = toList M.types
      ; funcs = ft ++ ift
      ; tables = tt ++ itt
      ; mems = mt ++ imt
      ; globals = gt ++ igt
      ; elems = rt
      ; datas = replicate (Vec≤.length M.datas) _
      ; locals = []
      ; labels = []
      ; return = nothing
      ; refs = x
      }
    C′ = record
       { types = []
       ; funcs = Context.funcs C
       ; tables = []
       ; mems = []
       ; globals = igt
       ; elems = []
       ; datas = []
       ; locals = []
       ; labels = []
       ; return = nothing
       ; refs = Context.refs C
       }

  field
    typesOk        : All FuncTypeOk (toList M.types)
    funcsOk        : Pointwise (FuncOk C) (toList M.funcs) ft
    tablesOk       : Pointwise (TableOk C) (toList M.tables) tt
    memsOk         : Pointwise (MemOk C) (toList M.mems) mt
    globalsOk      : Pointwise (GlobalOk C′) (toList M.globals) gt
    elemsOk        : Pointwise (ElemOk C) (toList M.elems) rt
    datasOk        : All (DataOk C) (toList M.datas)
    startOk        : maybe (StartOk C) ⊤ M.start
    importsOk      : Pointwise (ImportOk C) (toList M.imports) it
    exportsOk      : Pointwise (ExportOk C) (toList M.exports) et
    memsCount      : Vec≤.length M.mems ≤ 1
    exportDisjoint : AllPairs _≢_ (map (λ x → toString (Export.name x)) (toList M.exports))