summaryrefslogtreecommitdiff
path: root/src/Wasm/Data.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Wasm/Data.agda')
-rw-r--r--src/Wasm/Data.agda138
1 files changed, 57 insertions, 81 deletions
diff --git a/src/Wasm/Data.agda b/src/Wasm/Data.agda
index f7ed8da..d849cc6 100644
--- a/src/Wasm/Data.agda
+++ b/src/Wasm/Data.agda
@@ -14,9 +14,12 @@ 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; Constant)
+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
@@ -71,89 +74,69 @@ private
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
+record Function (C : Inst.Context) (τ : FuncType) : Set where
private
- module Cₘ = Context Cₘ
-
- type = lookup Cₘ.funcs idx
-
- private
- module type = FuncType type
+ module τ = FuncType τ
field
locals : List ValType
private
- C = Inst.Context ∋ record (makeContext Cᵢ Cₘ refs)
- { locals = type.from ++ locals
- ; labels = type.to ∷ []
- ; return = just type.to
+ C′ = Inst.Context ∋ record C
+ { locals = τ.from ++ locals
+ ; labels = τ.to ∷ []
+ ; return = just τ.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
+ body : Expression C′ τ.to
+record Global (C : Inst.Context) (τ : GlobalType) : Set where
private
- module type = GlobalType type
+ module τ = GlobalType τ
field
- {body} : Expression C (type.type ∷ [])
- constant : Constant body
+ {body} : Expression C (τ.type ∷ [])
+ constant : SequenceConstant 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
+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 ∷ [])} → Constant offset → ElemMode C (TableType.type (lookup (Inst.Context.tables C) table))
+ 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.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
+ 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 type ∷ []))
- constant : All Constant inits
- mode : ElemMode C type
+ {inits} : List (Expression C (ref τ ∷ []))
+ constant : All SequenceConstant inits
+ mode : ElemMode C τ
-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
+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 ∷ [])} → Constant offset → 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.InstructionRef offset x → DataModeRef (active memory {offset} constant) x
+ activeRef : ∀ {x} memory {offset} constant → Inst.SequenceRef 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
+record Data (C : Inst.Context) : Set where
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 : ∀ {C} → Data C → Fin (length (Inst.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
+record Exports (C : Inst.Context) (Cₑ : ExternTypes) : Set where
private
- C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
module Cₑ = ExternTypes Cₑ
module C = Inst.Context C
field
@@ -169,7 +152,7 @@ record Exports (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (
field
namesDisjoint : AllPairs _≢_ names
-ExportsRef : ∀ {Cᵢ Cₘ refs Cₑ} → Exports Cᵢ Cₘ refs Cₑ → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
+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
@@ -181,47 +164,42 @@ record Imports (Cᵢ : ExternTypes) : Set where
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)))
+ {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 = it.globals
+ ; globals = gt
; elems = rt
- ; datas = n
+ ; datas = #datas
}
+ C′ = makeGlobalContext it Cₘ refs
+
+ C = makeContext it Cₘ refs
+
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)
+ 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 it Cₘ refs et
+ exports : Exports C 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
+ 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
@@ -230,7 +208,9 @@ private
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
@@ -241,16 +221,12 @@ private
addTwoModule : Module addTwoImports addTwoExports
addTwoModule = record
- { ft = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ []
- ; tables = []
+ { 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))
+ ; body = local-get zero ∙ local-get (suc zero) ∙ i32-binop i32.add ∙ nop
} ∷ []
; globals = []
; elems = []
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 02:58:07 +0000