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

module Wasm.Semantics
  {a} (ExternAddr : Set a)
  where

open import Data.Fin using (Fin; zero; toℕ; inject≤)
open import Data.List using (List; []; _∷_; _++_; length; lookup; allFin)
open import Data.List.Relation.Unary.Linked using (Linked)
open import Data.Maybe using (Maybe; maybe; map)
open import Data.Nat using (ℕ; _≤_; _≥?_; _≤?_)
open import Data.Product using (_×_; ∃; ∃₂; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_)
open import Data.Unit using (⊤)
open import Data.Vec as Vec using (Vec)
open import Level using () renaming (suc to ℓsuc)
open import Relation.Binary using (REL)
open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst; module ≡-Reasoning)
open import Relation.Nary using (substₙ)
open import Relation.Nullary.Decidable using (True)
open import Wasm.Data
open import Wasm.Type hiding (_,_)
open import Wasm.Util.List.Map as Map using (Map)
open import Wasm.Util.List.Prefix as Prefix using (Prefix; length≤) renaming (Map to PrefixMap)
open import Wasm.Value

open import Wasm.Data.Instruction as Inst using ()

record StoreTypes : Set₁ where
  field
    hostFuncs : List FuncType
    funcs     : List FuncType
    tables    : List TableType
    mems      : List MemType
    globals   : List GlobalType
    elems     : List RefType
    datas     : ℕ

data Num : NumType → Set where
  i32 : I32 → Num i32
  i64 : I64 → Num i64
  f32 : F32 → Num f32
  f64 : F64 → Num f64

data Ref (S : StoreTypes) : RefType → Set a where
  null   : ∀ τ → Ref S τ
  func   : Fin (length (StoreTypes.funcs S)) → Ref S funcref
  extern : ExternAddr → Ref S externref

data Value (S : StoreTypes) : ValType → Set a where
  num : ∀ {τ} → Num τ → Value S (num τ)
  ref : ∀ {τ} → Ref S τ → Value S (ref τ)

default : ∀ {S} τ → Value S τ
default (num i32) = num (i32 zero)
default (num i64) = num (i64 zero)
default (num f32) = num (f32 0f32)
default (num f64) = num (f64 0f64)
default (ref τ)   = ref (null τ)

data Result (S : StoreTypes) : List ValType → Set a where
  [_]  : ∀ {τs} → Map (Value S) τs → Result S τs
  trap : ∀ {τs} → Result S τs

record ExportsInst (S : StoreTypes) (Cₑ : ExternTypes) : Set where
  private
    module S = StoreTypes S
    module Cₑ = ExternTypes Cₑ
  field
    funcs   : Map (λ τ → ∃ λ i → lookup S.funcs i ≡ τ) Cₑ.funcs
    tables  : Map (λ τ → ∃ λ i → lookup S.tables i ≡ τ) Cₑ.tables
    mems    : Map (λ τ → ∃ λ i → lookup S.mems i ≡ τ) Cₑ.mems
    globals : Map (λ τ → ∃ λ i → lookup S.globals i ≡ τ) Cₑ.globals

record ModuleInst (S : StoreTypes) (C : Inst.Context) : Set₁ where
  private
    module S = StoreTypes S
    module C = Inst.Context C
  field
    {et}    : ExternTypes
    funcs   : Map (λ τ → ∃ λ i → lookup S.funcs i ≡ τ) C.funcs
    tables  : Map (λ τ → ∃ λ i → lookup S.tables i ≡ τ) C.tables
    mems    : Map (λ τ → ∃ λ i → lookup S.mems i ≡ τ) C.mems
    globals : Map (λ τ → ∃ λ i → lookup S.globals i ≡ τ) C.globals
    elems   : Map (λ τ → ∃ λ i → lookup S.elems i ≡ τ) C.elems
    datas   : Vec (Fin S.datas) C.datas
    exports : ExportsInst S et

record TableInst (S : StoreTypes) (τ : TableType) : Set a where
  private
    module τ = TableType τ
  field
    elems      : List (Ref S τ.type)
    {minBound} : True (length elems ≥? toℕ (Limits.min′ τ.limits))
    {maxBound} : maybe (λ max → True (length elems ≤? toℕ max)) ⊤ (Limits.max τ.limits)

record MemInst (τ : MemType) : Set where
  private
    module τ = MemType τ
  field
    pages      : List (Vec Byte 65536)
    {minBound} : True (length pages ≥? toℕ (Limits.min′ τ.limits))
    {maxBound} : maybe (λ max → True (length pages ≤? toℕ max)) ⊤ (Limits.max τ.limits)

record WasmFuncInst (S : StoreTypes) (τ : FuncType) : Set₁ where
  field
    {context} : Inst.Context
    modinst   : ModuleInst S context
    code      : Function context τ

data FunctionInst (S : StoreTypes) (τ : FuncType) : Set₁ where
  host : ∀ {i} → lookup (StoreTypes.hostFuncs S) i ≡ τ → FunctionInst S τ
  wasm : WasmFuncInst S τ → FunctionInst S τ

record Store (types : StoreTypes) : Set (ℓsuc a) where
  inductive
  private
    module types = StoreTypes types
  field
    funcs   : Map (FunctionInst types) types.funcs
    tables  : Map (TableInst types) types.tables
    mems    : Map MemInst types.mems
    globals : Map (λ g → Value types (GlobalType.type g)) types.globals
    elems   : Map (λ τ → List (Ref types τ)) types.elems
    datas   : Vec (List Byte) types.datas

data FrameInstruction (C : Inst.Context) : (stackTy labelTy : List (List ValType)) (τ : FuncType) → Set where
  [_] : ∀ {τ₁ τ₂ τ₃} → Inst.Sequence (record C {labels = []}) (τ₂ ++ τ₁ ⟶ τ₃) → FrameInstruction C (τ₁ ∷ []) [] (τ₂ ⟶ τ₃)
  _∷_ : ∀ {τs₁ τs₂ τ₁′ τ₂′ τ′ τ} → let C′ = record C { labels = τ₂′ ∷ (Inst.Context.labels C) } in Inst.Sequence C′ (τ′ ++ τ₁′ ⟶ τ₂′) → FrameInstruction C τs₁ τs₂ (τ₁′ ⟶ τ) → FrameInstruction C (τ₁′ ∷ τs₁) (τ₂′ ∷ τs₂) (τ′ ⟶ τ)

record Frame (S : StoreTypes) (τ : FuncType) : Set (ℓsuc a) where
  field
    context   : Inst.Context
  private
    module context = Inst.Context context
  field
    modinst   : ModuleInst S context
    {stackTy} : List (List ValType)
    {labelTy} : List (List ValType)
    locals    : Map (Value S) (context.locals)
    stack     : Map (Map (Value S)) stackTy
    insts     : FrameInstruction context stackTy labelTy τ

record Thread (S : StoreTypes) (τ : List ValType) : Set (ℓsuc a) where
  field
    {frameTy} : List (List ValType)
    frames    : Linked (λ τ₁ τ₂ → Frame S (τ₁ ⟶ τ₂)) ([] ∷ frameTy ++ τ ∷ [])