29 lines
722 B
Idris
29 lines
722 B
Idris
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
|