Innovative representation of IMP programming language

Imp.agda

module Imp where

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

data Vec (A : Set) : ℕ → Set where
  [] : Vec A Z
  _∷_ : ∀ {n} → A → Vec A n → Vec A (S n)

binop : Set → Set
binop X = X → X → X

_+_ : ℕ → ℕ → ℕ
Z + n = n
(S n) + m = S (n + m)

append : ∀ {A n m} → Vec A n → Vec A m → Vec A (n + m)
append [] ys = ys
append (x ∷ xs) ys = x ∷ append xs ys

data Fin : ℕ → Set where
  fZ : ∀ n → Fin (S n)
  fS : ∀ n → Fin n → Fin (S n)

data Expr (A : Set) (size : ℕ) : Set where
  var : ∀ {n} → Fin n → Expr A size
  const : A → Expr A size
  comp : binop A → Expr A size → Expr A size → Expr A size

data Bool : Set where
  true false : Bool

if : {A : Set} → Bool → A → A → A
if true x _ = x
if false _ y = y

pred : Set → Set
pred X = X → Bool

data StmtList (A : Set) : ℕ → Set where
  empty : ∀ {n} → StmtList A n
  assign : ∀ {n} → Fin n → Expr A n → StmtList A n → StmtList A n
  intro : ∀ {n} → Expr A n → StmtList A n → StmtList A (S n)
  ifP : ∀ {k n} → pred A → Expr A n → StmtList A (k + n) → StmtList A n → StmtList A n
  whileP : ∀ {k n} → pred A → Expr A n → StmtList A (k + n) → StmtList A n → StmtList A n

lookup : ∀ {A n} → Vec A n → Fin n → A
lookup [] ()
lookup (_∷_ {n} x xs) (fZ .n) = x
lookup (_∷_ {n} x xs) (fS .n f) = lookup xs f

eval : ∀ {A} size → Expr A size → Vec A size → A
eval size (var x) env = {!!}
eval size (const x) env = {!!}
eval size (comp x expr expr₁) env = {!!}