Idris implementation of Pierre-Evariste Dagand demo (in Agda) at Collège de France

compiler.idr

module Main

%default total

infixr 20 <>

StackType : Type
StackType = List Type

data Stack : List Type -> Type where
  SNil : Stack []
  (<>) : (x : t) -> Stack ts -> Stack (t :: ts)

data Value : Type -> Type where
  C : Nat -> Value Nat
  B : Bool -> Value Bool

data Expr : Type -> Type where
  VAL : Value a -> Expr a
  ADD : Expr Nat -> Expr Nat -> Expr Nat
  IF  : Expr Bool -> Expr a -> Expr a -> Expr a

infixr 20 #

data Code : StackType -> StackType -> Type where
  PUSH : (x : Value t) -> Code ts (t :: ts)
  PADD : Code (Nat :: Nat :: ts) (Nat :: ts)
  PIF  : Code ts a -> Code ts a -> Code (Bool :: ts) a
  (#)  : Code a b -> Code b c -> Code a c

x : Expr Nat
x =
  IF (VAL (B True))
  (IF (VAL (B False))
    (VAL (C 3))
    (VAL (C 9)))
  (IF (VAL (B True))
    (VAL (C 4))
    (VAL (C 1)))

evalE : Expr a -> a
evalE (VAL (C x)) = x
evalE (VAL (B x)) = x
evalE (ADD x y)   = evalE x + evalE y
evalE (IF p x y)  = if evalE p then evalE x else evalE y

evalS : Code a b -> Stack a -> Stack b
evalS (PUSH (C x)) s        = x <> s
evalS (PUSH (B x)) s        = x <> s
evalS PADD (x <> y <> s)      = (x + y) <> s
evalS (PIF x y) (True <> s)  = evalS x s
evalS (PIF x y) (False <> s) = evalS y s
evalS (x # y) s             = evalS y (evalS x s)

compile : Expr a -> Code ts (a :: ts)
compile (VAL v)    = PUSH v
compile (ADD x y)  = compile y # compile x # PADD
compile (IF p x y) = compile p # PIF (compile x) (compile y)

correctness : (e : Expr a)
              -> (s : Stack ts)
              -> evalS (compile e) s = (evalE e) <> s
correctness (VAL (C x)) s = Refl
correctness (VAL (B x)) s = Refl
correctness (ADD x y) s =
  rewrite correctness y s in
  rewrite correctness x (evalE y <> s)
  in Refl
correctness (IF b x y) s with (correctness b s)
  correctness (IF b x y) s | p with (evalE b)
    correctness (IF b x y) s | p | True =
      rewrite p in rewrite correctness x s in Refl
    correctness (IF b x y) s | p | False =
      rewrite p in rewrite correctness y s in Refl