module be where data Nat : Set where zero : Nat succ : Nat -> Nat data Fin : Nat -> Set where fz : forall n -> Fin (succ n) fs : forall n -> Fin n -> Fin (succ n) data Stmt : Nat -> Set where skip : {n : Nat} -> Stmt n seq : {n : Nat} -> Stmt n -> Stmt n -> Stmt n block : {n : Nat} -> Stmt (succ n) -> Stmt n exit : {n : Nat} -> Fin n -> Stmt n data Cont : Nat -> Set where kstop : Cont zero kseq : forall n -> Stmt n -> Cont n -> Cont n kblock : forall n -> Cont n -> Cont (succ n) data DP (T : Set) (S : T -> Set) : Set where dp : (t : T) -> S t -> DP T S record State : Set where constructor state field blocks : Nat stmt : Stmt blocks cont : Cont blocks kexit : {n : Nat}(m : Fin n)(k : Cont n) -> DP Nat Cont kexit () kstop kexit {n} m (kseq .n s k) = kexit m k kexit (fz .n) (kblock n k) = dp n k kexit (fs .n m) (kblock n k) = kexit m k step : State -> State step (state .zero skip kstop) = state zero skip kstop step (state blocks skip (kseq .blocks s k)) = state blocks s k step (state .(succ n) skip (kblock n k)) = state n skip k step (state blocks (seq s s') k) = state blocks s (kseq blocks s' k) step (state blocks (block s) k) = state (succ blocks) s (kblock blocks k) step (state blocks (exit m) k) with kexit m k ... | dp n' k' = state n' skip k' iterate : {S : Set} -> Nat -> (S -> S) -> S -> S iterate zero f s = s iterate (succ n) f s = iterate n f (f s)