module HomeworkTwelve
%default total

data Op = Push Nat | Pop | Add

Stack : Type 
Stack = List Nat

data Step : Stack -> Op -> Stack -> Type where
  SPush : Step xs (Push n) (n::xs)
  SPop : Step (n::xs) Pop xs
  SAdd : Step (n1::n2::xs) Add ((n1+n2)::xs)

Ops : Type
Ops = List Op

data Steps : Stack -> Ops -> Stack -> Type where
  SEmpty : Steps xs [] xs
  SSeq : Step xs o ys -> Steps ys os zs -> Steps xs (o::os) zs

stepsEx : Steps [] [Push 3, Push 5, Add] [8]
stepsEx = SSeq SPush (SSeq SPush (SSeq SAdd SEmpty))