diff options
Diffstat (limited to 'src/Wasm/Expression')
| -rw-r--r-- | src/Wasm/Expression/Instructions.agda | 219 | ||||
| -rw-r--r-- | src/Wasm/Expression/Modules.agda | 128 | ||||
| -rw-r--r-- | src/Wasm/Expression/Types.agda | 112 | ||||
| -rw-r--r-- | src/Wasm/Expression/Utilities.agda | 52 | ||||
| -rw-r--r-- | src/Wasm/Expression/Values.agda | 122 |
5 files changed, 0 insertions, 633 deletions
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 diff --git a/src/Wasm/Expression/Modules.agda b/src/Wasm/Expression/Modules.agda deleted file mode 100644 index 912d6da..0000000 --- a/src/Wasm/Expression/Modules.agda +++ /dev/null @@ -1,128 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - ------------------------------------------------------------------------- --- 2.5 Modules - -module Wasm.Expression.Modules where - -open import Data.Maybe using (Maybe) -open import Wasm.Expression.Types -open import Wasm.Expression.Utilities using (Vec′; module Indices) -open import Wasm.Expression.Values using (Byte; Name) -open import Wasm.Expression.Instructions using (Expr) - ------------------------------------------------------------------------- --- 2.5.1 Indices - --- NOTE: defined in Wasm.Expression.Utilities - ------------------------------------------------------------------------- --- 2.5.2 Types - --- NOTE: no new definitions - ------------------------------------------------------------------------- --- 2.5.3 Functions - -record Func : Set where - field - type : Indices.TypeIdx - locals : Vec′ ValType - body : Expr - ------------------------------------------------------------------------- --- 2.5.4 Tables - -Table : Set -Table = TableType - ------------------------------------------------------------------------- --- 2.5.5 Memories - -Mem : Set -Mem = MemType - ------------------------------------------------------------------------- --- 2.5.6 Globals - -record Global : Set where - field - type : GlobalType - init : Expr - ------------------------------------------------------------------------- --- 2.5.7 Element Segments - -data ElemMode : Set where - passive : ElemMode - active : (table : Indices.TableIdx) → (offset : Expr) → ElemMode - declarative : ElemMode - -record Elem : Set where - field - type : RefType - init : Vec′ Expr - mode : ElemMode - ------------------------------------------------------------------------- --- 2.5.8 Data Segments - -data DataMode : Set where - passive : DataMode - active : (memory : Indices.MemIdx) → (offset : Expr) → DataMode - -record Data : Set where - field - init : Vec′ Byte - mode : DataMode - ------------------------------------------------------------------------- --- 2.5.9 Start Function - -Start : Set -Start = Indices.FuncIdx - ------------------------------------------------------------------------- --- 2.5.10 Exports - -data ExportDesc : Set where - func : Indices.FuncIdx → ExportDesc - table : Indices.TableIdx → ExportDesc - mem : Indices.MemIdx → ExportDesc - global : Indices.GlobalIdx → ExportDesc - -record Export : Set where - field - name : Name - desc : ExportDesc - ------------------------------------------------------------------------- --- 2.5.11 Imports - -data ImportDesc : Set where - func : Indices.TypeIdx → ImportDesc - table : TableType → ImportDesc - mem : MemType → ImportDesc - global : GlobalType → ImportDesc - -record Import : Set where - field - mod : Name - name : Name - desc : ImportDesc - ------------------------------------------------------------------------- --- Module definition - -record Mod : Set where - field - types : Vec′ FuncType - funcs : Vec′ Func - tables : Vec′ Table - mems : Vec′ Mem - globals : Vec′ Global - elems : Vec′ Elem - datas : Vec′ Data - start : Maybe Start - imports : Vec′ Import - exports : Vec′ Export diff --git a/src/Wasm/Expression/Types.agda b/src/Wasm/Expression/Types.agda deleted file mode 100644 index 02661e8..0000000 --- a/src/Wasm/Expression/Types.agda +++ /dev/null @@ -1,112 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - ------------------------------------------------------------------------- --- 2.3 Types - -module Wasm.Expression.Types where - -open import Data.Maybe using (Maybe; just; nothing) -open import Data.Product using (_×_) -open import Data.Sum using (_⊎_) -open import Wasm.Expression.Values using (UnsignedInteger) -open import Wasm.Expression.Utilities using (Vec′) - ------------------------------------------------------------------------- --- 2.3.1 Number Types - -data NumType : Set where - i32 : NumType - i64 : NumType - f32 : NumType - f64 : NumType - ------------------------------------------------------------------------- --- 2.3.2 Reference Types - -data RefType : Set where - funcref : RefType - externref : RefType - ------------------------------------------------------------------------- --- 2.3.3 Value Types - -ValType : Set -ValType = NumType ⊎ RefType - ------------------------------------------------------------------------- --- 2.3.4 Result Types - -ResultType : Set -ResultType = Vec′ ValType - ------------------------------------------------------------------------- --- 2.3.5 Function Types - -record FuncType : Set where - constructor _⟶_ - field - from : ResultType - to : ResultType - ------------------------------------------------------------------------- --- 2.3.6 Limits - -record Limits : Set where - field - min : UnsignedInteger 32 - max : Maybe (UnsignedInteger 32) - ------------------------------------------------------------------------- --- 2.3.7 Memory Types - -MemType : Set -MemType = Limits - ------------------------------------------------------------------------- --- 2.3.8 Table Types - -TableType : Set -TableType = Limits × RefType - ------------------------------------------------------------------------- --- 2.3.9 Global Types - -data Mut : Set where - const : Mut - var : Mut - -GlobalType : Set -GlobalType = Mut × ValType - ------------------------------------------------------------------------- --- 2.3.10 External Types - -data ExternType : Set where - func : FuncType → ExternType - table : TableType → ExternType - mem : MemType → ExternType - global : GlobalType → ExternType - -func? : ExternType → Maybe FuncType -func? (func t) = just t -func? (table t) = nothing -func? (mem t) = nothing -func? (global t) = nothing - -table? : ExternType → Maybe TableType -table? (func t) = nothing -table? (table t) = just t -table? (mem t) = nothing -table? (global t) = nothing - -mem? : ExternType → Maybe MemType -mem? (func t) = nothing -mem? (table t) = nothing -mem? (mem t) = just t -mem? (global t) = nothing - -global? : ExternType → Maybe GlobalType -global? (func t) = nothing -global? (table t) = nothing -global? (mem t) = nothing -global? (global t) = just t diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda deleted file mode 100644 index 129af14..0000000 --- a/src/Wasm/Expression/Utilities.agda +++ /dev/null @@ -1,52 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -module Wasm.Expression.Utilities where - -open import Data.Fin using (Fin) -open import Data.Nat using (ℕ; _^_) -open import Data.Vec.Bounded using (Vec≤) -open import Wasm.Constants - -Vec′ : ∀ {a} → Set a → Set a -Vec′ A = Vec≤ A 2^32 - -data Signedness : Set where - Signed : Signedness - Unsigned : Signedness - -data BitWidth : Set where - 32Bit : BitWidth - 64Bit : BitWidth - -module BitWidth′ where - toℕ : BitWidth → ℕ - toℕ 32Bit = 32 - toℕ 64Bit = 64 - -module Indices where - TypeIdx : Set - TypeIdx = Fin 2^32 - - FuncIdx : Set - FuncIdx = Fin 2^32 - - TableIdx : Set - TableIdx = Fin 2^32 - - MemIdx : Set - MemIdx = Fin 2^32 - - GlobalIdx : Set - GlobalIdx = Fin 2^32 - - ElemIdx : Set - ElemIdx = Fin 2^32 - - DataIdx : Set - DataIdx = Fin 2^32 - - LocalIdx : Set - LocalIdx = Fin 2^32 - - LabelIdx : Set - LabelIdx = Fin 2^32 diff --git a/src/Wasm/Expression/Values.agda b/src/Wasm/Expression/Values.agda deleted file mode 100644 index 283e325..0000000 --- a/src/Wasm/Expression/Values.agda +++ /dev/null @@ -1,122 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - ------------------------------------------------------------------------- --- 2.2 Values - -module Wasm.Expression.Values where - -open import Data.Char using (Char; toℕ) -open import Data.Empty using (⊥) -open import Data.Fin using (Fin) -open import Data.Nat using (ℕ; zero; suc; _^_; pred) -open import Wasm.Constants -open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit) - -infix 8 +_ -_ - ------------------------------------------------------------------------- --- 2.2.1 Bytes - -Byte : Set -Byte = Fin 256 - ------------------------------------------------------------------------- --- 2.2.2 Integers - -UnsignedInteger : ℕ → Set -UnsignedInteger n = Fin (2 ^ n) - -data SignedInteger : ℕ → Set where - +_ : ∀ {n} → Fin n → SignedInteger (suc n) - -[1+_] : ∀ {n} → Fin n → SignedInteger (suc n) - -UninterpretedInteger : ℕ → Set -UninterpretedInteger = UnsignedInteger - ------------------------------------------------------------------------- --- 2.2.3 Floating-Point - -signif : BitWidth → ℕ -signif 32Bit = 23 -signif 64Bit = 52 - -expon : BitWidth → ℕ -expon 32Bit = 8 -expon 64Bit = 11 - -data FloatMag : BitWidth → Set where - nan : ∀ {w} → (n : Fin (pred (2 ^ (signif w)))) → FloatMag w - ∞ : ∀ {w} → FloatMag w - normal : ∀ {w} → (e : Fin (pred (pred (2 ^ (expon w))))) → (t : Fin (2 ^ (signif w))) → FloatMag w - subnormal : ∀ {w} → (t : Fin (pred (2 ^ (signif w)))) → FloatMag w - zero : ∀ {w} → FloatMag w - -data Float : BitWidth → Set where - +_ : ∀ {w} → FloatMag w → Float w - -_ : ∀ {w} → FloatMag w → Float w - ------------------------------------------------------------------------- --- 2.2.4 Names - -module _ where - open import Data.Bool using (Bool; true; false; if_then_else_) - open import Data.List using (List; []; _∷_; length; map; sum) - open import Data.Nat using (_≤ᵇ_; _<_; z≤n; s≤s) - open import Data.Nat.Properties using (≤-step) - open import Data.Product using (_×_; _,_; proj₂; map₂) - open import Data.String using (String; toList) - - halfEven? : ℕ → Bool × ℕ - halfEven? zero = true , 0 - halfEven? (suc zero) = false , 0 - halfEven? (suc (suc n)) = map₂ suc (halfEven? n) - - n≢0⇒halfEven?<n : ∀ n → proj₂ (halfEven? (suc n)) < (suc n) - n≢0⇒halfEven?<n zero = s≤s z≤n - n≢0⇒halfEven?<n (suc zero) = s≤s (n≢0⇒halfEven?<n zero) - n≢0⇒halfEven?<n (suc (suc n)) = s≤s (≤-step (n≢0⇒halfEven?<n n)) - - asBits : ℕ → List Bool - asBits n = All.wfRec <-wellFounded _ Pred helper n - where - open import Data.Nat.Induction using (<-wellFounded) - open import Data.Nat.Properties using (module ≤-Reasoning) - open import Induction.WellFounded using (WfRec; module All) - open import Relation.Binary.PropositionalEquality using (cong; inspect; [_]) - - open ≤-Reasoning - - Pred : ℕ → Set - Pred n = List Bool - - helper : ∀ n → WfRec _<_ Pred n → List Bool - helper zero rec = [] - helper (suc n) rec with halfEven? (suc n) | inspect halfEven? (suc n) - ... | true , m | [ m≡n+1/2 ] = false ∷ rec m (begin-strict - m ≡˘⟨ cong proj₂ m≡n+1/2 ⟩ - proj₂ (halfEven? (suc n)) <⟨ n≢0⇒halfEven?<n n ⟩ - suc n ∎) - ... | false , m | [ m≡n/2 ] = true ∷ rec m (begin-strict - m ≡˘⟨ cong proj₂ m≡n/2 ⟩ - proj₂ (halfEven? (suc n)) <⟨ n≢0⇒halfEven?<n n ⟩ - suc n ∎) - - utf8Bytes : Char → ℕ - utf8Bytes c with asBits (toℕ c) - ... | bits = if length bits ≤ᵇ 7 then - 1 - else if length bits ≤ᵇ 11 then - 2 - else if length bits ≤ᵇ 16 then - 3 - else - 4 - - byteLength : String → ℕ - byteLength s = sum (map utf8Bytes (toList s)) - - data Name : Set where - name : ∀ s → {len : byteLength s < 2^32} → Name - - toString : Name → String - toString (name s) = s |