From 904924c33720c3481f738966f32e9c34736f92cf Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 10 Aug 2021 19:11:38 +0100 Subject: Rewrite so only valid modules can be constructed. --- src/Wasm/Expression/Instructions.agda | 219 ---------------------------------- 1 file changed, 219 deletions(-) delete mode 100644 src/Wasm/Expression/Instructions.agda (limited to 'src/Wasm/Expression/Instructions.agda') diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda deleted file mode 100644 index 3fa96be..0000000 --- a/src/Wasm/Expression/Instructions.agda +++ /dev/null @@ -1,219 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - ------------------------------------------------------------------------- --- 2.4 Types - -module Wasm.Expression.Instructions where - -open import Data.List using (List) -open import Data.Maybe using (Maybe) -open import Data.Product using (∃) -open import Data.Sum using (_⊎_) -open import Wasm.Expression.Values using (UnsignedInteger; UninterpretedInteger; Float) -open import Wasm.Expression.Types using (ValType; RefType) -open import Wasm.Expression.Utilities - ------------------------------------------------------------------------- --- 2.4.1 Numeric Instructions - -module IntOp (w : BitWidth) where - data Unary : Set where - clz : Unary - ctz : Unary - popcnt : Unary - - data Binary : Set where - add : Binary - sub : Binary - mul : Binary - div : Signedness → Binary - rem : Signedness → Binary - and : Binary - or : Binary - xor : Binary - shl : Binary - shr : Signedness → Binary - rotl : Binary - rotr : Binary - - data Test : Set where - eqz : Test - - data Rel : Set where - eq : Rel - ne : Rel - lt : Signedness → Rel - gt : Signedness → Rel - le : Signedness → Rel - ge : Signedness → Rel - - data IntInstr : Set where - const : UninterpretedInteger (BitWidth′.toℕ w) → IntInstr - iunop : Unary → IntInstr - ibinop : Binary → IntInstr - itestop : Test → IntInstr - irelop : Rel → IntInstr - extend8-s : IntInstr - extend16-s : IntInstr - trunc-f : BitWidth → Signedness → IntInstr - trunc-sat-f : BitWidth → Signedness → IntInstr - reinterpret-f : IntInstr - -data IntInstr : Set where - ixx : ∀ w → IntOp.IntInstr w → IntInstr - i64-extend32-s : IntInstr - i32-wrap-i64 : IntInstr - i64-extend-i32 : Signedness → IntInstr - -module FloatOp (w : BitWidth) where - data Unary : Set where - abs : Unary - neg : Unary - sqrt : Unary - ceil : Unary - floor : Unary - trunc : Unary - nearest : Unary - - data Binary : Set where - add : Binary - sub : Binary - mul : Binary - div : Binary - min : Binary - max : Binary - copysign : Binary - - data Rel : Set where - eq : Rel - ne : Rel - lt : Rel - gt : Rel - le : Rel - ge : Rel - - data FloatInstr : Set where - const : Float w → FloatInstr - funop : Unary → FloatInstr - fbinop : Binary → FloatInstr - frelop : Rel → FloatInstr - convert-i : BitWidth → Signedness → FloatInstr - reinterpret-i : FloatInstr - -data FloatInstr : Set where - fxx : ∀ w → FloatOp.FloatInstr w → FloatInstr - f32-demote-f64 : FloatInstr - f64-promote-f32 : FloatInstr - -data NumInstr : Set where - int : IntInstr → NumInstr - float : FloatInstr → NumInstr - ------------------------------------------------------------------------- --- 2.4.2 Reference Instructions - -data RefInstr : Set where - null : RefType → RefInstr - is-null : RefInstr - func : Indices.FuncIdx → RefInstr - ------------------------------------------------------------------------- --- 2.4.3 Parametric Instructions - -data ParametricInstr : Set where - drop : ParametricInstr - select : Maybe (List ValType) → ParametricInstr - ------------------------------------------------------------------------- --- 2.4.4 Variable Instructions - -data VarInstr : Set where - local-get : Indices.LocalIdx → VarInstr - local-set : Indices.LocalIdx → VarInstr - local-tee : Indices.LocalIdx → VarInstr - global-get : Indices.GlobalIdx → VarInstr - global-set : Indices.GlobalIdx → VarInstr - ------------------------------------------------------------------------- --- 2.4.5 Table Instructions - -data TableInstr : Set where - get : Indices.TableIdx → TableInstr - set : Indices.TableIdx → TableInstr - size : Indices.TableIdx → TableInstr - grow : Indices.TableIdx → TableInstr - fill : Indices.TableIdx → TableInstr - copy : Indices.TableIdx → Indices.TableIdx → TableInstr - init : Indices.TableIdx → Indices.ElemIdx → TableInstr - drop : Indices.ElemIdx → TableInstr - ------------------------------------------------------------------------- --- 2.4.6 Memory Instructions - -record MemArg : Set where - field - offset : UnsignedInteger 32 - align : UnsignedInteger 32 - -module IntMem (w : BitWidth) where - data IntMemInstr : Set where - load : MemArg → IntMemInstr - store : MemArg → IntMemInstr - load8 : Signedness → MemArg → IntMemInstr - load16 : Signedness → MemArg → IntMemInstr - store8 : MemArg → IntMemInstr - store16 : MemArg → IntMemInstr - -data IntMemInstr : Set where - ixx : ∀ w → IntMem.IntMemInstr w → IntMemInstr - i64-load32 : Signedness → MemArg → IntMemInstr - i64-store32 : MemArg → IntMemInstr - -module FloatMem (w : BitWidth) where - data FloatMemInstr : Set where - load : MemArg → FloatMemInstr - store : MemArg → FloatMemInstr - -FloatMemInstr : Set -FloatMemInstr = ∃ FloatMem.FloatMemInstr - -data MemInstr : Set where - int : IntMemInstr → MemInstr - float : FloatMemInstr → MemInstr - size : MemInstr - grow : MemInstr - fill : MemInstr - copy : MemInstr - init : Indices.DataIdx → MemInstr - drop : Indices.DataIdx → MemInstr - ------------------------------------------------------------------------- --- 2.4.7 Control Instructions - -BlockType : Set -BlockType = Indices.TypeIdx ⊎ Maybe ValType - -data Instr : Set where - num : NumInstr → Instr - ref : RefInstr → Instr - parametric : ParametricInstr → Instr - var : VarInstr → Instr - table : TableInstr → Instr - mem : MemInstr → Instr - nop : Instr - unreachable : Instr - block : BlockType → List Instr → Instr - loop : BlockType → List Instr → Instr - if-else : BlockType → List Instr → List Instr → Instr - br : Indices.LabelIdx → Instr - br-if : Indices.LabelIdx → Instr - br-table : Vec′ Indices.LabelIdx → Indices.LabelIdx → Instr - return : Instr - call : Indices.FuncIdx → Instr - call-indirect : Indices.TableIdx → Indices.TypeIdx → Instr - ------------------------------------------------------------------------- --- 2.4.8 Expressions - -Expr : Set -Expr = List Instr -- cgit v1.2.3