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