From 0b581ec922b40284291d6814578bd2e68049c8b7 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 21 Dec 2021 15:14:54 +0000 Subject: Define execBeats, a wrapper to execute beat-wise instructions. --- src/Helium/Semantics/Denotational/Core.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src/Helium/Semantics/Denotational/Core.agda') diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index bbddc57..54f0375 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -104,7 +104,7 @@ _,′_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Reference n Γ τ -- Statements infixr 1 _∙_ -infix 4 _≔_ +infix 4 _≔_ _⟵_ infixl 2 if_then_else_ skip : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ @@ -119,6 +119,9 @@ return e _ = e _≔_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ → Statement n Γ τ′ (ref ≔ e) cont σ ρ = e σ ρ >>= λ (σ , v) → Reference.set ref σ ρ v >>= λ (σ , v) → cont σ v +_⟵_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Op₁ τ → Statement n Γ τ′ +ref ⟵ e = ref ≔ ⦇ e (! ref) ⦈ + label : ∀ {n ls} {Γ : Sets n ls} → smap _ (Reference n Γ) n Γ ⇉ Statement n Γ τ → Statement n Γ τ label {n = n} s = uncurry⊤ₙ n s vars where -- cgit v1.2.3