jvm.agda

open import Agda.Builtin.Int using (Int; pos)
open import Data.Bool using (T)
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat using (ℕ)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Vec using (Vec; []; _∷_; _[_]=_; here; there; _++_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary.Decidable using (True; isYes)
open import Relation.Nullary using (Dec; yes; no)

data JvmType : Set where
  int long float double ref : JvmType

_≟_ : (a : JvmType) → (b : JvmType) → Dec (a ≡ b)
int ≟ int = yes refl
int ≟ long = no λ()
int ≟ float = no λ()
int ≟ double = no λ()
int ≟ ref = no λ()
long ≟ int = no λ()
long ≟ long = yes refl
long ≟ float = no λ()
long ≟ double = no λ()
long ≟ ref = no λ()
float ≟ int = no λ()
float ≟ long = no λ()
float ≟ float = yes refl
float ≟ double = no λ()
float ≟ ref = no λ()
double ≟ int = no λ()
double ≟ long = no λ()
double ≟ float = no λ()
double ≟ double = yes refl
double ≟ ref = no λ()
ref ≟ int = no λ()
ref ≟ long = no λ()
ref ≟ float = no λ()
ref ≟ double = no λ()
ref ≟ ref = yes refl

infixl 20 _,_

data OperandStack : Set where
  empty : OperandStack
  _,_ : OperandStack → JvmType → OperandStack

Locals : ℕ → Set
Locals = Vec JvmType

infix 4 _[_]≟_

_[_]≟_ : {n : ℕ} → (v : Locals n) → (i : Fin n) → (a : JvmType) → Dec (v [ i ]= a)
_[_]≟_ (x ∷ xs) zero a with x ≟ a
...                       | yes x≡a rewrite x≡a = yes here
...                       | no ¬x≡a = no λ { here → ¬x≡a refl }
_[_]≟_ (x ∷ xs) (suc n) a with xs [ n ]≟ a
...                          | yes xsn≡a = yes (there xsn≡a)
...                          | no ¬xsn≡a = no λ { (there xsn≡a) → ¬xsn≡a xsn≡a }

data SequentialCode {n : ℕ} (l : Locals n) : OperandStack → OperandStack → Set where
  iconst   : ∀ {s} → Int → SequentialCode l s (s , int)
  iadd     : ∀ {s} → SequentialCode l (s , int , int) (s , int)
  iload    : ∀ {s} → (i : Fin n) → {True (l [ i ]≟ int)} → SequentialCode l s (s , int)
  istore   : ∀ {s} → (i : Fin n) → {True (l [ i ]≟ int)} → SequentialCode l (s , int) s
  _,_ : ∀ {s t u} → SequentialCode l s t → SequentialCode l t u → SequentialCode l s u

BasicBlockRef : ℕ → Set
BasicBlockRef = Fin

data Jump (bc : ℕ) : OperandStack → OperandStack → Set where
  ifICmpEq : ∀ {s} → BasicBlockRef bc × BasicBlockRef bc → Jump bc (s , int , int) s
  ireturn : ∀ {s} → Jump bc (s , int) s

data BasicBlock {n : ℕ} (l : Locals n) (bc : ℕ) : Set where
  _,_ : ∀ {s} → SequentialCode l empty s → Jump bc s empty → BasicBlock l bc

record Method {n : ℕ} (args : Locals n) : Set where
  field
    localsCount : ℕ
    locals : Locals localsCount
    blockCount : ℕ
    blocks : Vec (BasicBlock (args ++ locals) blockCount) blockCount

simpleFunc : Method []
simpleFunc =
  record
    { localsCount = _
    ; locals = int ∷ float ∷ long ∷ []
    ; blockCount = _
    ; blocks =
      iconst (pos 1) ,
      iload zero ,
      iadd ,
      istore zero ,
      iload zero ,
      iconst (pos 100) ,
      ifICmpEq (⟨ suc zero , zero ⟩)
      ∷
      iload zero ,
      ireturn
      ∷
      []
    }