Agda compiler, from Conor McBride

Test1.agda

module Test1 where

{- numbers -}
data Nat : Set where
   zero :              Nat
   suc  : (n : Nat) -> Nat
{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

infixr 5 _+_
_+_ : Nat -> Nat -> Nat
zero + m  = m
suc n + m = suc (n + m)

one = 1
two = 2

{- Hutton's razor -}
data Expr : Set where
  val       : (e : Nat)      -> Expr
  _+'_      : (e1 e2 : Expr) -> Expr

{- Write an evaluator -}
{--}
evalE : Expr -> Nat
evalE (val e)    = e
evalE (e1 +' e2) = evalE e1 + evalE e2
--}


{- Build a stack machine language -}
data Inst : Nat -> Nat -> Set where
  PUSH : (v : Nat) -> {n : Nat} -> Inst n (1 + n)
  ADD  :              {n : Nat} -> Inst (2 + n) (1 + n)

Rel : Set -> Set1
Rel I = I -> I -> Set

data List {I : Set}(X : Rel I) : Rel I where
  []  : {i : I}                            -> List X i i
  _*_ : {i j k : I} -> X i j -> List X j k -> List X i k
infixr 4 _*_

infixr 4 _++_
_++_ : forall {I}{X}{i j k : I} -> List X i j -> List X j k -> List X i k
[] ++ ys       = ys
(x * xs) ++ ys = x * (xs ++ ys)

{- Compile expressions to stack machine -}
{--}
compile : Expr -> {n : Nat} -> List Inst n (1 + n)
compile (val e)    = PUSH e * []
compile (e1 +' e2) = compile e1 ++ compile e2 ++ ADD * []
--}

{- Run lists of instructions! -}

data Elt : Nat -> Nat -> Set where
  E : Nat -> {n : Nat} -> Elt (1 + n) n

{--}
evalI : {i j : Nat} -> List Inst i j -> List Elt i 0 -> List Elt j 0
evalI [] vs = vs
evalI (PUSH v * is) vs        = evalI is (E v * vs)
evalI (ADD * is) (() * [])
evalI (ADD * is) (E y * E x * vs) = evalI is (E (x + y) * vs)
--}

ex1 : List Elt 1 0
ex1 = evalI (compile (val 2 +' val 2)) []