module Wasm.Types where
open import Prelude renaming (Nat to ℕ) hiding (const; min; max)
record Sized (A : Set) : Set where
  field
    --| Bit width: A has size of (2 ^ ∥ A ∥)
    ∥_∥ : A → ℕ
open Sized ⦃ ... ⦄
data numtype : Set where
  i32 i64 f32 f64 : numtype
u32 = Fin (2 ^ 32)
u64 = Fin (2 ^ 64)
record _↔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from-to : ∀ a → from (to a) ≡ a
    to-from : ∀ b → to (from b) ≡ b
instance
  Sized-numtype : Sized numtype
  ∥_∥ ⦃ Sized-numtype ⦄ i32 = 5
  ∥_∥ ⦃ Sized-numtype ⦄ i64 = 6
  ∥_∥ ⦃ Sized-numtype ⦄ f32 = 5
  ∥_∥ ⦃ Sized-numtype ⦄ f64 = 6
data vectype : Set where
  v128 : vectype
instance
  Sized-vectype : Sized vectype
  ∥_∥ ⦃ Sized-vectype ⦄ v128 = 7
data reftype : Set where
  funcref externref : reftype
data valtype : Set where
  num : numtype → valtype
  vec : vectype → valtype
  ref : reftype → valtype
resulttype : Set
resulttype = List valtype
data functype : Set where
  _⇒_ : (input output : resulttype) → functype
-- data valueOf : valtype → Set where
record limits : Set where
  field
    min : u32
    max : Maybe u32
record limited (A : Set) : Set where
  field
    proj : A → u32
    L : limits
memtype : Set
memtype = limits
tabletype = limited reftype
data mut : Set where
  const var : mut
record globaltype : Set where
  field
    inner-type : valtype
    mutability : mut
data externtype : Set where
  func : functype → externtype
  table : tabletype → externtype
  mem : memtype → externtype
  global : globaltype → externtype

module JVM.Types where
open import Prelude hiding (lzero; null) -- using (_≡_; ¬_)
data type : Set
data value : type → Set
data primitive-type : Set
data primitive-value : primitive-type → Set
data nullable (A : Set) : Set
data reference-type : Set
data reference-value : reference-type → Set
data type where
  prim-type : primitive-type → type
  ref-type : reference-type → type
data value where
  prim-value : ∀ {@0 A} → primitive-value A → value (prim-type A)
  ref-value : ∀ {@0 A} → nullable (reference-value A) → value (ref-type A)
data primitive-type where
  byte short int long char : primitive-type
  float double : primitive-type
  boolean : primitive-type
  returnAddress : primitive-type
data primitive-value where
  bzero : primitive-value byte
  szero : primitive-value short
  izero : primitive-value int
  lzero : primitive-value long
  czero : primitive-value char
  fzero : primitive-value float
  dzero : primitive-value double
  false true : primitive-value boolean
elim-⊥ : ∀ {a} {@0 A : Set a} (@0 x : ⊥) → A
elim-⊥ ()
default-prim-value : (A : primitive-type) (@0 not-retAddr : ¬ (A ≡ returnAddress)) → primitive-value A
default-prim-value byte _ = bzero
default-prim-value short _ = szero
default-prim-value int _ = izero
default-prim-value long _ = lzero
default-prim-value char _ = czero
default-prim-value float _ = fzero
default-prim-value double _ = dzero
default-prim-value boolean _ = false
default-prim-value returnAddress not-retAddr = elim-⊥ (not-retAddr refl)
data nullable A where
  null : nullable A
  non-null : A → nullable A
data reference-type where
  class-type interface-type : reference-type
  array-type : type → reference-type
data reference-value where
default-value : (A : type) (@0 not-retAddr : ¬ (A ≡ prim-type returnAddress)) → value A
default-value (prim-type A) not-retAddr = prim-value (default-prim-value A λ is-retAddr → not-retAddr (cong prim-type is-retAddr))
default-value (ref-type A) _ = ref-value null
array-element-type : (A : type) → type
array-element-type (ref-type (array-type A)) = array-element-type A
array-element-type A = A

module JVM.Memory where
data area : Set where
  global thread-local : area
data memory : area → Set where
  pc stack : memory thread-local
  heap method-area : memory global

module JVM.Memory where
data area : Set where
  global thread-local : area
data memory : area → Set where
  pc stack : memory thread-local
  heap method-area : memory global

{ agdaPackages ? (import <nixpkgs> {}).agdaPackages }:
let inherit (agdaPackages) mkDerivation agda agda-prelude;
 in
mkDerivation {
  pname = "bytecode";
  version = "0.1.0";
  src = ./.;
  everythingFile = "src/Spec.agda";
  buildInputs = [ agda-prelude ];
  meta = false;
}

name: bytecode
include: src
depend: agda-prelude