{-# 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 Function as _ using (_∋_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Wasm.Data.Instruction as Inst using (Expression; Constant)
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ᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.funcs Cₘ))) : Set where
  private
    module Cₘ = Context Cₘ

  type = lookup Cₘ.funcs idx

  private
    module type = FuncType type

  field
    locals : List ValType

  private
    C = Inst.Context ∋ record (makeContext Cᵢ Cₘ refs)
      { locals  = type.from ++ locals
      ; labels  = type.to ∷ []
      ; return  = just type.to
      }
  field
    body : Expression C type.to

record Global (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.globals Cₘ))) : Set where
  private
    module Cₘ = Context Cₘ
    C = Inst.Context ∋ makeGlobalContext Cᵢ Cₘ refs

  type = lookup Cₘ.globals idx

  private
    module type = GlobalType type

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

GlobalRef : ∀ {Cᵢ Cₘ refs idx} → Global Cᵢ Cₘ refs idx → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
GlobalRef global x = Inst.InstructionRef (Global.body global) x

data ElemMode (C : Inst.Context) : RefType → Set where
  passive : ∀ {τ} → ElemMode C τ
  active : ∀ table {offset : Expression C (num i32 ∷ [])} → Constant 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.InstructionRef offset x → ElemModeRef (active table {offset} constant) x

record Elem (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.elems Cₘ))) : Set where
  private
    module Cₘ = Context Cₘ
    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs

  type = lookup Cₘ.elems idx

  field
    {inits}  : List (Expression C (ref type ∷ []))
    constant : All Constant inits
    mode     : ElemMode C type

data ElemRef {Cᵢ} {Cₘ} {refs} {idx} (elem : Elem Cᵢ Cₘ refs idx) (x : Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ))) : Set where
  initsRef : Any (λ init → Inst.InstructionRef 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 ∷ [])} → Constant offset → DataMode C


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

record Data (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (Context.datas Cₘ)) : Set where
  private
    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
  field
    init : List Byte
    mode : DataMode C

DataRef : ∀ {Cᵢ Cₘ refs idx} → Data Cᵢ Cₘ refs idx → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
DataRef dta x = DataModeRef (Data.mode dta) x

record Exports (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (Cₑ : ExternTypes) : Set where
  private
    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
    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ₘ refs Cₑ} → Exports Cᵢ Cₘ refs Cₑ → Fin (length (ExternTypes.funcs Cᵢ ++ 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)

infixr 5 _∷_

data DList : ∀ {n} → (A : Fin n → Set) → Set₁ where
  [] : ∀ {A} → DList {0} A
  _∷_ : ∀ {n A} → A zero → DList {n} (λ i → A (suc i)) → DList A

data DAny : ∀ {n A} → (∀ {i} → A i → Set) → DList {n} A → Set₁ where
  here  : ∀ {n A} {P : ∀ {i} → A i → Set} {x xs} → P x → DAny {suc n} {A} P (x ∷ xs)
  there : ∀ {n A} {P : ∀ {i} → A i → Set} {x xs} → DAny (λ {i} → P {suc i}) xs → DAny {suc n} {A} P (x ∷ xs)

record Module (it et : ExternTypes) : Set₁ where
  private
    module it = ExternTypes it
  field
    ft     : List FuncType
    tables : List TableType
    mems   : List MemType
    rt     : List RefType
    n      : ℕ
    start  : Maybe (Fin (length (it.funcs ++ ft)))
  private
    Cₘ = Context ∋ record
      { funcs   = ft
      ; tables  = tables
      ; mems    = mems
      ; globals = it.globals
      ; elems   = rt
      ; datas   = n
      }
  field
    refs     : List (Fin (length (it.funcs ++ ft)))
    funcs    : DList (Function it Cₘ refs)
    globals  : DList (Global it Cₘ refs)
    elems    : DList (Elem it Cₘ refs)
    datas    : DList (Data it Cₘ refs)
    startOk  : maybe (λ x → lookup (it.funcs ++ ft) x ≡ ([] ⟶ [])) ⊤ start
    exports  : Exports it Cₘ refs et
    memCount : length it.mems + length mems ≤ 1
    refsUsed : All (λ i → DAny (λ g → GlobalRef g i) globals
                        ⊎ DAny (λ e → ElemRef e i) elems
                        ⊎ DAny (λ 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 Relation.Binary.PropositionalEquality using (refl)
    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
      { ft = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ []
      ; tables = []
      ; mems = []
      ; rt = []
      ; n = 0
      ; start = nothing
      ; refs = []
      ; funcs = record
        { locals = []
        ; body = seq (local-get zero) (seq (frame (local-get (suc zero))) (i32-binop i32.add))
        } ∷ []
      ; globals = []
      ; elems = []
      ; datas = []
      ; startOk = _
      ; exports = record
        { funcs = ("addTwo" , zero) ∷ []
        ; tables = []
        ; mems = []
        ; globals = []
        ; funcsOk = refl ∷ []
        ; tablesOk = []
        ; memsOk = []
        ; globalsOk = []
        ; namesDisjoint = [] ∷ []
        }
      ; memCount = z≤n
      ; refsUsed = []
      }