DTComp.idr

-- https://www.cs.nott.ac.uk/~psymp4/files/dependently-typed-compilers.pdf

data Exp : Type -> Type where
  Val : t -> Exp t
  Add : Exp Nat -> Exp Nat -> Exp Nat
  If  : Eq t => Exp Bool -> Exp t -> Exp t -> Exp t

eval : Exp t -> t
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (If x y z) = ifThenElse (eval x) (eval y) (eval z)

data Stack : List Type -> Type where
  Eps : Stack []
  (|>) : t -> Stack ts -> Stack (t :: ts)

infixr 7 |>

data Code : List Type -> List Type -> Type where
  PUSH  : t -> Code ts (t :: ts)
  IF    : Code s s' -> Code s s' -> Code (Bool :: s) s'
  ADD   : Code (Nat :: Nat :: s) (Nat :: s)
  (+++) : Code s s' -> Code s' s'' -> Code s s'' 

infixl 7 +++ 

exec : Code s s' -> Stack s -> Stack s'
exec (PUSH x) s          = x |> s
exec (IF c1 c2) (b |> s) = ifThenElse b (exec c1 s) (exec c2 s)
exec ADD (m |> n |> s)   = (n + m) |> s
exec (c1 +++ c2) s       = exec c2 (exec c1 s)

compile : Exp t -> Code s (t :: s)
compile (Val x)    = PUSH x
compile (Add x y)  = compile x +++ compile y +++ ADD
compile (If b x y) = compile b +++ IF (compile x) (compile y)

distributeIf : (f : t1 -> t2) -> (b : Bool) -> (x : t1) -> (y : t1) ->
               f (ifThenElse b x y) = ifThenElse b (f x) (f y)
distributeIf _ False x y = Refl
distributeIf _ True  x y = Refl

correct : (e : Exp t) -> (s : Stack ts) -> exec (compile e) s = eval e |> s 
correct (Val x) s = Refl
correct (Add x y) s = 
  rewrite correct x s  in
  rewrite correct y (eval x |> s) in
  Refl
correct (If b x y) s =
  rewrite correct b s in
  rewrite distributeIf (|> s) (eval b) (eval x) (eval y) in
  rewrite correct x s in
  rewrite correct y s in
  Refl

DTComp2.idr

-- https://www.cs.nott.ac.uk/~psymp4/files/dependently-typed-compilers.pdf
data Exp : Type -> Type where
  Val : t -> Exp t
  Add : Exp Nat -> Exp Nat -> Exp Nat
  If  : Eq t => Exp Bool -> Exp t -> Exp t -> Exp t

eval : Exp t -> t
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (If x y z) = if eval x then eval y else eval z

data Stack : List Type -> Type where
  Eps : Stack []
  (|>) : t -> Stack ts -> Stack (t :: ts)

infixr 7 |>

data Code : List Type -> List Type -> Type where
  PUSH  : t -> Code ts (t :: ts)
  IF    : Code s s' -> Code s s' -> Code (Bool :: s) s'
  ADD   : Code (Nat :: Nat :: s) (Nat :: s)
  (+++) : Code s s' -> Code s' s'' -> Code s s'' 

infixl 7 +++ 

exec : Code s s' -> Stack s -> Stack s'
exec (PUSH x) s          = x |> s
exec (IF c1 c2) (b |> s) = if b then exec c1 s else exec c2 s
exec ADD (m |> n |> s)   = (n + m) |> s
exec (c1 +++ c2) s       = exec c2 (exec c1 s)

compile : Exp t -> Code s (t :: s)
compile (Val x)    = PUSH x
compile (Add x y)  = compile x +++ compile y +++ ADD
compile (If b x y) = compile b +++ IF (compile x) (compile y)

distributeIf : (b : Bool ) -> (t : ty) -> (e : ty) -> (f : ty -> ty2) -> f (if b then t else e) = if b then f t else f e
distributeIf False t e f = Refl
distributeIf True t e f = Refl

excludedMiddle : (b : _) -> Either (eval b === True) (eval b === False)
excludedMiddle b with (eval b)
    _ | True = Left Refl
    _ | False = Right Refl

correct : (e : Exp t) -> (s : Stack ts) -> exec (compile e) s = eval e |> s
correct (Val x) s = Refl
correct (Add x y) s = 
  rewrite correct x s  in
  rewrite correct y (eval x |> s) in
  Refl
correct (If b x y) s =
    rewrite correct b s in
    case excludedMiddle b of
        Left prf  => rewrite prf in correct x s
        Right prf => rewrite prf in correct y s
    
        

Idris 2 proof that I'm stuck on.

Ok, ran %logging "elab.rewrite" 10 and learned that if/then/else doesn't work well with rewrite, but there is an ifThenElse function.

Added version that works with normal if / then / else