[755] | 1 | module be where |
---|

| 2 | |
---|

| 3 | data Nat : Set where |
---|

| 4 | zero : Nat |
---|

| 5 | succ : Nat -> Nat |
---|

| 6 | |
---|

| 7 | data Fin : Nat -> Set where |
---|

| 8 | fz : forall n -> Fin (succ n) |
---|

| 9 | fs : forall n -> Fin n -> Fin (succ n) |
---|

| 10 | |
---|

| 11 | data Stmt : Nat -> Set where |
---|

| 12 | skip : {n : Nat} -> Stmt n |
---|

| 13 | seq : {n : Nat} -> Stmt n -> Stmt n -> Stmt n |
---|

| 14 | block : {n : Nat} -> Stmt (succ n) -> Stmt n |
---|

| 15 | exit : {n : Nat} -> Fin n -> Stmt n |
---|

| 16 | |
---|

| 17 | data Cont : Nat -> Set where |
---|

| 18 | kstop : Cont zero |
---|

| 19 | kseq : forall n -> Stmt n -> Cont n -> Cont n |
---|

| 20 | kblock : forall n -> Cont n -> Cont (succ n) |
---|

| 21 | |
---|

| 22 | data DP (T : Set) (S : T -> Set) : Set where |
---|

| 23 | dp : (t : T) -> S t -> DP T S |
---|

| 24 | |
---|

| 25 | record State : Set where |
---|

| 26 | constructor state |
---|

| 27 | field |
---|

| 28 | blocks : Nat |
---|

| 29 | stmt : Stmt blocks |
---|

| 30 | cont : Cont blocks |
---|

| 31 | |
---|

| 32 | kexit : {n : Nat}(m : Fin n)(k : Cont n) -> DP Nat Cont |
---|

| 33 | kexit () kstop |
---|

| 34 | kexit {n} m (kseq .n s k) = kexit m k |
---|

| 35 | kexit (fz .n) (kblock n k) = dp n k |
---|

| 36 | kexit (fs .n m) (kblock n k) = kexit m k |
---|

| 37 | |
---|

| 38 | step : State -> State |
---|

| 39 | step (state .zero skip kstop) = state zero skip kstop |
---|

| 40 | step (state blocks skip (kseq .blocks s k)) = state blocks s k |
---|

| 41 | step (state .(succ n) skip (kblock n k)) = state n skip k |
---|

| 42 | step (state blocks (seq s s') k) = state blocks s (kseq blocks s' k) |
---|

| 43 | step (state blocks (block s) k) = state (succ blocks) s (kblock blocks k) |
---|

| 44 | step (state blocks (exit m) k) with kexit m k |
---|

| 45 | ... | dp n' k' = state n' skip k' |
---|

| 46 | |
---|

| 47 | iterate : {S : Set} -> Nat -> (S -> S) -> S -> S |
---|

| 48 | iterate zero f s = s |
---|

| 49 | iterate (succ n) f s = iterate n f (f s) |
---|