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

Last change on this file was 755, checked in by campbell, 9 years ago

An experimental branch of the Cminor semantics.

File size: 1.4 KB
Line 
1module be where
2
3data Nat : Set where
4  zero : Nat
5  succ : Nat -> Nat
6
7data Fin : Nat -> Set where
8  fz : forall n -> Fin (succ n)
9  fs : forall n -> Fin n -> Fin (succ n)
10
11data 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
17data 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
22data DP (T : Set) (S : T -> Set) : Set where
23  dp : (t : T) -> S t -> DP T S
24
25record State : Set where
26  constructor state
27  field
28    blocks : Nat
29    stmt : Stmt blocks
30    cont : Cont blocks
31
32kexit : {n : Nat}(m : Fin n)(k : Cont n) -> DP Nat Cont
33kexit () kstop
34kexit {n} m (kseq .n s k) = kexit m k
35kexit (fz .n) (kblock n k) = dp n k
36kexit (fs .n m) (kblock n k) = kexit m k
37
38step : State -> State
39step (state .zero skip kstop) = state zero skip kstop
40step (state blocks skip (kseq .blocks s k)) = state blocks s k
41step (state .(succ n) skip (kblock n k)) = state n skip k
42step (state blocks (seq s s') k) = state blocks s (kseq blocks s' k)
43step (state blocks (block s) k) = state (succ blocks) s (kblock blocks k)
44step (state blocks (exit m) k) with kexit m k
45... | dp n' k' = state n' skip k'
46
47iterate : {S : Set} -> Nat -> (S -> S) -> S -> S
48iterate zero f s = s
49iterate (succ n) f s = iterate n f (f s)
Note: See TracBrowser for help on using the repository browser.