source: Deliverables/D3.3/Cminor-experiment/be.agda @ 808

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)