diff options
Diffstat (limited to 'src/Wasm/Data/Instruction.agda')
| -rw-r--r-- | src/Wasm/Data/Instruction.agda | 219 |
1 files changed, 115 insertions, 104 deletions
diff --git a/src/Wasm/Data/Instruction.agda b/src/Wasm/Data/Instruction.agda index 2e56368..8be89c6 100644 --- a/src/Wasm/Data/Instruction.agda +++ b/src/Wasm/Data/Instruction.agda @@ -12,6 +12,8 @@ open import Relation.Binary.PropositionalEquality using (_≡_) open import Wasm.Type open import Wasm.Value +infixr 4 _∙_ _∙₁_ _∙₂_ + record Context : Set where field funcs : List FuncType @@ -193,146 +195,155 @@ blockTypeAsFunc {C} (idx τ) = τ blockTypeAsFunc (val x) = [] ⟶ x ∷ [] blockTypeAsFunc nothing = [] ⟶ [] -data Instruction : Context → FuncType → Set where +data Instruction (C : Context) : FuncType → Set +data Sequence (C : Context) : FuncType → Set + +data Instruction C where ---- Numeric instructions -- const - i32-const : ∀ {C} → (c : I32) → Instruction C ([] ⟶ num i32 ∷ []) - i64-const : ∀ {C} → (c : I64) → Instruction C ([] ⟶ num i64 ∷ []) - f32-const : ∀ {C} → (c : F32) → Instruction C ([] ⟶ num f32 ∷ []) - f64-const : ∀ {C} → (c : F64) → Instruction C ([] ⟶ num f64 ∷ []) + i32-const : (c : I32) → Instruction C ([] ⟶ num i32 ∷ []) + i64-const : (c : I64) → Instruction C ([] ⟶ num i64 ∷ []) + f32-const : (c : F32) → Instruction C ([] ⟶ num f32 ∷ []) + f64-const : (c : F64) → Instruction C ([] ⟶ num f64 ∷ []) -- unop - i32-unop : ∀ {C} → (op : i32.Unary) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i64-unop : ∀ {C} → (op : i64.Unary) → Instruction C (num i64 ∷ [] ⟶ num i64 ∷ []) - f32-unop : ∀ {C} → (op : f32.Unary) → Instruction C (num f32 ∷ [] ⟶ num f32 ∷ []) - f64-unop : ∀ {C} → (op : f64.Unary) → Instruction C (num f64 ∷ [] ⟶ num f64 ∷ []) + i32-unop : (op : i32.Unary) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i64-unop : (op : i64.Unary) → Instruction C (num i64 ∷ [] ⟶ num i64 ∷ []) + f32-unop : (op : f32.Unary) → Instruction C (num f32 ∷ [] ⟶ num f32 ∷ []) + f64-unop : (op : f64.Unary) → Instruction C (num f64 ∷ [] ⟶ num f64 ∷ []) -- binop - i32-binop : ∀ {C} → (op : i32.Binary) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) - i64-binop : ∀ {C} → (op : i64.Binary) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i64 ∷ []) - f32-binop : ∀ {C} → (op : f32.Binary) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num f32 ∷ []) - f64-binop : ∀ {C} → (op : f64.Binary) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num f64 ∷ []) + i32-binop : (op : i32.Binary) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) + i64-binop : (op : i64.Binary) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i64 ∷ []) + f32-binop : (op : f32.Binary) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num f32 ∷ []) + f64-binop : (op : f64.Binary) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num f64 ∷ []) -- testop - i32-testop : ∀ {C} → (op : i32.Test) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i64-testop : ∀ {C} → (op : i64.Test) → Instruction C (num i64 ∷ [] ⟶ num i32 ∷ []) + i32-testop : (op : i32.Test) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i64-testop : (op : i64.Test) → Instruction C (num i64 ∷ [] ⟶ num i32 ∷ []) -- relop - i32-relop : ∀ {C} → (op : i32.Rel) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) - i64-relop : ∀ {C} → (op : i64.Rel) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i32 ∷ []) - f32-relop : ∀ {C} → (op : f32.Rel) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num i32 ∷ []) - f64-relop : ∀ {C} → (op : f64.Rel) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num i32 ∷ []) + i32-relop : (op : i32.Rel) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) + i64-relop : (op : i64.Rel) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i32 ∷ []) + f32-relop : (op : f32.Rel) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num i32 ∷ []) + f64-relop : (op : f64.Rel) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num i32 ∷ []) -- cvtop - i32-cvtop : ∀ {C τ} → (op : i32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i32 ∷ []) - i64-cvtop : ∀ {C τ} → (op : i64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i64 ∷ []) - f32-cvtop : ∀ {C τ} → (op : f32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f32 ∷ []) - f64-cvtop : ∀ {C τ} → (op : f64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f64 ∷ []) + i32-cvtop : ∀ {τ} → (op : i32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i32 ∷ []) + i64-cvtop : ∀ {τ} → (op : i64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i64 ∷ []) + f32-cvtop : ∀ {τ} → (op : f32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f32 ∷ []) + f64-cvtop : ∀ {τ} → (op : f64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f64 ∷ []) ---- Reference instructions - ref-null : ∀ {C} τ → Instruction C ([] ⟶ ref τ ∷ []) - ref-is-null : ∀ {C τ} → Instruction C (ref τ ∷ [] ⟶ num i32 ∷ []) - ref-func : ∀ {C x} → (x∈refs : x ∈ Context.refs C) → Instruction C ([] ⟶ ref funcref ∷ []) + ref-null : ∀ τ → Instruction C ([] ⟶ ref τ ∷ []) + ref-is-null : ∀ {τ} → Instruction C (ref τ ∷ [] ⟶ num i32 ∷ []) + ref-func : ∀ {x} → (x∈refs : x ∈ Context.refs C) → Instruction C ([] ⟶ ref funcref ∷ []) ---- Parametric instructions - drop : ∀ {C τ} → Instruction C (τ ∷ [] ⟶ []) - select : ∀ {C τ} → Instruction C (num i32 ∷ τ ∷ τ ∷ [] ⟶ τ ∷ []) + drop : ∀ {τ} → Instruction C (τ ∷ [] ⟶ []) + select : ∀ {τ} → Instruction C (num i32 ∷ τ ∷ τ ∷ [] ⟶ τ ∷ []) ---- Variable instructions - local-get : ∀ {C} x → Instruction C ([] ⟶ lookup (Context.locals C) x ∷ []) - local-set : ∀ {C} x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ []) - local-tee : ∀ {C} x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ lookup (Context.locals C) x ∷ []) - global-get : ∀ {C} x → Instruction C ([] ⟶ GlobalType.type (lookup (Context.globals C) x) ∷ []) - global-set : ∀ {C} x → let g = lookup (Context.globals C) x in GlobalType.mut g ≡ var → Instruction C (GlobalType.type g ∷ [] ⟶ []) + local-get : ∀ x → Instruction C ([] ⟶ lookup (Context.locals C) x ∷ []) + local-set : ∀ x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ []) + local-tee : ∀ x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ lookup (Context.locals C) x ∷ []) + global-get : ∀ x → Instruction C ([] ⟶ GlobalType.type (lookup (Context.globals C) x) ∷ []) + global-set : ∀ x → let g = lookup (Context.globals C) x in GlobalType.mut g ≡ var → Instruction C (GlobalType.type g ∷ [] ⟶ []) ---- Table instructions - table-get : ∀ {C} x → Instruction C (num i32 ∷ [] ⟶ ref (TableType.type (lookup (Context.tables C) x)) ∷ []) - table-set : ∀ {C} x → Instruction C (ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ []) - table-size : ∀ {C} (x : Fin (length (Context.tables C))) → Instruction C ([] ⟶ num i32 ∷ []) - table-grow : ∀ {C} x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ [] ⟶ num i32 ∷ []) - table-fill : ∀ {C} x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ []) - table-copy : ∀ {C} x y → TableType.type (lookup (Context.tables C) x) ≡ TableType.type (lookup (Context.tables C) y) → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - table-init : ∀ {C} x y → TableType.type (lookup (Context.tables C) x) ≡ lookup (Context.elems C) y → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - elem-drop : ∀ {C} (x : Fin (length (Context.elems C))) → Instruction C ([] ⟶ []) + table-get : ∀ x → Instruction C (num i32 ∷ [] ⟶ ref (TableType.type (lookup (Context.tables C) x)) ∷ []) + table-set : ∀ x → Instruction C (ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ []) + table-size : ∀ (x : Fin (length (Context.tables C))) → Instruction C ([] ⟶ num i32 ∷ []) + table-grow : ∀ x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ [] ⟶ num i32 ∷ []) + table-fill : ∀ x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ []) + table-copy : ∀ x y → TableType.type (lookup (Context.tables C) x) ≡ TableType.type (lookup (Context.tables C) y) → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + table-init : ∀ x y → TableType.type (lookup (Context.tables C) x) ≡ lookup (Context.elems C) y → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + elem-drop : ∀ (x : Fin (length (Context.elems C))) → Instruction C ([] ⟶ []) ---- Memory instructions -- load - i32-load : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i64-load : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) - f32-load : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f32 ∷ []) - f64-load : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f64 ∷ []) + i32-load : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i64-load : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) + f32-load : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f32 ∷ []) + f64-load : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f64 ∷ []) -- loadN - i32-load8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i32-load16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i64-load8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) - i64-load16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) - i64-load32 : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) + i32-load8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i32-load16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i64-load8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) + i64-load16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) + i64-load32 : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) -- store - i32-store : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) - i64-store : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) - f32-store : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num f32 ∷ num i32 ∷ [] ⟶ []) - f64-store : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num f64 ∷ num i32 ∷ [] ⟶ []) + i32-store : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) + i64-store : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) + f32-store : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num f32 ∷ num i32 ∷ [] ⟶ []) + f64-store : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num f64 ∷ num i32 ∷ [] ⟶ []) -- storeN - i32-store8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) - i32-store16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) - i64-store8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) - i64-store16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) - i64-store32 : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) + i32-store8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) + i32-store16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) + i64-store8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) + i64-store16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) + i64-store32 : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) -- other - memory-size : ∀ {C} → length (Context.mems C) > 0 → Instruction C ([] ⟶ num i32 ∷ []) - memory-grow : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - memory-fill : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - memory-copy : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - memory-init : ∀ {C} (x : Fin (Context.datas C)) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - data-drop : ∀ {C} (x : Fin (Context.datas C)) → Instruction C ([] ⟶ []) + memory-size : length (Context.mems C) > 0 → Instruction C ([] ⟶ num i32 ∷ []) + memory-grow : length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + memory-fill : length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + memory-copy : length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + memory-init : (x : Fin (Context.datas C)) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + data-drop : (x : Fin (Context.datas C)) → Instruction C ([] ⟶ []) ---- Control instructions - nop : ∀ {C} → Instruction C ([] ⟶ []) - unreachable : ∀ {C τ} → Instruction C τ - block : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in - Instruction (record C {labels = FuncType.to τ ∷ Context.labels C}) τ → Instruction C τ - loop : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in - Instruction (record C {labels = FuncType.from τ ∷ Context.labels C}) τ → Instruction C τ - if : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in - (then else : Instruction (record C {labels = FuncType.to τ ∷ Context.labels C}) τ) → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ) - br : ∀ {C τ₁ τ₂} l → Instruction C (lookup (Context.labels C) l ++ τ₁ ⟶ τ₂) - br_if : ∀ {C} l → let τ = lookup (Context.labels C) l in Instruction C (num i32 ∷ τ ⟶ τ) - br_table : ∀ {C τ₁ τ₂} ls l → let τ = lookup (Context.labels C) l in All (λ l → lookup (Context.labels C) l ≡ τ) ls → Instruction C (τ ++ τ₁ ⟶ τ₂) - return : ∀ {C τ τ₁ τ₂} → Context.return C ≡ just τ → Instruction C (τ ++ τ₁ ⟶ τ₂) - call : ∀ {C} x → Instruction C (lookup (Context.funcs C) x) - call_indirect : ∀ {C} x τ → TableType.type (lookup (Context.tables C) x) ≡ funcref → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ) - - ---- Sequencing - frame : ∀ {C τ τ₁ τ₂} → Instruction C (τ₁ ⟶ τ₂) → Instruction C (τ₁ ++ τ ⟶ τ₂ ++ τ) - seq : ∀ {C τ₁ τ₂ τ₃} → Instruction C (τ₁ ⟶ τ₂) → Instruction C (τ₂ ⟶ τ₃) → Instruction C (τ₁ ⟶ τ₃) + block : (bt : BlockType C) → let τ = blockTypeAsFunc bt in + Sequence (record C {labels = FuncType.to τ ∷ Context.labels C}) τ → Instruction C τ + loop : (bt : BlockType C) → let τ = blockTypeAsFunc bt in + Sequence (record C {labels = FuncType.from τ ∷ Context.labels C}) τ → Instruction C τ + if : (bt : BlockType C) → let τ = blockTypeAsFunc bt in + (then else : Sequence (record C {labels = FuncType.to τ ∷ Context.labels C}) τ) → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ) + br_if : ∀ l → let τ = lookup (Context.labels C) l in Instruction C (num i32 ∷ τ ⟶ τ) + call : ∀ x → Instruction C (lookup (Context.funcs C) x) + call_indirect : ∀ x τ → TableType.type (lookup (Context.tables C) x) ≡ funcref → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ) + +data Sequence C where + nop : ∀ {τ} → Sequence C (τ ⟶ τ) + unreachable : ∀ {τ} → Sequence C τ + br : ∀ {τ₁ τ₂} l → Sequence C (lookup (Context.labels C) l ++ τ₁ ⟶ τ₂) + br_table : ∀ {τ₁ τ₂} ls l → let τ = lookup (Context.labels C) l in All (λ l → lookup (Context.labels C) l ≡ τ) ls → Sequence C (τ ++ τ₁ ⟶ τ₂) + return : ∀ {τ τ₁ τ₂} → Context.return C ≡ just τ → Sequence C (τ ++ τ₁ ⟶ τ₂) + _∙_ : ∀ {τ₀ τ₁ τ₂ τ₃} → Instruction C (τ₁ ⟶ τ₂) → Sequence C (τ₂ ++ τ₀ ⟶ τ₃) → Sequence C (τ₁ ++ τ₀ ⟶ τ₃) Expression : Context → List ValType → Set -Expression C τ = Instruction C ([] ⟶ τ) +Expression C τ = Sequence C ([] ⟶ τ) -data InstructionRef {C} : ∀ {τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set where +data InstructionRef {C} : ∀ {τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set +data SequenceRef {C} : ∀ {τ} → Sequence C τ → Fin (length (Context.funcs C)) → Set + +data InstructionRef {C} where ---- Direct ref-func : ∀ {x} x∈refs → InstructionRef (ref-func {C} {x} x∈refs) x call : ∀ x → InstructionRef (call {C} x) x ---- Structural - 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 + block : ∀ {x} bt {i} → SequenceRef i x → InstructionRef (block {C} bt i) x + loop : ∀ {x} bt {i} → SequenceRef i x → InstructionRef (loop {C} bt i) x + if₁ : ∀ {x} bt {i₁} → SequenceRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x + if₂ : ∀ {x} bt i₁ {i₂} → SequenceRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x + +data SequenceRef {C} where + _∙₁_ : ∀ {x τ₀ τ₁ τ₂ τ₃ i} → InstructionRef i x → ∀ i* → SequenceRef (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) x + _∙₂_ : ∀ {x τ₀ τ₁ τ₂ τ₃} i {i*} → SequenceRef i* x → SequenceRef (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) x + +data InstructionConstant {C} : ∀ {τ} → Instruction C τ → Set +data SequenceConstant {C} : ∀ {τ} → Sequence C τ → Set + +data InstructionConstant {C} 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) + i32-const : ∀ c → InstructionConstant (i32-const c) + i64-const : ∀ c → InstructionConstant (i64-const c) + f32-const : ∀ c → InstructionConstant (f32-const c) + f64-const : ∀ c → InstructionConstant (f64-const c) -- refs - ref-null : ∀ τ → Constant (ref-null τ) - ref-func : ∀ {x} x∈refs → Constant (ref-func {x = x} x∈refs) + ref-null : ∀ τ → InstructionConstant (ref-null τ) + ref-func : ∀ {x} x∈refs → InstructionConstant (ref-func {x = x} x∈refs) -- global - global-get : ∀ {x} → GlobalType.mut (lookup (Context.globals C) x) ≡ const → Constant (global-get x) + global-get : ∀ {x} → GlobalType.mut (lookup (Context.globals C) x) ≡ const → InstructionConstant (global-get x) - ---- Structural - frame : ∀ {τ τ₁ τ₂ i} → Constant i → Constant (frame {C} {τ} {τ₁} {τ₂} i) - seq : ∀ {τ₁ τ₂ τ₃ i₁ i₂} → Constant i₁ → Constant i₂ → Constant (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) +data SequenceConstant {C} where + nop : ∀ {τ} → SequenceConstant (nop {C} {τ}) + _∙_ : ∀ {τ₀ τ₁ τ₂ τ₃ i i*} → InstructionConstant i → SequenceConstant i* → SequenceConstant (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) |