module HomeworkSeventeen

%default total

data Prog = Push Nat | Pop | Add | Seq Prog Prog

Stack : Type
Stack = List Nat

data BS : Stack -> Prog -> Stack -> Type where
  BS_Push : BS s (Push n) (n::s)
  BS_Pop  : BS (n::s) Pop s
  BS_Add  : BS (n::m::s) Add (n+m::s)
  BS_Seq  : BS s p s0 -> BS s0 q s' -> BS s (Seq p q) s'

pushPop : BS s (Push n `Seq` Pop) s
pushPop = BS_Seq BS_Push BS_Pop

sumProg : BS s ((Push n1 `Seq` Push n2) `Seq` Add) ((n2+n1)::s)
sumProg = (BS_Push `BS_Seq` BS_Push) `BS_Seq` BS_Add

gen : Nat -> Prog
gen Z = Seq (Seq (Push 1) (Push 1)) Add
gen (S n) = Seq (Seq (gen n) (Push 1)) Add

p : (n : Nat) -> BS s (gen n) ((n+2)::s)
p Z = sumProg
p (S m) = ((p m) `BS_Seq` BS_Push) `BS_Seq` BS_Add