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

module Wasm.Data where

open import Data.Fin using (Fin; zero; suc)
open import Data.List using (List; []; _∷_; _++_; length; lookup; map)
open import Data.List.Relation.Binary.Pointwise using (Pointwise)
open import Data.List.Relation.Unary.All using (All)
open import Data.List.Relation.Unary.Any using (Any)
open import Data.List.Relation.Unary.AllPairs using (AllPairs)
open import Data.Maybe using (Maybe; just; nothing; maybe)
open import Data.Nat using (ℕ; suc; _+_; _≤_; z≤n)
open import Data.Product using (_×_; _,_; proj₁)
open import Data.Sum using (_⊎_)
open import Data.Unit using (⊤)
open import Data.Vec using (Vec)
open import Data.Vec.Relation.Unary.Any using () renaming (Any to VecAny)
open import Function as _ using (_∋_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Wasm.Data.Instruction as Inst using (Expression; SequenceConstant)
open import Wasm.Util.List.Map using (Map)
open import Wasm.Util.List.Map.Any using () renaming (Any to MapAny)
open import Wasm.Value using (Byte; Name)
open import Wasm.Type

record ExternTypes : Set where
  field
    funcs   : List FuncType
    tables  : List TableType
    mems    : List MemType
    globals : List GlobalType

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

private
  makeContext : (Cᵢ : ExternTypes) → (Cₘ : Context) → (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) → Inst.Context
  makeContext Cᵢ Cₘ refs = record
    { funcs   = Cᵢ.funcs ++ Cₘ.funcs
    ; tables  = Cᵢ.tables ++ Cₘ.tables
    ; mems    = Cᵢ.mems ++ Cₘ.mems
    ; globals = Cᵢ.globals ++ Cₘ.globals
    ; elems   = Cₘ.elems
    ; datas   = Cₘ.datas
    ; locals  = []
    ; labels  = []
    ; return  = nothing
    ; refs    = refs
    }
    where
    module Cᵢ = ExternTypes Cᵢ
    module Cₘ = Context Cₘ

  makeGlobalContext : (Cᵢ : ExternTypes) → (Cₘ : Context) → (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) → Inst.Context
  makeGlobalContext Cᵢ Cₘ refs = record
    { funcs   = Cᵢ.funcs ++ Cₘ.funcs
    ; tables  = []
    ; mems    = []
    ; globals = Cᵢ.globals
    ; elems   = []
    ; datas   = 0
    ; locals  = []
    ; labels  = []
    ; return  = nothing
    ; refs    = refs
    }
    where
    module Cᵢ = ExternTypes Cᵢ
    module Cₘ = Context Cₘ

record Function (C : Inst.Context) (τ : FuncType) : Set where
  private
    module τ = FuncType τ

  field
    locals : List ValType

  private
    C′ = Inst.Context ∋ record C
      { locals  = τ.from ++ locals
      ; labels  = τ.to ∷ []
      ; return  = just τ.to
      }
  field
    body : Expression C′ τ.to

record Global (C : Inst.Context) (τ : GlobalType) : Set where
  private
    module τ = GlobalType τ

  field
    {body}   : Expression C (τ.type ∷ [])
    constant : SequenceConstant body

GlobalRef : ∀ {C τ} → Global C τ → Fin (length (Inst.Context.funcs C)) → Set
GlobalRef global x = Inst.SequenceRef (Global.body global) x

data ElemMode (C : Inst.Context) : RefType → Set where
  passive : ∀ {τ} → ElemMode C τ
  active : ∀ table {offset : Expression C (num i32 ∷ [])} → SequenceConstant offset → ElemMode C (TableType.type (lookup (Inst.Context.tables C) table))
  declarative : ∀ {τ} → ElemMode C τ

data ElemModeRef {C : Inst.Context} : ∀ {τ} → ElemMode C τ → Fin (length (Inst.Context.funcs C)) → Set where
  activeRef : ∀ {x} table {offset} constant → Inst.SequenceRef offset x → ElemModeRef (active table {offset} constant) x

record Elem (C : Inst.Context) (τ : RefType) : Set where
  field
    {inits}  : List (Expression C (ref τ ∷ []))
    constant : All SequenceConstant inits
    mode     : ElemMode C τ

data ElemRef {C τ} (elem : Elem C τ) (x : Fin (length (Inst.Context.funcs C))) : Set where
  initsRef : Any (λ init → Inst.SequenceRef init x) (Elem.inits elem) → ElemRef elem x
  modeRef  : ElemModeRef (Elem.mode elem) x → ElemRef elem x

data DataMode (C : Inst.Context) : Set where
  passive : DataMode C
  active  : ∀ (memory : Fin (length (Inst.Context.mems C))) {offset : Expression C (num i32 ∷ [])} → SequenceConstant offset → DataMode C


data DataModeRef {C : Inst.Context} : DataMode C → Fin (length (Inst.Context.funcs C)) → Set where
  activeRef : ∀ {x} memory {offset} constant → Inst.SequenceRef offset x → DataModeRef (active memory {offset} constant) x

record Data (C : Inst.Context) : Set where
  field
    init : List Byte
    mode : DataMode C

DataRef : ∀ {C} → Data C → Fin (length (Inst.Context.funcs C)) → Set
DataRef dta x = DataModeRef (Data.mode dta) x

record Exports (C : Inst.Context) (Cₑ : ExternTypes) : Set where
  private
    module Cₑ = ExternTypes Cₑ
    module C = Inst.Context C
  field
    funcs     : List (Name × Fin (length (C.funcs)))
    tables    : List (Name × Fin (length (C.tables)))
    mems      : List (Name × Fin (length (C.mems)))
    globals   : List (Name × Fin (length (C.globals)))
    funcsOk   : Pointwise (λ (_ , x) τ → lookup C.funcs x ≡ τ) funcs Cₑ.funcs
    tablesOk  : Pointwise (λ (_ , x) τ → lookup C.tables x ≡ τ) tables Cₑ.tables
    memsOk    : Pointwise (λ (_ , x) τ → lookup C.mems x ≡ τ) mems Cₑ.mems
    globalsOk : Pointwise (λ (_ , x) τ → lookup C.globals x ≡ τ) globals Cₑ.globals
  names = map proj₁ funcs ++ map proj₁ tables ++ map proj₁ mems ++ map proj₁ globals
  field
    namesDisjoint : AllPairs _≢_ names

ExportsRef : ∀ {C Cₑ} → Exports C Cₑ → Fin (length (Inst.Context.funcs C)) → Set
ExportsRef exports x = Any (λ (_ , y) → y ≡ x) (Exports.funcs exports)

record Imports (Cᵢ : ExternTypes) : Set where
  private
    module Cᵢ = ExternTypes Cᵢ
  field
    funcs   : Vec (Name × Name) (length Cᵢ.funcs)
    tables  : Vec (Name × Name) (length Cᵢ.tables)
    mems    : Vec (Name × Name) (length Cᵢ.mems)
    globals : Vec (Name × Name) (length Cᵢ.globals)

record Module (it et : ExternTypes) : Set₁ where
  private
    module it = ExternTypes it
  field
    {ft}     : List FuncType
    tables   : List TableType
    mems     : List MemType
    {gt}     : List GlobalType
    {rt}     : List RefType
    {#datas} : ℕ
    start    : Maybe (Fin (length (it.funcs ++ ft)))
    refs     : List (Fin (length (it.funcs ++ ft)))
  private
    Cₘ = Context ∋ record
      { funcs   = ft
      ; tables  = tables
      ; mems    = mems
      ; globals = gt
      ; elems   = rt
      ; datas   = #datas
      }
    C′ = makeGlobalContext it Cₘ refs

  C = makeContext it Cₘ refs

  field
    funcs    : Map (Function C) ft
    globals  : Map (Global C′) gt
    elems    : Map (Elem C) rt
    datas    : Vec (Data C) #datas
    startOk  : maybe (λ x → lookup (it.funcs ++ ft) x ≡ ([] ⟶ [])) ⊤ start
    exports  : Exports C et
    memCount : length it.mems + length mems ≤ 1
    refsUsed : All (λ i → MapAny (λ g → GlobalRef g i) globals
                        ⊎ MapAny (λ e → ElemRef e i) elems
                        ⊎ VecAny (λ d → DataRef d i) datas
                        ⊎ ExportsRef exports i)
                   refs

private
  module Test where
    open import Data.List.Relation.Binary.Pointwise using ([]; _∷_)
    open import Data.List.Relation.Unary.All using ([])
    open import Data.List.Relation.Unary.AllPairs using ([]; _∷_)
    open import Data.Vec using ([])
    open import Relation.Binary.PropositionalEquality using (refl)
    open import Wasm.Util.List.Map using (Map; []; _∷_)
    open Inst

    addTwoImports : ExternTypes
    addTwoImports = record { funcs = [] ; tables = [] ; mems = [] ; globals = [] }

    addTwoExports : ExternTypes
    addTwoExports = record { funcs = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ [] ; tables = [] ; mems = [] ; globals = [] }

    addTwoModule : Module addTwoImports addTwoExports
    addTwoModule = record
      { tables = []
      ; mems = []
      ; start = nothing
      ; funcs = record
        { locals = []
        ; body = local-get zero ∙ local-get (suc zero) ∙ i32-binop i32.add ∙ nop
        } ∷ []
      ; globals = []
      ; elems = []
      ; datas = []
      ; startOk = _
      ; exports = record
        { funcs = ("addTwo" , zero) ∷ []
        ; tables = []
        ; mems = []
        ; globals = []
        ; funcsOk = refl ∷ []
        ; tablesOk = []
        ; memsOk = []
        ; globalsOk = []
        ; namesDisjoint = [] ∷ []
        }
      ; memCount = z≤n
      ; refsUsed = []
      }