Define execBeats, a wrapper to execute beat-wise instructions.

1 files changed, 4 insertions, 1 deletions

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