gistfile1.txt

%default total

-- 2.1.1

%elim
data binop : Type where
  Plus : binop
  Times : binop

%elim
data exp : Type where
  Const : Nat -> exp
  Binop : binop -> exp -> exp -> exp

binopDenote : binop -> Nat -> Nat -> Nat
binopDenote Plus = plus
binopDenote Times = mult

expDenote : exp -> Nat
expDenote (Const n) = n
expDenote (Binop b e1 e2) = (binopDenote b) (expDenote e1) (expDenote e2)

{-
> expDenote (Const 42)
42 : Nat
> expDenote (Binop Plus (Const 2) (Const 2))
4 : Nat
> expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))
28 : Nat
-}

-- 2.1.2

data instr : Type where
  iConst : Nat -> instr
  iBinop : binop -> instr

prog : Type
prog = List instr

stack : Type
stack = List Nat

instrDenote : instr -> stack -> Maybe stack
instrDenote (iConst n) s                = Just (n :: s)
instrDenote (iBinop b) (arg1::arg2::s') = Just ((binopDenote b) arg1 arg2 :: s')
instrDenote (iBinop b) _                = Nothing

progDenote : prog -> stack -> Maybe stack
progDenote []      s = Just s
progDenote (i::p') s = case instrDenote i s of
  Nothing => Nothing
  Just s' => progDenote p' s'

-- 2.1.3

compile : exp -> prog
compile (Const n) = [iConst n]
compile (Binop b e1 e2) = compile e2 ++ compile e1 ++ [iBinop b]

{-
> compile (Const 42)
[iConst 42] : List instr
> compile (Binop Plus (Const 2) (Const 2))
[iConst 2, iConst 2, iBinop Plus] : List instr
> compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))
[iConst 7, iConst 2, iConst 2, iBinop Plus, iBinop Times] : List instr
> progDenote (compile (Const 42)) []
Just [42] : Maybe (List Nat)
> progDenote (compile (Binop Plus (Const 2) (Const 2))) []
Just [4] : Maybe (List Nat)
> progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))) []
Just [28] : Maybe (List Nat)
-}

-- 2.1.4

compileCorrect : (e : exp) -> progDenote (compile e) [] = Just (expDenote e `Prelude.List.(::)` [])
compileCorrect = ?compileCorrectTheorem

compileCorrect' : (e : exp) -> (p : prog) -> (s : stack) ->
                  progDenote (compile e ++ p) s = progDenote p (expDenote e :: s)
compileCorrect' = ?compileCorrect'Lemma