23 lines
522 B
Idris
23 lines
522 B
Idris
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))
|