21 lines
809 B
Agda
21 lines
809 B
Agda
|
module Project.Do where
|
|||
|
|
|
|||
|
|
open import Project.Definitions using (Letk; Kont; Exp; Value; State; Type; kont; halt; letk; clo; zero; suc; mkState; `_; `ℕ; _·_; _⇒_; _,_; _[_∶_])
|
|||
|
|
open import Project.Util using (_$_)
|
|||
|
|
|
|||
|
|
data StepResult (A : Type) : Set where
|
|||
|
|
part : State A → StepResult A
|
|||
|
|
done : Value A → StepResult A
|
|||
|
|
|
|||
|
|
-- Apply the continuation to the value, resulting in a state.
|
|||
|
|
do-kont : ∀ {Tv Tω} (L : Letk Tv Tω) → Value Tv → State Tω
|
|||
|
|
do-kont {Tv} {Tω} (letk {Tc} Γ C E k) v =
|
|||
|
|
let Γ′ = Γ , Tv in
|
|||
|
|
let E′ = E [ Tv ∶ v ] in
|
|||
|
|
mkState Tc Γ′ C E′ k
|
|||
|
|
|
|||
|
|
do-apply : ∀ {A B Tω} → Value (A ⇒ B) → Value A → Kont Tω B → StepResult Tω
|
|||
|
|
do-apply (clo {Γ} {A} {B} body e) v k =
|
|||
|
|
let Γ′ = Γ , A in
|
|||
|
|
let E′ = e [ A ∶ v ] in
|
|||
|
|
part $ mkState B Γ′ body E′ k
|