Add some headers

src/Project/Cesk.agda

@@ -11,6 +11,9 @@ open Aexp
 open Value
 open State
 
+-------------------------------------------------------------------------------
+-- Step for atomics
+
 astep : ∀ {Tω Γ A} → Aexp Tω Γ A → Env Tω Γ → Value Tω A
 astep (value v) _ = v
 astep zero _  = zero
@@ -18,16 +21,23 @@ astep (suc c) e = suc $ astep c e
 astep (` id) e = lookup e id
 astep (ƛ body) e = clo body e
 
-inject : {A : Type} → Exp A ∅ A → State A
+-------------------------------------------------------------------------------
-inject {A} C = mkState A ∅ C ∅ halt
+-- Step
 
 step : ∀ {Tω : Type} → State Tω → StepResult Tω
+-- Atomic expressions
 step (mkState Tc Γ (atomic x) E K) = apply-kont K $ astep x E
+
+-- Natural numbers
 step (mkState Tc Γ (case C isZ isS) E K) with astep C E
 ... | zero = part $ mkState Tc Γ isZ E K
 ... | suc n = part $ mkState Tc Γ (isS · value n) E K
+
+-- Function application
 step (mkState Tc Γ (x₁ · x₂) E K) with astep x₁ E
 ... | clo body env = apply-proc-clo body env (astep x₂ E) K
+
+-- Call/cc
 step (mkState Tc Γ (x₁ ∘ x₂) E K) with astep x₁ E
 ... | cont k =
   let val = astep x₂ E in
@@ -40,10 +50,18 @@ step {Tω} (mkState Tc Γ (call/cc {A} aexp) E K) with astep aexp E
   part $ mkState Tω Γ′ body E′ halt
 step (mkState Tc Γ (abort V⊥) E K) with astep V⊥ E
 ... | ()
+
+-- Let-bindings
 step (mkState Tc Γ (`let {A} C₁ C₂) E K) =
   let K′ = letk Γ C₂ E K in
   part $ mkState A Γ C₁ E (kont K′)
 
+-------------------------------------------------------------------------------
+-- Evaluation
+
+inject : {A : Type} → Exp A ∅ A → State A
+inject {A} C = mkState A ∅ C ∅ halt
+
 data EvalResult : Set where
   complete : ∀ {A} → StepResult A → EvalResult
   exhausted : ∀ {A} → State A → EvalResult