diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-08-12 16:58:32 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-08-12 16:58:32 +0100 |
| commit | f1d1cb690e7e0487e18d235a919af1c147f39884 (patch) | |
| tree | 4e7a7b85f5f045f3781760a05d86e550f0621fa6 | |
| parent | 904924c33720c3481f738966f32e9c34736f92cf (diff) | |
Fill in definition of `Constant`.
| -rw-r--r-- | src/Wasm/Data/Instruction.agda | 41 |
1 files changed, 29 insertions, 12 deletions
diff --git a/src/Wasm/Data/Instruction.agda b/src/Wasm/Data/Instruction.agda index 69853f0..2e56368 100644 --- a/src/Wasm/Data/Instruction.agda +++ b/src/Wasm/Data/Instruction.agda @@ -304,18 +304,35 @@ data Instruction : Context → FuncType → Set where Expression : Context → List ValType → Set Expression C τ = Instruction C ([] ⟶ τ) -data InstructionRef : ∀ {C τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set where +data InstructionRef {C} : ∀ {τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set where ---- Direct - ref-func : ∀ {C x} x∈refs → InstructionRef (ref-func {C} {x} x∈refs) x - call : ∀ {C} x → InstructionRef (call {C} x) x + ref-func : ∀ {x} x∈refs → InstructionRef (ref-func {C} {x} x∈refs) x + call : ∀ x → InstructionRef (call {C} x) x ---- Structural - block : ∀ {C x} bt {i} → InstructionRef i x → InstructionRef (block {C} bt i) x - loop : ∀ {C x} bt {i} → InstructionRef i x → InstructionRef (loop {C} bt i) x - if₁ : ∀ {C x} bt {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x - if₂ : ∀ {C x} bt i₁ {i₂} → InstructionRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x - frame : ∀ {C x τ τ₁ τ₂} {i} → InstructionRef i x → InstructionRef (frame {C} {τ} {τ₁} {τ₂} i) x - seq₁ : ∀ {C x τ₁ τ₂ τ₃} {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x - seq₂ : ∀ {C x τ₁ τ₂ τ₃} i₁ {i₂} → InstructionRef i₂ x → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x - -data Constant : ∀ {C τ} → Instruction C τ → Set where + block : ∀ {x} bt {i} → InstructionRef i x → InstructionRef (block {C} bt i) x + loop : ∀ {x} bt {i} → InstructionRef i x → InstructionRef (loop {C} bt i) x + if₁ : ∀ {x} bt {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x + if₂ : ∀ {x} bt i₁ {i₂} → InstructionRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x + frame : ∀ {x τ τ₁ τ₂} {i} → InstructionRef i x → InstructionRef (frame {C} {τ} {τ₁} {τ₂} i) x + seq₁ : ∀ {x τ₁ τ₂ τ₃} {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x + seq₂ : ∀ {x τ₁ τ₂ τ₃} i₁ {i₂} → InstructionRef i₂ x → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x + +data Constant {C} : ∀ {τ} → Instruction C τ → Set where + ---- Direct + -- const + i32-const : ∀ c → Constant (i32-const c) + i64-const : ∀ c → Constant (i64-const c) + f32-const : ∀ c → Constant (f32-const c) + f64-const : ∀ c → Constant (f64-const c) + + -- refs + ref-null : ∀ τ → Constant (ref-null τ) + ref-func : ∀ {x} x∈refs → Constant (ref-func {x = x} x∈refs) + + -- global + global-get : ∀ {x} → GlobalType.mut (lookup (Context.globals C) x) ≡ const → Constant (global-get x) + + ---- Structural + frame : ∀ {τ τ₁ τ₂ i} → Constant i → Constant (frame {C} {τ} {τ₁} {τ₂} i) + seq : ∀ {τ₁ τ₂ τ₃ i₁ i₂} → Constant i₁ → Constant i₂ → Constant (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) |